Formalizing Determinacy of Concurrent Revisions

TL;DR

This paper formalizes the determinacy of concurrent revisions using Isabelle/HOL, providing a rigorous operational semantics and proof, while addressing ambiguities and simplifying the verification process.

Contribution

It presents a formal Isabelle/HOL model of concurrent revisions' operational semantics and a proof of determinacy, clarifying design challenges.

Findings

Formalization highlights subtle semantic ambiguities

Simplifies the proof of determinacy

Provides insights into concurrency control verification

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.