Specification and Verification of Distributed Systems

Peter Ladkin

Office: D6-131; Tel: (106)-5326 Computer Lab: D6-129; Tel: (106)-5325 Sprechstunden: Wednesday 11.00-12.00

ladkin@rvs.uni-bielefeld.de
http://www.rvs.uni-bielefeld.de

All course notes are available only via WWW under my home page or RVS course page.

In the course, we study how to perform verifications, using the TLA+ specification language and the TLA logic. We use an implementation of a bounded buffer and part of a Lazy Caching algorithm as examples.

In the Seminar, we will work through a set of preliminary specifications of the Radio Link Protocol, a form of sliding window protocol, that will be used in the TDMA cellular phone technology.

Formal proofs in TLA+ exist:—

• A buffer defined as an array implements an abstract buffer:

Formal but Lively Buffers in TLA+

• The Lazy Caching algorithm of Afek, Brown and Merritt (ACM Transactions on Programming Languages and Systems, Jan 1993) implements a sequentially consistent memory

Lazy Caching: An Assertional View Ladkin, Lamport, Roegel and Olivier Distributed Computing, to appear.

Section 1: General Background

4

What is a specification? It is a means of describing what a system is supposed to do. When the system does what the specification says, the system fulfils the specification. How do we know when a system fulfils a specification? We prove it mathematically. Can we just look at the code and see that it works? No. Mistakes are almost always made. Do mathematicians do formal proofs? Generally, no they don’t. They are concerned with proving a hard theorem. Their proofs are semi-formal.

Why should computer scientists do formal proofs?

Because, if they work with concurrent systems, many, many mistakes have been made in published algorithms, even in the best journals.

E.g., Lamport’s Bakery algorithm for mutual exclusion is incorrectly explained in many operating system textbooks.

What is a concurrent system? One that isn’t sequential. What is a sequential system? One that isn’t concurrent.

OK,OK, a sequential system is one that executes one thread of control. A concurrent system has many threads of control.

What’s a thread of control?

Consider your favorite C program. It starts at the beginning, moves on down the code statements, goes into subroutines and returns, and finishes (maybe). Control passes from one statement to the next.

At any point, control is at a unique place. The thread is the list of statements executed by the program.

How can I have many threads?

Build an operating system, for example (a real one, like Unix).

You may have L^{A}TEX running in one window, while you’re performing shell commands in another, and viewing a compiled L^{A}TEX file in another, using xdvi.

Or, you have a transaction processing machine, like the one which processes your bank card money withdrawals from an Automated Teller Machine (ATM). It must handle many transactions at the same time. Each one forms a different thread.

Or, you have an airplane such as the Airbus A320/A330/A340 series, in which the pilot’s control commands are input to a flight control computer which interacts with the flight guidance management system and also the autopilot. The flight control computer figures out itself how best to interpret the pilot’s commands, and moves the control surfaces according to its calculations.

Isn’t this risky?

Look at the RISKS-Digest (ed. by Peter Neumann) at

       http://catless.ncl.ac.uk/Risks/

for articles, including many by me, about the A320/A330/A340 accidents/incidents that may concern the computers.

So what are the technical problems? A typical (classical) one: two threads want to access the same memory location at the same time: one to read, another to write. How do I write such concurrent programs? With a great deal of care.

What are the industrial problems?

• How to encourage industrial developers to write specifications of their systems at a high-enough level to permit logical analysis

• How to provide them the tools to do this What sort of tools are useful?

• A formal specification language

• A proof method, that shows how you prove systems fulfil their specifications

• A automated proof-checker that helps in doing low-level proof steps Is there just a system, and a specification?

No, normally there are many intermediate specifications. Even the system itself is described by a very-low-level specification.

People nowadays don’t try to prove real code correct, they work with a very close description of the operation of the code, but written in a specification language.

One needs to show that each specification is fulfilled by the next more-detailed specification.

How does one do this?

There are many notions of fulfil. The most straightforward one is logical implication. The high-level specification is a logical formula and this is implied by the logical formula that is the lower-level specification History: this hierarchichal method was first developed by SRI International for defining and proving the SIFT flight control system correct. SRI’s verification system was known as HDM (Hierarchical Development Methodology), and was superceded by EHDM (Extended HDM).

SIFT details at

   http://www.csl.sri.com/ft-history.html

SRI has an ongoing Formal Methods program. Details at

   http://www.csl.sri.com/sri-csl-fm.html

More about some interesting aircraft control system computer ‘features’ is in John Rushby’s home page (link on the Formal Methods page), under ‘Images and Anomalies’.

What are some of the discoveries about control system concurrency?

The problems of

Byzantine Agreement: How can many processors agree on a correct value when one of them is lying?

For example, two flight control computers calculate values and check with each other to make sure they calculated the same value.

But they didn’t!

Hint: you can’t figure out which one is wrong with only two channels (processors).

The Airbus A320/A330/A340 control system uses two identical channels for fault-tolerance. So they can’t tolerate Byzantine faults. But do they need to?

The Boeing B777 control system has only one flight control computer—but the back-up is a very simple direct-law control system, and the switch is under pilot control.

Which is better? Who knows?

Clock Synchronisation: The AFTI-F16 aircraft had two independent channels that worked without synchronising the clocks of each channel. They got slightly different readings from the sensors, with interesting consequences. See Rushby.

Arbitration: Buridan’s Ass. (Lamport has pointed out that the arbitration problem exists in all analogue-to-digital conversions.) Apparently, engineers don’t worry about arbitration.

What about a problem with transaction processing systems?

Sequential Consistency: Suppose many transactions are happening to the same account at the same time. If they’re all reads, no problem. If some of them are writes, there may be a problem. How do we ensure that the system behaves as if one transaction happened after the other (even if they really all happened at once)?

Specification Methods for Concurrent

Systems

• Logic–the Assertional Method

• Algebra–process algebras

• Petri Nets

• Various industrial methods that are insufficient for verifying the system but good for organising it.

The Assertional Method

One treats the system as a state machine. This state machine may have infinitely many states. For each possible system action, one describes (by a logical formula) a property of the state that must hold for the action to take place (a precondition) and a property of the state that must hold after the action has happened (a postcondition).

For sequential systems, developed by Floyd and Hoare (late 1960’s). For concurrent systems, by Ashcroft (1975), further developed by Owicki and Gries (1976).

Temporal logic methods (Pnueli 1977) are most suitable for proofs of liveness properties (Owicki, Lamport, Manna, Pnueli, and many others).

A good incarnation is TLA, the Temporal Logic of Actions and its associated specification language TLA+.

If Q is a logical formula expressing a system property, then □Q expresses that it always holds, and ◇Q that it will hold at some state in the future.

A specification has the form

Init ∧ □S ∧ Fair

where S is the safety property (which must always hold in any state), and Fair says

□◇¬Enabled (A) ∨ □◇A

or something similar.

Process Algebra

CCS: Robin Milner CSP: Tony Hoare Processes are fundamental, and are defined by algebraic equations:

P = a ; P

is a process that executes a, then repeats.

P = a ; P'
P' = b ; P

describes two processes. P executes a, then P', which executes b and returns to P.

The actions, however, are joint between two or more processes:

S = P || P' || P''
P = a ; P
P' = a ; b ; P'
P'' = b ; P''

is a system S which executes a joint action between P and P', then one between P' and P'', then ....

We will study the assertional method for specifying and verifying systems.

We will learn what a proof is, and how to do one.

We will discuss the essential classes of system properties:

safety and liveness

Every system property is a conjunction of a safety property with a liveness property (Alpern and Schneider 1987).

And to learn about the tools that exist, join in my seminar.

Section 2: Writing Specifications in TLA+

26

First, an abstract buffer with two operations

push(something) and pop

The figure shows the state of the buffer before each operation and the state after

[figure: buffer; buffer′; < b,x,y,d >; pop; < x,y,d >; < b,x,y,d >; push(a); < b,x,y,d,a >]

Here is a more concrete version of the buffer It’s an array ⊥ is the symbol for ‘nothing here’

[figure: Buffer; Buffer′; ⊥; b; x; y; ⊥; d; ⊥; push(a); ⊥; b; x; y; ⊥; d; a; ⊥; b; x; y; ⊥; d; a; move(6); ⊥; b; x; y; d; ⊥; a; ⊥; b; x; y; d; ⊥; a; move(2); b; ⊥; x; y; d; ⊥; a; b; ⊥; x; y; d; ⊥; a; pop; ⊥; ⊥; x; y; d; ⊥; a]

Here’s how the concrete buffer is supposed to correspond to the abstract buffer as a data structure

[figure: ConcreteBuffer; AbstractBuffer; ⊥; b; x; y; ⊥; d; ⊥; < b,x,y,d >; ⊥; b; x; y; ⊥; d; a; < b,x,y,d,a >; ⊥; b; x; y; d; ⊥; a; < b,x,y,d,a >; b; ⊥; x; y; d; ⊥; a; < b,x,y,d,a >]

And here’s how the operations correspond How does this fit together?

The concrete buffer simulates the abstract buffer

• they start in ‘equivalent’ states

• every action of the concrete buffer corresponds either to an action or to a non-action of the abstract buffer

• when the concrete buffer is sufficiently ‘live’, then the abstract buffer actually does some desired action This method of state machine simulation is common to many methods, for example

• TLA of Lamport

• Input/Output machines of Tuttle, Lynch, Vaandrager

• the method of Lam and Shankar (also TL-based)

An alternative is to have actions only—then the operation of the system is an abstract machine simulation, but not a state machine simulation, since one doesn’t have state How does one specify the actions? Here’s one from the abstract buffer

module AbstractBuffer

actions push(a) =^{Δ} ∧ a ∈ Data ∧ Len(buffer) < N ∧ buffer′ = buffer ∘ ⟨a ⟩

Why is it written like this?

Let’s compare two ways of writing this action

module AbstractBuffer

actions push(a) =^{Δ} ∧ a ∈ Data ∧ Len(buffer) < N ∧ buffer′ = buffer ∘ ⟨a ⟩

badly-written actions

push(a) =^{Δ}

a ∈ Data ∧ Len(buffer) < N ∧ buffer′ = buffer ∘ ⟨a ⟩ If that didn’t persuade you, try this

module AbstractBuffer

actions push(a|b) =^{Δ} ∧ a ∈ Data ∧ Len(buffer) < N ∧ ∨ buffer′ = buffer ∘ ⟨a ⟩ ∨ buffer′ = buffer ∘ ⟨b ⟩

badly-written actions

push(a|b) =^{Δ}

a ∈ Data ∧ Len(buffer) < N ∧ (buffer′ = buffer ∘ ⟨a ⟩ ∨ buffer′ = buffer ∘ ⟨b ⟩)

Now we shall see how to write the two specifications. First, we define the starting states of the variables.

module AbstractBuffer

predicates

Init =^{Δ} buffer = ⟨ ⟩

module ConcreteBuffer

predicates

Init =^{Δ} ∀ n ∈ 1..N : Buffer[n] = ⊥ Next, we define the push actions

module Buffer Actions

abstract actions push(a) =^{Δ} ∧ a ∈ Data ∧ Len(buffer) < N ∧ buffer′ = buffer ∘ ⟨a ⟩

concrete actions push(a) =^{Δ} ∧ a ∈ Data ∧ Buffer[N ] = ⊥ ∧ Buffer′[N ] = a ∧ ∀ i ∈ 1..(N − 1) : unchanged Buffer[i] And now the pop actions

module Buffer Actions

abstract actions pop =^{Δ} ∧ Len(buffer) > 0 ∧ buffer′ = tail(buffer)

concrete actions pop =^{Δ} ∧ Buffer[1] ≠ ⊥ ∧ Buffer′[1] = ⊥ ∧ ∀ i ∈ 2..N : unchanged Buffer[i] And there’s one concrete action left

module Buffer Actions

abstract actions

no − op =^{Δ} unchanged buffer concrete actions

move(k) =^{Δ} ∧ k ∈ 2..N ∧ Buffer[k] ≠ ⊥ ∧ Buffer[k − 1] = ⊥ ∧ Buffer′[k] = ⊥ ∧ Buffer′[k − 1] = Buffer[k] ∧ ∀ i ∈ 1..(k − 2) : unchanged Buffer[i] ∧ ∀ i ∈ (k + 1)..N : unchanged Buffer[i] We have the initial conditions and the actions. But we don’t yet have a specification

A specification defines the initial conditions and the actions—

and also the sentence that says

• the system starts in the initial condition

• if variables change values, it must be because of a defined action (safety)

• it’s always true that some desired action eventually happens if it can (liveness)

