1queuelive prophecy3

Example of using a prophecy variable to avoid a quantifier alternation in a liveness proof.

include order


instance nat : unbounded_sequence

module signal(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
    }
}

type id

isolate bar = {

    action send(x:id)

    action recv

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

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

        instance sending : signal(id)
        instance receiving : signal(id)

        before send {
            sending.raise(x);
            queue(tail) := x;
            tail := tail.next;
        }

        before recv {
            require head < tail;
            call receiving.raise(queue(head));
            head := head.next;
        }

To detemine the "work" that neads to be done to receive message X from the queue, we prophecy the index in the queue at the time the message X is sent.

We use the notation (t whenfirst p) which returns the value of term t at the first time that predicate p is true.

In this case, we want to identifiy the value of the tail pointer at the first time the message X is sent, since this is the location in the queue that will hold messge X. The 'work_needed' predicate is tus defined to be the set of queue positions up to the one that will hold X. We do this to avoid using a quantifier to define work_needed as the set of positions up to the least one currently holding X.

To do this proof, we use tactic l2s_auto2. This differs from l2s_auto in that we require that there is always work left to be done only after the work_start event. This work must also satisfy the 'work_end' predicate. The 'work_end' predicate represents the work that actually causes the the desired eventuality to occur (as opposed to work that needs to be done before this, but does not cause the eventuality). In this case work_done is true for queue cells that contain X. The invariant the there is always work to be done satisfying work_end means in this case that there is always a queue cell above the head pointer that contans X, so we can guarantee that the head pointer never skips over X without X being received.

        temporal property
        forall X. ((globally eventually receiving.now)
                   & (eventually sending.now & sending.value = X) ->
                     (eventually receiving.now & receiving.value = X))
        proof {
            tactic skolemize;
            tactic l2s_auto2 with {
                definition work_created(X) = (X < tail)
                definition work_needed(X) = X <= (tail whenfirst (sending.now & sending.value = _X))
                definition work_done(X) = (X < head)
                definition work_end(X) =  queue(X) = _X
                definition work_start = (sending.now & sending.value = _X)
                definition work_progress = receiving.now
            }
            showgoals
        }
    }
} with nat

export bar.send
export bar.recv