Safely Sliding Windows: The Specs

Thorsten Gerdsmeier, Dirk Henkel, Peter B. Ladkin RVS Group Research Report RVS-RR-97-05b Universität Bielefeld

1 July, 1997 last changed 19 November, 1997

Introduction

This paper introduces five TLA^{+} specifications that have been written for the safety part of a verification proof for a sliding-window-style message retransmission mechanism^{1} with linear arithmetic (SWLA). This safety proof is provided in [Hen97]. SWLA is the linear arithmetic version of the sliding window message retransmission mechanism with modular arithmetic (SWMA), which is part of the Radio Link Protocol (RLP1), the datalink layer protocol for TDMA mobile cellular radio being analysed by the FCAR project of the Telecommunications Software Group at INRS-Télécommunications in Montréal [Fer96]. These specifications and the accompanying proofs contribute to the verification of SWLA using TLA and TLA^{+}.

Documents on the Temporal Logic of Actions (TLA) calculus and the corresponding specification language TLA^{+} can be found at the TLA website of Leslie Lamport [Lam]. A tutorial on TLA verification has been written by Peter Ladkin [Lad97].

TLA provides a clear separation between safety and liveness properties. The following specifications concern only safety properties. To obtain complete specifications we must add liveness properties. Liveness properties in TLA specifications have the form of Boolean combinations of fairness properties. The specifications have been designed, so to speak, with these liveness properties in mind, so we don’t believe that adding them will change the general idea of how the five specified systems work. The only sure way to know, however, would be to add them and provide the relevant proofs.

System verification must be performed relative to stated requirements. For SWLA (as well as for RLP1) we require that the protocol implements a reliable, asynchronous first-in first-out message-transfer stream. We specify this by means of a variable buffer which contains the messages that have been sent but not received, in order. Reliability is ensured by the implicit criterion that sent messages do not disappear; asynchrony by the independence of send and receive actions (corresponding to the buffer’s push and pop actions); FIFO by the standard FIFO property of a buffer. The AbstractBuffer (AB) is thus a state machine which embodies exactly the requirements of the communication system. The AB specification in TLA was first formulated and used in [Lad96].

1It has been pointed out by Michael Ferguson that the meaning of the word “protocol” in telecommunications engeneering is far richer than its informal use by specification engineers and network textbook writers. We find the mathematical operation far better described as a “retransmission mechanism”, as Ferguson suggests.

For both SWLA and AB we give formal specifications of their safety properties: the TLA formulas I .Safety and V .Safety. Proving that SWLA-safety implies AB-safety is equivalent to proving that I .Safety logically implies V .Safety. One may try this directly, but it’s easier to do it in several small steps via a hierarchy of specifications. We use three intermediate specifications II .Safety, III .Safety and IV .Safety, which show a continuous development from the simplicity of I .Safety to the details of V .Safety. The whole safety proof [Hen97] is accomplished in four steps of the form “(N + 1).Safety implies N .Safety”.

The approach to the system verification differs from that of Mokkedem, Ferguson and Johnston [MFJ97]. They describe invariants, and prove using the TLA logic that these invariants logically follow from an implementation specified in TLA. We follow the “traditional” TLA format, in which all specifications, including the requirement, have the form of a state machine. In this example, the requirement state machine embodies, as we have argued, exactly the properties of a reliable, asynchronous FIFO channel. It is notable that the required invariant in [MFJ97] does not appear to be logically equivalent to a TLA specification as defined by Lamport [Lam94], thus it is not guaranteed that the TLA logic suffices to prove it (but Mokkedem, Ferguson and Johnston have indeed succeeded in proving it).

The five safety specifications are given in six TLA^{+} modules. The first one is a collection of some common definitions. It is extend’d by each of the five specification modules I to V . Module I , the “requirement”, specifies the safety properties of AB, which is just a sequence with fixed maximum length and the two actions Push and Pop. As we said above, the purpose of any reliable, asynchronous FIFO message-transmission mechanism must be to simulate this precisely. Module II is a translation of AB into set notation. Module III introduces a distinction between sender and receiver sides. In Module IV the message transfer from sender to receiver is split into two seperate actions. Module V specifies the safety properties of SWLA. Besides Push and Pop, it defines four actions that make up the message transfer. Each module is preceeded by some commentary that should give an idea of how the specified system works.