First some notation. [A]_{x} means A ∨ (x′ = x) [A]_{⟨x,y ⟩} means A ∨ (x′ = x ∧ y′ = y) Intuitively, [A]_{x} means

Either A or x doesn’t change value

module AbstractBuffer

imports Sequences

parameters buffer : variable Data, N : constant

predicates Init =^{Δ} buffer = ⟨ ⟩

module AbstractBuffer (continued) actions

push(a) =^{Δ} ∧ a ∈ Data ∧ Len(buffer) < N ∧ buffer′ = buffer ∘ ⟨a ⟩

pop =^{Δ} ∧ Len(buffer) > 0 ∧ buffer′ = tail(buffer)

temporal Spec =^{Δ} ∧ Init ∧ □[pop ∨ ∃ b : push(b)]_{buffer} ∧ WF_{buffer}(pop)

module ConcreteBuffer

parameters Buffer : variable Data, N : constant

assertions

⊥ ∉ Data predicates

Init =^{Δ} ∧ ∀ n ∈ 1..N : Buffer[n] = ⊥

module ConcreteBuffer (continued) actions

push(a) =^{Δ} ∧ a ∈ Data ∧ Buffer[N ] = ⊥ ∧ Buffer′[N ] = a ∧ ∀ i ∈ 1..(N − 1) : unchanged Buffer[i]

pop =^{Δ} ∧ Buffer[1] ≠ ⊥ ∧ Buffer′[1] = ⊥ ∧ ∀ i ∈ 2..N : unchanged Buffer[i]

module ConcreteBuffer (continued) actions

move(k) =^{Δ} ∧ k ∈ 2..N ∧ Buffer[k] ≠ ⊥ ∧ Buffer[k − 1] = ⊥ ∧ Buffer′[k] = ⊥ ∧ Buffer′[k − 1] = Buffer[k] ∧ ∀ i ∈ 1..(k − 2) : unchanged Buffer[i] ∧ ∀ i ∈ (k + 1)..N : unchanged Buffer[i] module ConcreteBuffer (will this never end?) temporal

Spec =^{Δ} ∧ Init ∧ □[\begin{matrix}∨ pop \\ ∨ ∃ b : push(b) \\ ∨ ∃ k : move(k)]_{Buffer} \end{matrix} ∧ WF_{Buffer}(pop) ∧ WF_{Buffer}(∃ k : move(k))

Section 3: Verification in TLA

51

Verification means that one has • A description of an implementation

• A specification One must prove that the description of the implementation fulfils the specification. For logical methods, ‘fulfils’ = ‘implies’ For real systems, one must use hierarchical methods in order to control the complexity.

Hierarchical methods: one describes an implementation I , then a more abstract view A_{1} and proves that

I ⇒ A_{1}

One describes then an even more abstract view A_{2} and proves that

A_{1} ⇒ A_{2}

But if that’s true, of course, then simply

I ⇒ A_{2}

and there’s little need for the intermediate step.

It’s when there are many separate parts that need to be brought together that hierarchical decomposition pays off.

A simple hierarchical decomposition:

Level 1 a database distributed over 5 different sites with query points over many more

Level 2 • a specification of a serial database

• a specification of a database split into 5 pieces

• a specification of a reliable protocol for queries

Level 3 • a specification of an implementation of a serial database

• a specification of an implementation of a database split into 5 pieces

• a specification of an implementation of a reliable protocol for queries We start at the beginning. We have two specifications.

module Specifications

temporal

Conc − Buffer − Spec =^{Δ} ∧ Init ∧ □[\begin{matrix}∨ pop \\ ∨ ∃ b : push(b) \\ ∨ ∃ k : move(k)]_{Buffer} \end{matrix}

∧ WF_{Buffer}(pop)

∧ WF_{Buffer}(∃ k : move(k))

Abs − Buffer − Spec =^{Δ} ∧ Init ∧ □[\begin{matrix}∨ pop \\ ∨ ∃ b : push(b)]_{buffer} \end{matrix}

∧ WF_{buffer}(pop)

We want to show that Conc-Buffer-Spec ⇒ Abs-Buffer-Spec But it doesn’t! Conc-Buffer-Spec has a variable Buffer which doesn’t occur in Abs-Buffer-Spec Abs-Buffer-Spec has a variable buffer which doesn’t occur in Conc-Buffer-Spec But are these variables essential? We merely want to specify a buffer, without really caring what specific object is a buffer.

An implementation builds a data structure buffer from ‘concrete’ data structures that it contains.

In ‘real’ programming languages, a set is ‘implemented’ as a bit array. The set (abstract data structure) is a statically-defined function of the basic data structure (bit array = sequence of adjacent words).

We define such a function: call it buffer. We want to know that this always behaves as a buffer, no matter how the underlying ‘concrete’ data structures behave.

Where predicate A contains an occurrence of the variable buffer, let A be A[buffer/buffer], that is, A with all occurrences of buffer replaced by buffer.

Thus we prove

∀ ∀ ∀∀ ∀ ∀ Buffer : Conc−Buffer−Spec ⇒ Abs−Buffer−Spec

Or, more formally, ..........

module Theorems

include ConcreteBuffer as CB(N) include AbstractBuffer as AB(N)

buffer =^{Δ} ...........

theorems ∀ ∀ ∀∀ ∀ ∀ Buffer : CB(N ).Spec ⇒ AB(N ).Spec What does include mean?

It means that the variables, definitions, operations, from ConcreteBuffer are visible in this buffer, with the same names, except that every operation or temporal definition is prefixed with the given name of the include-ed module.

Similarly for AbstractBuffer.

One can include variable s and constant s with names other than the original ones – see Michael Blume’s Einführung or the TLA+ Manual.

Section 4: Proofs in TLA

61

Now to the proof. The proof is formal, formally laid out in a hierarchical style, in which substeps constitute a logically correct proof of each step.

Technically, it is an inverse natural deduction proof style.

There are two numbering schemes in pf.sty One is absolute—

the.full.path.number

One is relative—

⟨TheLevelNumber⟩TheStepNumber Here are examples of the same proof with both schemes.

1. A ∧ (P ∧ Q ∧ R) Proof: 1.1. A

Proof: I guess A just is true. 1.2. P ∧ Q ∧ R

Proof: 1.2.1. P ∧ Q

Proof:

1.2.1.1. P

Proof: I guess P just is true. 1.2.1.2. Q

Proof: I guess Q just is true. 1.2.1.3. Q.E.D.

Proof: Conjoin 1.2.1.1 and 1.2.1.2. 1.2.2. R

Proof: I guess R just is true. 1.2.3. Q.E.D.

Proof: Conjoin 1.2.1 and 1.2.2. 1.3. Q.E.D.

Proof: Conjoin 1.1 and 1.2.

⟨1⟩1. A ∧ (P ∧ Q ∧ R) Proof: ⟨2⟩1. A

Proof: I guess A just is true. ⟨2⟩2. P ∧ Q ∧ R

Proof: ⟨3⟩1. P ∧ Q

Proof:

⟨4⟩1. P

Proof: I guess P just is true. ⟨4⟩2. Q

Proof: I guess Q just is true. ⟨4⟩3. Q.E.D.

Proof: Conjoin ⟨4⟩1 and ⟨4⟩2. ⟨3⟩2. R

Proof: I guess R just is true. ⟨3⟩3. Q.E.D.

Proof: Conjoin ⟨3⟩1 and ⟨3⟩2. ⟨2⟩3. Q.E.D.

Proof: Conjoin ⟨2⟩1 and ⟨2⟩2.

Proof step numbers in the buffer example are relative.

See if you can assign path-numbers to the proof steps as we go So, how do we prove ⟨0⟩1. ∀ ∀ ∀∀ ∀ ∀ Buffer : CB(N ).Spec ⇒ AB(N ).Spec ?? We can prove it if we treat Buffer like a variable (which it is): ⟨1⟩1. CB(N ).Spec ⇒ AB(N ).Spec Remember, we have a state function buffer =^{Δ} f (Buffer) that interprets buffer.

By convention, we let

buffer =^{Δ} f (Buffer)

(this is the Refinement Mapping) and AB(N ).Spec is AB(N ).Spec, with every occurrence of buffer replaced by buffer. Then, we prove ⟨2⟩1. CB(N ).Spec ⇒ AB(N ).Spec Predicate logic allows us to conclude what we want from this.

Each specification is a conjunction

Init ∧ □[action ∨ action ∨ ...]_{variables} ∧ Liveness It seems most reasonable to prove the conjunction bit by bit: ⟨3⟩1. CB(N ).Spec ⇒ AB(N ).Init ⟨3⟩2. CB(N ).Spec ⇒ □[\begin{matrix}∨ AB(N ).pop \\ ∨ ∃ a : AB(N )push(a) ]_{buffer} \end{matrix}

⟨3⟩3. CB(N ).Spec ⇒ WF_{buffer}(AB(N ).pop) ⟨3⟩4. Q.E.D.

Proof: Follows by propositional logic from the conjunction of steps ⟨3⟩1, ⟨3⟩2 and ⟨3⟩3.

In fact, it turns out that we may prove

⟨3⟩1. CB(N ).Spec ⇒ AB(N ).Init

Proof: ⟨4⟩1. CB(N ).Init ⇒ AB(N ).Init ⟨4⟩2. Q.E.D.

Proof: Follows directly by propositional logic.

⟨3⟩2. CB(N ).Spec ⇒ □[\begin{matrix}∨ AB(N ).pop \\ ∨ ∃ a : AB(N )push(a) ]_{buffer} \end{matrix}

Proof:

⟨4⟩1. ∧ CB(N ).Init

∧ □[\begin{matrix}∨ CB(N ).pop \\ ∨ ∃ a : CB(N ).push(a) \\ ∨ ∃ k : CB(N ).move(k)]_{Buffer} \end{matrix}

⇒ □[\begin{matrix}∨ AB(N ).pop \\ ∨ ∃ a : AB(N )push(a) ]_{buffer} \end{matrix}

⟨4⟩2. Q.E.D. Proof: Follows directly by propositional logic.

Consider now the step ⟨4⟩1. CB(N ).Init ⇒ AB(N ).Init

Proof: .... is simply math.

We may prove

⟨4⟩1. □[∨ CB(N ).pop ∨ ∃ a : CB(N ).push(a) ∨ ∃ k : CB(N ).move(k)]_{Buffer} ⇒ □[\begin{matrix}∨ AB(N ).pop \\ ∨ ∃ a : AB(N )push(a) ]_{buffer} \end{matrix}

Proof: ⟨5⟩1. (∨ CB(N ).pop ∨ ∃ a : CB(N ).push(a) ∨ ∃ k : CB(N ).move(k) ∨ Buffer′ = Buffer) ⇒ (\begin{matrix}∨ AB(N ).pop \\ ∨ ∃ a : AB(N )push(a) \\ ∨ buffer′ = buffer) \end{matrix}

⟨5⟩2. Q.E.D.

Proof: Follows directly by the TLA rule

STL.4 \frac{F ⇒ G}{□F ⇒ □G}

Let’s do it......

⟨5⟩1. (∨ CB(N ).pop ∨ ∃ a : CB(N ).push(a) ∨ ∃ k : CB(N ).move(k) ∨ Buffer′ = Buffer) ⇒ (\begin{matrix}∨ AB(N ).pop \\ ∨ ∃ a : AB(N )push(a) \\ ∨ buffer′ = buffer) \end{matrix}

Proof: ⟨6⟩1. CB(N ).pop ⇒ AB(N ).pop ⟨6⟩2. ∃ a : CB(N ).push(a) ⇒

∃ a : AB(N ).push(a)

⟨6⟩3. ∃ k : CB(N ).move(k) ⇒ buffer′ = buffer ⟨6⟩4. Buffer′ = Buffer ⇒ buffer′ = buffer ⟨6⟩5. Q.E.D.

Proof: Follows by propositional logic from ⟨6⟩1, ⟨6⟩2, ⟨6⟩3, and ⟨6⟩4: (A ⇒ X ) ∧ (B ⇒ Y ) ∧ (C ⇒ Z ) ∧ (D ⇒ Z )

⇒ (A ∨ B ∨ C ∨ D ⇒ X ∨ Y ∨ Z )

Now, part of this says: a concrete push is an abstract push.

⟨6⟩2. ∃ a : CB.push(a)

⇒

∃ a : AB.push(a)

Proof: Let: a : constant ⟨7⟩1. CB.push(a)

⇒

AB.push(a)

⟨7⟩2. Q.E.D.

Follows from ⟨7⟩1 by predicate logic.

⟨7⟩1. CB.push(a) ⇒

