Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Cyclic Commit Protocol Specifications

Thomas Rodeheffer

Abstract

A novel cyclic commit protocol uses extra metadata fields to implement transactional semantics without needing an explicit commit record. We describe and present specifications of two versions of cyclic commit: Simple Cyclic Commit (SCC) and Back-Pointer Cyclic Commit (BPCC). The specifications are written in TLA+ and checked with the TLC model checker.

Details

Publication typeTechReport
NumberMSR-TR-2008-125
Pages32
InstitutionMicrosoft Research
> Publications > Cyclic Commit Protocol Specifications