Examp4

This is the example from section 3.3 of the paper, using a stable scehduler to prove the cascaded queues without using lemmas when the second queue can be full.

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)

Test if the queue is full

    action full returns (x: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);
            }
        }

        before full {
            if ~exists X. pending(X) {
                x := false;
            }
        }

        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

    instance polling : signal

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

    action poll = {
        var x : time;
        var ok : bool;
        polling.raise;
        if ~q2.full {
            (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.

    temporal property
    forall X. ((globally eventually polling.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;
        showgoals;
        tactic ranking with {
            definition work_created[1](X) = q1.pending(X)
            definition work_needed[1](X) = q1.pending(X) & X <= _X
            definition work_invar[1] = q1.pending(_X) | q2.pending(_X)
            definition work_progress[1] = polling.now
            definition work_helpful[1] = ~exists X. q2.pending(X)
            definition work_created[2](X) = q1.pending(X) | q2.pending(X)
            definition work_needed[2](X) = (q1.pending(X) | q2.pending(X)) & X <= _X
            definition work_invar[2] = q1.pending(_X) | q2.pending(_X)
            definition work_progress[2] = q2.trying.now
            definition work_helpful[2] = exists X. q2.pending(X)
        }
        showgoals
    }
} with time

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