AB.push(a)

Proof: ⟨8⟩1. CB.push(a) ⇒ a ∈ Data

Proof: Immediate from the definition of CB.push.

⟨8⟩2. CB.push(a) ⇒ Len(buffer) < N ⟨8⟩3. CB.push(a) ⇒ buffer′ = buffer ∘ ⟨a ⟩ ⟨8⟩4. Q.E.D.

Proof: Follows immediately from ⟨8⟩1, ⟨8⟩2 and ⟨8⟩3 using propositional logic.

⟨8⟩2. CB.push(a) ⇒ Len(buffer) < N

Proof: ⟨9⟩1. CB.push(a) ⇒ Buffer[N ] = ⊥

Proof: Immediate from the definition of CB.push(a).

⟨9⟩2. Buffer[N ] = ⊥ ⇒

Len(SelectSeq(Buffer, NonVoid)) < N Proof: Follows from the definition of SelectSeq and Len, along with a certain amount of data structure manipulation, which is omitted.

⟨9⟩3. Q.E.D.

Proof: Follows from ⟨9⟩1, ⟨9⟩2 and the definition of buffer by propositional logic.

What do all these symbols mean?

Let: NonVoid(k) =^{Δ} k ≠ ⊥ buffer =^{Δ} SelectSeq(Buffer, NonVoid) FirstFull =^{Δ} Buffer[1] ≠ ⊥ NotEmpty =^{Δ} ∃ i ∈ 1 . . N : Buffer[i] ≠ ⊥

module Sequences

import Naturals

m . . n =^{Δ} {i ∈ Nat : (m ≤ i) ∧ (i ≤ n)}

Len(s) =^{Δ}

choose n : (n ∈ Nat) ∧ ((Domain s) = (1 . . n))

Head(s) =^{Δ} s[1]

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)]]

Seq(S) =^{Δ} union {[(1 . . n) → S] : n ∈ Nat} SubSeq(s, m, n) =^{Δ}

[i ∈ (1 . .(1 + n − m)) ↦ s[i + m − 1]]

module Sequences (continued) SelectSeq(s, test( )) =^{Δ} let F [ t : Seq({s[i] : i ∈ (1 . . Len(s))}) ] =^{Δ}

if t = ⟨ ⟩ then ⟨ ⟩

else if test(Head(t))

then ⟨Head(t)⟩∘ ; F [Tail(t)]
else F [Tail(t)]
in F [s]

⟨8⟩3. CB.push(a) ⇒ buffer′ = buffer ∘ ⟨a ⟩

Proof: ⟨9⟩1. CB.push(a) ⇒

SelectSeq(Buffer, NonVoid) =

SelectSeq([i ∈ 1 . .(N − 1) ↦ Buffer[i]],

NonVoid)

Proof: ⟨10⟩1. CB.push(a) ⇒ Buffer[N ] = ⊥

Proof: Immediate from the definition of CB.push(a).

⟨10⟩2. Buffer[N ] = ⊥ ⇒ SelectSeq(Buffer, NonVoid) = SelectSeq([i ∈ 1 . .(N − 1)

↦ Buffer[i]], NonVoid)

Proof: Follows immediately from the definition of SelectSeq using manipulations of the data structure.

⟨10⟩3. Q.E.D.

Proof: Follows immediately from ⟨10⟩1 and ⟨10⟩2 by propositional logic.

⟨9⟩1. (was on last slide)

⟨9⟩2. CB.push(a)

⇒

Buffer′ =

[i ∈ 1 . .(N − 1) ↦ Buffer[i]] ∘ ⟨a ⟩

Proof: Follows from the definition of CB.push and the sequence operations.

⟨9⟩3. SelectSeq([i ∈ 1 . .(N − 1) ↦ Buffer[i]]

∘ ⟨a ⟩, NonVoid) =

SelectSeq([i ∈ 1 . .(N −1) ↦ Buffer[i]], NonVoid) ∘ ⟨a ⟩

Proof: Follows from the definition of SelectSeq and NonVoid.

⟨9⟩4. Q.E.D.

Proof: Follows immediately from ⟨9⟩1, ⟨9⟩2, ⟨9⟩3 by propositional logic, substitution, and the definition of buffer.

This completes the proof. All the substeps have been proved.

Now we’ll take a look at the TLA special inference rules, and the proof scheme for TLA verifications Section 5: More About Proofs in TLA+

84

We return to the safety step ⟨4⟩1. □[∨ CB(N ).pop ∨ ∃ a : CB(N ).push(a) ∨ ∃ k : CB(N ).move(k)]_{Buffer} ⇒ □[\begin{matrix}∨ AB(N ).pop \\ ∨ ∃ a : AB(N )push(a) ]_{buffer} \end{matrix}

⟨5⟩1. (∨ CB(N ).pop ∨ ∃ a : CB(N ).push(a) ∨ ∃ k : CB(N ).move(k) ∨ Buffer′ = Buffer) ⇒ (\begin{matrix}∨ AB(N ).pop \\ ∨ ∃ a : AB(N )push(a) \\ ∨ buffer′ = buffer) \end{matrix}

⟨5⟩2. Q.E.D.

Proof: directly by the TLA rule

STL.4 \frac{F ⇒ G}{□F ⇒ □G}

What TLA proof rules are there? First, Temporal Logic rules These are valid for linear-time temporal logic STL 1 : \frac{F a tautology}{□F}

STL 2. ⊢ □F ⇒ F STL 3. ⊢ □□F ≡ □F

STL 4. \frac{F ⇒ G}{□F ⇒ □G}

STL 5. ⊢ □(F ∧ G) ≡ (□F ) ∧ (□G) STL 6. ⊢ (◇□F ) ∧ (◇□G) ≡ ◇□(F ∧ G) STL 7. ⊢ □◇□F ≡ ◇□F LATTICE . ≻ a well−founded partial order on a set S

c not free in F or G

F ∧ (c ∈ S) ⇒

(H_{c} ⇝ (G ∨ ∃d ∈ S : (c ≻ d) ∧ H_{d})) F ⇒ ((∃c ∈ S : H_{c}) ⇝ G)

What’s a well-founded partial order?

order: the numbers are ordered by < but it’s total: all numbers are comparable

Sets are ordered by ⊂ and it’s partial: not every pair of sets is comparable

Sequences are ordered by prefix it’s also partial well-founded: if you follow a chain of x_{1} > x_{2} > x_{3} > ..... it always stops

Try it with numbers, say x_{1} = 510

Try it with sequences, say x_{1} = ⟨5, 7, 24, 610, 7, 5, 4, 2, 3, 2⟩

Lattice is used for fairness proofs. It’s a way of ensuring that recursion stops (always provided you’ve written the recursion properly)

Think of G as the ground clause and H_{c} as the recursive call with parameter c

Use of temporal logic in safety proofs is pro forma, as we shall see Second, Basic TLA Rules These specifically involve the TLA ‘prime’ operator.

TLA 1.\frac{P ∧ (f′ = f ) ⇒ P′}{□P ≡ P ∧ □[P ⇒ P′]_{f}}

TLA 2. \frac{P ∧ [A]_{f} ⇒ Q ∧ [B]_{g}}{□P ∧ □[A]_{f} ⇒ □Q ∧ □[B]_{g}}

Third, Invariance Rules

INV1. \frac{I ∧ [N]_{f} ⇒ I′}{I ∧ □[N]_{f} ⇒ □I}

INV2. ⊢ □I ⇒ (□[N]_{f} ≡ □[N ∧ I ∧ I′]_{f} )

Fourth, Weak Fairness Rules

WF 1.

\frac{P ∧ [N]_{f} ⇒ (P′ ∨ Q′) P ∧ ⟨N ∧ A⟩_{f} ⇒ Q′ P ⇒ Enabled ⟨A⟩_{f}}{□[N]_{f} ∧ WF_{f} (A) ⇒ (P ⇝ Q)}

WF 2.

\frac{⟨N ∧ B⟩_{f} ⇒ ⟨M⟩_{g} P ∧ P′ ∧ ⟨N ∧ A⟩_{f} ∧ Enabled ⟨M⟩_{g} ⇒ B P ∧ Enabled ⟨M⟩_{g} ⇒ Enabled ⟨A⟩_{f} □[N ∧ ¬B]_{f} ∧ WF_{f} (A) ∧ □F ∧ ◇□Enabled ⟨M⟩_{g} ⇒ ◇□P}{□[N]_{f} ∧ WF_{f} (A) ∧ □F ⇒ WF_{g}(M)}

where

F , G, H_{c} are TLA formulas P, Q, I are predicates A, B, N, M are actions f , g are state functions Now to the proof scheme.

In the proof scheme, the steps that are new for each verification are indicated by ******Novel.****** in the proof The proof scheme helps to control the proof:

⟨0⟩1. (∀ ∀ ∀∀ ∀ ∀ y : Init_{1} ∧ □[N_{1}]_{v} ∧ L_{1}) ⇒ (Init_{2} ∧ □[N_{2}]_{w} ∧ L_{2})

Proof: ⟨1⟩1. (Init_{1} ∧ □[N_{1}]_{v} ∧ L_{1})

⇒ (Init_{2} ∧ □[N_{2}]_{w} ∧ L_{2})

Proof:

⟨2⟩1. Init_{1} ⇒ Init_{2}

Proof: ******Novel.******. ⟨2⟩2. Init_{1} ∧ □[N_{1}]_{v} ⇒ □[N_{2}]_{w}

Proof: See next slides. ⟨2⟩3. Init_{1} ∧ □[N_{1}]_{v} ∧ L_{1} ⇒ L_{2}

Proof: ******Novel.******. ⟨2⟩4. Q.E.D.

Proof: By propositional logic from ⟨2⟩1, ⟨2⟩2, ⟨2⟩3.

⟨1⟩2. Q.E.D.

Proof: By predicate logic from ⟨1⟩1.

Let’s look at safety:

⟨2⟩2. Init_{1} ∧ □[N_{1}]_{v} ⇒ □[N_{2}]_{w} Proof: First we must find an invariant: ⟨3⟩1. Init_{1} ∧ □[N_{1}]_{v} ⇒ □Inv ⟨3⟩2. □Inv ∧ □[N_{1}]_{v} ⇒ □[N_{2}]_{w} ⟨3⟩3. Q.E.D.

Proof: Immediate from ⟨3⟩1 and ⟨3⟩2 by propositional logic.

Now the substeps for the invariant:

⟨3⟩1. Init_{1} ∧ □[N_{1}]_{v} ⇒ □Inv

⟨4⟩1. Init_{1} ⇒ Inv

Proof: ******Novel.****** ⟨4⟩2. Inv ∧ □[N_{1}]_{v} ⇒ □Inv

Proof: ⟨5⟩1. Inv ∧ [N_{1}]_{v} ⇒ Inv′

Proof: ******Novel.****** ⟨5⟩2. Q.E.D.

Proof: Immediate from ⟨5⟩1 by Rule INV1.

⟨4⟩3. Q.E.D.

Proof: Immediate from ⟨4⟩1 and ⟨4⟩2 by propositional logic.

Now the rest:

⟨3⟩2. □Inv ∧ □[N_{1}]_{v} ⇒ □[N_{2}]_{w} Proof: ⟨4⟩1. □Inv ∧ □[N_{1}]_{v} ⇒ □[N_{1} ∧ Inv ∧ Inv′]_{v}

Proof: Immediate from INV2 using STL5. ⟨4⟩2. □[N_{1} ∧ Inv ∧ Inv′]_{v} ⇒ □[N_{2}]_{w}

Proof: ⟨5⟩1. [N_{1} ∧ Inv ∧ Inv′]_{v} ⇒ [N_{2}]_{w}

Proof: ******Novel.******. ⟨5⟩2. Q.E.D.

Proof: Immediate from ⟨5⟩1 by STL4. ⟨4⟩3. Q.E.D.

Proof: Immediate from ⟨4⟩1 and ⟨4⟩2 by propositional logic.

Section 5: Get Live! (If it’s safe)

⟨5⟩1. Inv ∧ [N_{1}]_{v} ⇒ Inv′

⟨6⟩1. Inv ∧ (N_{1} ∨ v′ = v) ⇒ Inv′ Proof: Suppose N_{1} =^{Δ} A_{1} ∨ A_{2} ∨ A_{3}, where A_{1}, A_{2}, A_{3} are the actions of the implementing module. ⟨7⟩1. Inv ∧ A_{1} ⇒ Inv′

Proof: ******************* ⟨7⟩2. Inv ∧ A_{2} ⇒ Inv′

Proof: ******************* ⟨7⟩3. Inv ∧ A_{3} ⇒ Inv′

