# Re: [tlaplus] Modelling thread preemption

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: