Write a Blog >>
Tue 21 Jan 2020 14:00 - 14:21 at Maurepas - Concurrency and linearity Chair(s): Zhong Shao

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: (GMT-06:00) Saskatchewan, Central America change

14:00 - 15:05: CPP 2020 - Concurrency and linearity at Maurepas
Chair(s): Zhong ShaoYale University
CPP-2020-papers14:00 - 14:21
Roy OverbeekVrije Universiteit Amsterdam
DOI Pre-print Media Attached
CPP-2020-papers14:21 - 14:43
Niccolò VeltriTallinn University of Technology, Andrea VezzosiIT University Copenhagen
DOI Pre-print Media Attached File Attached
CPP-2020-papers14:43 - 15:05
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