diff --git a/README.md b/README.md index 3d08787..ea403d8 100644 --- a/README.md +++ b/README.md @@ -4,12 +4,14 @@ This repository contains a TLA specification of [Peterson's algorithm](https://en.wikipedia.org/wiki/Peterson%27s_algorithm), an algorithm that allows multiple processes to share a single-use resource without conflict. +Peterson's algorithm is one of the simplest mutual exclusion concurrency +algorithms out there, but already has some potentially non-intuitive components, +e.g. understanding why a process "gives its turn away." + For a pretty-printed PDF version, see -[https://github.com/changlinli/peterson-tlaplus/releases/download/v1.0/Peterson.pdf](https://github.com/changlinli/peterson-tlaplus/releases/download/v1.0/Peterson.pdf). +[https://github.com/changlinli/peterson-tlaplus/releases/download/v1.1/Peterson.pdf](https://github.com/changlinli/peterson-tlaplus/releases/download/v1.1/Peterson.pdf). -This is meant as an intermediate introduction to TLA+ users. An example is -someone who has just finished Leslie Lamport's video course on TLA+. The -specification also has a lot of comments which I hope help even non-TLA+ users +This specification may seem long, but it is largely comments, which I hope help even non-TLA+ users understand the intuition behind Peterson's algorithm better. Note that I've chosen to take a loose translation of Peterson's algorithm as it