Proof: ******************* ⟨7⟩4. Inv ∧ v′ = v ⇒ Inv′

Proof: Since the only variables in Inv are v, this is immediate.

⟨7⟩5. Q.E.D.

Proof: Propositional Logic from ⟨7⟩1, ⟨7⟩2, ⟨7⟩3, ⟨7⟩4.

⟨5⟩1. [N_{1} ∧ Inv ∧ Inv′]_{v} ⇒ [N_{2}]_{w} Proof: ⟨6⟩1. A_{1} ∧ Inv ∧ Inv′ ⇒ [N_{2}]_{w}

Proof: ***************** ⟨6⟩2. A_{2} ∧ Inv ∧ Inv′ ⇒ [N_{2}]_{w}

Proof: **************** ⟨6⟩3. A_{3} ∧ Inv ∧ Inv′ ⇒ [N_{2}]_{w}

Proof: *************** ⟨6⟩4. (v′ = v) ⇒ [N_{2}]_{w}

Proof: ⟨7⟩1. v′ = v ⇒ w′ = w

Proof: Since the only variables in w are v, this is immediate.

⟨7⟩2. Q.E.D.

Proof: Immediate by propositional logic from ⟨7⟩1.

⟨6⟩5. Q.E.D.

Proof: Propositional Logic from ⟨6⟩1, ⟨6⟩2, ⟨6⟩3, ⟨6⟩4.

(Meta-Theorem!) Thus, we can see that a safety proof exists providing only that the proof obligations

Init_{1} ⇒ Init_{2}

For every action A

in the antecedent Spec

Inv ∧ A ⇒ Inv′

For every action A

in the antecedent Spec

A ∧ Inv ∧ Inv′ ⇒ (N_{2} ∨ w′ = w)

are proved.

In fact, we can go further, in principle. Write every action A in disjunctive normal form

A ⇔ B^{A}_{1} ∨ B^{A}_{2} ∨ ....

Then, by propositional logic, we only need

Init_{1} ⇒ Init_{2} and

Inv ∧ B ⇒ Inv′

B ∧ Inv ∧ Inv′ ⇒ (N_{2} ∨ w′ = w) for every disjunct B of any action in the antecedent spec.

But it’s less clean to write and remember.

What kind of thing is an invariant? Remember, it must remain true through every action.

Type information, for example

What else??

The buffer example is so straightforward that the invariant is just (N_{1} ∨ v′ = v) itself and I didn’t go down to the step level.

But in general one needs to go down to the step level What about those awful liveness properties? We need to prove

WF_{buffer}(pop)

given

WF_{Buffer}(pop) ∧ WF_{Buffer}(∃ k : move(k)) and the initial condition and safety property of ConcreteBuffer Intuitively, WF_{buffer}(pop) means

When pop can go, it must–sometime.

I.e., when pop is continually enabled, it must go sometime Is AB.pop enabled? Is CB.pop enabled?

ConcreteBuffer  AbstractBuffer ⊥ ⊥ b ⊥ d ⊥ ⊥  \overline{}< b,d >

Intuitively, AB.pop is enabled when the buffer is nonempty. So Buffer is also nonempty, but there may not be anything in Buffer[1], so CB.pop is not enabled.

So AB.pop may be enabled, even though CB.pop is not What’s the formal definition of WF_{v}(A)?

□◇¬Enabled ⟨A⟩_{v} ∨ □◇⟨A⟩_{v}

that is

□◇¬Enabled (A ∧ v′ ≠ v) ∨ □◇(A ∧ v′ ≠ v)

Remember [A]_{v} =^{Δ} (A ∨ v′ = v)

Likewise, we can write ⟨A⟩_{v} =^{Δ} (A ∧ v′ ≠ v)

Then ¬[¬A]_{v} ⇔ ⟨A⟩_{v} and ¬⟨¬A⟩_{v} ⇔ [A]_{v} and ¬[A]_{v} ⇔ ⟨¬A⟩_{v} and ¬⟨A⟩_{v} ⇔ [¬A]_{v}

etc.

What’s the formal definition of Enabled? Suppose I have an action such as

pop =^{Δ} ∧ Len(buffer) > 0 ∧ buffer′ = tail(buffer)

It has variable buffer, and next value buffer′. If I say there is a next value, that means I can do pop, in principle That’s exactly what Enabled says: Enabled(pop) =^{Δ}

∃ newvalue : ∧ Len(buffer) > 0 ∧ newvalue = tail(buffer)

In general, let action A have flexible variables y, z

Enabled(A) =^{Δ} ∃ newy, newz : A(y′/newy, z′/newz)

where

• newy and newz are new symbols not otherwise occurring in A;

• A(y′/newy, z′/newz) is A, but with newy substituted for every occurrence of y′, similarly for newz So, Enabled(pop) =^{Δ}

∃ newvalue : ∧ Len(buffer) > 0 ∧ newvalue = tail(buffer)

⇔

∧ Len(buffer) > 0

∧ ∃ newvalue : newvalue = tail(buffer)

But ∃ newvalue : newvalue = tail(buffer) is true!

Why? Let ϕ(x) =^{Δ} (x = tail(buffer)). Then ϕ(tail(buffer)) is true (it’s an axiom for equality!) So, we may invoke the rule \frac{ϕ(t)}{∃x : ϕ(x)}

to infer that ∃ newvalue : ϕ(newvalue) is true So

∧ Len(buffer) > 0 ∧ ∃ newvalue : newvalue = tail(buffer)

⇔

∧ Len(buffer) > 0 ∧ true

⇔

Len(buffer) > 0 Similarly,

Enabled(CB.pop ∧ Buffer′ ≠ Buffer)

⇔

∃ Newbuf : ∧ Buffer[1] ≠ ⊥ ∧ Newbuf [1] = ⊥ ∧ ∀ i ∈ 2..N : Newbuf [i] = Buffer[i]

⇔

∧ Buffer[1] ≠ ⊥ ∧ ∃ Newbuf : ∧ Newbuf [1] = ⊥ ∧ ∀ i ∈ 2..N : Newbuf [i] = Buffer[i] We’ll show ∃ Newbuf : ∧ Newbuf [1] = ⊥ ∧ ∀ i ∈ 2..N : Newbuf [i] = Buffer[i]

is true. Define

TheRealNewBuf =^{Δ} [Buffer except !1 = ⊥] Then

∧ TheRealNewBuf [1] = ⊥ ∧ ∀ i ∈ 2..N : TheRealNewBuf [i] = Buffer[i]

follows immediately from the definition

So, Enabled⟨CB.pop ⟩_{Buffer} ⇔ (Buffer[1] ≠ ⊥)

Finally, you try it now with ∃ k : CB.move(k). it’s very similar to CB.pop Next time:

Using the WF rules Remember the Weak Fairness Rules

WF 1.

\frac{P ∧ [N]_{f} ⇒ (P′ ∨ Q′) P ∧ ⟨N ∧ A⟩_{f} ⇒ Q′ P ⇒ Enabled ⟨A⟩_{f}}{□[N]_{f} ∧ WF_{f} (A) ⇒ (P ⇝ Q)}

WF 2.

\frac{⟨N ∧ B⟩_{f} ⇒ ⟨M⟩_{g} P ∧ P′ ∧ ⟨N ∧ A⟩_{f} ∧ Enabled ⟨M⟩_{g} ⇒ B P ∧ Enabled ⟨M⟩_{g} ⇒ Enabled ⟨A⟩_{f} □[N ∧ ¬B]_{f} ∧ WF_{f} (A) ∧ □F ∧ ◇□Enabled ⟨M⟩_{g} ⇒ ◇□P}{□[N]_{f} ∧ WF_{f} (A) ∧ □F ⇒ WF_{g}(M)}

where

F , G, H_{c} are TLA formulas P, Q, I are predicates A, B, N, M are actions f , g are state functions ⟨3⟩1.

∧ □[\begin{matrix}∨ ∃ a : CB.push(a) \\ ∨ CB.pop \\ ∨ ∃ k : CB.move(k)]_{Buffer}] \end{matrix}

∧ WF_{Buffer}(CB.pop)

∧ WF_{Buffer}(∃ k : CB.move(k))

⇒
WF_{buffer}(AB.pop)

Proof: ⟨4⟩1. ⟨\begin{matrix}∨ ∃ a : CB.push(a) \\ ∨ CB.pop \\ ∨ ∃ k : CB.move(k)) ∧ CB.pop ⟩_{Buffer} \end{matrix}

⇒
⟨AB.pop ⟩_{buffer}

Proof: ***************** ⟨4⟩2.

∧ FirstFull ∧ FirstFull′ ∧ ⟨CB.pop ⟩_{Buffer} ∧ Enabled⟨AB.pop ⟩_{buffer}

⇒ CB.pop

Proof: ******************* ⟨4⟩3.

∧ FirstFull

∧ Enabled⟨AB.pop ⟩_{buffer} ⇒ Enabled⟨CB.pop ⟩_{Buffer}

Proof: ***************** ⟨4⟩4.

∧ □[\begin{matrix}∧ ∨ ∃ a : CB.push(a) ∨ CB.pop ∨ ∃ k : CB.move(k) \\ ∧ ¬CB.pop]_{Buffer} \end{matrix}

∧ WF_{Buffer}(CB.pop)

∧ WF_{Buffer}(∃ k : CB.move(k)) ∧ ◇□Enabled⟨AB.pop ⟩_{buffer}

⇒

◇□FirstFull Proof: ***************

⟨4⟩5. Q.E.D. Proof: Follows from ⟨4⟩1, ⟨4⟩2, ⟨4⟩3 and ⟨4⟩4 using TLA Proof Rule WF2 with N =^{Δ} (∃ a : CB.push(a)∨CB.pop∨∃ k : CB.move(k)), f = Buffer, A =^{Δ} B =^{Δ} CB.pop, M =^{Δ} AB.pop, g = buffer, P =^{Δ} FirstFull, □F =^{Δ} WF_{Buffer}(∃ k : CB.move(k)).

Section 7: The Lazy Caching Algorithm and Invariants

[figure: mem; …; in[1]; out[1]; c[1]; ch[1]; Processor 1; Processor N; in[N ]; out[N ]; c[N ]; ch[N ]]

118

dch q[1] ch[1]

q[2] ch[2]

q[N ]

ch[N ]

Serial Database

[figure: cin[1]; cout[1]; cc[1]; ch[1]; Processor 1; Processor N; cin[N ]; cout[N ]; cc[N ]; ch[N ]]

120

module LazyCache

import MemParams, ChannelInterface, Sequences, Naturals

parameters c, in, out, mem : variable

⊥ =^{Δ} choose i : i ∉ Data

Restrict(f ) =^{Δ}

{g ∈ [Addr → Data ∪ {⊥}] : ∀ a ∈ Addr : g[a] ∈ {f [a], ⊥}}

module LazyCache: the Initial condition Init =^{Δ} ∧ mem ∈ [Addr → InitData] ∧ c ∈ [Proc → Restrict(mem)] ∧ in = [i ∈ Proc ↦ ⟨ ⟩] ∧ out = [i ∈ Proc ↦ ⟨ ⟩]

module LazyCache: Actions

Read(i, d, a) =^{Δ} ∧ out[i] = ⟨ ⟩ ∧ ∀ j ∈ 1 . . Len(in[i]) : Len(in[i][j ]) = 2 ∧ c[i][a] = d ∧ ChanOp(ch[i], ⟨i, “Rd” , d, a ⟩) ∧ ∀ j ∈ Proc \{i} : unchanged ch[j ] ∧ unchanged ⟨c, in, out, mem ⟩

module LazyCache: Actions

Write(i, d, a) =^{Δ} ∧ ChanOp(ch[i], ⟨i, “Wr” , d, a ⟩) ∧ out′ = [out except ![i] = out[i] ∘ ⟨⟨d, a ⟩⟩] ∧ ∀ j ∈ Proc \{i} : unchanged ch[j ] ∧ unchanged ⟨c, in, mem ⟩ MemWrite(i) =^{Δ}

∧ out[i] ≠ ⟨ ⟩ ∧ out′ = [out except ![i] = Tail(out[i])] ∧ in′ = [j ∈ Proc ↦ in[j ] ∘ if j = i then ⟨Head(out[i]) ∘ ⟨“∗” ⟩⟩ else ⟨Head(out[i])⟩ ]

∧ mem′ = [mem except ![Head(out[i])[2]] = Head(out[i])[1] ]

∧ unchanged ⟨c, ch ⟩