Acknowledgements

The specifications were developed jointly with Prof. Dr. Jean-Charles Grégoire of INRS-Télécommunications à l’Université de Québec in Montréal. Petra Korff also contributed to the analysis and verification of some of the former high-level specifications with which we worked. Some of the explanatory commentary to the specifications is based on notes by Prof. Dr. Grégoire.

References

[Fer] Michael J. Ferguson: Selected publications. Available through

http://www.inrs-telecom.uquebec.ca/users/telesoft/

[Fer96] Michael J. Ferguson: Formalization and validation of the Radio Link Protocol (RLP1). To be published in Computer Networks and ISDN Systems, 1996. Available through [Fer].

[Hen97] Dirk Henkel: Safely sliding windows. Technical Report RVS-RR-97-05a, RVS Group, Universität Bielefeld, Technische Fakultät, May 1997. Available through [Lad].

[Lad] Peter B. Ladkin: Abstracts of RVS research publications.

Available through http://www.rvs.uni-bielefeld.de

[Lad96] Peter B. Ladkin: Formal but lively buffers in TLA^{+}. Technical Report RVS-RR-96-07, RVS Group, Universität Bielefeld, Technische Fakultät, January 1996. Available through [Lad].

[Lad97] Peter B. Ladkin: Using the Temporal Logic of Actions: A tutorial on TLA verification. Technical Report RVS-RR-97-08, RVS Group, Universität Bielefeld, Technische Fakultät, June 1997. Available through [Lad].

[Lam] Leslie Lamport: TLA – The Temporal Logic of Actions.

http://www.research.digital.com/SRC/tla/

[Lam94] Leslie Lamport: The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems, 16(3):872-923, May 1994. Also available through [Lam].

[MFJ97] Abdelillah Mokkedem, Michael J. Ferguson, and Robert deB. Johnston: A TLA solution to the specification and verification of the RLP1 retransmission protocol. Formal Methods Europe symposium, September 1997. Available through [Fer].

[Gre97] Jean-Charles Gregoire: TLA + PROMELA: conjecture, check, proof – engineering new protocols using methods and formal notations. Formal Methods Europe symposium, September 1997.

1 Common Definitions

Some declarations, assumptions and definitions will be needed in several of the following specifications. They are collected in the module CommonDefinitions.

Messages is the Set of all Objects that can be passed through the buffer we specify. It specifically does not contain the constant ⊥_{Messages}. BufferLength is the maximum number of such objects that can be held in the buffer at any time. We require Bufferlength ≥ 1.

We introduce a simple notation for intervals of natural numbers and some operators on sequences: Len(s) denotes the length of a sequence s; Tail(s) is ”s without its first element”; s ∘ t the concatenation of the sequences s and t.

The last four definitions refer to sets of pairs of the form (index, message) where index is a natural number. MinPair(S) is that pair (or one of those pairs) with the least index in S, MinIndex(S) is this least index. Similarly for Max-functions with the greatest index. These functions are defined only on nonempty sets.

module CommonDefinitions

extends Naturals

constants BufferLength, Messages, ⊥_{Messages} assumption BufferLength > 0 assumption ⊥_{Messages} ∉ Messages

l . . u =^{Δ} {i ∈ Nat : l ≤ i ∧ i ≤ u} Len(s) =^{Δ} choose n : ∧ n ∈ Nat ∧ Domain s = 1 . . n

Tail(s) =^{Δ} [i ∈ 1 . . (Len(s) − 1) ↦ s[i + 1]] s ∘ t =^{Δ} [i ∈ 1 . . (Len(s) + Len(t)) ↦ if i ≤ Len(s) then s[i] else t[i − Len(s)]]

MinPair(S) =^{Δ} choose z : \begin{matrix}∧ z ∈ S \\ ∧ ∀ y ∈ S : z[1] ≤ y[1] \end{matrix}

