Proving Liveness with TLA

Summary

The TLA Toolbox now has support for proving liveness properties (i.e. that something will eventually happen). I try it out on the Xen vchan protocol. Working on a liveness proof with the TLA+ Toolbox. Table of Contents Background The vchan protocol is used for efficient communication between Xen virtual machines. In 2018, I made a TLA+ specification of vchan: I created a specification of the protocol from the C code, used the model checker (TLC) to test that the protocol worked on small models, and wrote a machine-verified proof of Integrity (that the data received always matched what was sent). I also outlined a proof of Availability (that data sent will eventually arrive, rather than the system deadlocking or going around in circles). But: Disappointingly, we can't actually prove Availability using TLAPS, because currently it understands very little temporal logic However, newer versions of TLAPS (the TLA Proof System) have added proper support for temporal logic, so I decided to take another look. In this post, I'll start with a simple example of proving a liveness property, and then look at the real protocol. If you're not familiar with TLA, you might want to read the earlier post first, though I'll briefly introduce concepts as we meet them here. A simple channel specification We'll start with a simple model of a one-way channel. There is a sender and a receiver, and they have access to a shared buffer of size BufferSize (which is a non-zero natural number): 1 2 CONSTANT BufferSize ASSUME BufferSizeType == BufferSize \in Nat \ {0} The model just keeps track of the total number of bytes sent and received (not the actual data): 1 2 VARIABLES Sent, Got vars == << Sent, Got >> \* For referring to both variables together The amount of data currently in the buffer (BufferUsed) is the difference between these counters, and the free space (BufferFree) is the difference between that and the total buffer size: 1 2 BufferUsed == Sent - Got BufferFree == BufferSize - Buffe...