CacheUpdate(i) =^{Δ} ∧ in[i] ≠ ⟨ ⟩ ∧ in′ = [in except ![i] = Tail(in[i])] ∧ c′ = [c except ![i][Head(in[i])[2]] = Head(in[i])[1] ]

∧ unchanged ⟨out, ch, mem ⟩

module LazyCache: Actions

MemRead(i) =^{Δ} ∧ ∃ a ∈ Addr : in′ = [in except ![i] = in[i] ∘ ⟨⟨mem[a], a ⟩⟩] ∧ unchanged ⟨out, c, mem, ch ⟩

CacheInval(i) =^{Δ} ∧ c′ ∈ {[c except ![i] ∈ Restrict(c[i])]} ∧ unchanged ⟨in, out, mem, ch ⟩

Next(i) =^{Δ}

∨ ∃ d ∈ Data, a ∈ Addr : ∨ Read(i, d, a) ∨ Write(i, d, a)

∨ MemWrite(i) ∨ CacheUpdate(i) ∨ MemRead(i) ∨ CacheInval(i)

module LazyCache: Specification

vars =^{Δ} ⟨c, in, out, mem, ch ⟩

Spec =^{Δ} ∧ Init ∧ □[∃ i ∈ Proc : Next(i)]_{vars} ∧ ∀ i ∈ Proc : ∨ WF_{vars}(CacheUpdate(i)) ∨ WF_{vars}(MemWrite(i))

module CCache: Definitions

import MemParams, ChannelInterface, Sequences, Naturals parameters cc, cin, cout : variable

module CCache: Init

module CCache: Actions

Init =^{Δ} ∧ cc ∈ [Proc → [Addr → InitData]] ∧ ∀ i, j ∈ Proc : cc[i] = cc[j ] ∧ cin = [i ∈ Proc ↦ ⟨ ⟩] ∧ cout = [i ∈ Proc ↦ ⟨ ⟩] Read(i, d, a) =^{Δ}

∧ cout[i] = ⟨ ⟩ ∧ ∀ j ∈ (1 . . Len(cin[i])) : cin[i][j ][1] ≠ i ∧ cc[i][a] = d ∧ ChanOp(ch[i], ⟨i, “Rd” , d, a ⟩) ∧ ∀ j ∈ Proc \{i} : unchanged ch[j ] ∧ unchanged ⟨cc, cin, cout ⟩

Write(i, d, a) =^{Δ} ∧ ChanOp(ch[i], ⟨i, “Wr” , d, a ⟩) ∧ cout′ = [cout except ![i] = cout[i] ∘ ⟨⟨i, “Wr” , d, a ⟩⟩]

∧ ∀ j ∈ Proc \{i} : unchanged ch[j ]

∧ unchanged ⟨cc, cin ⟩ MemWrite(i) =^{Δ}

∧ cout[i] ≠ ⟨ ⟩ ∧ cout′ = [cout except ![i] = Tail(cout[i])] ∧ cin′ = [j ∈ Proc ↦ cin[j ] ∘ ⟨Head(cout[i])⟩] ∧ unchanged ⟨cc, ch ⟩

CacheUpdate(i) =^{Δ} ∧ cin[i] ≠ ⟨ ⟩ ∧ cin′ = [cin except ![i] = Tail(cin[i])] ∧ cc′ = [cc except ![i][Head(cin[i])[4]] = Head(cin[i])[3]]

∧ unchanged ⟨cout, ch ⟩

module CCache: Actions

Next(i) =^{Δ}

∨ ∃ d ∈ Data, a ∈ Addr : ∨ Read(i, d, a) ∨ Write(i, d, a) ∨ MemWrite(i) ∨ CacheUpdate(i)

module CCache: Specification

vars =^{Δ} ⟨cc, cin, cout, ch ⟩

Spec =^{Δ}

∧ Init ∧ □[∃ i ∈ Proc : Next(i)]_{vars} ∧ ∀ i ∈ Proc : ∧ WF_{vars}(CacheUpdate(i)) ∧ WF_{vars}(MemWrite(i))

A predicate needed to state the invariant CCInv.3(p)

Let:

∀ i ∈ Proc : NotRefresh_{i}(j ) =^{Δ} ∧ j ∈ 1 . . Len(lcin[i]) ∧ lcin[i][j ][2] ≠ “Rd”

The first two components of the invariant

Let: CCInv.1(p) =^{Δ} Len(lcin[p]) = Len(in[p])

CCInv.2(p) =^{Δ} c[p] ∈ Restrict(vc[p])

Either there’s no MemWrite in the queue..

Let: NoMemWrite(a, p) =^{Δ} ∧ p ∈ Proc ∧ vc[p][a] = mem[a] ∧ ∀ k ∈ 1 . . Len(in[p]) : ∨ in[p][k][2] ≠ a ∨ in[p][k][1] = mem[a] .. or the last MemWrite is the value of mem Let: LastIsMem(a, p) =^{Δ}

∧ p ∈ Proc

∧ ∃ k ∈ 1 . . Len(in[p]) : ∧ NotRefresh_{p}(k) ∧ in[p][k][1] = mem[a] ∧ in[p][k][2] = a ∧ ∀ j ∈ k + 1 . . Len(in[p]) : ∨ in[p][j ][2] ≠ a ∨ in[p][j ][1] = mem[a] .. and the first MemWrite is the value of vc Let: FirstIsVC (a, p) =^{Δ}

∧ p ∈ Proc

∧ ∃ k ∈ 1 . . Len(in[p]) : ∧ NotRefresh_{p}(k) ∧ in[p][k][2] = a ∧ ∀ j ∈ 1 . . k − 1 : ∨ in[p][j ][2] ≠ a ∨ in[p][j ][1] = vc[p][a] .. and between MemWrites are just repeats of the last one

Let: MemWritesFromTo(m, n, p) =^{Δ} ∧ p ∈ Proc ∧ m ∈ 1 . . Len(in[p]) ∧ n ∈ 1 . . Len(in[p]) ∧ m < n ∧ NotRefresh_{p}(m) ∧ NotRefresh_{p}(n) ∧ ∀ j ∈ m + 1 . . n − 1 : ¬NotRefresh_{p}(j )

⇒

∀ j ∈ m + 1 . . n − 1 : ∨ in[p][j ][2] ≠ in[p][m][2] ∨ in[p][j ][1] = in[p][m][1] ...so here’s the third component of the invariant

Let: BetweenMemWrites(p) =^{Δ}

∀ m, n ∈ 1 . . Len(in[p]) : MemWritesFromTo(m, n, p)

CCInv.3(p) =^{Δ}

∧ BetweenMemWrites(p) ∧ ∀ a ∈ Addr : ∨ NoMemWrite(a, p) ∨ ∧ LastIsMem(a, p) ∧ FirstIsVC (a, p)

...and the invariant itself

Let: CCInv(p) =^{Δ} ∧ CCInv.1(p) ∧ CCInv.2(p) ∧ CCInv.3(p)

CCInv.1 =^{Δ} ∀ p ∈ Proc : CCInv.1(p) CCInv.2 =^{Δ} ∀ p ∈ Proc : CCInv.2(p) CCInv.3 =^{Δ} ∀ p ∈ Proc : CCInv.3(p)

CCInv =^{Δ} CCInv.1 ∧ CCInv.2 ∧ CCInv.3 Section 8: The Invariants for Lazy Caching

141

[figure: <d_{1},a_{1},*>; <d_{2},a_{2}>; <d_{3},a_{3}>; in[i]; c[i]; ⇒; <d,a,*>; <d_{1},a_{1},*>; <d_{2},a_{2}>; <d_{3},a_{3}>; in′[i]; c′[i]]

MemWrite(i) (for in[i])

[figure: <d_{1},a_{1},*>; <d_{2},a_{2}>; <d_{3},a_{3}>; in[i]; c[i]; ⇒; <d,a>; <d_{1},a_{1}>; <d_{2},a_{2},*>; <d_{3},a_{3}>; in′[j]; c′[j]]

MemWrite(i) (for in[j])

[figure: <d_{1},a_{1},*>; <d_{2},a_{2}>; <d_{3},a_{3}>; i W; j; j; hin[i]+in[i]; vc[i]; ⇒; <d,a,*>; <d_{1},a_{1},*>; <d_{2},a_{2}>; <d_{3},a_{3}>; i W; i W; j; j; in′[i]+hin′[i]; vc′[i]]

HMemWrite(i)

[figure: <d_{1},a_{1},*>; <d_{2},a_{2}>; <d_{3},a_{3}>; <d,a>; in[i]; c[i]; ⇒; <d_{1},a_{1},*>; <d_{2},a_{2}>; <d_{3},a_{3}>; in′[i]; <d,a>; c′[i]]

CacheUpdate(i)

[figure: <d_{1},a_{1},*>; <d_{2},a_{2}>; <d_{3},a_{3}>; <d,a>; i W; j; p; j; hin[i]+in[i]; <d_{4},a>; vc[i]; ⇒; <d_{1},a_{1},*>; <d_{2},a_{2}>; <d_{3},a_{3}>; i W; j; p; in′[i]+hin′[i]; <d,a>; vc′[i]]

HCacheUpdate(i)

[figure: <d_{1},a_{1},*>; <d_{2},a_{2}>; <d_{3},a_{3}>; in[i]; c[i]; ⇒; <d,a>; <d_{1},a_{1},*>; <d_{2},a_{2}>; <d_{3},a_{3}>; in′[i]; c′[i]]

MemRead(i)

[figure: <d_{1},a_{1},*>; <d_{2},a_{2}>; <d_{3},a_{3}>; i W; j; j; hin[i]+in[i]; vc[i]; ⇒; <d,a>; <d_{1},a_{1},*>; <d_{2},a_{2}>; <d_{3},a_{3}>; i R; i W; j; j; in′[i]+hin′[i]; vc′[i]]

HMemRead(i)

<d_{1},a,*> <d_{3},a> <d_{3},a,*> <d_{2},a> i W i R i W i R hin[i]+in[i]^{}vc[i]  NotRefresh_{i} NotRefresh_{i} ¬NotRefresh_{i} ¬NotRefresh_{i}

Illustrating NotRefresh_{i}(k)

[figure: <d_{1},a,*>; <d_{2},a>; <d,a,*>; <d_{2},a>; i W; i R; i W; i R; hin[i]+in[i]; vc[i]]

Can this happen?

[figure: <d_{1},a,*>; <d,a>; <d,a>; <d,a,*>; <d_{2},a>; i W; i R; i R; i W; i R; hin[i]+in[i]; vc[i]]

MemWritesFromTo(2, 7, i)

Hence the invariant

BetweenMemWrites(i) =^{Δ} ∀ m, n ∈ 1 . . Len(in[i]) : MemWritesFromTo(m, n, i)

where

MemWritesFromTo(m, n, i) =^{Δ} ∧ i ∈ Proc ∧ m ∈ 1 . . Len(in[i]) ∧ n ∈ 1 . . Len(in[i]) ∧ m < n ∧ NotRefresh_{i}(m) ∧ NotRefresh_{i}(m) ∧ ∀ j ∈ m + 1 . . n − 1 : ¬NotRefresh_{i}(j ) ⇒ ∀ j ∈ m + 1 . . n − 1 :

∨ in[i][j ][2] ≠ in[i][m][2] ∨ in[i][j ][1] = in[i][m][1]

[figure: <d_{2},a>; <d_{2},a>; <d,a,*>; <d_{2},a>; i R; i R; i W; i R; hin[i]+in[i]; vc[i]]

But what about this??

So every refresh of “a” that follows the last write of “a” had better contain the same data value as that write.

[figure: <d,a>; <d,a>; <d_{2},a>; <d_{2},a>; i R; i R; i R; i R; hin[i]+in[i]; vc[i]]

Or this??

So if there are only refreshes, they had better all have the same value. What value?

[figure: <d_{2},a>; <d_{2},a>; <d_{2},a>; <d_{2},a>; i R; i R; i R; i R; hin[i]+in[i]; <d,a>; vc[i]]

Ummmm, any old value?

The same value that has already been written in vc[i][a].

[figure: <d,a>; mem; <d_{2},a>; <d_{2},a>; <d_{2},a>; <d_{2},a>; i R; i R; i R; i R; hin[i]+in[i]; <d_{2},a>; vc[i]]

But aren’t we forgetting something?

Final invariant:

• Refreshes between adjacent writes must be the same as the first one;

• When there are only refreshes in in[i], they must be the same as in vc and in mem;

• Otherwise, it’s vc until the first Write, and mem beyond the last one NoMemWrite(a, p) =^{Δ}

