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
Subtitle of host publicationProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs
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

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

Keywords

  • Concurrency control models
  • Isabelle/HOL
  • Proof assistants

Fingerprint Dive into the research topics of 'Formalizing determinacy of concurrent revisions'. Together they form a unique fingerprint.

Cite this