TLA+ implementation of Peterson's mutual exclusion algorithm. Demonstrates absence of deadlock and liveness given fair processes.

peterson_multi.tla

--------------------------- 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