Formalization, by specification refinement, of concurrent mutual exclusion algorithms.
- mutexAbstractN: abstract specification of N-process mutual exclusion problem
- mutexAbstract: abstract specification of two-process mutual exclusion problem. Refines mutexAbstractN
- simpleMutex: simple algorithm using just a "trying" variable for each process (may deadlock). Refines mutexAbstract
- Peterson: Petersons's algorithm. Refines mutexAbstract
- PetersonAtomic: a variant of Petersons's algorithm. Refines Peterson
- BakeryAtomic: simplified version of Lamport's Bakery algorithm. Refines mutexAbstractN