stealing.tla

----------------------------- MODULE stealing -----------------------------
EXTENDS TLC, Sequences, Integers, FiniteSets

PT == INSTANCE PT

\* Assume input is the dynamic task graph:
\*
\*                T1
\*             /   \    \
\*            T2    T3  T4
\*         /  \  \
\*        T5  T6 T7


\*CONSTANTS Managers, Executers

\* Model parameters
\* Managers and Executers must have a unique ID for TLC to work as intented
\* Assume that the id of an executer that belongs to a specific manager
\* has as id the id of the manager + 1
Managers == {1,3} \* unique manager IDs
Executers == {2,4} \* unique executer IDs
Tasks == <<1,2,3,4,5,6,7>>
MakeDeps == << {2,3,4}, {5,6,7}, {}, {}, {}, {}, {} >>
\* Stop dependencies: for each task, list the tasks that have a stop dependency on them
StopDeps == << 0, 1, 1, 1, 2, 2, 2 >>
\*Start dependencies: for each task, list the tasks that have a start dependency on them
StartDeps == << 0, 4, 4, 0, 7, 7, 0 >> 
StartCtr == << 0, 0, 0, 2, 0, 0, 2 >>
StopCtr == << 3, 3, 0, 0, 0, 0, 0 >>
validExecutionOrders == { << 5, 6, 7, 2, 3, 4, 1 >>
                          \*<< 5, 6, 7, 3, 2, 4, 1 >>, 
                          \*<< 5, 6, 3, 7, 2, 4, 1 >>,
                          \*<< 6, 5, 7, 2, 3, 4, 1 >>,
                          \*<< 6, 5, 7, 3, 2, 4, 1 >>,
                          \*<< 6, 5, 3, 7, 2, 4, 1 >>,
                          \*<< 3, 5, 6, 7, 2, 4, 1 >>,
                          \*<< 3, 6, 5, 7, 2, 4, 1 >>    
                        }

executerID(mID) == mID + 1
managerID(eID) == eID -1

seqToSet(seq) ==  { seq[i] : i \in DOMAIN seq }

allCtrZero(sctr) == IF Cardinality({ ctr \in seqToSet(sctr) : ctr > 0 }) > 0 THEN FALSE ELSE TRUE

validExecutionOrder(order, valids) == IF Cardinality ({ valid \in valids : order = valid }) > 0 THEN TRUE ELSE FALSE

\* helper function for the manager:
\* removes a message from its own queue + adds a new message to itself (which can be empty)
\* adds a message to an external queue (which can be empty)
\* leaves all other queues as is
\* this helper function is needed because we can only have one state update to a variable in a block
updateChannels(id1, msg1, id2, msg2, channels) ==
    [ id \in DOMAIN(channels) |-> 
      CASE id = id1 -> Tail(channels[id1]) \o msg1
           [] id = id2 -> channels[id2] \o msg2
           [] OTHER -> channels[id]
    ]              

\*Msg types
TASK_MAKE_AND_SCHEDULE == 1 \* message to trigger "making" and "scheduling" the child tasks of a task  
TASK_EXECUTED          == 2 \* message to trigger a task has "finished executing"
TASK_DONE              == 3 \* message to trigger the finalization of a task, i.e. when a task's children are done an therefore all its stop dependencies are resolved
MANA_TERM              == 4 \* message to stop the manager process
TASK_STEAL             == 5 \* message to steal a task
TASK_STEAL_FAILED      == 6 \* message to signal there is nothing to steal
TASK_STOLEN            == 7 \* message to pass a stolen task to the thief

