Examp2

This is the example from section 3.2 of the paper where we chain liveness lemmas to prove liveness of a cascade of queues.

include order

instance time : 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
    }
}

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 unbounded_queue with time = {

This action sends a message. Since the queue is unbounded, this action always succeeds.

    action send(x:time)

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:time, ok:bool)

    specification {
        var latest : time
        var pending(X:time) : bool

        after init {
            latest := 0;
            pending(X) := false;
        }

        instance sending : signal1(time)
        instance trying : signal
        instance receiving : signal1(time)

        before send {
            require x > latest;
            pending(x) := true;
            latest := x;
            sending.raise(x);   # ghost action to signal a send
        }

        before recv {
            trying.raise;      # ghost action signalling polling of queue
            ok := false;
            if some (y:time) pending(y) minimizing y {
                ok := true;
                x := y;
                pending(x) := false;
                receiving.raise(x);
            }
        }

        invariant pending(X) -> X <= latest

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]
        (globally eventually trying.now)
        ->
        forall X. globally (sending.now & sending.value = X) ->
                           (eventually receiving.now & receiving.value = X)
        proof {
            tactic skolemize;
            tactic l2s_auto4 with {
                definition work_created(X) = pending(X)
                definition work_needed(X) = pending(X) & X <= _X
                definition work_done(X:time) = false
                definition work_end(X:time) = pending(_X)
                definition work_start = ~((sending.now & sending.value = _X) ->
                           (eventually receiving.now & receiving.value = _X))
                definition work_progress = trying.now
            }
            showgoals
        }
    }
}

This isolate represents a cascade of two queues. We want to prove that every message sent on the first queue is eventually received from the second queue.

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

This action polls q1, and if a message is available, it sends it on q2.

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

We need invariants to guarantee the

    invariant forall X. q1.pending(X) -> X > q2.latest
    invariant q2.latest <= q1.latest

This is a system property we want to prove. That is, if we infinitely often poll both q1 and q2, then every message X sent on q1 should eventually be received on q2.

Using the liveness properties of q1 and q2 this property can be proved wthout the use of a ranking. The progress contition (that we eventually receive X from q1) is sufficient to establish the eventuality in one step, assuming liveness of q2.

Notice we use the 'instantiate' tactic to bring the needed lemmas, plugging in the skolem symbol '_X' for X.

    temporal property
    forall X. ((globally eventually q1.trying.now)
               & (globally eventually q2.trying.now)
               -> (globally q1.sending.now & q1.sending.value = X ->
                     (eventually q2.receiving.now & q2.receiving.value = X)))
    proof {
        tactic skolemize;
        instantiate q1.lpq with X = _X;
        instantiate q2.lpq with X = _X;
        tactic ranking with {
            definition work_created = true
            definition work_needed = true
            definition work_invar = eventually (q1.receiving.now & q1.receiving.value = _X)
            definition work_progress = q1.receiving.now & q1.receiving.value = _X
            definition work_helpful = true
        }
        showgoals
    }
} with time

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