Thomas Rodeheffer
September 2008
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.
![]() PDF file |
| Type: | TechReport |
| Number: | MSR-TR-2008-125 |
| Pages: | 32 |
| Institution: | Microsoft Research |