(*--algorithm stealing
    variables eChannels = [e \in Executers |-> <<>>]; \* channels to communicate with executers
              mChannels = [m \in Managers  |-> <<>>]; \* channels to communicate with managers
              tCtr = 0; \* ctr to count the number of tasks executed
              stopCtr = StopCtr; \*todo make function to fill this in based on deps
              startCtr = StartCtr;
              doneTasks = <<>>; \* to track the tasks that are executed
    
process manager \in Managers
    variables ready = {}; \* tasks ready for execution
              pending = {}; \* tasks with unresolved start dependecies
              eID = executerID(self); \* ID of the executer associated with this manager
              terminate = FALSE; \* flag to stop the manager
              \* support variables
              msg;
              sdep = 0;
              tdep = 0;
              newMsg = <<>>;
              extMsg = <<>>;
              extID = 1;
              stealing = FALSE; \* variable to track if a manager is stealing
              stolenTasks = {}; \* keep track of tasks that were stolen
              foundStolen = {};
    begin 
        SetupManager:
            \* bootstrap: give the first task to the first manager
            if self = 1 then
                ready := {Head(Tasks)};
            end if;
            \*print <<"Readied ", self, " queue: ", ready>>;
        \*CheckTerminate:
            \* stop manager execution by force
          \*  if terminate then
           \*     goto Done;
            \*end if;
        CheckTasksDone:
            \* reset all local vars to be safe
            sdep := 0;
            tdep := 0;
            newMsg := <<>>;
            extMsg := <<>>;
            extID := 1;
            foundStolen := {};
            \* stop manager execution when all tasks have been executed
            \*print <<"TCtr: ", tCtr, " ts: ", doneTasks, " stop ctr: ", stopCtr>>;
            if tCtr >= Len(Tasks) then
                print <<"Tasks done: ", doneTasks >>;
                assert allCtrZero(startCtr);
                assert allCtrZero(stopCtr);
                assert validExecutionOrder(doneTasks, validExecutionOrders);
                goto Done;
            end if;
        CheckMsgs:
            \* Messages
            if mChannels[self] /= <<>> then
               msg := Head(mChannels[self]);
               \*print <<"Processing msg: ", msg>>;
               if msg.msg = TASK_MAKE_AND_SCHEDULE then
                    \* "create" and "schedule" the child tasks of a given task
                    ready := ready \union { r \in MakeDeps[msg.id] : StartCtr[r] = 0};
                    pending := pending \union { p \in MakeDeps[msg.id] : StartCtr[p] > 0};
                    \*print <<"Make and schedule: ", msg, " ready: ", ready, " pending: ", pending >>;
               elsif msg.msg = TASK_EXECUTED /\ StopCtr[msg.id] = 0 then
                    \*print <<"Sending Task Done: ", msg.id, " on: ", eID>>;
                    newMsg := <<[msg |-> TASK_DONE, id |-> msg.id]>>;
               elsif msg.msg = TASK_STEAL /\ ready /= {} then
                     with task \in ready do
                          ready := ready \ {task};
                          extID := msg.thief;
                          extMsg := << [msg |-> TASK_STOLEN, id |-> task, victim |-> self]>>;
                     end with;
               elsif msg.msg = TASK_STEAL /\ ready = {} then
                    extID := msg.thief;
                    extMsg := << [msg |-> TASK_STEAL_FAILED, victim |-> self] >>;
               elsif msg.msg = TASK_STEAL_FAILED then
                    stealing := FALSE;
               elsif msg.msg = TASK_STOLEN then
                    stolenTasks := stolenTasks \union {<<msg.id, msg.victim>>};
                    \* send the task to the executer
                    \* should we model that we can be already executing? probably..
                    eChannels[eID] := eChannels[eID] \o << msg.id >>;
                    stealing := FALSE;
               elsif msg.msg = TASK_DONE then
                    \*print <<"Task done: ", msg.id, " ", stopCtr >>;
                    \* if the task is stolen, forward it to the owner
                    foundStolen :=  { st \in stolenTasks: Head(st) = msg.id};
                    if foundStolen /= {} then
                            with stolen \in foundStolen do
                                stolenTasks := stolenTasks \ foundStolen;
                                extID := Head(Tail(stolen));
                                extMsg := << [msg |-> TASK_DONE, id |-> msg.id] >>;
                            end with;
                    else
                        tCtr := tCtr + 1;
                        doneTasks := doneTasks \o <<msg.id>>;
                        \*if msg.id = Head(Tasks) then
                        \*    print <<"Root tasks done ", tCtr, " ", doneTasks>>;
                        \*end if; 
                        if msg.id /= Head(Tasks) then \* skip the root task, it has nothing pending on it
                            \* update start dependency
                            sdep := StartDeps[msg.id];
                            if sdep /= 0 then \* there is a start dependency, 0 is no dependencies
                                startCtr[sdep] := startCtr[sdep] - 1;
                                if startCtr[sdep] = 0 then
                                    \*ready the task for execution because all start dependencies are resolved
                                    \*print <<"ready task: ", sdep>>;
                                    ready := ready \union {sdep};
                                    pending := pending \ {sdep};
                                end if;
                            end if;
                            \* update stop dependency
                            tdep := StopDeps[msg.id];
                            \*print <<"tdep: ", tdep, " for: ", msg.id>>;
                            if tdep /= 0 then
                                stopCtr[tdep] := stopCtr[tdep] - 1;
                                \*print <<"stop ctr: ", stopCtr[tdep], " for: ", msg.id>>;
                                if stopCtr[tdep] = 0 then
                                    newMsg := <<[msg |-> TASK_DONE, id |-> tdep]>>;
                                end if;
                            end if;
                        end if;
                    end if;
               end if;
               mChannels := updateChannels(self, newMsg, extID, extMsg, mChannels);
            end if; 
        Schedule:
            \*print <<"Check schedule: ", ready >>; 
            if ready /= {} then
                with task \in ready do
                    ready := ready \ {task};
                    eChannels[eID] := eChannels[eID] \o <<task>>;
                \*print <<"Scheduled from", self, " ", eChannels>>;
                end with;
            elsif ~stealing then
                stealing := TRUE;
                with worker \in Managers \ {self} do
                    mChannels[worker] := mChannels[worker] \o << [ msg |-> TASK_STEAL, thief |-> self ] >>; 
                end with;
            end if;
            goto CheckTasksDone;
end process;

fair process executer \in Executers
    variables mid = managerID(self);
              tid;
    begin
        Execute:
            if eChannels[self] /= <<>> then
                tid := Head(eChannels[self]);
                eChannels[self] := Tail(eChannels[self]);
                \*print <<"Executing ", tid>>;
                mChannels[mid] := mChannels[mid] \o <<[msg |-> TASK_MAKE_AND_SCHEDULE, id |-> tid], [msg |-> TASK_EXECUTED, id |-> tid]>>;
            end if;
            goto Execute;
end process;
end algorithm; *)

