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

An unbounded 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 returns the messages at the head of the queue but does not remove it. It returns a success code 'ok' and a value 'x' if 'ok' is true. If the queue is empty, 'ok is false.

    action peek returns (x:id, 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 peek {
            ok := head < tail;
            if ok {
                x := queue(head);
            }
        }

        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 head < tail -> 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 = head < tail -> recv_trying.now
            }
            showgoals
        }

If we keep pulling from the queue, eventually a send will succeed

        temporal property [nb]
        ((globally eventually head < tail -> 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] = head < tail -> 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
        }
    }
}

This isolate represents the system of two queues.

isolate m = {
    instance q1 : bounded_queue
    instance q2 : bounded_queue

Transfer a message from q1 to q2, if possible. First peeks into q1. If there is a message, it sends to q2. If send is successful, the message is remved from q1, else we leave the message in q1.

    instance polling : signal

    action poll = {
        var x : id;
        var ok : bool;
        polling.raise;
        (x,ok) := q1.peek;
        if ok {
            ok := q2.send(x);
            if ok {
                (x,ok) := q1.recv;
            }
        }
    }

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

    temporal property [poll_lemma]
    forall X. (eventually q1.receiving.now & q1.receiving.value = X)
              -> (eventually q2.sending.now & q2.sending.value = X)

    proof {
        tactic skolemize;
        showgoals;
        tactic l2s_auto with {
            definition work_created = false
            definition work_needed = true
            definition work_done = false
            definition work_start = q1.receiving.now & q1.receiving.value = _X
            definition work_progress = false
        }
        showgoals
    }

    temporal property [live]
    forall X.
    (globally eventually q2.head < q2.tail -> q2.recv_trying.now) &
    (globally eventually polling.now)
    & (eventually q1.sending.now & q1.sending.value = X) ->
    (eventually q2.receiving.now & q2.receiving.value = X)
    proof {
        tactic skolemize;
        instantiate fpull;
        instantiate q1.lpq with X = _X;
        instantiate q2.lpq with X = _X;
        instantiate poll_lemma with X = _X;
        tactic l2s with {
            invariant false
        }
        showgoals
    }

}

export m.q1.send
export m.poll
export m.q2.recv