Using TLA+ to Write Specifications for an Asynchronous Interface
This chapter is from the book
This chapter is from the book
This chapter is from the book
We now specify an interface for transmitting data between asynchronous devices. A sender and a receiver connected as shown here.
Data is sent on val , and the rdy and ack lines are used for synchronization. The sender must wait for an acknowledgment (an Ack) for one data item before it can send the next. The interface next. The interface uses the standard two-phase handshake protocol, uses the standard two-phase handshake protocol, described by the following sample behavior:
(It doesn't matter what value val has in the initial state.)
It's easy to see from this sample behavior what the set of all possible behaviors should be—once we decide what the data values are that can be sent. But, before writing the TLA+ specification that describes these behaviors, let's look at what I've just done.
In writing this behavior, I made the decision that val and rdy should change in a sigle step. The values of the variables val and rdy represent voltages on some set of wires in the physical device. Voltages on different wires don't change at precisely the same instant. I decided to ignore this aspect of the physical system and pretend that the values of val and rdy represented by those voltages change instantaneously. This simplifies the specification, but at the price of ignoring what may be an important detail of the system. In an actual implementation of the protocol, the voltage on the rdy line shouldn't change until the voltages on the val lines have stabilized; but you won't learn that from my specification. Had I wanted the specification to convey this requirement, I would have written a behavior in which the value of val and the value of rdy change in separate steps.
A specification is an abstraction. It describes some aspects of the system and ignores others. We want the specification to be as simple as possible, so we want to ignore as many details as we can. But, whenever we omit some aspect of the system from the specification, we admit a potential source of error. With my specification, we can verify the correctness of a system that uses this interface, and the system could still fail because the implementer didn't know that the val line should stabilize before the rdy line is changed.
The hardest part of writing a specification is choosing the proper abstraction. I can teach you about TLA+, so expressing an abstract view of a system as a TLA+ specification becomes a straightforward task. But I don't know how to teach you about abstraction. A good engineer knows how to abstract the essence of a system and suppress the unimportant details when specifying and designing it. The art of abstraction is learned only through experience.
When writing a specification, you must first choose the abstraction. In a TLA+specification, this means choosing the variables that represent the system's state and the granularity of the steps that change those variables' values. Should the rdy and ack lines be represented as separate variables or as a single variable? Should val and rdy change in one step, two steps, or an arbitrary number of steps? To help make these choices, I recommend that you start by writing the first few steps of one or two sample behaviors, just as I did at the beginning of this section. Chapter 7 has more to say about these choices.