From c62b0ba5b3d153a720de1194252c169da7bd3e95 Mon Sep 17 00:00:00 2001 From: Changlin Li Date: Thu, 25 Jul 2019 12:39:57 -0400 Subject: [PATCH 1/3] Update README to v1.1 Now that we have a new PDF out --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 3d08787..66f0494 100644 --- a/README.md +++ b/README.md @@ -5,7 +5,7 @@ algorithm](https://en.wikipedia.org/wiki/Peterson%27s_algorithm), an algorithm that allows multiple processes to share a single-use resource without conflict. 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 From 69b4d19240633b6c47e9bbdb21b8c3f452043f0c Mon Sep 17 00:00:00 2001 From: Changlin Li Date: Fri, 26 Jul 2019 09:46:36 -0400 Subject: [PATCH 2/3] Add comment on Peterson's algorithm Explain briefly why it was chosen for TLA+ --- README.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/README.md b/README.md index 66f0494..3085635 100644 --- a/README.md +++ b/README.md @@ -4,6 +4,10 @@ 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.1/Peterson.pdf](https://github.com/changlinli/peterson-tlaplus/releases/download/v1.1/Peterson.pdf). From 314a7e522432677b89423188916351b6ee635d87 Mon Sep 17 00:00:00 2001 From: Changlin Li Date: Fri, 26 Jul 2019 09:48:48 -0400 Subject: [PATCH 3/3] Remove comment about TLA+ users This isn't really meant just for TLA+ users --- README.md | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/README.md b/README.md index 3085635..ea403d8 100644 --- a/README.md +++ b/README.md @@ -11,9 +11,7 @@ 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.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