1 2Process Algorithm
2 FinerGrained Algorithm 3 Process Sets 4 Locks 5 The Grain of Atomicity Prev: Session 6 Next: Session 8 Contents 
1 A 2Process Algorithm
We begin with about the simplest multiprocess algorithm I can think
of. It has a single variable
The algorithm begins like a uniprocess algorithm with its name, an
opening
algorithm Add2 { variable x = 0 ;This is followed by two processes. A process has a name and an identifier, which we call its id. The name must be a legal TLA+ identifier; the id can be any value. Different processes must have different names and unequal ids.
I have named the first process
process (A = 3)This is followed by the process's code, which is enclosed in { } braces. That code must begin with a label.
I gave the second process the sensible name B
and the silly id 7 . Here is the complete algorithm
algorithm Add2 { variable x = 0 ; process (A = 3) { a: x := x + 1 } process (B = 7) { b: x := x + 1 } }Quiz Why couldn't I have given process B the id
"B" instead of 7 ?
Show the answer.
Answer
The ids of different processes must be unequal.
Since TLA+ doesn't specify whether or not a number equals a string, we
don't know whether or not
The algorithm satisfies the postcondition
The invariant must use the
(pc[3] = "Done") /\ (pc[7] = "Done") => (x = 2)Run the translator on the specification Session7 , create
a new model, and add the formula above to the Invariants
section of the What to check? section of the model's Model
Overview tab. Running TLC should confirm that the algorithm
satisfies its postcondition.
We would also expect our tiny algorithm to terminate. As with uniprocess algorithms, we have to add a fairness requirement to ensure that the algorithm actually takes steps. Termination and fairness are discussed later. For now, we just consider invariance properties.
Examine the algorithm's TLA+ translation. Like the translation
of a uniprocess algorithm, it begins with a
In formula
[i \in D > exp]explained in Session 6. The expression exp
uses the TLA+ CASE construct. You should be able to
deduce the meaning of the construct from this example. The
translation always uses self as the name of a bound
variable that takes values in ProcSet .
You should also be able to deduce the meaning of the expressions
containing the EXCEPT construct in the definitions of
a and b .
Observe that process names and labels are used as identifiers in the translation. Make sure that they are distinct from one another and from variable names and any identifiers declared or defined elsewhere in the module. PlusCal allows some repeated use of the same identifier in an algorithm—for example, you can use the same label in different processes. However, don't do that because the translator changes names to eliminate clashes, making the correspondence between the translation and the algorithm a little harder to see. 2 A FinerGrained Algorithm
You could write a program in many languages in which a variable
We now consider an algorithm whose steps more closely resemble those
of the program—an algorithm that increments
Splitting the incrementing of
algorithm Add2FG { variable x = 0 ; process (A = 3) variable ta = 1 ; { a1: ta := x ; a2: x := ta + 1 } process (B = 7) variable tb = 1 ; { b1: tb := x ; b2: x := tb + 1 } }If you've done any multithreaded programming, you should realize that this algorithm doesn't satisfy the postcondition of the original algorithm. It can terminate with x not equal to
2 . Run TLC on the model that checks the invariant
asserting this postcondition and look at the error trace. As you
probably expected, it shows that each process read x
before the other process changed its value, so they both set
x to 1 . We'll see later how to fix the
finergrained algorithm so it satisfies the postcondition
x = 2 . But first, more about processes.
3 Process SetsInstead of writing our two algorithms with two separate processes, we can write them with a single process set containing two processes. Here is how we rewrite the finergrained algorithm. The process set begins:
process (AB \in {3,7})This declares two processes, one with id 3 and the other
with id 7 , just as before. However,
instead of naming each process separately, it gives the name
AB to the process set containing the two processes.
The complete declaration of the process set is:
process (AB \in {3,7}) variable t = 1 ; { ab1: t := x ; ab2: x := t + 1 }Replace the two processes A and B in the
finegrained algorithm with this single process set AB
and run the translator. The translation of the twoprocess
version began like this, where I've deleted some things:
VARIABLES x, pc, ta, tb vars == << x, pc, ta, tb >> ProcSet == {3} \cup {7} Init == /\ x = 0 /\ ta = 1 /\ tb = 1 /\ pc = [self \in ProcSet > CASE self = 3 > "a1" [] self = 7 > "b1"] a1 == /\ pc[3] = "a1" /\ ta' = x /\ pc' = [pc EXCEPT ![3] = "a2"] /\ UNCHANGED << x, tb >> a2 == ... b1 == /\ pc[7] = "b1" /\ tb' = x /\ pc' = [pc EXCEPT ![7] = "b2"] /\ UNCHANGED << x, ta >> b2 == ...Compare it with the translation of the new algorithm having a single process set. Observe that it differs in the following ways.
Spec that describes
the complete algorithm, self is a bound variable
that is quantified over all the process ids.
A multiprocess algorithm can contain any number of individual processes and process sets. However, there can be no name conflict between different processes and process sets, and the ids of different processes must be different. 4 Locks
Our finegrained algorithms that takes two steps to add 1 to
A lock is easy to represent with the PlusCal
One way to describe a lock is with a variable called a
semaphore. The lock is free if the value of the variable
is
algorithm Add2FGSem { variable x = 0, sem = 1 ; process (AB \in {3,7}) variable t = 1 ; { lock: await sem = 1 ; sem := 0 ; ab1: t := x ; ab2: x := t + 1; unlock: sem := 1 ; } }Replace the algorithm in specification Session7
by this version, and run TLC to check that the postcondition
is now satisfied.
Puzzle Use TLC to find out what the algorithm does if you replace the Lock operation with:
lock: sem := sem  1 ; await sem = 0 ;Explain why the algorithm does what it does. Show the answer.
Answer
The modified algorithm behaves exactly like the original one.
A
From a programming perspective, one would say that the assignment to
/\ sem = 1 /\ sem' = sem  1 /\ sem' = 0 /\ sem' = 0These two formulas are equivalent. It's obvious that the first equals TRUE iff sem equals 1 and
sem' equals 0. You should convince yourself that the
second formula also equals TRUE only in this case.
Since all the other formulas in the translation are
identical, this means that the definitions of formula
Spec for the two versions are equivalent, so the
algorithms are equivalent.
^{note}
Whenever you are not sure what a PlusCal statement should do, you can find the answer in the TLA+ translation. {3,7} with a set of
N elements, for an arbitrary natural number
N , so it satisfies the postcondition
x = N . Check that it satisfies this postcondition
for a few values of N . Also write and check an
invariant asserting that two processes cannot be between their
lock and unlock steps at the same
time.
Show the answer.
Answer TLC can find any errors in your algorithm
by checking that it has no deadlock and that it satisfies the
postcondition.
You should also check an invariant asserting there is
at most one
process between
\A i, j \in ProcSet : (pc[i] \in {"ab1, ab2"}) /\ (pc[j] \in {"ab1, ab2"}) => (i = j) \A i \in ProcSet : \A j \in ProcSet \ {i} : ~ ( (pc[i] \in {"ab1, ab2"}) /\ (pc[j] \in {"ab1, ab2"}) ) Locks are used in programs to make everything between a Lock step and the matching Unlock step act like a single step. They are not needed for that purpose in PlusCal. Any computation that you want to act like a single step can be written as a single PlusCal step. Locks should be used in PlusCal only in an algorithm that is meant to model their use in a program's code. If you have trouble describing a computation as a single step, it means that you don't know how to describe mathematically what is being computed. Learning how requires learning how to use the full power of TLA+ when writing PlusCal expressions, which takes practice. 5 The Grain of Atomicity
An algorithm is an abstract model of some code and/or hardware.
We want it to be as accurate as necessary and as simple as
possible. Simplicity means having a coarser grain of
atomicity—that is, taking as few steps as possible, which means
having as few labels as possible.
However, accuracy requires not having too coarse a grain of
atomicity, which means not having too few labels.
For example, algorithm
Now consider a still finergrained algorithm
process (AB \in {3,7}) variable t = 1 ; { ab1a: t := x ; ab1b: t := t + 1 ; ab2: x := t }This probably more accurately represents the actual execution of the program by a computer. It allows the possibility of one process performing a step between the steps ab1a and
ab1b of the other process—a possibility not allowed
by algorithm Add2FG . However, that additional
possibility makes no difference to the possible results produced by
the algorithm. Any step that a process performs between steps
ab1a and ab1b of the other process
has the exact same effect as if that step were performed after
the ab1b step. This is because an
ab1b step
reads and modifies
only the value of the processlocal variable t , which
cannot be read or modified by the other process.
In general, a step of a process that reads or modifies only
processlocal variables can be combined with the preceding or
following step of that process. Thus, we can combine step
back to top
