Previously
The previous post on the subject introduced the project I’m working on and why I’ve decided to use TLA+.
This post will take off from the end of that to complicate my specification to include something closer to what I need to implement.
Atomic labels
Closing the first post, I’ve said that a “step” in TLA+ is marked by a “label” and is “atomic”.
In the context of a process block, a label is anything that looks like This: (alpha and then a :). A label has a body of statements that happen inside it that will occur atomically, in the order they appear.
The best way I can explain it is with an example:
----------------------------- MODULE spec_loop -----------------------------
EXTENDS TLC, Integers
(*--algorithm loop
variables
accumulator = 0; \* Start with a value of 0.
define
AccumlatorLessThanEqualOne == accumulator <= 1 \* We'll use this as invariant.
end define;
fair process p \in {1,2} \* 2 processes will run at the same time.
begin
Increase_Accumulator:
accumulator := accumulator + 1;
Decrease_Accumulator:
accumulator := accumulator - 1;
end process
end algorithm;*)
=============================================================================
I’ve omitted the translation of the PlusCal code to TLC as it’s machine-generated and not that interesting.
I’ve set up my model to this:
What to check?-Temporal formulaDeadlock- checkedProperties- something that should eventually be true.Termination, both processes should terminate.
Invariants- citing the IDE “Formulas true in every reachable state”.AccumlatorLessThanEqualOne- the value of theaccumulatorvariable should be <= 1
The last part, the one where I set the AccumlatorLessThanEqualOne invariant, is the one that will make the model fail.
The model will fail because there is at least one state where the value of accumulator is not <= 1.
The TLA+ will report on such state:
The UI requires highlights in red what changed between a step and the next:
- At the
Initial predicate, the start of the model checking, the accumulator value is0, both processes will execute theIncrease_Accumulatorstep next, theAccumlatorLessThanEqualOneinvariant is not violated. - The model checking picks process 2 to execute its
Increase_Accumulatorstep: that will increaseaccumulatorby 1. All fine and dandy. - The model checking will, then, pick process 1 to execute, and that too will complete the
Increase_Accumulatorstep, adding 1 to theaccumulatorand violating, thus, theAccumlatorLessThanEqualOneinvariant.
The model checker output reads Invariant AccumlatorLessThanEqualOne is violated..
There is, indeed, a flow in which one process executes both steps, the Increase_Accumulator and Decrease_Accumulator ones, in sequence, and accumulator is never > 1.
But the model checker just verified that our logic will not hold under the pressure of concurrency.
There is a fix for this: before increasing the accumulator value, wait for it to be precisely 0:
----------------------------- MODULE spec_loop -----------------------------
EXTENDS TLC, Integers
CONSTANTS Loop, NULL
(*--algorithm loop
variables
accumulator = 0;
define
AccumlatorLessThanEqualOne == accumulator <= 1
end define;
fair process p \in {1,2}
begin
Increase_Accumulator:
await accumulator = 0; \* If the accumulator value is not 0, wait.
accumulator := accumulator + 1;
Decrease_Accumulator:
accumulator := accumulator - 1;
end process
end algorithm;*)
=============================================================================
This solution passes, and it shows the use of a powerful feature of TLA+: the await keyword.
The keyword will stop executing that process step until the condition after await is met.
Atomic PHP
My purpose in using TLA+ is to develop good specifications for ideas that I will then have to translate into code.
That code happens to be PHP, and I need to understand what “atomic” means in the context of PHP.
I wrote a small script to test out what atomic execution means in PHP:
<?php
$isWorker = isset($argv[1]);
if($isWorker){
$id = $argv[1];
foreach(range(1,200) as $k){
echo $id; // Print the process name.
}
exit(0);
}
foreach(range(1,2) as $n){
$command = PHP_BINARY . ' ' . escapeshellarg(__FILE__) . ' ' . $n;
$specs = [STDIN, STDOUT, STDERR];
proc_open($command, $specs, $pipes);
}
sleep(1); // Dumb wait for all processes to be done.
echo "\n";
exit(0);
Running the script will yield a variation of this output:
22222222222222222111111111111111111112111212221212121212121212121212121212121212
12121212121212121212121212121212121212121212121212121212121212121212121212121212
12121212121212121212121212121212121212121212121212121212121212121212121212121212
12121212121212121212121212121212121212121212121212121212121212121212121212121212
12121212121212121212121212121212121212121212121212121212121212121212121212121222
Note: I’ve used
proc_openas it’s a “fire and forget” function that will not block the execution of the main script waiting for the processes to finish. Usingpassthru, as an example would stop the main script to wait for the started script to complete.
The processes get their turn to print in a non-deterministic order.
A note: using smaller numbers will incur in some execution caching that will unwrap the execute the foreach a first time and will then store and just print a string; that is why there is a 200 max in there.
The processes will print when they are allocated CPU time; the allocation of that CPU time cannot be known before the execution, which means the atomicity of PHP is a single instruction.
The takeaway is: after each PHP instruction, the CPU might be allocated to another PHP thread.
There is no guarantee another PHP thread will not get the CPU and do something between two adjacent PHP instructions, like an echo following another in the example code.
This information will come in handy later when it is time to translate the specification to code.
A first Loop specification
After exploring some key concepts, it’s time to get back to the Loop specification.
The first version of the specification leaves much to be desired but is helpful to illustrate more logic and TLA+ constructs I will use.
----------------------------- MODULE spec_loop -----------------------------
EXTENDS TLC, Integers, FiniteSets
CONSTANTS Loop, NULL
(*--algorithm loop
variables
jobsCount = 5,
maxParallelism = 2,
_startedRegister = [x \in 1..jobsCount |-> FALSE];
define
StartedCount == Cardinality({x \in DOMAIN _startedRegister: _startedRegister[x] = TRUE})
NextNotStarted == CHOOSE x \in DOMAIN _startedRegister: _startedRegister[x] = FALSE
end define;
fair process loop = Loop
begin
StartInitialBatch:
while StartedCount < maxParallelism do
with p = NextNotStarted do
_startedRegister[p] := TRUE;
end with;
end while;
end process
fair process worker \in 1..5
begin
WaitToStart:
await _startedRegister[self] = TRUE;
Work:
goto Done;
end process;
end algorithm;*)
=============================================================================
I’ve imported the FiniteSets module into my specification. This module contains functions, like the Cardinality one, that allows me to operate on sets.
Sets are lists of elements of the same type: {1, 2, 3} is a set of integers with a cardinality of 3, 1..3 is a quick way of defining the set {1, 2, 3}.
This version of the specification defines two types of processes: one is the Loop, the other is the worker.
There will be one Loop and 0 or more workers at any given moment.
The first construct I’m introducing is the _startedRegister variable.
I’m sure someone with more experience would develop a better solution, but I’m stuck with my knowledge of the subject.
Any _variableName prefixed with _ indicates a “technical” variable that I’ve defined in the specification, but that will most likely not be translated to PHP code.
To understand the purpose of the _startedRegister variable, look at the worker process: the process worker will start in the WaitToStart phase and will move to the next phase, the Work one, only when it is started from the Loop.
The definition of the _startedRegister variable is _startedRegister = [x \in 1..jobsCount |-> FALSE] and it can be read like “a map from jobs to the boolean false value”. It’s better understood in PHP array terms:
$_startedRegister = [1 => false, 2 => false, 3 => false, 4 => false, 5 => false];
So, when the Loop sets the flag for process 2 to TRUE, the await condition of worker 2 will be satisfied, and it will start.
The StartedCount and NextNotStarted definitions are operators. They are like user-defined functions in PHP.
It’s worth reiterating TLA+ is not an implementation language but a specification one; it expresses operations, for the most, using mathematical definitions and logic operations.
StartedCount == Cardinality({x \in DOMAIN _startedRegister: _startedRegister[x] = TRUE}) means “StartedCount is the number of keys of _startedRegister for which the value for that key is true”.
Translate that to PHP:
global $_startedRegister;
function StartedCount(){
return array_count(array_filter($_startedRegister));
}
On the same note, NextNotStarted picks the key first element in _startedRegister the value of which is false; DOMAIN _startedRegister is like array_keys($_startedRegister.
To end the syntax tour, with is used to define a local variable.
Read more about TLA+ syntax through Leslie Lamport’s video course, on the Learn TLA+ site and from Hillel Wayne’s book.
Running the specification now, checking for Deadlock and Termination will fail due to a deadlock.
I’ve defined five workers to run, but only 2 will be started in the StartInitialBatch phase of the Loop; TLA+ is telling me 3 workers are deadlocked: they will await forever for something that will never happen.
Maybe start all the processes?
After some work, I came up with a second iteration of the specification that is starting all the processes:
----------------------------- MODULE spec_loop -----------------------------
EXTENDS TLC, Integers, FiniteSets, Sequences
CONSTANTS Loop, JobSet, Parallelism, NULL
(*--algorithm loop
variables
jobsCount = Cardinality(JobSet),
_startedRegister = [x \in JobSet |-> FALSE],
_exitStatusRegister = <<>>,
exitStati = <<>>;
define
StartedCount == Cardinality({x \in DOMAIN _startedRegister: _startedRegister[x] = TRUE})
NextNotStarted == CHOOSE x \in DOMAIN _startedRegister: _startedRegister[x] = FALSE
Running == StartedCount - Len(exitStati)
ParallelismRespected == Running <= Parallelism
CompletedCount == Len(exitStati)
end define;
fair process loop = Loop
begin
StartInitialBatch:
while StartedCount < Parallelism do
with p = NextNotStarted do
_startedRegister[p] := TRUE;
end with;
end while;
CheckExits:
if Len(_exitStatusRegister) > 0 then
CollectExitStatus:
with status = Head(_exitStatusRegister) do
exitStati := Append(exitStati, status);
end with;
_exitStatusRegister := Tail(_exitStatusRegister);
CheckExitedCount:
if Len(exitStati) = jobsCount then
goto Done;
end if;
MaybeStartOneMore:
if StartedCount < jobsCount then
with p = NextNotStarted do
_startedRegister[p] := TRUE;
end with;
end if;
goto CheckExits;
else
goto CheckExits;
end if;
end process
fair process worker \in JobSet
begin
WaitToStart:
await _startedRegister[self] = TRUE;
Work:
skip;
Exit:
_exitStatusRegister := Append(_exitStatusRegister, 0);
end process;
end algorithm;*)
\* BEGIN TRANSLATION
\* [...]
\* END TRANSLATION
OneWorderPerJobStarted == <>[](StartedCount = Cardinality(JobSet))
AllWorkersCompleted == <>[](CompletedCount = Cardinality(JobSet))
=============================================================================
I will not go through the specification line by line and concentrate on important parts.
At the bottom, after the translation, I’ve defined a temporal formula: it looks like an operator between parentheses and temporal “symbols” before it.
Specifically:
<>means “Eventually”; there is at least one state where the condition between the parentheses is true.[]means “Always”; what is between the parentheses is always true.
“Eventually always” means “When it happens for the first time, then it should keep being true”.
Eventually, a flower pot will fall and break apart; it will then always be broken. If someone came and put the pot back together, then it would violate the “always” part, and the model verification would fail.
The rest of the code is operators to make the code more readable.
I’ve added one more technical variable, the _exitStatusRegister one. This is a sequence, denoted with <<>>. In sequences, order matters; in sets, type matters.
That represents a worker process ending and returning its exit status to the Loop process.
This specification is not doing all I need it to do, but will pass verification with the following settings:
What to check?-Temporal formulaDeadlock- checkedPropertiesTerminationOneWorderPerJobStartedAllWorkersCompleted
InvariantsParallelismRespected
ConstantsJobSet <- [ model value ] {J1, J2, J3, J4, J5}Parallelism <- 2
Five jobs and a parallelism of two.
This is good enough to try and translate it into code.
Translating the specification
<?php
function worker()
{
exit(0); // Just exit, like skip.
}
function startWorker($key)
{
$command = sprintf("%s %s %s", PHP_BINARY, escapeshellarg(__FILE__), $key);
return proc_open($command, [STDIN, STDOUT, STDERR], $pipes);
}
function loop(array $jobSet, $parallelism)
{
$batchSize = min(count($jobSet), $parallelism);
$started = [];
$exitStati = [];
foreach (range(1, $batchSize) as $k) {
$started[] = startWorker($k);
}
while (true) {
$procKeysToRemove = [];
foreach ($started as $process) {
$procStatus = proc_get_status($process);
if ($procStatus['running']) {
continue;
}
$exitStati[] = $procStatus['exitcode'];
$procKeysToRemove[] = array_search($process, $started, true);
if (count($exitStati) === count($jobSet)) {
break 2;
}
if (count($started) < count($jobSet)) {
$started[] = startWorker(++$k);
}
}
// Reduce the checked set as they complete.
foreach ($procKeysToRemove as $key) {
unset($started[$key]);
$started = array_values($started);
}
}
return $exitStati;
}
if (!isset($argv[1])) {
$exitStati = loop(range(1, 5), 2);
echo "\n", print_r($exitStati, true);
} else {
worker();
}
The code should work on any machine, should one want to try it out.
Just one note: calling proc_get_status a second time on an already exited process will yield an exit value of -1. To cope with that and to get a smaller optimization to the loop logic, I remove the processes from the $started array when done.
The non-technical variables from the specification are all there, and the loop works, but with two significant issues:
- That
while( true )is a CPU-locking loop. If the workers were running long enough, it would hoard CPU time running continuously, bringing the CPU load to 100% with wasted energy consumption: most of those cycles would not update a state. - The workers do something, but what? There is no communication from them back to the loop. Did they fail? Did they explode?
As pipes for the workers, I’m setting the STD ones, but that is just to make the code shorter. Letting the workers print to the same output stream as the loop is a bad idea as it does not allow to control the print order, and thus formatting, and does not allow the Loop to get any information beyond an exit status.
Next
In my next post, I will add pipes and Inter-Process Communication (IPC) to the mix to see how the specification and the PHP code will evolve.