Modelling thread preemption

[Catalin Marinas]

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

[1] https://git.kernel.org/pub/scm/linux/kernel/git/cmarinas/kernel-tla.git/tree/asidalloc.tla

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:

sched.tla:

------------------------------ 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

[Stephan Merz]

Hi,

I made a few changes to your module:

- I turned your procedures into macros: that's not essential, but since there is no recursion, the procedure bodies contain simple straight-line code, and you have a label in front of every call anyway, it looks more natural to me, the translation to TLA+ gets simpler, and the number of states is reduced a lot due to the rather useless intermediate states.

- I removed the startup code from the threads: I didn't understand why the initial processor assignment would be based on a race rather than on a decision by the scheduler (through the "schedule" operation). This allowed me to get rid of your hack with making ProcSet dynamic: a thread can execute only if it is the chosen one, although the set of potentially executable threads is static.

- Consequently, I initialized "running" to the empty set. I also rewrote the invariant to a formulation that looks easier to me.

For your module, verification of liveness fails because the generated fairness condition is

        /\ \A self \in running : WF_vars(Thread(self)) /\ WF_vars(do_work(self))

and TLC can only handle quantifiers over constant sets in liveness checking. With the above modifications, the bound of the quantifier is THREADS and liveness checking becomes possible. However, TLC produces a counter-example in which a terminated thread gets scheduled repeatedly although there is some non-terminated thread.

I therefore rewrote the schedule operation so that it will only schedule threads that have not finished (and "idle" if all threads have finished). Now, assuming weak fairness we still get a counter-example in which an executable thread gets scheduled but pre-empted before it does any work. This happens because the thread is not persistently executable (it can't execute while the interrupt handler is active). Using strong fairness for the threads the liveness condition is checked.

The overall module is below. I am not saying that it is better than yours: some changes are purely stylistic in nature.

Best regards,

Stephan

------------------------------- MODULE sched -------------------------------

EXTENDS Naturals, Sequences, FiniteSets, TLC

CONSTANTS CPU,

 THREADS

 

ASSUME CPU \notin THREADS

(* --algorithm sched {

variables

 running = {};

 current = "idle";

 worked = [t \in THREADS |-> FALSE];

define {

 executable ==  \* threads eligible for scheduling

   {th \in THREADS : ~ worked[th]}

 SchedInv == \/ current = "idle" /\ running = {}

             \/ running = {current}

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

}

macro do_work(thread)

{

 worked[thread] := TRUE;

}

macro do_handler()

{

 skip; \* some work

}

macro schedule()

{

 \* pick any executable thread, even the current one

 if (executable = {}) {

   running := {}; current := "idle"

 } else {

   with (t \in executable) {

     running := {t};

     current := t

   }

 };

}

\* Threads

fair+ process (Thread \in THREADS)

{

main:

 while (TRUE) { 

   await(current = self);

   do_work(self)

 }

}

\* Interrupts

fair process (Interrupt = CPU)

{

interrupt:

 while (TRUE) {

 \* stop current thread

 running := {};

 current := "idle";

handler:

 do_handler();

resched:

 schedule();

 }

}

} *)

=============================================================================

On 12 Jan 2018, at 15:09, Catalin Marinas <catalin...@gmail.com> wrote:

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 TLA+ process matches closely the way Linux kernel programmers think about concurrency and preemption. The interrupt handler is modelled as yet another TLA+ process. All these processes (threads and interrupt handler) race to modify some CPU state (not defined here).

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Catalin Marinas]

Hi Stephan,

Thanks for your reply. Some comments below, inlined:

On Friday, 12 January 2018 17:34:24 UTC, Stephan Merz wrote:

- I turned your procedures into macros: that's not essential, but since there is no recursion, the procedure bodies contain simple straight-line code, and you have a label in front of every call anyway, it looks more natural to me, the translation to TLA+ gets simpler, and the number of states is reduced a lot due to the rather useless intermediate states.

My spec was simplified to keep it short but something like do_work() is going to be large enough not to be a macro. Also, a macro does not allow labels and I really want to check a race condition between threads. For example, a thread is updating two CPU registers, say ttbr0 and ttbr1 (page table pointers). Being interrupted between these two non-atomic updates can have implications if the interrupt handler or another scheduled thread touch the same registers.

