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 }
... continue reading