Formalizing determinacy of concurrent revisions

Roy Overbeek*

*Corresponding author for this work

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

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 languageEnglish
Title of host publicationCPP 2020 - Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2020
EditorsJasmin Blanchette, Catalin Hritcu
PublisherAssociation for Computing Machinery, Inc
Pages258-269
Number of pages12
ISBN (Electronic)9781450370974
DOIs
Publication statusPublished - 20 Jan 2020
Event9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, co-located with POPL 2020 - New Orleans, United States
Duration: 20 Jan 202021 Jan 2020

Publication series

NameCPP 2020 - Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2020

Conference

Conference9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, co-located with POPL 2020
CountryUnited States
CityNew Orleans
Period20/01/2021/01/20

    Fingerprint

Keywords

  • Concurrency control models
  • Isabelle/HOL
  • Proof assistants

Cite this

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, co-located with POPL 2020 (pp. 258-269). (CPP 2020 - Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2020). Association for Computing Machinery, Inc. https://doi.org/10.1145/3372885.3373820