\*------------------------------ MODULE Stealing ------------------------------
\*EXTENDS TLC, Sequences, Integers

\*PT == INSTANCE PT

\*CONSTANTS Tasks, StopDeps, StartDeps, MakeDeps
\* Assume input is the dynamic task graph:
\*
\*                T1
\*             /   \    \
\*            T2    T3  T4
\*         /  \  \
\*        T5  T6 T7

\*Tasks     == {1, 2, 3, 4, 5, 6, 7}
\*MakeDeps  == << <<2, 3, 4>>, <<5, 6, 7>>, <<>>, <<>>, <<>>, <<>>, <<>> >>
\*StopDeps  == << <<2, 3, 4>>, <<5, 6, 7>>, <<>>, <<>>, <<>>, <<>>, <<>> >>
\*StartDeps == << <<>>, <<>>, <<>>, <<2, 3>>, <<>>, <<>>, <<5, 6>> >>
\*Executers == {1}
\*Managers  == {1}
\* BEGIN TRANSLATION (chksum(pcal) = "368357e3" /\ chksum(tla) = "337d1daf")
CONSTANT defaultInitValue
VARIABLES eChannels, mChannels, tCtr, stopCtr, startCtr, doneTasks, pc, ready, 
          pending, eID, terminate, msg, sdep, tdep, newMsg, extMsg, extID, 
          stealing, stolenTasks, foundStolen, mid, tid

vars == << eChannels, mChannels, tCtr, stopCtr, startCtr, doneTasks, pc, 
           ready, pending, eID, terminate, msg, sdep, tdep, newMsg, extMsg, 
           extID, stealing, stolenTasks, foundStolen, mid, tid >>

ProcSet == (Managers) \cup (Executers)

