Formalization of Concurrent Revisions

Roy Overbeek 📧

December 25, 2018

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


Concurrent revisions is a concurrency control model developed by Microsoft Research. It has many interesting properties that distinguish it from other well-known models such as transactional memory. One of these properties is determinacy: programs written within the model always produce the same outcome, independent of scheduling activity. The concurrent revisions model has an operational semantics, with an informal proof of determinacy. This document contains an Isabelle/HOL formalization of this semantics and the proof of determinacy.


BSD License


Session Concurrent_Revisions