Liveness

In this example, we have two unbounded queues. Commands are sent on queue q1. Periodically, commands are read from q1 and responses are sent on q2. We prove that a response to every command is eventually received at the output of q2.

The proof is done compositionally. That is, we prove that q1 znd q2 are live in isolation. That is, for each queue, if the output is polled infinitely often, then every message sent is eventually received. Then we combine liveness of q1 and q2 to prove liveness of the system.

include order

instance nat : unbounded_sequence

A signal with zero parameters

module signal = {
    action raise

    specification {
        relation now
        after init { now := false; }
        before raise {
            now := true;
            now := false;
        }
        invariant ~now
    }
}

A signal with one parameter

module signal1(data) = {
    action raise(val:data)

    specification {
        relation now
        var value : data
        after init { now := false; }
        before raise {
            value := val;
            now := true;
            now := false;
        }
        invariant ~now
    }
}

The type of messages (we can also think of the messages as message ids)

type id

A bounded queue module, with liveness property. Notice this module is an isolate and depends on the theory of the index type 'nat'.

module isolate bounded_queue with nat = {

This action sends a message. Since the queue is unbounded, returns ok=true if action succeeds.

    action send(x:id) returns (ok:bool)

This action receives a message. It returns a success code 'ok' and a value 'x' if 'ok' is true. If the queue is empty, 'ok is false.

    action recv returns (x:id, ok:bool)

    specification {
        var head : nat
        var tail : nat
        var queue(X:nat) : id

        after init {
            head := 0;
            tail := 0;
        }

        instance send_trying : signal
        instance sending : signal1(id)
        instance recv_trying : signal
        instance receiving : signal1(id)

        before send {
            send_trying.raise;
            if tail = head { # guarantee room to send if queue is empty
                ok := true;
            }
            if ok {
                queue(tail) := x;
                tail := tail.next;
                sending.raise(x);   # ghost action to signal a send
            }
        }

        before recv {
            recv_trying.raise;      # ghost action signalling polling of queue
            ok := head < tail;
            if ok {
                receiving.raise(queue(head));   # ghost action to signal a receive
                x := queue(head);
                head := head.next;
            }
        }

This is the liveness property of the queue. It says that if messages X is eventually sent and if the queue is polled infinitely often, then message X is eventually received.

        temporal property [lpq]
        forall X. ((globally eventually recv_trying.now)
                   & (eventually sending.now & sending.value = X) ->
                     (eventually receiving.now & receiving.value = X))
        proof {
            tactic skolemize;
            tactic l2s_auto with {
                definition work_created(X) = (X < tail)
                definition work_needed(X) = ~exists Y. Y < X & queue(Y) = _X
                definition work_done(X) = (X < head)
                definition work_start = (sending.now & sending.value = _X)
                definition work_progress = recv_trying.now
            }
            showgoals
        }

If we keep pulling from the queue, eventually a send will succeed. That is, the queue cannot keep blocking sends forever if we infinitely often poll it.

This is an example of a two-phase eventuality proof. The first phase empties the queue. This guarantees progress when we received from the queue. The second phase sends a message on an empty queue. This phase guarantees progress when we send and message, but only if phase 1 is complete (i.e., if the queue is empty). For each phase, we define work_created, work_needed, work_done and work_progress.

The phases are ordered lexically by their names. That is, phase 2 starts when phase 1 is complete.

        temporal property [nb]
        ((globally eventually recv_trying.now)
        & (globally eventually send_trying.now)
        -> (globally eventually sending.now))
        proof {
            tactic skolemize;
            tactic l2s_auto with {
                definition work_start = ($l2s_g. ~sending.now)
                definition work_created[1](X) = (X <= tail)
                definition work_needed[1](X) = (X <= tail)
                definition work_done[1](X) = (X <= head)
                definition work_progress[1] = recv_trying.now
                definition work_created[2] = true
                definition work_needed[2] = true
                definition work_done[2] = false
                definition work_progress[2] = send_trying.now
            }
            showgoals
        }
    }
}

instance q : bounded_queue
export q.send
export q.recv