Init == (* Global variables *)
        /\ eChannels = [e \in Executers |-> <<>>]
        /\ mChannels = [m \in Managers  |-> <<>>]
        /\ tCtr = 0
        /\ stopCtr = StopCtr
        /\ startCtr = StartCtr
        /\ doneTasks = <<>>
        (* Process manager *)
        /\ ready = [self \in Managers |-> {}]
        /\ pending = [self \in Managers |-> {}]
        /\ eID = [self \in Managers |-> executerID(self)]
        /\ terminate = [self \in Managers |-> FALSE]
        /\ msg = [self \in Managers |-> defaultInitValue]
        /\ sdep = [self \in Managers |-> 0]
        /\ tdep = [self \in Managers |-> 0]
        /\ newMsg = [self \in Managers |-> <<>>]
        /\ extMsg = [self \in Managers |-> <<>>]
        /\ extID = [self \in Managers |-> 1]
        /\ stealing = [self \in Managers |-> FALSE]
        /\ stolenTasks = [self \in Managers |-> {}]
        /\ foundStolen = [self \in Managers |-> {}]
        (* Process executer *)
        /\ mid = [self \in Executers |-> managerID(self)]
        /\ tid = [self \in Executers |-> defaultInitValue]
        /\ pc = [self \in ProcSet |-> CASE self \in Managers -> "SetupManager"
                                        [] self \in Executers -> "Execute"]

SetupManager(self) == /\ pc[self] = "SetupManager"
                      /\ IF self = 1
                            THEN /\ ready' = [ready EXCEPT ![self] = {Head(Tasks)}]
                            ELSE /\ TRUE
                                 /\ ready' = ready
                      /\ pc' = [pc EXCEPT ![self] = "CheckTasksDone"]
                      /\ UNCHANGED << eChannels, mChannels, tCtr, stopCtr, 
                                      startCtr, doneTasks, pending, eID, 
                                      terminate, msg, sdep, tdep, newMsg, 
                                      extMsg, extID, stealing, stolenTasks, 
                                      foundStolen, mid, tid >>

CheckTasksDone(self) == /\ pc[self] = "CheckTasksDone"
                        /\ sdep' = [sdep EXCEPT ![self] = 0]
                        /\ tdep' = [tdep EXCEPT ![self] = 0]
                        /\ newMsg' = [newMsg EXCEPT ![self] = <<>>]
                        /\ extMsg' = [extMsg EXCEPT ![self] = <<>>]
                        /\ extID' = [extID EXCEPT ![self] = 1]
                        /\ foundStolen' = [foundStolen EXCEPT ![self] = {}]
                        /\ IF tCtr >= Len(Tasks)
                              THEN /\ PrintT(<<"Tasks done: ", doneTasks >>)
                                   /\ Assert(allCtrZero(startCtr), 
                                             "Failure of assertion at line 118, column 17.")
                                   /\ Assert(allCtrZero(stopCtr), 
                                             "Failure of assertion at line 119, column 17.")
                                   /\ Assert(validExecutionOrder(doneTasks, validExecutionOrders), 
                                             "Failure of assertion at line 120, column 17.")
                                   /\ pc' = [pc EXCEPT ![self] = "Done"]
                              ELSE /\ pc' = [pc EXCEPT ![self] = "CheckMsgs"]
                        /\ UNCHANGED << eChannels, mChannels, tCtr, stopCtr, 
                                        startCtr, doneTasks, ready, pending, 
                                        eID, terminate, msg, stealing, 
                                        stolenTasks, mid, tid >>

