# Formalization of Concurrent Revisions

 Title: Formalization of Concurrent Revisions Author: Roy Overbeek (Roy /dot/ Overbeek /at/ cwi /dot/ nl) Submission date: 2018-12-25 Abstract: 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. BibTeX: @article{Concurrent_Revisions-AFP, author = {Roy Overbeek}, title = {Formalization of Concurrent Revisions}, journal = {Archive of Formal Proofs}, month = dec, year = 2018, note = {\url{http://isa-afp.org/entries/Concurrent_Revisions.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License