| Mixing TLA+ and PlusCal looks a bit adventurous to me. If you start along these lines, why not go all the way to a TLA+ spec? But then, it seems to me that you just model a non-deterministic choice between invoking the interrupt handler or continuing processing the current thread, and PlusCal's either-or statement can be used for that. Below is a spec along these lines, including relevant fairness properties that ensure that (i) the interrupt handler is invoked from time to time and (ii) that every unfinished thread will eventually be scheduled. These guarantee the liveness property that you want. Regards, Stephan ------------------------------- MODULE sched ------------------------------- EXTENDS Sequences, TLC CONSTANTS CPU, THREADS (* --algorithm sched { variables current = "idle"; in_interrupt = FALSE; worked = [t \in THREADS |-> FALSE]; define { TypeInv == /\ current \in THREADS \cup {"idle"} /\ worked \in [THREADS -> BOOLEAN] AllWorked == <>(\A t \in THREADS : worked[t]) } procedure interrupt() { interrupt_handler: in_interrupt := TRUE; \* re-schedule with (t \in THREADS) current := t; ret_from_interrupt: in_interrupt := FALSE; return; } procedure thread() { main_loop: while (TRUE) { either { call interrupt() } or { skip }; continue: assert ~in_interrupt; worked[current] := TRUE; } } process (Processor = CPU) { start_cpu: with (t \in THREADS) { current := t; call thread(); }; } } *) \* BEGIN TRANSLATION \* elided \* END TRANSLATION Fairness == \* ensure progress /\ WF_vars(Next) \* make sure that the interrupt handler will be activated eventually /\ SF_vars(main_loop(CPU) /\ pc'[CPU] = "interrupt_handler") \* make sure every non-finished thread is eventually scheduled /\ \A t \in THREADS : SF_vars(interrupt_handler(CPU) /\ ~worked[t] /\ current' = t) FairSpec == Spec /\ Fairness =============================================================================
|