CheckMsgs(self) == /\ pc[self] = "CheckMsgs"
                   /\ IF mChannels[self] /= <<>>
                         THEN /\ msg' = [msg EXCEPT ![self] = Head(mChannels[self])]
                              /\ IF msg'[self].msg = TASK_MAKE_AND_SCHEDULE
                                    THEN /\ ready' = [ready EXCEPT ![self] = ready[self] \union { r \in MakeDeps[msg'[self].id] : StartCtr[r] = 0}]
                                         /\ pending' = [pending EXCEPT ![self] = pending[self] \union { p \in MakeDeps[msg'[self].id] : StartCtr[p] > 0}]
                                         /\ UNCHANGED << eChannels, tCtr, 
                                                         stopCtr, startCtr, 
                                                         doneTasks, sdep, tdep, 
                                                         newMsg, extMsg, extID, 
                                                         stealing, stolenTasks, 
                                                         foundStolen >>
                                    ELSE /\ IF msg'[self].msg = TASK_EXECUTED /\ StopCtr[msg'[self].id] = 0
                                               THEN /\ newMsg' = [newMsg EXCEPT ![self] = <<[msg |-> TASK_DONE, id |-> msg'[self].id]>>]
                                                    /\ UNCHANGED << eChannels, 
                                                                    tCtr, 
                                                                    stopCtr, 
                                                                    startCtr, 
                                                                    doneTasks, 
                                                                    ready, 
                                                                    pending, 
                                                                    sdep, tdep, 
                                                                    extMsg, 
                                                                    extID, 
                                                                    stealing, 
                                                                    stolenTasks, 
                                                                    foundStolen >>
                                               ELSE /\ IF msg'[self].msg = TASK_STEAL /\ ready[self] /= {}
                                                          THEN /\ \E task \in ready[self]:
                                                                    /\ ready' = [ready EXCEPT ![self] = ready[self] \ {task}]
                                                                    /\ extID' = [extID EXCEPT ![self] = msg'[self].thief]
                                                                    /\ extMsg' = [extMsg EXCEPT ![self] = << [msg |-> TASK_STOLEN, id |-> task, victim |-> self]>>]
                                                               /\ UNCHANGED << eChannels, 
                                                                               tCtr, 
                                                                               stopCtr, 
                                                                               startCtr, 
                                                                               doneTasks, 
                                                                               pending, 
                                                                               sdep, 
                                                                               tdep, 
                                                                               newMsg, 
                                                                               stealing, 
                                                                               stolenTasks, 
                                                                               foundStolen >>
                                                          ELSE /\ IF msg'[self].msg = TASK_STEAL /\ ready[self] = {}
                                                                     THEN /\ extID' = [extID EXCEPT ![self] = msg'[self].thief]
                                                                          /\ extMsg' = [extMsg EXCEPT ![self] = << [msg |-> TASK_STEAL_FAILED, victim |-> self] >>]
                                                                          /\ UNCHANGED << eChannels, 
                                                                                          tCtr, 
                                                                                          stopCtr, 
                                                                                          startCtr, 
                                                                                          doneTasks, 
                                                                                          ready, 
                                                                                          pending, 
                                                                                          sdep, 
                                                                                          tdep, 
                                                                                          newMsg, 
                                                                                          stealing, 
                                                                                          stolenTasks, 
                                                                                          foundStolen >>
                                                                     ELSE /\ IF msg'[self].msg = TASK_STEAL_FAILED
                                                                                THEN /\ stealing' = [stealing EXCEPT ![self] = FALSE]
                                                                                     /\ UNCHANGED << eChannels, 
                                                                                                     tCtr, 
                                                                                                     stopCtr, 
                                                                                                     startCtr, 
                                                                                                     doneTasks, 
                                                                                                     ready, 
                                                                                                     pending, 
                                                                                                     sdep, 
                                                                                                     tdep, 
                                                                                                     newMsg, 
                                                                                                     extMsg, 
                                                                                                     extID, 
                                                                                                     stolenTasks, 
                                                                                                     foundStolen >>
                                                                                ELSE /\ IF msg'[self].msg = TASK_STOLEN
                                                                                           THEN /\ stolenTasks' = [stolenTasks EXCEPT ![self] = stolenTasks[self] \union {<<msg'[self].id, msg'[self].victim>>}]
                                                                                                /\ eChannels' = [eChannels EXCEPT ![eID[self]] = eChannels[eID[self]] \o << msg'[self].id >>]
                                                                                                /\ stealing' = [stealing EXCEPT ![self] = FALSE]
                                                                                                /\ UNCHANGED << tCtr, 
                                                                                                                stopCtr, 
                                                                                                                startCtr, 
                                                                                                                doneTasks, 
                                                                                                                ready, 
                                                                                                                pending, 
                                                                                                                sdep, 
                                                                                                                tdep, 
                                                                                                                newMsg, 
                                                                                                                extMsg, 
                                                                                                                extID, 
                                                                                                                foundStolen >>
                                                                                           ELSE /\ IF msg'[self].msg = TASK_DONE
                                                                                                      THEN /\ foundStolen' = [foundStolen EXCEPT ![self] = { st \in stolenTasks[self]: Head(st) = msg'[self].id}]
                                                                                                           /\ IF foundStolen'[self] /= {}
                                                                                                                 THEN /\ \E stolen \in foundStolen'[self]:
                                                                                                                           /\ stolenTasks' = [stolenTasks EXCEPT ![self] = stolenTasks[self] \ foundStolen'[self]]
                                                                                                                           /\ extID' = [extID EXCEPT ![self] = Head(Tail(stolen))]
                                                                                                                           /\ extMsg' = [extMsg EXCEPT ![self] = << [msg |-> TASK_DONE, id |-> msg'[self].id] >>]
                                                                                                                      /\ UNCHANGED << tCtr, 
                                                                                                                                      stopCtr, 
                                                                                                                                      startCtr, 
                                                                                                                                      doneTasks, 
                                                                                                                                      ready, 
                                                                                                                                      pending, 
                                                                                                                                      sdep, 
                                                                                                                                      tdep, 
                                                                                                                                      newMsg >>
                                                                                                                 ELSE /\ tCtr' = tCtr + 1
                                                                                                                      /\ doneTasks' = doneTasks \o <<msg'[self].id>>
                                                                                                                      /\ IF msg'[self].id /= Head(Tasks)
                                                                                                                            THEN /\ sdep' = [sdep EXCEPT ![self] = StartDeps[msg'[self].id]]
                                                                                                                                 /\ IF sdep'[self] /= 0
                                                                                                                                       THEN /\ startCtr' = [startCtr EXCEPT ![sdep'[self]] = startCtr[sdep'[self]] - 1]
                                                                                                                                            /\ IF startCtr'[sdep'[self]] = 0
                                                                                                                                                  THEN /\ ready' = [ready EXCEPT ![self] = ready[self] \union {sdep'[self]}]
                                                                                                                                                       /\ pending' = [pending EXCEPT ![self] = pending[self] \ {sdep'[self]}]
                                                                                                                                                  ELSE /\ TRUE
                                                                                                                                                       /\ UNCHANGED << ready, 
                                                                                                                                                                       pending >>
                                                                                                                                       ELSE /\ TRUE
                                                                                                                                            /\ UNCHANGED << startCtr, 
                                                                                                                                                            ready, 
                                                                                                                                                            pending >>
                                                                                                                                 /\ tdep' = [tdep EXCEPT ![self] = StopDeps[msg'[self].id]]
                                                                                                                                 /\ IF tdep'[self] /= 0
                                                                                                                                       THEN /\ stopCtr' = [stopCtr EXCEPT ![tdep'[self]] = stopCtr[tdep'[self]] - 1]
                                                                                                                                            /\ IF stopCtr'[tdep'[self]] = 0
                                                                                                                                                  THEN /\ newMsg' = [newMsg EXCEPT ![self] = <<[msg |-> TASK_DONE, id |-> tdep'[self]]>>]
                                                                                                                                                  ELSE /\ TRUE
                                                                                                                                                       /\ UNCHANGED newMsg
                                                                                                                                       ELSE /\ TRUE
                                                                                                                                            /\ UNCHANGED << stopCtr, 
                                                                                                                                                            newMsg >>
                                                                                                                            ELSE /\ TRUE
                                                                                                                                 /\ UNCHANGED << stopCtr, 
                                                                                                                                                 startCtr, 
                                                                                                                                                 ready, 
                                                                                                                                                 pending, 
                                                                                                                                                 sdep, 
                                                                                                                                                 tdep, 
                                                                                                                                                 newMsg >>
                                                                                                                      /\ UNCHANGED << extMsg, 
                                                                                                                                      extID, 
                                                                                                                                      stolenTasks >>
                                                                                                      ELSE /\ TRUE
                                                                                                           /\ UNCHANGED << tCtr, 
                                                                                                                           stopCtr, 
                                                                                                                           startCtr, 
                                                                                                                           doneTasks, 
                                                                                                                           ready, 
                                                                                                                           pending, 
                                                                                                                           sdep, 
                                                                                                                           tdep, 
                                                                                                                           newMsg, 
                                                                                                                           extMsg, 
                                                                                                                           extID, 
                                                                                                                           stolenTasks, 
                                                                                                                           foundStolen >>
                                                                                                /\ UNCHANGED << eChannels, 
                                                                                                                stealing >>
                              /\ mChannels' = updateChannels(self, newMsg'[self], extID'[self], extMsg'[self], mChannels)
                         ELSE /\ TRUE
                              /\ UNCHANGED << eChannels, mChannels, tCtr, 
                                              stopCtr, startCtr, doneTasks, 
                                              ready, pending, msg, sdep, tdep, 
                                              newMsg, extMsg, extID, stealing, 
                                              stolenTasks, foundStolen >>
                   /\ pc' = [pc EXCEPT ![self] = "Schedule"]
                   /\ UNCHANGED << eID, terminate, mid, tid >>

