Formally proving the correctness of synchronization primitives

AutoResetEvent.cfg

INIT Init
NEXT Next

CONSTANT Setters = 3

INVARIANTS 
    IsEventuallySet 
    NoWaiterDeadlock

AutoResetEvent.tla

---- MODULE AutoResetEvent ----
EXTENDS Naturals, FiniteSets, Sequences

CONSTANT Setters

VARIABLE
    state,
    waiter,
    threads

----

Wait == 
    CASE state = "UNSET" ->
        /\ state' = "WAITING"
        /\ waiter' = "WAITING"
      [] state = "SET" ->
        /\ state' = "UNSET"
        /\ UNCHANGED waiter
      [] OTHER ->
        waiter = "EMPTY"
    
Set ==
    CASE state = "SET" ->
        UNCHANGED <<waiter, state>>
      [] state = "UNSET" ->
        /\ state' = "SET"
        /\ UNCHANGED waiter
      [] state = "WAITING" ->
        /\ state' = "UNSET"
        /\ waiter = "WAITING"
        /\ waiter' = "NOTIFIED"

----

(* Generates a sequence of sequences where each sequence
   contains setter threads id from 1.."setters" along with
   the waiting thread id of 0 in a different position for
   each sequence.
   
   The waiting thread id, looking over all sequences, appears
   in at least all positions of the sequence excluding the
   last position. This is so that a call to Wait above doesn't
   deadlock with no thread available to Set it
*)

GenSetterThreads(setters) ==
    [s \in 1..setters |-> 
        LET Injective(f) == \A a,b \in DOMAIN f : f[a] = f[b] => a = b IN
        LET SetToSeq(set) == CHOOSE f \in [1..Cardinality(set) -> set] : Injective(f) IN
        LET GenSeq(a,b) == IF a = b THEN <<a>> ELSE SetToSeq(a..b) IN
        GenSeq(1, s - 1) \o <<0>> \o GenSeq(s, setters)
    ]

GenThreads(setters) ==
    IF setters > 0 THEN GenSetterThreads(setters) ELSE <<<<0>>>>
    
Init ==
    /\ state = "UNSET"
    /\ waiter = "EMPTY"
    /\ LET ToSet(s) == { s[i] : i \in DOMAIN s } IN
        /\ threads \in ToSet(GenThreads(Setters))

Next ==
    IF threads = <<>> THEN
        UNCHANGED <<threads, state, waiter>>
    ELSE LET tid == Head(threads) IN
        /\ threads' = Tail(threads)
        /\ \/ tid = 0 /\ Wait
           \/ Set

----

NoWaiterDeadlock ==
    threads = <<>> => waiter \notin {"WAITING"}

IsEventuallySet ==
    threads = <<>> => 
        /\ state = "SET"
        /\ waiter \in {"EMPTY", "NOTIFIED"}

====