1 The Specification

2 The Protocol

3 Processes

4 Project

Prev:  Session 11 part 1

Contents
 ↑

top

 ↑

top

 ↑

top

 ↑

top

 ↑

top

 ↑

top

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.