Schedule(self) == /\ pc[self] = "Schedule"
                  /\ IF ready[self] /= {}
                        THEN /\ \E task \in ready[self]:
                                  /\ ready' = [ready EXCEPT ![self] = ready[self] \ {task}]
                                  /\ eChannels' = [eChannels EXCEPT ![eID[self]] = eChannels[eID[self]] \o <<task>>]
                             /\ UNCHANGED << mChannels, stealing >>
                        ELSE /\ IF ~stealing[self]
                                   THEN /\ stealing' = [stealing EXCEPT ![self] = TRUE]
                                        /\ \E worker \in Managers \ {self}:
                                             mChannels' = [mChannels EXCEPT ![worker] = mChannels[worker] \o << [ msg |-> TASK_STEAL, thief |-> self ] >>]
                                   ELSE /\ TRUE
                                        /\ UNCHANGED << mChannels, stealing >>
                             /\ UNCHANGED << eChannels, ready >>
                  /\ pc' = [pc EXCEPT ![self] = "CheckTasksDone"]
                  /\ UNCHANGED << tCtr, stopCtr, startCtr, doneTasks, pending, 
                                  eID, terminate, msg, sdep, tdep, newMsg, 
                                  extMsg, extID, stolenTasks, foundStolen, mid, 
                                  tid >>