MaxPair(S) =^{Δ} choose z : \begin{matrix}∧ z ∈ S \\ ∧ ∀ y ∈ S : z[1] ≥ y[1] \end{matrix}

MinIndex(S) =^{Δ} MinPair(S)[1] MaxIndex(S) =^{Δ} MaxPair(S)[1]

2 An Abstract Buffer

Module I contains a straight-forward specification of an abstract buffer. Its only variable is the sequence buffer. At the beginning, buffer is empty. If the buffer is at any time not full (i.e. shorter than BufferLength), a message can be Push’d onto it at the rear end. If the buffer is not empty, its first message can be Pop’d off. Thus the messages are Pop’d in FIFO order.

module I

extends CommonDefinitions

variables buffer

Init =^{Δ} buffer = ⟨ ⟩

Push(a) =^{Δ} ∧ a ∈ Messages ∧ Len(buffer) < BufferLength ∧ buffer′ = buffer ∘ ⟨a ⟩

Pop =^{Δ} ∧ buffer ≠ ⟨ ⟩ ∧ buffer′ = Tail(buffer)

SomeAction =^{Δ} ∨ ∃ a : Push(a) ∨ Pop

Safety =^{Δ} ∧ Init ∧ □[SomeAction]_{buffer}

3 Set Notation

Specification II is a translation of the buffer into set notation. Instead of the sequence buffer we now use the set tSet. Like buffer in specification I , tSet starts empty.

To preserve the FIFO property of the buffer, we must know in which order the messages in the buffer have been Push’d. Thus Push(a) does not simply add the message a to tSet but a pair (index, a) where index is the current number of the Push action. Accordingly, Pop takes the elements out of tSet in ascending order of index.

The current indices for the Push and Pop actions are stored in the counter variables index_{s} and index_{r}. Both start at 0; every Push increments index_{s}; every Pop increments index_{r}. Thus index_{s} is the index of the next element to be Push’d and index_{r} is the index of the next element to be Pop’d.

The difference between index_{s} and index_{r} equals the size of tSet, thus it can be used to specify that the buffer must not be full at the beginning of a Push.

module II

extends CommonDefinitions

variables tSet, index_{r}, index_{s}

Vars =^{Δ} ⟨tSet, index_{s}, index_{r} ⟩ Init =^{Δ} ∧ tSet = ∅ ; ∧ index_{s} = 0 ; ∧ index_{r} = 0

Push(a) =^{Δ} ∧ a ∈ Messages ∧ index_{s} − index_{r} < BufferLength ∧ tSet′ = tSet ∪ {⟨index_{s}, a ⟩} ∧ index′_{s} = index_{s} + 1 ∧ unchanged index_{r}

Pop =^{Δ} ∧ ∃ a : ∧ ⟨index_{r}, a ⟩ ∈ tSet ∧ tSet′ = tSet \ {⟨index_{r}, a ⟩} ∧ index′_{r} = index_{r} + 1 ∧ unchanged index_{s}

SomeAction =^{Δ} ∨ ∃ a : Push(a) ∨ Pop

Safety =^{Δ} ∧ Init ∧ □[SomeAction]_{Vars}

4 Sender and Receiver

In this module, we split tSet into two different variables, rSet and sSet. We are slowly evolving towards a specification with distinct sender and receiver sides. At this stage though, we keep index_{r} and index_{s} as global variables. In particular, the sender action Push uses the information in the receiver variable index_{r}.

The buffer is now the (disjoint) union of rSet and sSet. Its actual size still equals the difference between index_{s} and index_{r}.

The only changes to Push and Pop are that we now Push to sSet but Pop from rSet. A new action Transfer is added to the model, to represent the transfer of information from rSet to sSet. This action picks non-deterministically a pair from sSet and moves it to rSet. Indexing and index_{r} become critical as pairs are Transfer’d in non-deterministic order, but must be Pop’d in FIFO order.

module III

extends CommonDefinitions

variables sSet, rSet, index_{s}, index_{r}

Vars =^{Δ} ⟨sSet, rSet, index_{s}, index_{r} ⟩ Init =^{Δ} ∧ index_{r} = 0 ; ∧ index_{s} = 0 ; ∧ sSet = ∅ ; ∧ rSet = ∅

