Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
TLA+ implementation of Peterson's mutual exclusion algorithm. Demonstrates absence of deadlock and liveness given fair processes.
--------------------------- MODULE peterson_multi ---------------------------
EXTENDS TLC, Integers, Sequences
CONSTANT ThreadCount
Threads == 1..ThreadCount
AllOtherFlagsLessThan(item, flags) ==
\A q \in Threads \ {item}: flags[q] < item
(*--algorithm peterson_multi
variables
flags = [t \in Threads |-> 0],
turns = [t \in 1..(ThreadCount - 1) |-> 1];
fair process p \in Threads
begin
P1: with t \in 1..(ThreadCount - 1) do
flags[self] := t;
turns[t] := self;
await AllOtherFlagsLessThan(self, flags) \/ turns[t] /= self;
end with;
CS: skip;
P_2: flags[self] := 0;
end process;
end algorithm*)
\* BEGIN TRANSLATION
\* END TRANSLATION
Liveness ==
\A t \in Threads:
<>(pc[t] = "CS")
=============================================================================
\* Modification History
\* Last modified Sat Jan 26 12:55:10 PST 2019 by eric
\* Created Sat Jan 26 12:47:13 PST 2019 by eric
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.