manager(self) == SetupManager(self) \/ CheckTasksDone(self)
                    \/ CheckMsgs(self) \/ Schedule(self)

Execute(self) == /\ pc[self] = "Execute"
                 /\ IF eChannels[self] /= <<>>
                       THEN /\ tid' = [tid EXCEPT ![self] = Head(eChannels[self])]
                            /\ eChannels' = [eChannels EXCEPT ![self] = Tail(eChannels[self])]
                            /\ mChannels' = [mChannels EXCEPT ![mid[self]] = mChannels[mid[self]] \o <<[msg |-> TASK_MAKE_AND_SCHEDULE, id |-> tid'[self]], [msg |-> TASK_EXECUTED, id |-> tid'[self]]>>]
                       ELSE /\ TRUE
                            /\ UNCHANGED << eChannels, mChannels, tid >>
                 /\ pc' = [pc EXCEPT ![self] = "Execute"]
                 /\ UNCHANGED << tCtr, stopCtr, startCtr, doneTasks, ready, 
                                 pending, eID, terminate, msg, sdep, tdep, 
                                 newMsg, extMsg, extID, stealing, stolenTasks, 
                                 foundStolen, mid >>

executer(self) == Execute(self)

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

Next == (\E self \in Managers: manager(self))
           \/ (\E self \in Executers: executer(self))
           \/ Terminating

Spec == /\ Init /\ [][Next]_vars
        /\ \A self \in Executers : WF_vars(executer(self))

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

\* END TRANSLATION 

=============================================================================
\* Modification History
\* Last modified Thu Nov 16 14:04:47 CET 2023 by caherzee
\* Created Thu Oct 19 16:25:45 CEST 2023 by caherzee