[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Modelling thread preemption


I came up with a different approach which mimics better what the CPU and an OS kernel does. Basically there is a single PlusCal process (as there is a single PC per CPU) which can be interrupted and a different thread scheduled in. I no longer use the generated Spec but I defined my own PreemptableNext / PreemptableSpec which either handles the interrupt entry/return or continues running the current thread.

It does look like reverse engineering what PlusCal generates though. Although I tried adding some fairness properties, checking AllWorked fails (I have to read some more about these). I assumed this was expected since PreemptableNext is allowed to keep taking an interrupt and the threads would not make any progress (DoS can happen in real OS as well). As a quick test to check that it actually preempts threads, I added a counter increment/decrement and without interrupts disabled around this update I hit the SchedInv.

BTW, is it allowed to just do "UNCHANGED vars" and TLC only take into account those that haven't been modified by the action? If I am to develop the model further, I find it a bit tedious to keep updating HandleInt and ReturnInt actions for any new variable.


------------------------------ MODULE sched2 --------------------------------
EXTENDS Naturals, Sequences, FiniteSets, TLC


(* --algorithm sched {
current = "idle";
in_interrupt = FALSE;
interrupts_on = FALSE;
worked = [t \in THREADS |-> FALSE];
thread_pc = [t \in THREADS |-> "start_thread"];
thread_stack = [t \in THREADS |-> << >>];

\* concurrency test
count = 0;

define {
\* Handle interrupt. Save current thread context and invoke handler
HandleInt(self) == /\ interrupts_on \* only when interrupts are enabled
   /\ interrupts_on' = FALSE \* turn interrupts off
   /\ in_interrupt' = TRUE
   /\ thread_pc' = [thread_pc EXCEPT ![current] = pc[self]]
   /\ thread_stack' = [thread_stack EXCEPT ![current] = stack[self]]
   /\ pc' = [pc EXCEPT ![self] = "interrupt_handler"]
   /\ UNCHANGED <<current, worked, stack, count>>

\* Return from interrupt. Restore current thread context
ReturnInt(self) == /\ pc[self] = "ret_from_interrupt"
   /\ pc' = [pc EXCEPT ![self] = thread_pc[current]]
   /\ stack' = [stack EXCEPT ![self] = thread_stack[current]]
   /\ in_interrupt' = FALSE
   /\ interrupts_on' = TRUE \* re-enable interrupts
   /\ UNCHANGED <<current, worked, thread_pc, thread_stack, count>>

Interrupt(self) == HandleInt(self) \/ ReturnInt(self)

TypeInv == /\ current \in THREADS \cup {"idle"}
   /\ worked \in [THREADS -> BOOLEAN]

SchedInv == count < Cardinality(THREADS)

AllWorked == <>(\A t \in THREADS : worked[t])

procedure interrupt()
\* re-schedule
with (t \in THREADS)
current := t;
\* Never pass this point
await FALSE;

procedure thread()
interrupts_on := TRUE;
while (TRUE) {
assert ~in_interrupt;
worked[current] := TRUE;

\* Concurrency test (should not trigger if ~interrupts_on)
interrupts_on := FALSE;
count := count + 1;
count := count - 1;
interrupts_on := TRUE;

process (Processor = CPU)
with (t \in THREADS) {
current := t;
call thread();
} *)
\* removed

PreemptNext == Interrupt(CPU) \/ Next

PreemptSpec == Init /\ [][PreemptNext]_vars