POPL 2020 (series) / CPP 2020 (series) / The 9th ACM SIGPLAN International Conference on Certified Programs and Proofs /
Formalizing Determinacy of Concurrent Revisions
Concurrent revisions is a concurrency control model designed to guarantee \emph{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.
Tue 21 Jan Times are displayed in time zone: Saskatchewan, Central America change
Tue 21 Jan
Times are displayed in time zone: Saskatchewan, Central America change
| 14:00 - 14:21 Talk | Formalizing Determinacy of Concurrent Revisions CPP Roy OverbeekVrije Universiteit Amsterdam DOI Pre-print Media Attached | ||
| 14:21 - 14:43 Talk | Formalizing π-calculus in Guarded Cubical Agda CPP DOI Pre-print Media Attached File Attached | ||
| 14:43 - 15:05 Talk | Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages CPP Arjen RouvoetDelft University of Technology, Casper Bach PoulsenDelft University of Technology, Robbert KrebbersDelft University of Technology, Eelco VisserDelft University of Technology DOI Pre-print Media Attached File Attached | ||