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