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
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.