Hi,
The usual disclaimer for a first post to this group, I’m new to TLA+ (and I already found it useful discovering a couple of software bugs [1]).
What I’m trying to model now is OS thread preemption on a single CPU [2] (uniprocessor; my final model has multiple CPUs). Basically only one thread can run at a time (and modify the CPU state) while it can be interrupted and scheduled out at any point (well, based on the labels granularity). Modelling each thread as a PlusCal process matches closely the way Linux kernel programmers think about concurrency and preemption. The interrupt handler is modelled as yet another PlusCal process. All these processes (threads and interrupt handler) race to modify some CPU state (not defined here).
Since only one process is allowed to run at a time, I found it easier to make ProcSet non-constant: the union of a dynamically changing "running" processes and the CPU. Note that an interrupt handler doesn’t run in parallel with any other process ("running" is emptied temporarily).
While it seems to work, the downside is that "running" being non-constant causes TLC to not be able to check some temporal properties ("AllWorked" in the spec below), complaining that it cannot handle the temporal formula Spec (I used 'pcal -wf' for fairness). If I ignore this property, it seems to check successfully but wanted to ensure that each thread is eventually scheduled.
Defining the process Thread \in THREADS wouldn't go well with enforcing a single thread "active" at a time (between two schedule() calls) unless I add some "await" statement after every label (not really feasible).
The alternative I was thinking of is to define a single process (per CPU) which would either call the interrupt handler or the current thread. However, modelling thread preemption would require modelling the thread execution as a state machine manually with something like a "thread_pc", pretty much mimicking what PlusCal generates but harder to read.
My question: is there a better solution? Or I should go for a deeper abstraction than just modelling OS threads directly?
Thanks,
Catalin
In the ARM architecture (and not only), the TLB entries (cache for virtual to physical address translation) are tagged with an ASID (application-specific id), unique per process (threads of an application share the same ASID). Since the number of ASIDs can be smaller than the number of processes running, we have an algorithm in Linux to re-use such ASIDs without forcing a temporary stop of all the CPUs when running out. TLC confirmed one bug+fix that we were investigating (the CnP case in the spec) and discovered a new one after nearly 200 steps (
http://lists.infradead.org/pipermail/linux-arm-kernel/2018-January/551765.html).
[2] Simplified preemptible threads model. SMP, various threads state and type invariants removed here to keep things short:
------------------------------ MODULE sched ---------------------------------
EXTENDS Naturals, Sequences, FiniteSets, TLC
CONSTANTS CPU,
THREADS
(* --algorithm sched {
variables
running = THREADS;
current = "idle";
worked = [t \in THREADS |-> FALSE];
define {
SchedInv == /\ \A t \in running : current \in {t, "idle"}
/\ current # "idle" => Cardinality(running) <= 1
AllWorked == <>(\A t \in THREADS : worked[t])
}
procedure do_work(thread)
{
do_work:
worked[thread] := TRUE;
return;
}
procedure do_handler()
{
do_handler:
skip; \* some work
return;
}
procedure schedule()
{
schedule:
\* pick any thread, even the current one
with (t \in THREADS) {
running := {t};
current := t;
};
return;
}
\* Threads
process (Thread \in running)
{
init_thread:
\* only a single thread allowed at the same time
running := {self};
current := self;
start_thread:
assert self \in running;
main:
while (TRUE)
call do_work(self);
}
\* Interrupts
process (Interrupt = CPU)
{
interrupt:
while (TRUE) {
\* stop current thread
running := {};
handler:
call do_handler();
resched:
call schedule();
}
}
} *)
==============================================================================
sched.cfg:
SPECIFICATION Spec
CONSTANT defaultInitValue = defaultInitValue
\* Add statements after this line.
CONSTANTS CPU = p1
THREADS = {t1, t2}
INVARIANTS SchedInv
\*PROPERTY AllWorked