### 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.

### License

BSD License

### Topics

- Computer science/Concurrency

### Session Concurrent_Revisions

- Data
- Occurrences
- Renaming
- Substitution
- OperationalSemantics
- Executions
- Determinacy

## Cite

×

Concurrent_Revisions-AFP

    @article{Concurrent_Revisions-AFP,
      author  = {Roy Overbeek},
      title   = {Formalization of Concurrent Revisions},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/Concurrent_Revisions.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Jan 3, 2019 : Isabelle2018