With additional labels, the only way to stop a thread when scheduled out is to add "await(current = self)" for every label.

 

- I removed the startup code from the threads: I didn't understand why the initial processor assignment would be based on a race rather than on a decision by the scheduler (through the "schedule" operation). This allowed me to get rid of your hack with making ProcSet dynamic: a thread can execute only if it is the chosen one, although the set of potentially executable threads is static.

This was indeed a hack. I could have added an await(current = self) at the start instead.

 

- Consequently, I initialized "running" to the empty set. I also rewrote the invariant to a formulation that looks easier to me.

Since Thread was defined "\in running", I needed "running" (and ProcSet) to include all processes initially otherwise Init doesn't do what's expected. Defining Thread \in THREADS needs additional await statements on each label of the process.

 

For your module, verification of liveness fails because the generated fairness condition is

        /\ \A self \in running : WF_vars(Thread(self)) /\ WF_vars(do_work(self)) 

 

and TLC can only handle quantifiers over constant sets in liveness checking. With the above modifications, the bound of the quantifier is THREADS and liveness checking becomes possible.

Indeed.

 

However, TLC produces a counter-example in which a terminated thread gets scheduled repeatedly although there is some non-terminated thread.

I therefore rewrote the schedule operation so that it will only schedule threads that have not finished (and "idle" if all threads have finished). Now, assuming weak fairness we still get a counter-example in which an executable thread gets scheduled but pre-empted before it does any work. This happens because the thread is not persistently executable (it can't execute while the interrupt handler is active). Using strong fairness for the threads the liveness condition is checked.

Thanks for the hints and reworked module.

I'll keep thinking about a different level of abstraction (too much programming may have affected my mental modelling ;)).

 

Catalin

[Catalin Marinas]

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

==============================================================================

[Stephan Merz]

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

=============================================================================

[Catalin Marinas]

Hi Stephan,

On Friday, 19 January 2018 16:05:58 UTC, Stephan Merz wrote:

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?

The software programs I plan to model are easier to write (and read) in PlusCal than TLA+ (see the asidalloc.tla I mentioned in the original post). Also, working with a team of programmers it makes it simpler to reason about/review an algorithm.
 

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.

This was just a simple example and your proposed spec only has a single action for a thread ("continue"). The real algorithms I want to model contain a lot more actions per thread, each of them being preemptable by an interrupt. The liveness properties are not the end goal of my model, more of a check that that the threads are scheduled before going for checking different invariants.

I'll try to clarify what I'd like to model: a CPU (or more) executing a series of actions as described by a thread. Such series of actions can be suspended at (almost) any point and the interrupt handler actions executed. As with the thread, the interrupt handler won't have a single action and this is relevant on multi-CPU models. This is analogous to threads in an application running concurrently and being occasionally preempted by a signal handler.

One way to model this is my original post with threads and interrupt handler being separate processes (as an interrupt is asynchronous) but to model the thread preemption/suspension I ended up with a non-constant ProcSet.

What I'd really need here is a PlusCal extension which allows one to describe the process as:

  process (proc1 \in PROCS1 : P1(proc1))
  ...
  process (proc2 \in PROCS2 : P2(proc2))
  ...

PlusCal would generate a constant ProcSet == PROCS1 \cup PROCS2

However, every action of the process will only be enabled if P(self). For procedures, since they are shared by all processes, the actions would be enabled if:

continue(self):
  /\ pc[self] = "continue"
  /\ \/ (self \in PROCS1 /\ P1(self))
     \/ (self \in PROCS2 /\ P2(self))

Is PlusCal amenable to (backwards-compatible) changes?


As for not mixing PlusCal with TLA+, an alternative I've been thinking about (not sure it works, I haven't tried yet) is to define the thread processes in a separate module (say "threads") and instantiate it in the main "processor" module:

  T == INSTANCE threads

The CPU process either calls the interrupt handler or advances a T!Next step.

I would still prefer a PlusCal extension as suggested above though.
 

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.

Many thanks, especially for the fairness properties.

Regards,

Catalin