Push(a) =^{Δ} ∧ a ∈ Messages ∧ index_{s} − index_{r} < BufferLength ∧ sSet′ = sSet ∪ {⟨index_{s}, a ⟩} ∧ index′_{s} = index_{s} + 1 ∧ unchanged ⟨rSet, index_{r} ⟩

Pop =^{Δ} ∧ ∃ a : ∧ ⟨index_{r}, a ⟩ ∈ rSet ∧ rSet′ = rSet \ {⟨index_{r}, a ⟩} ∧ index′_{r} = index_{r} + 1 ∧ unchanged ⟨sSet, index_{s} ⟩

Transfer =^{Δ} ∧ ∃ p : ∧ p ∈ sSet ∧ sSet′ = sSet \{p} ∧ rSet′ = rSet ∪ {p} ∧ unchanged ⟨index_{s}, index_{r} ⟩

SomeAction =^{Δ} ∨ ∃ a : Push(a) ∨ Pop ∨ Transfer

Safety =^{Δ} ∧ Init ∧ □[SomeAction]_{Vars}

5 Copy and Purge

Specification IV introduces a first degree of asynchronism between both sides of communication. An index-message pair is no longer Transfer’d but rather Copy’d from sSet to rSet and later Purge’d from sSet, when it has been Pop’d for certain. As a consequence rSet is not disjoint from, but rather a subset of sSet. This asynchronism is a first step towards handling loss of data between sender and receiver: the sender became careful, she keeps a sent message until she knows it has been Pop’d.

In the Specifications II and III , the difference index_{s} −index_{r} was controlled to ensure that the buffer didn’t exceed the maximum length. Here, we use the term index_{s} − MinIndex(sSet) instead, since MinIndex(sSet) can linger below index_{r}. The size control is now completely local to the sender side.

This is the only change to Push. Pop has not changed at all. In contrast to III .Transfer, Copy allows multiple copying of the same pair to rSet. Since we are dealing with sets, such multiple copies are idempotent. Purge can handle several messages at once: it non-deterministically picks an already-Pop’d message in sSet and deletes this and all older messages.

The sender and the receiver side are not yet completely separated. Copy is a common action using both sSet and rSet. Purge could be regarded as a sender action, but it still uses the receiver information in index_{r}, thus index_{r} remains a global variable.

module IV

extends CommonDefinitions

variables sSet, rSet, index_{r}, index_{s}

Vars =^{Δ} ⟨sSet, rSet, index_{r}, index_{s} ⟩ Init =^{Δ} ∧ index_{r} = 0 ; ∧ index_{s} = 0 ; ∧ sSet = ∅ ; ∧ rSet = ∅

Push(a) =^{Δ} ∧ a ∈ Messages ∧ ∨ sSet = ∅ ∨ index_{s} − MinIndex(sSet) < BufferLength ∧ sSet′ = sSet ∪ {⟨index_{s}, a ⟩} ∧ index′_{s} = index_{s} + 1 ∧ unchanged ⟨rSet, index_{r} ⟩

Pop =^{Δ} ∧ ∃ a : ∧ ⟨index_{r}, a ⟩ ∈ rSet ∧ rSet′ = rSet \{⟨index_{r}, a ⟩} ∧ index′_{r} = index_{r} + 1 ∧ unchanged ⟨sSet, index_{s} ⟩

Copy =^{Δ} ∧ ∃ p : ∧ p ∈ sSet ∧ p[1] ≥ index_{r} ∧ rSet′ = rSet ∪ {p} ∧ unchanged ⟨sSet, index_{s}, index_{r} ⟩ Purge =^{Δ} ∧ ∃ p ∈ sSet : ∧ p[1] < index_{r} ∧ sSet′ = sSet \ {pair ∈ sSet : pair[1] ≤ p[1]} ∧ unchanged ⟨rSet, index_{r}, index_{s} ⟩ SomeAction =^{Δ} ∨ ∃ a : Push(a) ∨ Pop ∨ Copy ∨ Purge Safety =^{Δ} ∧ Init ∧ □[SomeAction]_{Vars}

