Re: [tlaplus] Modelling thread preemption

Hi,

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.

Thanks.

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

CONSTANTS	CPU,
		THREADS

(* --algorithm sched {
variables
	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()
{
interrupt_handler:
	\* re-schedule
	with (t \in THREADS)
		current := t;
ret_from_interrupt:
	\* Never pass this point
	await FALSE;
}

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

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

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

PreemptNext == Interrupt(CPU) \/ Next

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