mutex.tla

------------------------------- MODULE mutex -------------------------------
EXTENDS Integers, FiniteSets, Sequences, TLC
CONSTANTS threadcount, maxiterations
ASSUME threadcount \in Nat
(*--algorithm mutex
\* https://disco.ethz.ch/courses/podc_allstars/lecture/chapter5.pdf
\* Algorithm 5.3 Mutual Exclusion: Test-and-Set
variables
  R = 0,
  X = 0;
fair+ process thread \in 1..threadcount
variables
  t = -1,
  x = -1,
  ec = 0,
  iterations = 0
begin
  Outer:
  while iterations < maxiterations do
    Entry: \*How can I prevent this from spinning infinitely in one thread?
      t := R || R := 1;
      if (t = 1) then
        ec := ec + 1;
        goto Entry;
      end if;
    CriticalSectionRead:
      x := X;
    CriticalSectionWrite:
      X := x + 1;
    Exit:
      R := 0;
      iterations := iterations + 1
  end while;
end process
end algorithm
*)
\* BEGIN TRANSLATION
\* END TRANSLATION
ReduceSet(op(_, _), set, acc) ==
  LET f[s \in SUBSET set] == \* here's where the magic is
    IF s = {} THEN acc
    ELSE LET z == CHOOSE z \in s: TRUE
         IN op(z, f[s \ {z}])
  IN f[set]
ReduceSeq(op(_, _), seq, acc) == ReduceSet(LAMBDA i, a: op(seq[i], a), DOMAIN seq, acc)
add(a,b) == a+b
CriticalThreads == {y \in 1..threadcount : pc[y] = "CriticalSectionRead" \/ pc[y] = "CriticalSectionWrite"}
MutualExclusion == Cardinality(CriticalThreads) <= 1
xisgood == <>[](X = ReduceSeq(add, iterations, 0))
entrycgood == Cardinality({e \in 1..threadcount : ec[e] >= 10}) < 1
=============================================================================

Invariants
MutualExclusion
entrycgood //only used for testing

Temporal properties
xisgood