6 Sliding Window with Linear Arithmetic

Module V specifies the sliding-window-style message retransmission mechanism with linear arithmetic. We introduce full decoupling between sender and receiver by modeling communications as two one-way communication channels: a forward channel fBuffer for the messages and a backward channel bBuffer for acknowledgements. These are the only common variables of the sender and the receiver sides.

The communication channels are handled as if they might lose data: sender and receiver can send messages rsp. acknowledgements repeatedly; the sender keeps the sent messages until they have been acknowledged, and the receiver acknowledges only what he has already Pop’d.

Rather than Copying a pair from one side to the other, the pair is put into fBuffer with SendMsg, and read from there by ReadMsg. fBuffer contains either one index-message pair or the zero element ⟨0, ⊥_{Messages} ⟩ which indicates ”no message”. SendMsg copies an arbitrary message from sSet into fBuffer, no matter if this overwrites an unread earlier message. Reading a message deletes it from fBuffer and puts it into rSet.

SendAck and ReadAck replace IV .Purge: SendAck copies index_{r} into bBuffer. Thus bBuffer contains the index of the oldest message, that might not yet be Pop’d. It can be understood as meaning ”precisely those messages older than this index are guaranteed to be Pop’d”. ReadAck removes all messages from sSet with an index older (i.e. smaller) than that in bBuffer. In contrast to fBuffer, bBuffer is never reset to 0.

module V

extends CommonDefinitions

variables sSet, rSet, index_{r}, index_{s}, fBuffer, bBuffer

Vars =^{Δ} ⟨sSet, rSet, index_{r}, index_{s}, fBuffer, bBuffer ⟩ Init =^{Δ} ∧ index_{r} = 0 ∧ index_{s} = 0 ∧ sSet = ∅ ∧ rSet = ∅ ∧ fBuffer = ⟨0, ⊥_{Messages} ⟩ ∧ bBuffer = 0

Push(a) =^{Δ} ∧ a ∈ Messages ∧ (sSet = ∅) ∨ (index_{s} − MinIndex(sSet) < BufferLength) ∧ sSet′ = sSet ∪ {⟨index_{s}, a ⟩} ∧ index′_{s} = index_{s} + 1 ∧ unchanged ⟨rSet, index_{r}, fBuffer, bBuffer ⟩

Pop =^{Δ} ∧ ∃ a : ∧ ⟨index_{r}, a ⟩ ∈ rSet ∧ rSet′ = rSet \ {⟨index_{r}, a ⟩} ∧ index′_{r} = index_{r} + 1 ∧ unchanged ⟨sSet, index_{s}, fBuffer, bBuffer ⟩ SendMsg =^{Δ} ∧ ∃ p : ∧ p ∈ sSet ∧ fBuffer′ = p ∧ unchanged ⟨index_{s}, index_{r}, sSet, rSet, bBuffer ⟩ ReadMsg =^{Δ} ∧ fBuffer ≠ ⟨0, ⊥_{Messages} ⟩ ∧ fBuffer[1] < index_{r} + BufferLength ∧ fBuffer[1] ≥ index_{r} ∧ rSet′ = rSet ∪ {fBuffer} ∧ fBuffer′ = ⟨0, ⊥_{Messages} ⟩ ∧ unchanged ⟨index_{s}, index_{r}, sSet, bBuffer ⟩ SendAck =^{Δ} ∧ bBuffer′ = index_{r} ∧ unchanged ⟨index_{s}, index_{r}, sSet, rSet, fBuffer ⟩ ReadAck =^{Δ} ∧ sSet′ = sSet \{pair ∈ sSet : pair[1] < bBuffer} ∧ unchanged ⟨index_{s}, index_{r}, rSet, fBuffer, bBuffer ⟩ SomeAction =^{Δ} ∨ ∃ a : Push(a) ∨ Pop ∨ SendMsg ∨ ReadMsg ∨ SendAck ∨ ReadAck Safety =^{Δ} ∧ Init ∧ □[SomeAction]_{Vars}