∧ p ∈ Proc ∧ vc[p][a] = mem[a] ∧ ∀ k ∈ 1 . . Len(in[p]) : ∨ in[p][k][2] ≠ a ∨ in[p][k][1] = mem[a]

LastIsMem(a, p) =^{Δ} ∧ p ∈ Proc ∧ ∃ k ∈ 1 . . Len(in[p]) : ∧ NotRefresh_{p}(k) ∧ in[p][k][1] = mem[a] ∧ in[p][k][2] = a ∧ ∀ j ∈ k + 1 . . Len(in[p]) : ∨ in[p][j ][2] ≠ a ∨ in[p][j ][1] = mem[a]

FirstIsVC (a, p) =^{Δ} ∧ p ∈ Proc ∧ ∃ k ∈ 1 . . Len(in[p]) : ∧ NotRefresh_{p}(k) ∧ in[p][k][2] = a ∧ ∀ j ∈ 1 . . k − 1 : ∨ in[p][j ][2] ≠ a ∨ in[p][j ][1] = vc[p][a]

CCInv.3(p) =^{Δ}

∧ BetweenMemWrites(p) ∧ ∀ a ∈ Addr : ∨ NoMemWrite(a, p) ∨ ∧ LastIsMem(a, p) ∧ FirstIsVC (a, p)

That’s not all: CCInv.1(p) =^{Δ} Len(hin[p]) = Len(in[p]) CCInv.2(p) =^{Δ} c[p] ∈ Restrict(vc[p])

Finally, CCInv =^{Δ} ∀ p ∈ Proc : ∧ CCInv.1(p) ∧ CCInv.2(p) ∧ CCInv.3(p)

Here’s BetweenMemWrites

∧ i ∈ Proc ∧ HMemWrite(i) ∧ p ∈ Proc ∧ CCInv.1(p) ∧ BetweenMemWrites(p) ∧ ∀ a ∈ Addr : ∨ LastIsMem(a, p) ∨ NoMemWrite(a, p)

⇒ BetweenMemWrites′(p)

Here’s FirstIsVC

∧ i ∈ Proc ∧ HMemWrite(i) ∧ p ∈ Proc ∧ CCInv.1(p) ∧ a ∈ Addr ∧ FirstIsVC (a, p)

⇒ FirstIsVC′(a, p)

With NoMemWrite(Head(out[i])[2], p), things are less simple:

∧ i ∈ Proc ∧ HMemWrite(i) ∧ p ∈ Proc ∧ CCInv.1(p) ∧ NoMemWrite(Head(out[i])[2], p) ⇒ ∨ NoMemWrite′(Head(out[i])[2], p) ∨ FirstIsVC′(Head(out[i])[2], p)

But LastIsMem is easier:

∧ i ∈ Proc ∧ HMemWrite(i) ∧ p ∈ Proc ⇒ LastIsMem′(Head(out[i])[2], p)

so we can conclude

∧ i ∈ Proc ∧ HMemWrite(i) ∧ p ∈ Proc ∧ CCInv.1(p) ∧ NoMemWrite(Head(out[i])[2], p) ⇒ ∨ NoMemWrite′(Head(out[i])[2], p) ∨ ∧ LastIsMem′(Head(out[i])[2], p) ∧ FirstIsVC′(Head(out[i])[2], p)

The proof for the other values of a for NoMemWrite is straightforward.

There’s a symmetric problem with FirstIsVC and HCacheUpdate.

In the buffer example, no invariant was needed, but liveness is non-trivial (we haven’t seen it yet)

LazyCache is interesting because the safety proof is non-trivial.... even though liveness is trivial.

How does it all work?

Section 9: How the Lazy Caching Invariants are Proved

<d_{1},a,*> <d_{3},a> <d_{3},a,*> <d_{2},a> i W i R i W i R hin[i]+in[i]^{}vc[i]  NotRefresh_{i} NotRefresh_{i} ¬NotRefresh_{i} ¬NotRefresh_{i}

Illustrating NotRefresh_{i}(k)

[figure: <d_{1},a,*>; <d,a>; <d,a>; <d,a,*>; <d_{2},a>; i W; i R; i R; i W; i R; hin[i]+in[i]; vc[i]]

MemWritesFromTo(2, 7, i)

BetweenMemWrites(i) =^{Δ} ∀ m, n ∈ 1 . . Len(in[i]) : MemWritesFromTo(m, n, i)

where

MemWritesFromTo(m, n, i) =^{Δ} ∧ i ∈ Proc ∧ m ∈ 1 . . Len(in[i]) ∧ n ∈ 1 . . Len(in[i]) ∧ m < n ∧ NotRefresh_{i}(m) ∧ NotRefresh_{i}(n) ∧ ∀ j ∈ m + 1 . . n − 1 : ¬NotRefresh_{i}(j ) ⇒ ∀ j ∈ m + 1 . . n − 1 :

∨ in[i][j ][2] ≠ in[i][m][2] ∨ in[i][j ][1] = in[i][m][1]

[figure: <f,a>; mem; <f,a>; <f,a>; <e,a>; <e,a>; <d,a>; i R; i W; i R; i W; i R; <d,a>; vc[i]; LastIsMem; BetweenMemWrites; FirstIsVC]

Illustrating the entire invariant Final invariant:

• Refreshes between adjacent writes must be the same as the first one (BetweenMemWrites);

• When there are only refreshes in in[i], they must be the same as in vc and in mem (NoMemWrite);

• Otherwise, it’s vc until the first Write, and mem beyond the last one (FirstIsVC, LastIsMem)

NoMemWrite(a, p) =^{Δ} ∧ p ∈ Proc ∧ vc[p][a] = mem[a] ∧ ∀ k ∈ 1 . . Len(in[p]) : ∨ in[p][k][2] ≠ a ∨ in[p][k][1] = mem[a]

CCInv.3(p) =^{Δ}

∧ BetweenMemWrites(p) ∧ ∀ a ∈ Addr : ∨ NoMemWrite(a, p) ∨ ∧ LastIsMem(a, p) ∧ FirstIsVC (a, p)

That’s not all: CCInv.1(p) =^{Δ} ∧ Len(hin[p]) = Len(in[p]) ∧ Len(hout[p]) = Len(out[p]) ∧ ∀ a ∈ Addr : ∀ d ∈ Data : ∀ j ∈ 1 . . Len(in[i]) : Len(in[i][j ]) = 3 ≡ ∧ hin[i][j ][1] = i ∧ hin[i][j ][2] = “Wr”

CCInv.2(p) =^{Δ} c[p] ∈ Restrict(vc[p])

Finally, CCInv =^{Δ} ∀ p ∈ Proc : ∧ CCInv.1(p) ∧ CCInv.2(p) ∧ CCInv.3(p)

[figure: <d_{1},a_{1},*>; <d_{2},a_{2}>; <d_{3},a_{3}>; in[i]; c[i]; ⇒; <d,a>; <d_{1},a_{1},*>; <d_{2},a_{2}>; <d_{3},a_{3}>; in′[i]; c′[i]]

MemWrite(i)

Here’s BetweenMemWrites for HMemWrite

∧ i ∈ Proc ∧ HMemWrite(i) ∧ p ∈ Proc ∧ CCInv.1(p) ∧ BetweenMemWrites(p) ∧ ∀ a ∈ Addr : ∨ LastIsMem(a, p) ∨ NoMemWrite(a, p)

⇒ BetweenMemWrites′(p)

∧ i ∈ Proc ∧ HMemWrite(i) ∧ p ∈ Proc ∧ CCInv.1(p) ∧ a ∈ Addr ∧ FirstIsVC (a, p)

⇒ FirstIsVC′(a, p)

With NoMemWrite(Head(out[i])[2], p), things are less simple:

∧ i ∈ Proc ∧ HMemWrite(i) ∧ p ∈ Proc ∧ CCInv.1(p) ∧ NoMemWrite(Head(out[i])[2], p) ⇒ ∨ NoMemWrite′(Head(out[i])[2], p) ∨ FirstIsVC′(Head(out[i])[2], p)

But LastIsMem is easier:

∧ i ∈ Proc ∧ HMemWrite(i) ∧ p ∈ Proc ⇒ LastIsMem′(Head(out[i])[2], p)

so we can conclude

∧ i ∈ Proc ∧ HMemWrite(i) ∧ p ∈ Proc ∧ CCInv.1(p) ∧ NoMemWrite(Head(out[i])[2], p) ⇒ ∨ NoMemWrite′(Head(out[i])[2], p) ∨ ∧ LastIsMem′(Head(out[i])[2], p) ∧ FirstIsVC′(Head(out[i])[2], p)

The proof for the other values of a for NoMemWrite is straightforward.

There’s a symmetric problem with FirstIsVC and HCacheUpdate.

[figure: <d_{1},a_{1},*>; <d_{2},a_{2}>; <d_{3},a_{3}>; <d,a>; in[i]; c[i]; ⇒; <d_{1},a_{1},*>; <d_{2},a_{2}>; <d_{3},a_{3}>; in′[i]; <d,a>; c′[i]]

CacheUpdate(i)

The proof of the simulation is straightforward, given the invariant. HRead simulates LC.Read HWrite simulates LC.Write HMemWrite simulates LC.MemWrite HCacheUpdate simulates either CacheUpdate (NotRefresh(Head(in[i]))) or a no-op HMemRead and HCacheInval both simulate noops In the buffer example, no invariant was needed, but liveness is non-trivial (we haven’t seen it yet)

LazyCache is interesting because the safety proof is non-trivial.... even though liveness is trivial.

Section 10: Liveness Proofs: The Intuition

192

We consider Lazy Caching

193

Weak Fairness is asserted of both LC.MemWrite and LC.CacheUpdate, or CC.MemWrite and CC.CacheUpdate

The refinement mapping to Complete Cache is

cc ← vc cin ← [i ∈ Proc ↦ SelectSeq(hin[i], P[2] ≠ “Rd” )] cout ← hout ch ← ch

So, only NotRefresh items are selected from hin. ¬NotRefresh elements are invisible.

[figure: <f,a>; mem; <f,a>; ...; <f,a>; <e,a>; ...; <e,a>; <d,a>; i R; j R; i W; i R; j W; i W; i R; <d,a>; vc[i]; ⇒; <f,a>; ...; <e,a>; i W; j W; i W; cin[i]; <d,a>; vc[i]]

The refinement mapping to CCache We have a similar situation as with the abstract buffer.

When there is a NotRefresh in hin[i], but ¬NotRefresh(Head(in[i])), then CC .CacheUpdate is Enabled (check it) since some NotRefresh is at the Head of cin, by definition. But LC .CacheUpdate will be a CC.no-op.

WF_{hvars}(HCacheUpdate) ≡ ∨ □◇¬Enabled⟨HCacheUpdate(i)⟩_{hvars}

∨ □◇⟨HCacheUpdate(i)⟩_{hvars}

Fix a state, now. If there’s something in in[i] now, there’s must be something in in[i][1]. And it stays there until a HCacheUpdate(i). So, either ◇HCacheUpdate(i)

or □Enabled(HCacheUpdate(i)). □Enabled(HCacheUpdate(i)) ≡

¬◇¬Enabled(HCacheUpdate(i)) so it contradicts ◇¬Enabled(HCacheUpdate(i)) and thus □◇¬Enabled(HCacheUpdate(i)). Conclusion: ◇HCacheUpdate(i).

So, for any state, Enabled(HCacheUpdate(i)) ⇒ ◇HCacheUpdate(i) Thus □(Enabled(HCacheUpdate(i)) ⇒ ◇HCacheUpdate(i)) This is a special condition called ‘leads to’: Enabled(HCacheUpdate(i)) ⇝ HCacheUpdate(i)

Intuition: because Enabled(CC .CacheUpdate(i))

⇒ Enabled(HCacheUpdate(i)) and Enabled(HCacheUpdate(i)) ⇝ HCacheUpdate(i)) we can prove Enabled(CC .CacheUpdate(i)) ⇝ HCacheUpdate(i) (A ⇒ B ⇝ C implies A ⇝ C )

So, since Enabled(CC .CacheUpdate(i)) ⇝ HCacheUpdate(i) and since Enabled(CC .CacheUpdate(i)) stays true until the NotRefresh is popped (and maybe afterwards), HCacheUpdate(i) will repeat until the NotRefresh is popped, hence intuitively Enabled(CC .CacheUpdate(i)) ⇝ CC .CacheUpdate(i)

Section 11: Lively Buffers, formally

201

Again, the concrete-abstract buffer correspondence as data structure

