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.