learning_tla/learn_tla/core/07-concurrency.md

7. Concurrency

Processes

Processes and ids

• To define concurrent process, wrap begin blocks in process <name> = <id> and end process.
• Processes cannot share label names
• Processes can share state
• They usually need some synchronization. Consider this model:

---- MODULE core7_1_reader_writer ----
EXTENDS Integers, Sequences, TLC

(* --algorithm reader_writer
variables
  queue = <<>>;
  total = 0;

process writer = 1
begin
  AddToQueue:
    queue := Append(queue, 1);
end process;

process reader = 0
begin
  ReadFromQueue:
    total := total + Head(queue);
    queue := Tail(queue);
end process;
end algorithm; *)
====

When running the model, it will fail trying to read from an empty queue. Some approaches we could have:

• skip dequeuing if queue is empty
• block reader until queue is not empty
• return a default value
• report an error of our own, instead of having TLC flag it

Invariants can use the process id applied to pc, like pc[0] for the reader PC in that example.

Process sets

Process values do not have to be plain values, like naturals or strings, so we can write

---- MODULE foo ----
Writers == {1, 2, 3}
(*----algoorithm foo
process writer \in Writers
\* ...
end process
end algorithm*)
=====

Using a goto <first label in process> is equivalent to placing the whole process in a while TRUE loop.

self

In a process, self is the value of the current process (its id).

• self is available in macros
• self is NOT available in processes defined with a constant value instead process name \in set.

await

• A process containing await statements will only run if ALL the statements in the CURRENT label evaluate to TRUE
• await interacts a little oddly with variable updates
  • it will be based on the updated value if directly embedded
  • but not if the variable is used via a defined operator.
  • do not uses updates variables in await statements
• if no label in a process can run, possibly because they contain at least one await evaluating to FALSE, the spec deadlocks.

Example 7.7 will then deadlock, because the reader will never be able to read. We can make this succeed by disabling DEADLOCK_CHECK in the .CFG.

Procedures

• Procedures are like macros, but can contain labels
• Defined in Sequences
• Procedure MUST include a return statement
• The return statement MUST be reached
• unlike macros, they are not called just by name by using call Name(val1, ...);
• call statements MUST be followed by
  • either a goto
  • or a label
  • or another return, if the call was from within a procedure

Finding more invariants

• Never forget the type invariant, like in the 7.11 threads example:

---- MODULE foo ----
\* Must be AFTER the PlusCal translation.
TypeInvariant ==
    /\ counter \in 0..NumThreads
    /\ tmp     \in [Threads -> 0..NumThreads] \* tmp is a function by process value
    /\ lock    \in Threads \union {NULL}
====

• In the threads example, any process (thread) value is >= counter. Two ways to write it:

CounterNotLtTmp1 ==
  tmp \in [Threads -> 0..counter]
CounterNotLtTmp2 ==
  \A t \in Threads:
    tmp[t] <= counter