[figure: ConcreteBuffer; AbstractBuffer; ⊥; b; x; y; ⊥; d; ⊥; < b,x,y,d >; ⊥; b; x; y; ⊥; d; a; < b,x,y,d,a >; ⊥; b; x; y; d; ⊥; a; < b,x,y,d,a >; b; ⊥; x; y; d; ⊥; a; < b,x,y,d,a >]

Here’s again how the operations correspond The refinement mapping

NonVoid(k) =^{Δ} k ≠ ⊥ buffer =^{Δ} SelectSeq(Buffer, NonVoid)

and auxiliary definitions

FirstFull =^{Δ} Buffer[1] ≠ ⊥ NotEmpty =^{Δ} ∃ i ∈ 1 . . N : Buffer[i] ≠ ⊥ NotStuffed =^{Δ} ∃ i ∈ 1 . .(N − 1) : Buffer[i] = ⊥ Descending(Buffer) =^{Δ}

∑ _{i=1}^{N} (Buffer[i] = ⊥).2^{N −i} MaxDescending =^{Δ} ∑ _{i=1}^{N} 2^{N −i} The Weak Fairness Rules

WF 1.

\frac{P ∧ [N]_{f} ⇒ (P′ ∨ Q′) P ∧ ⟨N ∧ A⟩_{f} ⇒ Q′ P ⇒ Enabled ⟨A⟩_{f}}{□[N]_{f} ∧ WF_{f} (A) ⇒ (P ⇝ Q)}

WF 2.

\frac{⟨N ∧ B⟩_{f} ⇒ ⟨M⟩_{g} P ∧ P′ ∧ ⟨N ∧ A⟩_{f} ∧ Enabled ⟨M⟩_{g} ⇒ B P ∧ Enabled ⟨M⟩_{g} ⇒ Enabled ⟨A⟩_{f} □[N ∧ ¬B]_{f} ∧ WF_{f} (A) ∧ □F ∧ ◇□Enabled ⟨M⟩_{g} ⇒ ◇□P}{□[N]_{f} ∧ WF_{f} (A) ∧ □F ⇒ WF_{g}(M)}

where

F , G, H_{c} are TLA formulas P, Q, I are predicates A, B, N, M are actions f , g are state functions

The Lattice Rule \frac{≻ a well−founded partial order on a set S c not free in F or G F ∧ (c ∈ S) ⇒ (H_{c} ⇝ (G ∨ ∃d ∈ S : (c ≻ d) ∧ H_{d}))}{F ⇒ ((∃c ∈ S : H_{c}) ⇝ G)} For the buffer liveness proof, we use TLA Proof Rule WF2 with

N =^{Δ} ∨ ∃ a : CB.push(a) ∨ CB.pop ∨ ∃ k : CB.move(k)

A =^{Δ} B =^{Δ} CB.pop

M =^{Δ} AB.pop

f = Buffer g = buffer P =^{Δ} FirstFull □F =^{Δ} WF_{Buffer}(∃ k : CB.move(k))

The conclusion of the WF2 rule gives us the liveness property we want

⟨2⟩3.

∧ □[\begin{matrix}∨ ∃ a : CB.push(a) \\ ∨ CB.pop \\ ∨ ∃ k : CB.move(k)]_{Buffer} \end{matrix}

∧ WF_{Buffer}(CB.pop)

∧ WF_{Buffer}(∃ k : CB.move(k))

⇒ WF_{buffer}(AB.pop)

It is justified by giving the four premises. The fourth premise is the most difficult to prove. The others are straightforward.

Proof:

⟨3⟩1. ⟨\begin{matrix}∧ ∨ ∃ a : CB.push(a) ∨ CB.pop ∨ ∃ k : CB.move(k) \\ ∧ CB.pop ⟩_{Buffer} \end{matrix}

⇒ ⟨AB.pop ⟩_{buffer} ⟨3⟩2.

∧ FirstFull ∧ FirstFull′ ∧ ⟨CB.pop ⟩_{Buffer} ∧ Enabled⟨AB.pop ⟩_{buffer}

⇒ CB.pop ⟨3⟩3.

∧ FirstFull

∧ Enabled⟨AB.pop ⟩_{buffer}

⇒ Enabled⟨CB.pop ⟩_{Buffer} The hard one—-

⟨3⟩4.

∧ □[\begin{matrix}∧ ∨ ∃ a : CB.push(a) ∨ CB.pop ∨ ∃ k : CB.move(k) \\ ∧ ¬CB.pop]_{Buffer} \end{matrix}

∧ WF_{Buffer}(CB.pop) ∧ WF_{Buffer}(∃ k : CB.move(k)) ∧ ◇□Enabled⟨AB.pop ⟩_{buffer}

⇒

◇□FirstFull A reminder of how the proof goes

⟨3⟩1. ⟨\begin{matrix}∧ ∨ ∃ a : CB.push(a) ∨ CB.pop ∨ ∃ k : CB.move(k) \\ ∧ CB.pop ⟩_{Buffer} \end{matrix}

⇒ ⟨AB.pop ⟩_{buffer} Proof: ⟨4⟩1.

∧ ∨ ∃ a : CB.push(a) ∨ CB.pop ∨ ∃ k : CB.move(k))

∧ CB.pop ≡ CB.pop

⟨4⟩2. ⟨CB.pop ⟩_{Buffer} ⇒ ⟨AB.pop ⟩_{buffer} ⟨3⟩2.

∧ FirstFull ∧ FirstFull′ ∧ ⟨CB.pop ⟩_{Buffer} ∧ Enabled⟨AB.pop ⟩_{buffer}

⇒ CB.pop

Just look at it ⟨3⟩3.

∧ FirstFull ∧ Enabled⟨AB.pop ⟩_{buffer}

⇒ Enabled⟨CB.pop ⟩_{Buffer} ⟨4⟩1. FirstFull

⇒

Enabled⟨CB.pop ⟩_{Buffer}

⟨3⟩4.

∧ □[\begin{matrix}∧ ∨ ∃ a : CB.push(a) ∨ CB.pop ∨ ∃ k : CB.move(k) \\ ∧ ¬CB.pop]_{Buffer} \end{matrix}

∧ WF_{Buffer}(CB.pop)

∧ WF_{Buffer}(∃ k : CB.move(k)) ∧ ◇□Enabled⟨AB.pop ⟩_{buffer} ⇒ ◇□FirstFull

Proof:

First, a simplified version

⟨4⟩1.

∧ □[\begin{matrix}∨ ∃ a : CB.push(a) \\ ∨ ∃ k : CB.move(k)]_{Buffer} \end{matrix}

∧ WF_{Buffer}(CB.pop)

∧ WF_{Buffer}(∃ k : CB.move(k)) ∧ ◇□NotEmpty ⇒ ◇□FirstFull Lecture 12: The Bridge Rule: Towards a Schema for Liveness The Bridge Rule

Let X , Y , Z be propositional variables (that is, symbols standing for any sentences). Then

\frac{\begin{matrix}□X ∧ Y ⇒ □Y \\ □X ⇒ □(Z ⇒ ◇Y ) \end{matrix}}{□X ∧ ◇□Z ⇒ ◇□Y}

Now for an interpretation.

Suppose X is an action, which is a disjunction of actions. Then □X is a safety property. Let Y be a condition. We show

□X ∧ Y ⇒ □Y

X will be N ∧ ¬B, and Y will be something like the extra enabling condition for the concrete action.

We thus show that Y is an invariant if B never happens.

The formula □X ⇒ □(Z ⇒ ◇Y ) is the same as (defined to be) □X ⇒ (Z ⇝ Y ) which is the conclusion of the Lattice Rule. The conclusion of the Bridge Rule is □X ∧ ◇□Z ⇒ ◇□Y which is the form of the fourth hypothesis of WF2. Thus the Bridge Rule bridges the logical gap between the Lattice Rule and the fourth WF2 premise.

How is □X ∧ Y ⇒ □Y proved? Using INV1:

\frac{□X ∧ Y ⇒ Y′}{□X ∧ Y ⇒ □Y}

How is □X ⇒ □(Z ⇒ ◇Y ) proved? Using the Lattice Rule. And we draw the conclusion □X ∧ ◇□Z ⇒ ◇□Y which is the temporal premise of WF2.

In the proof of the Bridge Rule, we use the TL rules

STL7 ⊢ □◇□F ≡ ◇□F

STL2^{◇} ⊢ F ⇒ ◇F

STL4^{◇} \frac{F ⇒ G}{◇F ⇒ ◇G}

STL6^{◇} ⊢ (□◇F ) ∨ (□◇G) ≡ □◇(F ∨ G)

The latter three are easily shown from their normal forms by using □¬ ≡ ¬◇ and ◇¬ ≡ ¬□.

e.g. STL2^{◇} by using the contrapositive: A ⇒ B if and only if ¬B ⇒ ¬A

STL6^{◇} by using De Morgan’s laws

⟨5⟩1. \frac{□X ∧ FF ⇒ □FF □X ⇒ □(NE ⇒ ◇FF )}{□X ∧ ◇□NE ⇒ ◇□FF}

Proof:

⟨6⟩1. \frac{Z ∧ FF ⇒ □FF}{□Z ⇒ □(FF ⇒ □FF )}
⟨6⟩2. \frac{□X ⇒ □(NE ⇒ ◇FF ) □X ⇒ □(FF ⇒ □FF )}{□X ⇒ □(NE ⇒ □◇FF )}

⟨6⟩3. \frac{□X ⇒ □(NE ⇒ □Y )}{□X ∧ □NE ⇒ □Y}
⟨6⟩4. \frac{□X ∧ □NE ⇒ □Y}{□(X ∧ NE) ⇒ □Y}
⟨6⟩5. \frac{□(X ∧ NE) ⇒ □Y )}{◇□(X ∧ NE) ⇒ ◇□Y}
⟨6⟩6. \frac{◇□(X ∧ NE) ⇒ ◇□Y )}{◇□X ∧ ◇□NE ⇒ ◇□Y}
⟨6⟩7. \frac{◇□X ∧ ◇□NE ⇒ ◇□Y}{□X ∧ ◇□NE ⇒ ◇□Y}
⟨6⟩8. \frac{□X ∧ ◇□NE ⇒ ◇□◇FF}{□X ∧ ◇□NE ⇒ ◇□FF}

⟨6⟩9. Q.E.D.

222

⟨6⟩1. \frac{Z ∧ FF ⇒ □FF}{□Z ⇒ □(FF ⇒ □FF )}

Proof: Follows immediately by trivial propositional logic and then STL4.

⟨6⟩2. \frac{□X ⇒ □(NE ⇒ ◇FF ) □X ⇒ □(FF ⇒ □FF )}{□X ⇒ □(NE ⇒ □◇FF )}

Proof: ****************

⟨6⟩3. \frac{□X ⇒ □(NE ⇒ □Y )}{□X ∧ □NE ⇒ □Y}

Proof: This rule follows from PTL.

⟨6⟩4. \frac{□X ∧ □NE ⇒ □Y}{□(X ∧ NE) ⇒ □Y}

Proof: Immediate from STL5 and substitution of equivalent subformulas.

⟨6⟩5. \frac{□(X ∧ NE) ⇒ □Y )}{◇□(X ∧ NE) ⇒ ◇□Y}

Proof: Immediate from STL4^{◇}.

⟨6⟩6. \frac{◇□(X ∧ NE) ⇒ ◇□Y )}{◇□X ∧ ◇□NE ⇒ ◇□Y}

Proof: STL6 and substituting equivalent subformulas.

⟨6⟩7. \frac{◇□X ∧ ◇□NE ⇒ ◇□Y}{□X ∧ ◇□NE ⇒ ◇□Y}

Proof: Strengthening a hypothesis, using STL2^{◇}.

⟨6⟩8. \frac{□X ∧ ◇□NE ⇒ ◇□◇FF}{□X ∧ ◇□NE ⇒ ◇□FF}

Proof: STL7, and substituting equivalent subformulas.

⟨6⟩9. Q.E.D.

Proof: Note Y =^{Δ} ◇FF .

⟨6⟩2. \frac{□X ⇒ □(NE ⇒ ◇FF ) □X ⇒ □(FF ⇒ □FF )}{□X ⇒ □(NE ⇒ □◇FF )}

Proof:

⟨7⟩1. ∧ □(NE ⇒ ◇FF )

∧ □(FF ⇒ □FF ) ⇒

□(NE ⇒ □◇FF )

⟨7⟩2. Q.E.D. Proof: The conclusion of the rule follows from the premises using ⟨7⟩1, Modus Ponens, and propositional logic.

⟨7⟩1. ∧ □(NE ⇒ ◇FF )

∧ □(FF ⇒ □FF ) ⇒

□(NE ⇒ □◇FF ) Proof:

