Formalizing determinacy of concurrent revisions

Roy Overbeek

doi:10.1145/3372885.3373820

Formalizing determinacy of concurrent revisions

Roy Overbeek^*

^*Corresponding author for this work

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

1 Downloads (Pure)

Abstract

Concurrent revisions is a concurrency control model designed to guarantee determinacy, meaning that the outcomes of programs are uniquely determined. This paper describes an Isabelle/HOL formalization of the model's operational semantics and proof of determinacy. We discuss and resolve subtle ambiguities in the operational semantics and simplify the proof of determinacy. Although our findings do not appear to correspond to bugs in implementations, the formalization highlights some of the challenges involved in the design and verification of concurrency control models.

Original language	English
Title of host publication	CPP 2020
Subtitle of host publication	Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs
Editors	Jasmin Blanchette, Catalin Hritcu
Publisher	Association for Computing Machinery, Inc
Pages	258-269
Number of pages	12
ISBN (Electronic)	9781450370974
DOIs	https://doi.org/10.1145/3372885.3373820
Publication status	Published - Jan 2020
Event	9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, co-located with POPL 2020 - New Orleans, United States Duration: 20 Jan 2020 → 21 Jan 2020

Conference

Conference	9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, co-located with POPL 2020
Country/Territory	United States
City	New Orleans
Period	20/01/20 → 21/01/20

Keywords

Concurrency control models
Isabelle/HOL
Proof assistants

Access to Document

10.1145/3372885.3373820

Formalizing determinacy of concurrent revisionsFinal published version, 819 KBLicence: Article 25fa Dutch Copyright Act

Handle.net

Persistent link

Cite this

@inproceedings{fbeb927aaa9e4ee2a437132928c642f3,

title = "Formalizing determinacy of concurrent revisions",

abstract = "Concurrent revisions is a concurrency control model designed to guarantee determinacy, meaning that the outcomes of programs are uniquely determined. This paper describes an Isabelle/HOL formalization of the model's operational semantics and proof of determinacy. We discuss and resolve subtle ambiguities in the operational semantics and simplify the proof of determinacy. Although our findings do not appear to correspond to bugs in implementations, the formalization highlights some of the challenges involved in the design and verification of concurrency control models.",

keywords = "Concurrency control models, Isabelle/HOL, Proof assistants",

author = "Roy Overbeek",

year = "2020",

month = jan,

doi = "10.1145/3372885.3373820",

language = "English",

pages = "258--269",

editor = "Jasmin Blanchette and Catalin Hritcu",

booktitle = "CPP 2020",

publisher = "Association for Computing Machinery, Inc",

note = "9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, co-located with POPL 2020 ; Conference date: 20-01-2020 Through 21-01-2020",

}

Overbeek, R 2020, Formalizing determinacy of concurrent revisions. in J Blanchette & C Hritcu (eds), CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. Association for Computing Machinery, Inc, pp. 258-269, 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, co-located with POPL 2020, New Orleans, United States, 20/01/20. https://doi.org/10.1145/3372885.3373820

Formalizing determinacy of concurrent revisions. / Overbeek, Roy.
CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. ed. / Jasmin Blanchette; Catalin Hritcu. Association for Computing Machinery, Inc, 2020. p. 258-269.

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Formalizing determinacy of concurrent revisions

AU - Overbeek, Roy

PY - 2020/1

Y1 - 2020/1

N2 - Concurrent revisions is a concurrency control model designed to guarantee determinacy, meaning that the outcomes of programs are uniquely determined. This paper describes an Isabelle/HOL formalization of the model's operational semantics and proof of determinacy. We discuss and resolve subtle ambiguities in the operational semantics and simplify the proof of determinacy. Although our findings do not appear to correspond to bugs in implementations, the formalization highlights some of the challenges involved in the design and verification of concurrency control models.

AB - Concurrent revisions is a concurrency control model designed to guarantee determinacy, meaning that the outcomes of programs are uniquely determined. This paper describes an Isabelle/HOL formalization of the model's operational semantics and proof of determinacy. We discuss and resolve subtle ambiguities in the operational semantics and simplify the proof of determinacy. Although our findings do not appear to correspond to bugs in implementations, the formalization highlights some of the challenges involved in the design and verification of concurrency control models.

KW - Concurrency control models

KW - Isabelle/HOL

KW - Proof assistants

UR - http://www.scopus.com/inward/record.url?scp=85079457551&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85079457551&partnerID=8YFLogxK

U2 - 10.1145/3372885.3373820

DO - 10.1145/3372885.3373820

M3 - Conference contribution

AN - SCOPUS:85079457551

SP - 258

EP - 269

BT - CPP 2020

A2 - Blanchette, Jasmin

A2 - Hritcu, Catalin

PB - Association for Computing Machinery, Inc

T2 - 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, co-located with POPL 2020

Y2 - 20 January 2020 through 21 January 2020

ER -

Formalizing determinacy of concurrent revisions

Abstract

Conference

Keywords

Access to Document

Handle.net

Other files and links

Fingerprint

Cite this