Exploring TLA+ with two-phase commit

from blog Marc Brooker's Blog, | ↗ original
Exploring TLA+ with two-phase commit Using testable pseudocode to test a distributed algorithm There are very few distributed algorithms more widely known by working programmers than the two-phase commit atomic commit protocol. It’s a great algorithm to use for teaching purposes: two-phase commit is both extremely simple to write down, and has...