⟨8⟩1. ∧ □(NE ⇒ ◇FF )

∧ □(FF ⇒ □FF ) ⇒

∧ □(NE ⇒ ◇FF ) ∧ □(FF ⇒ ◇□FF )

⟨8⟩2. ∧ □(NE ⇒ ◇FF )

∧ □(FF ⇒ ◇□FF )
≡
∧ (NE ⇝ FF )
∧ (FF ⇝ □FF )

⟨8⟩3. ∧ (NE ⇝ FF )

∧ (FF ⇝ □FF ) ⇒

NE ⇝ □FF

⟨8⟩4. NE ⇝ □FF ≡ □(NE ⇒ ◇□FF ) ⟨8⟩5. □(NE ⇒ ◇□FF ) ⇒ □(NE ⇒ □◇□FF ) ⟨8⟩6. □(NE ⇒ □◇□FF ) ⇒ □(NE ⇒ □◇FF )

⟨8⟩1. ∧ □(NE ⇒ ◇FF )

∧ □(FF ⇒ □FF ) ⇒

∧ □(NE ⇒ ◇FF ) ∧ □(FF ⇒ ◇□FF )

Proof sketch: Uses STL4, STL2^{◇} and propositional logic.

⟨8⟩2. ∧ □(NE ⇒ ◇FF )

∧ □(FF ⇒ ◇□FF ) ≡ ∧ (NE ⇝ FF ) ∧ (FF ⇝ □FF )

Proof: Follows immediately from the definition of ⇝.

⟨8⟩3. ∧ (NE ⇝ FF )

∧ (FF ⇝ □FF ) ⇒

NE ⇝ □FF Proof sketch: Follows by transitivity of ⇝.

⟨8⟩4. NE ⇝ □FF ≡ □(NE ⇒ ◇□FF )

Proof: Follows immediately by the definition of ⇝.

⟨8⟩5. □(NE ⇒ ◇□FF ) ⇒ □(NE ⇒ □◇□FF )

Proof sketch: Follows by STL4 and STL7. ⟨8⟩6. □(NE ⇒ □◇□FF ) ⇒ □(NE ⇒ □◇FF )

Proof sketch: Follows by STL4 and STL2, using substitution of equivalent subformulas.

Done I haven’t yet finished analysing the proof obligations, so I won’t be able to give them here.

Let’s see how the proof finishes up.

The first Bridge Rule hypothesis

⟨5⟩2.

∧ □[\begin{matrix}∨ ∃ a : CB.push(a) \\ ∨ ∃ k : CB.move(k)]_{Buffer} \end{matrix}

∧ WF_{Buffer}(CB.pop)

∧ WF_{Buffer}(∃ k : CB.move(k))

∧ FirstFull ⇒ □FirstFull

Proof: ⟨6⟩1.

∧ □[\begin{matrix}∨ ∃ a : CB.push(a) \\ ∨ ∃ k : CB.move(k)]_{Buffer} \end{matrix}

∧ FirstFull ⇒ □FirstFull

⟨6⟩2. Q.E.D. Proof: Immediate from ⟨6⟩1 by adding a hypothesis.

⟨6⟩1.

∧ □[\begin{matrix}∨ ∃ a : CB.push(a) \\ ∨ ∃ k : CB.move(k)]_{Buffer} \end{matrix}

∧ FirstFull ⇒ □FirstFull

Proof: ⟨7⟩1.

∧ [\begin{matrix}∨ ∃ a : CB.push(a) \\ ∨ ∃ k : CB.move(k)]_{Buffer} \end{matrix}

∧ FirstFull ⇒ FirstFull′

Proof: Follows from the definitions of push and move.

⟨7⟩2. Q.E.D. Proof: Immediate by TLA Proof Rule INV1 from ⟨7⟩1, with the antecedent conjuncts in the other order.

Section 13: The Final Steps: use of the Lattice Rule and WF1 The Weak Fairness Rule WF1. WF 1.

\frac{P ∧ [N]_{f} ⇒ (P′ ∨ Q′) P ∧ ⟨N ∧ A⟩_{f} ⇒ Q′ P ⇒ Enabled ⟨A⟩_{f}}{□[N]_{f} ∧ WF_{f} (A) ⇒ (P ⇝ Q)}

We have seen how to get, using the Bridge Rule,

⟨4⟩4.

∧ □[\begin{matrix}∨ ∃ a : CB.push(a) \\ ∨ ∃ k : CB.move(k)]_{Buffer} \end{matrix}

∧ WF_{Buffer}(CB.pop)

∧ WF_{Buffer}(∃ k : CB.move(k)) ∧ ◇□NotEmpty ⇒ ◇□FirstFull

from

⟨5⟩3.

∧ □[∃ a : CB.push(a).....]_{Buffer} ∧ WF_{Buffer}(CB.pop) ∧ WF_{Buffer}(∃ k : CB.move(k)) ⇒ □(NotEmpty ⇒ ◇FirstFull)

Now we prove the latter.

First a temporal logic equivalence.

For X =^{Δ} ......:

⟨6⟩1. □X ⇒

(NotEmpty ∧ NotStuffed ⇒ ◇FirstFull) ≡ (NotEmpty ⇒ ◇FirstFull)

Proof: ⟨7⟩1. □X ⇒

¬NotStuffed ⇒ ◇FirstFull Proof: ⟨8⟩1. □X ⇒ ¬NotStuffed ⇒ FirstFull

Proof: Immediate from definitions. ⟨8⟩2. FirstFull ⇒ ◇FirstFull

Proof: Immediate from STL2. ⟨8⟩3. Q.E.D.

Proof: Immediately from ⟨8⟩1 and ⟨8⟩2. ⟨7⟩2. Q.E.D.

Proof: Propositional logic from ⟨7⟩1.

Substituting in the consequent, using this new equivalence, we prove

⟨6⟩2.

∧ □[∃ a : CB.push(a)......]_{Buffer} ∧ WF_{Buffer}(CB.pop) ∧ WF_{Buffer}(∃ k : CB.move(k)) ⇒ □(∧ NotEmpty ; ∧ NotStuffed ⇒ ◇FirstFull)

which is shown using the Lattice Rule First, we fiddle with the consequent

⟨7⟩2. ∧ □[∃ a : CB.push(a).........

∧ WF_{Buffer}(CB.pop) ∧ WF_{Buffer}(∃ k : CB.move(k))

⇒ □(∧ ∃ i ∈ 0 . . MaxDescending : Descending(Buffer) = i ∧ NotEmpty ∧ NotStuffed ⇒ ◇FirstFull)

We can do this because ∃ i ∈ 0 . . MaxDescending : Descending(Buffer) = i is provable from arithmetic, thus

⟨7⟩2. □(\begin{matrix}∃ i ∈ 0 . . MaxDescending : \\ Descending(Buffer) = i) \end{matrix}

by STL4. Thus A ⇒ □B is equivalent to A ⇒ □B ∧ □(∃ i ∈ 0 . . MaxDescending : .....) and then one uses STL5 to compactify the conclusion Thus the instantiations for the Lattice Rule are: ∃ i : H_{i} =^{Δ} ∧ ∃ i ∈ 0 . . MaxDescending : Descending(Buffer) = i ∧ NotEmpty ∧ NotStuffed

which suggests that H_{i} =^{Δ} ∧ i ∈ 0 . . MaxDescending : ∧ Descending(Buffer) = i ∧ NotEmpty ∧ NotStuffed

and G =^{Δ} FirstFull Then we show this using the Lattice Rule. The consequent of the premise, remember, is (H_{c} ⇝ (G ∨ ∃d ∈ S : (c ≻ d) ∧ H_{d})) Here’s the premise

⟨8⟩1.

∧ □[\begin{matrix}∨ ∃ a : CB.push(a) \\ ∨ ∃ k : CB.move(k)]_{Buffer} \end{matrix} ∧ WF_{Buffer}(CB.pop) ∧ WF_{Buffer}(∃ k : CB.move(k)) ∧ i ∈ 0 . . MaxDescending

⇒

□(∧ NotEmpty ∧ NotStuffed ∧ Descending(Buffer) = i) ⇒ ◇(\begin{matrix}∨ FirstFull \\ ∨ ∃ j ∈ 0 . . MaxDescending : ∧ j < i ∧ NotEmpty ∧ NotStuffed ∧ Descending(Buffer) = j ) \end{matrix} This step is justified by an application of WF1 (and simple propositional logic). The substeps consist of the premises of WF1, with the instantiations

N =^{Δ} ∃ a : CB.push(a) ∨ ∃ k : CB.move(k), A =^{Δ} ∃ k : CB.move(k), P =^{Δ} ∧ NotEmpty ∧ NotStuffed ∧ Descending(Buffer) = i

and Q =^{Δ} ∨ FirstFull ∨ ∃ j ∈ 0 . . MaxDescending : ∧ j < i ∧ NotEmpty ∧ NotStuffed ∧ Descending(Buffer) = j )

First, some trivial simplification of the consequent, from

∃ j ∈ 0 . . MaxDescending : j < i ∧ Θ

to ∃ j < i ∧ Θ, for appropriate Θ.

⟨9⟩1.

∧ ∃ j < i : Descending(Buffer) = j ≡ ∃ j ∈ 0 . . MaxDescending : ∧ j < i ∧ Descending(Buffer) = j

∧ ∃ j < i : Descending(Buffer′) = j ≡ ∃ j ∈ 0 . . MaxDescending : ∧ j < i ∧ Descending(Buffer′) = j

Proof: Pretty obvious from arithmetic and predicate logic.

The next step is the first premise of WF1, P ∧ [N]_{f} ⇒ (P′ ∨ Q′)

⟨9⟩2.

∧ NotEmpty ∧ NotStuffed ∧ Descending(Buffer) = i ∧ ∨ ∃ a : CB.push(a) ∨ ∃ k : CB.move(k) ∨ Buffer′ = Buffer

⇒ ∨ ∧ NotEmpty′ ∧ NotStuffed′ ∧ Descending(Buffer′) = i

∨ FirstFull′ ∨ ∃ j ∈ 0 . . MaxDescending : ∧ j < i ∧ NotEmpty′ ∧ NotStuffed′ ∧ Descending(Buffer′) = j The second premise of WF1, P ∧ ⟨N ∧ A⟩_{f} ⇒ Q′

⟨9⟩3.

∧ NotStuffed ∧ NotEmpty ∧ Descending(Buffer) = i ∧ ⟨\begin{matrix}∧ ∨ ∃ a : CB.push(a) ∨ ∃ k : CB.move(k) \\ ∧ ∃ k : CB.move(k)⟩_{Buffer} \end{matrix}

⇒

∨ FirstFull′

∨ ∃ j ∈ 0 . . MaxDescending : ∧ j < i ∧ NotStuffed′ ∧ NotEmpty′ ∧ Descending(Buffer′) = j This reduces to proving

⟨10⟩2.

∧ NotStuffed ∧ NotEmpty ∧ Descending(Buffer) = i ∧ ⟨∃ k : CB.move(k)⟩_{Buffer}

⇒ ∨ FirstFull′ ∨ ∃ j ∈ 0 . . MaxDescending : ∧ j < i ∧ NotStuffed′ ∧ NotEmpty′ ∧ Descending(Buffer′) = j And the third premise of WF1, P ⇒ Enabled ⟨A⟩_{f}

⟨9⟩4.

∧ NotStuffed ∧ NotEmpty ∧ Descending(Buffer) = i

⇒

Enabled⟨∃ k : CB.move(k)⟩_{Buffer} Proof: Follows by predicate logic from definitions.

The proofs of the first two premises involve some arithmetic.

In fact, we can prove

∧ Descending(Buffer) = i ∧ ∃ k : CB.move(k)

⇒

∃ j < i : Descending(Buffer′) = j

which enables us to prove both the first two premises.

Why is this? Let’s go back to the definition Descending(Buffer) =^{Δ} ∑ _{i=1}^{N} (Buffer[i] = ⊥).2^{N −i} Descending(Buffer) =^{Δ} ∑ _{i=1}^{N} (Buffer[i] = ⊥).2^{N −i} So, under a CB.move(k), where 2 ≤ k ≤ N , Buffer[k] = a (say) contributing 0 Buffer[k − 1] = ⊥ ” 2^{N −(k−1)} and Buffer′[k] = ⊥ contributing 2^{N −k} Buffer′[k − 1] = a ” 0 so Descending(Buffer) = Descending(Buffer′) + 2^{N −k}.(2 − 1)

So Descending(Buffer′) < Descending(Buffer) which is what we need I’ll spare you details of the arithmetic, but it’s necessary to have a TLA+ module for the Naturals