Designing a producer-consumer system with PlusCal/TLA

Our goal is to design a system that collects data from several inputs. This could be an embedded system reading inputs from several sensors, or a webserver reading requests from several input queues. We will consider a system with two inputs as depicted on the picture below. This system has two producers A and B and a consumer C that reads the data produced by A and B. The communication is asynchronous: messages are stored in bounded FIFO queues. Reading from the queue is blocking when the queue is empty, whereas writing is blocking when the queue is full. We cannot make any assumption about A and B: they can emit a message at any time.

A producer-consumer system with two producers A and B and a consummer C

Our goal is to design the most permissive algorithm for the consumer C that satisfies the following requirements:

By “most permissive”, we mean that our model should not make any assumption that is not required to match the three requirements above.

A minimal design

We first start with the following skeleton that the correspond to the system architecture above:

EXTENDS TLC, Sequences

(* PlusCal options (-wfNext) *)

CONSTANT QUEUE_SIZE

(*
--algorithm pc {
    variables
        qA = << >>;
        qB = << >>;

    macro send(m, q) { ... }
    macro recv(m, q) { ... }

    process (A = 1)
    {
    }

    process (B = 2)
    {
    }

    process (C = 3)
    {
    }
}
*)

In this model, qA and qB correspond to the queues from A to Cons on the one hand, and from B to Cons on the other hand. They are modeled using Sequences, which are simply lists of values. The queues are initialized to empty sequences << >>.

  1. Implement two macros send and recv that respectively send and receive a message m to/from queue (or sequence) q. These macros should implement the policies of bounded FIFO queues described above.
  2. Implement processes A, B and C in the most permissive way. Do not focus on the requirements yet: the goal is to get a very simple model that allows as many behaviors as possible. This includes many behaviors that do not match the requirements.
  3. Express the requirements above, and model-check your system choosing a small value for QUEUE_SIZE, for instance 5. We expect that your model has no deadlock, whereas the other requirements may be violated.

Make all messages distinct

Not surprisingly, some requirements are violated by our minimal model. We first choose to make sure that the absence of duplicate messages is satisfied. Protocols usually rely on a message structure composed of a header that carries data related to the protocol, and a payload that carries data relevant to the user of the protocol. We will ignore the payload in our model, since we are designing the protocol. Hence, messages are reduced to their headers.

  1. Which information should be carried by (the header of) your message in order to ensure that any two messages in the queues are distinct? Your solution should be realistic: it should be possible to model-check and to implement your solution.
  2. Extend your model to implement your solution, and model-check that your protocol guarantees that all the messages in the queues are distinct
  3. Explain why your model does not guarantee that every message sent is eventually received, whereas this requirement was satisfied by the first model

Every message sent is eventually received

Our goal is to fix the model in such a way that it satisfies all the requirements.

Analysing the counter-example

  1. Analyse the counter-example provided by the model-checker. What is the cause of violation of the property?
  2. What should you do now?

Giving priority to the message with the lowest ID

Our model is too permissive: some runs do not guarantee that every message sent is eventually received. In order to avoid this situation, our client chooses that we should always pick the first message with the lowest ID among all input queues.

  1. Implement this protocol in your model and model-check it.
  2. Explain what you observe.

Giving priority to the oldest messages in the queues

We came back to the client and explain that its solution still does not guarantee that all messages sent are eventually delivered. The client suggests to pick the oldest message in the queues instead of the message with the lowest ID.

  1. Our current model does not provide the age of a message. How could that be added to the protocol? Is it possible to model-check and implement the resulting protocol?

Bounding the time a message can wait in the queue

We explain to our client the issue with the oldest message first policy.

  1. As a first solution, the client suggests to bound the number of consecutive recv that can be made from the same queue. What do you think of this solution when there are more than two input queues?
  2. As a second solution, the client suggests to bound the number of consecutive receptions that ignore a queue. Implement this solution in your model. Check that the resulting model satisfies all requirements.