Model for "Investigating a Queue Hang"

Enqueue.cfg

SPECIFICATION Spec
\* Add statements after this line.
CONSTANTS 
    Threads = {t1}
    NULL = NULL
    Keys = {k1}
    MaxId = 1
    BUGMODE = TRUE

PROPERTY LockProp
INVARIANT TypeInv

Equeue.tla

https://gist.github.com/FeepingCreature/a8099d2bcf850a9c388ed045fa3b5c0e
---- MODULE Equeue ----
EXTENDS TLC, Sequences, Integers, FiniteSets
CONSTANTS Keys, Threads, MaxId, NULL
CONSTANT BUGMODE

EventType == [id: 1..MaxId, key: Keys, done: BOOLEAN]
EventQueueType == Seq(EventType)
(*--algorithm Equeue
variables
    lock = [k \in Keys |-> NULL];
    to_process \in {queue \in [1..MaxId -> EventType]: \* Slow
        \A i \in 1..Len(queue):
            /\ queue[i].id = i
            /\ ~queue[i].done
    };
    events = <<>>;
    next_id = 1;
    eid = [t \in Threads |-> NULL];

define
    ThreadPoolCount == Cardinality({i \in 1..Len(events): ~events[i].done})
    TypeInv ==
        /\ lock \in [Keys -> Threads \union {NULL}]
        /\ eid \in [Threads -> 1..MaxId \union {NULL}]
        /\ next_id \in 1..(MaxId+1)
        /\ events \in EventQueueType
    LockProp == [][
    \A k \in Keys:
        lock[k]' # NULL => lock[k] = NULL \/ UNCHANGED lock[k]
    ]_lock
end define;

fair process thread \in Threads
begin 
    ProcessEvent:
        await eid[self] # NULL;
        with k = CHOOSE k \in Keys: lock[k] = self,
             e = CHOOSE e \in 1..Len(events): events[e].id = eid[self]
        do
            lock[k] := NULL;
            events[e].done := TRUE;
            eid[self] := NULL;
        end with;
        goto ProcessEvent;
end process;

fair process queuer = "queuer"
begin
    Queue:
        await next_id <= MaxId;
        await ThreadPoolCount < Cardinality(Threads);
        with next_event = to_process[next_id], t \in Threads do
            await lock[next_event.key] = NULL;
            await eid[t] = NULL;
            lock[next_event.key] := t;
            eid[t] := next_event.id;
            events := Append(events, next_event);
        end with;        
        \* bug timez
        either next_id := next_id + 1; 
            or await BUGMODE;
        end either;
        goto Queue;
end process;

fair process pruner = "pruner"
begin
    Prune:
        await events # <<>>;
        await Head(events).done;
        with cutoff = CHOOSE x \in 1..Len(events):
            /\ \A i \in 1..x:
                events[i].done
            /\ x # Len(events) => ~events[x+1].done 
        do
            events := SubSeq(events, cutoff+1, Len(events));
        end with;
        goto Prune;
end process;

process checkdone = "checkdone"
begin
    CheckDone: \* Turns liveness check into deadlock check
        await events = <<>>;
        await next_id > MaxId;
    goto CheckDone;
end process;
end algorithm; *)
\* BEGIN TRANSLATION (chksum(pcal) = "84a578ae" /\ chksum(tla) = "4f294e7c")
VARIABLES lock, to_process, events, next_id, eid, pc

(* define statement *)
ThreadPoolCount == Cardinality({i \in 1..Len(events): ~events[i].done})
TypeInv ==
    /\ lock \in [Keys -> Threads \union {NULL}]
    /\ eid \in [Threads -> 1..MaxId \union {NULL}]
    /\ next_id \in 1..(MaxId+1)
    /\ events \in EventQueueType
LockProp == [][
\A k \in Keys:
    lock[k]' # NULL => lock[k] = NULL \/ UNCHANGED lock[k]
]_lock


vars == << lock, to_process, events, next_id, eid, pc >>

ProcSet == (Threads) \cup {"queuer"} \cup {"pruner"} \cup {"checkdone"}

Init == (* Global variables *)
        /\ lock = [k \in Keys |-> NULL]
        /\ to_process \in                {queue \in [1..MaxId -> EventType]:
                              \A i \in 1..Len(queue):
                                  /\ queue[i].id = i
                                  /\ ~queue[i].done
                          }
        /\ events = <<>>
        /\ next_id = 1
        /\ eid = [t \in Threads |-> NULL]
        /\ pc = [self \in ProcSet |-> CASE self \in Threads -> "ProcessEvent"
                                        [] self = "queuer" -> "Queue"
                                        [] self = "pruner" -> "Prune"
                                        [] self = "checkdone" -> "CheckDone"]

ProcessEvent(self) == /\ pc[self] = "ProcessEvent"
                      /\ eid[self] # NULL
                      /\ LET k == CHOOSE k \in Keys: lock[k] = self IN
                           LET e == CHOOSE e \in 1..Len(events): events[e].id = eid[self] IN
                             /\ lock' = [lock EXCEPT ![k] = NULL]
                             /\ events' = [events EXCEPT ![e].done = TRUE]
                             /\ eid' = [eid EXCEPT ![self] = NULL]
                      /\ pc' = [pc EXCEPT ![self] = "ProcessEvent"]
                      /\ UNCHANGED << to_process, next_id >>

thread(self) == ProcessEvent(self)

Queue == /\ pc["queuer"] = "Queue"
         /\ next_id <= MaxId
         /\ ThreadPoolCount < Cardinality(Threads)
         /\ LET next_event == to_process[next_id] IN
              \E t \in Threads:
                /\ lock[next_event.key] = NULL
                /\ eid[t] = NULL
                /\ lock' = [lock EXCEPT ![next_event.key] = t]
                /\ eid' = [eid EXCEPT ![t] = next_event.id]
                /\ events' = Append(events, next_event)
         /\ \/ /\ next_id' = next_id + 1
            \/ /\ BUGMODE
               /\ UNCHANGED next_id
         /\ pc' = [pc EXCEPT !["queuer"] = "Queue"]
         /\ UNCHANGED to_process

queuer == Queue

Prune == /\ pc["pruner"] = "Prune"
         /\ events # <<>>
         /\ Head(events).done
         /\ LET cutoff ==           CHOOSE x \in 1..Len(events):
                          /\ \A i \in 1..x:
                              events[i].done
                          /\ x # Len(events) => ~events[x+1].done IN
              events' = SubSeq(events, cutoff+1, Len(events))
         /\ pc' = [pc EXCEPT !["pruner"] = "Prune"]
         /\ UNCHANGED << lock, to_process, next_id, eid >>

pruner == Prune

CheckDone == /\ pc["checkdone"] = "CheckDone"
             /\ events = <<>>
             /\ next_id > MaxId
             /\ pc' = [pc EXCEPT !["checkdone"] = "CheckDone"]
             /\ UNCHANGED << lock, to_process, events, next_id, eid >>

checkdone == CheckDone

(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
               /\ UNCHANGED vars

Next == queuer \/ pruner \/ checkdone
           \/ (\E self \in Threads: thread(self))
           \/ Terminating

Spec == /\ Init /\ [][Next]_vars
        /\ \A self \in Threads : WF_vars(thread(self))
        /\ WF_vars(queuer)
        /\ WF_vars(pruner)

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION 
====