|
| Session 11 | The Alternating Bit Protocol |
| | Part 2. Liveness |
Leslie Lamport
Last modified on 28 November 2021
|
|
1 The Specification
We now add liveness requirements to algorithm ABSpec,
the specification of what the AB protocol does.
We will add the simplest requirement: that messages keep getting
sent and received. Fairness of process A asserts
that it must perform its a action (its only action) if
that action remains continuously enabled. That action is enabled
iff AVar.bit equals BVar.bit. In that
case process B's b action is disabled, so no
action other than a is enabled and the a
action must remain enabled until it is performed. Therefore,
weak fairness of process A implies that an a
step must eventually occur if AVar.bit equals
BVar.bit.
Similar reasoning shows that process B's
b action must eventually be executed when
AVar.bit is unequal to BVar.bit.
Executing an a step enables action b
and vice-versa. Thus, fairness of each process implies
that an infinite sequence of messages are sent and received.
Modify algorithm ABSpec in module Session11a
by adding the keyword fair before the
process declarations for processes A and
B (and running the translator).
We can check that we haven't made a silly mistake in specifying
liveness by checking that the state predicates
AVar.bit = BVar.bit
and
AVar.bit /= BVar.bit
are both true in infinitely many states. Modify the model you
created for the algorithm by adding
[]<>(AVar = BVar) /\ []<>(AVar /= BVar)
to the properties to be checked, and run the model.
TLC should report no error.
Exercise 1 Fairness of a process means that
if the process can continually take a step, then it must take one.
Fairness of the algorithm means that if it can continually take
a step, then it must take one. Modify algorithm ABSpec by
removing the fairness conditions on the processes and adding a
fairness condition on the entire algorithm. That is, remove the
keyword fair from the processes and replace
--algorithm with --fair algorithm. Explain
why this makes no difference to the algorithm, so the liveness
condition still holds.
Show the answer.
Answer A process A action and a
process B action can never both be enabled at the same
time. Therefore, the entire algorithm can continually take a step
iff one of the processes can, which implies that fairness of
the algorithm is equivalent to fairness of both its processes.
2 The Protocol
We have to add fairness to algorithm AB so it will satisfy
the liveness requirement that new messages keep being sent and
received.
The obvious way to do that is to make processes A and
B fair. (We don't want to require messages to be
lost, so we shouldn't add a fairness requirement to the
LoseMsgs process.)
Modify algorithm AB in module Session11b by
declaring each process to be a fair process.
Run TLC on the model in which you checked that AB
implements ABSpec. Since you've added the required
liveness property to ABSpec, there's no need to check
any other liveness property.
TLC reports an error. TLC's model checking algorithm is
nondeterministic because it uses multiple threads. Run it
multiple times until it produces an error trace with four different
states—that is, one that keeps cycling forever through those
four states, starting with the initial state. Observe that the
values of AVar and BVar never change, so
this trace describes a behavior that does not satisfy the fairness
properties required by algorithm ABSpec. Let's
check that it satisfies the fairness properties of algorithm
AB.
The first two steps of the trace add messages to the two message
queues, adding one message to each. The messages could be added
in either order. The next two steps each remove one of those
messages from a queue, again in either order.
The steps that add a message to a queue are performed by each of the
processes executing their sending action. Removing the message
from AtoB could be done by either process B
receiving the message or process LoseMsgs throwing it
away. Removing the message from BtoA must have been
done by process LoseMsgs, since process A
would have changed AVar had it received the message.
Because processes A and B of algorithm
AB keep sending messages, they each perform an infinite
number of actions, so their fairness requirements are satisfied.
However, they never make any progress because process A
never receives any of the ack messages that process B
keeps sending.
In a system with message loss, message delivery often is ensured by
repeatedly sending the message until it is received. Weak
fairness of the receiving process may not ensure that the message is
eventually received because the receive action is disabled each time
the message is lost. In that case, strong fairness can be
used. Even though the receive action is continually disabled,
it is continually enabled, which is enough to ensure that it eventually
occurs. So, let's try modifying algorithm AB
by making processes A and B strongly fair.
We've seen that we can make an action of a process strongly fair by
putting + after it's label, so we can make the processes
strongly fair by replacing the labels a: and
b: with a:+ and b:+.
Replacing the fair declaration by fair+ is
logically equivalent to putting + after all its
labels. Since the processes just have a single label,
we can add the + in either place.
However, putting the + after fair instead of
after the process's labels produces a TLA+ translation that TLC executes
more efficiently.
So, put the + after fair in
processes A and B, and run TLC.
TLC again reports an error. In fact, it produces the same error
traces as before. The action of each of the two processes is
always enabled. It's always possible for either process to send
a message. Therefore, even weak fairness requires both
A and B actions to be executed infinitely
often. Replacing weak fairness by strong fairness did not change
(the property represented by) the algorithm.
What we want to require is strong fairness of the actions represented
by the or clauses of processes A and
B. This is easy to express in TLA+, but impossible
to express directly in PlusCal. PlusCal allows fairness
conditions to be asserted only about actions described by labeled
statements.
Exercise 2 We can assert fairness for the
or clauses of processes A and
B by labeling those clauses. Do that and run
TLC on the resulting algorithm. Explain what happens.
Show the answer.
Answer Adding the label allows executions in
which control in a process reaches the or clause
even if there is no message for the process to receive.
This permits deadlock. See what happens if you prevent that
by putting the label after the clause's await statement.
It's possible to write a more complicated version of the algorithm,
using additional labels, that implements the fairness requirements of
ABSpec. (I haven't thought hard about it, but the
only way I see of doing it requires also rewriting the
LoseMsgs process and probably adding one or more
variables.)
We don't want to do that because adding labels requires introducing a
pc variable that can have multiple values, increasing the
number of reachable states. That may not make much difference
in a simple algorithm like the AB protocol, but in realistic
examples it could make model checking take much, much longer.
There's a simpler way to solve this problem: changing the
process structure.
3 Processes
We can split process A of algorithm AB
into two separate processes: one process that sends messages to
process B and the other that receives acks
sent by process B. The body of each process is
a while (TRUE) loop, the body of that loop
being either the either clause or the
or clause of process A.
The body of the sending
process is
as: while (TRUE) { AtoB := Append(AtoB, AVar) }
The body of the receiving process is
ar: while (TRUE) {
await BtoA /= << >> ;
if (Head(BtoA) = AVar.bit)
{ with (d \in Data)
{ AVar := [data |-> d, bit |-> 1 - AVar.bit] }
};
BtoA := Tail(BtoA)
}
Since the sending action is always enabled, we just need weak fairness
of the sending process to ensure that A keeps sending
messages to B. Since B keeps sending acks,
the receiving action is continually enabled. However, it can (but
needn't) also be continually disabled by the LoseMsgs
process removing those messages from the queue AtoB.
Therefore strong fairness is necessary to ensure that
acks keep getting received by A.
So, we make the sending process a fair process
and the receiving process a fair+ process.
Process B can similarly be split into a sending and a
receiving process. The resulting algorithm is called
AABB in module Session11d. Check that
this algorithm implements ABSpec with fairness
conditions. You can use a model obtained by cloning the model
of Session11b that checks if algorithm
AB satisfies algorithm ABSpec.
If we remove all fairness from them, algorithms AB and
AABB allow exactly the same behaviors. They are two
descriptions of the same algorithm. With a little knowledge of
TLA+, it's a straightforward exercise in propositional logic to show
that the TLA+ translations of the two algorithms are equivalent.
Processes are not an intrinsic part of an algorithm. They can be
viewed as arising from the particular way the algorithm/property is
written as a mathematical formula. There are many ways to write
a property as a formula, and they can yield different ways of
viewing the algorithm in terms of processes.
4 Project
Algorithm ABSpec requires the sender to keep sending
messages. In a real system, process A would receive
messages from its environment to be sent to B.
(Process B would probably deliver those messages to its
environment, but let's ignore that.) Write a new algorithm in
which, as in ABSpec, process A sends a
message to process B by simply setting BVar
equal to AVar. However, add an environment process
E that chooses the value that A is to send.
First write such an algorithm ABESpec in which process
E chooses the next value to be sent only after the
current message has been delivered to B. Choose
fairness conditions that don't require process E to
choose any values, but ensure that every value it has chosen is sent
and received. (This requires adding at least one new
variable.) Then modify algorithm AABB to obtain an
algorithm AABBE that includes the same environment
process E as in ABESpec and implements
algorithm ABESpec.
Next, do the same thing except allowing process E
to choose new values before previously chosen values are
delivered. Thus, the algorithms will maintain a queue of
values waiting to be sent.
This example illustrates that, when writing an algorithm, you have to
describe the environment as well as the part of the algorithm that you
have to implement.
(We've already seen that in algorithm AB, since
message loss is caused by the environment; it isn't meant to be
implemented.)
Few algorithms will produce correct results
regardless of what the environment does.
For example, the
algorithm AABBE you wrote will not work properly if the
environment process E can make arbitrary changes to the
message queues. Deciding what the environment must and must not
do is an important part of writing an algorithm.
|