Graph Marking (Quantified Permissions)
A graph marking algorithm (in the spirit of mark-and-sweep garbage collectors). Note that the example is supposed to yield 1 verification error (the encoding of a false reachability check).
field left: Ref
field right: Ref
field is_marked: Bool
/* Automatically chosen triggers are not always ideal, using hand-picked triggers can improve
* performance noticeably, as witnessed by this example.
*/
define INV(nodes)
!(null in nodes)
&& (forall n: Ref :: n in nodes ==> acc(n.left))
&& (forall n: Ref :: n in nodes ==> acc(n.right))
&& (forall n: Ref :: n in nodes ==> acc(n.is_marked))
&& (forall n: Ref :: {n.left in nodes}{n in nodes, n.left}
n in nodes && n.left != null ==> n.left in nodes)
&& (forall n: Ref :: {n.right in nodes}{n in nodes, n.right}
n in nodes && n.right != null ==> n.right in nodes)
method trav_rec(nodes: Set[Ref], node: Ref)
requires node in nodes && INV(nodes)
requires !node.is_marked
ensures node in nodes && INV(nodes)
/* We do not unmark nodes. This allows us to prove that the current node will be marked. */
ensures forall n: Ref :: {n in nodes, n.is_marked} n in nodes ==> (old(n.is_marked) ==> n.is_marked)
ensures node.is_marked
/* The nodes are not being modified. */
ensures forall n: Ref :: {n in nodes, n.left} n in nodes ==> (n.left == old(n.left))
ensures forall n: Ref :: {n in nodes, n.right} n in nodes ==> (n.right == old(n.right))
/* Propagation of the marker. */
ensures forall n: Ref :: {n in nodes, n.is_marked}{n in nodes, n.left.is_marked}
n in nodes ==> (old(!n.is_marked) && n.is_marked ==> (n.left == null || n.left.is_marked))
ensures forall n: Ref :: {n in nodes, n.is_marked}{n in nodes, n.right.is_marked}
n in nodes ==> (old(!n.is_marked) && n.is_marked ==> (n.right == null || n.right.is_marked))
{
node.is_marked := true
if (node.left != null && !node.left.is_marked) {
trav_rec(nodes, node.left)
}
if (node.right != null && !node.right.is_marked) {
trav_rec(nodes, node.right)
}
}
method client_success() {
var a: Ref; a := new(*); a.is_marked := false
var b: Ref; b := new(*); b.is_marked := false
a.left := b; a.right := null
b.left := null; b.right := a
var nodes: Set[Ref] := Set(a, b)
assert forall n: Ref :: n in nodes ==> !n.is_marked
trav_rec(nodes, a)
assert forall n: Ref :: n in nodes ==> n.is_marked
}
method client_failure() {
var a: Ref; a := new(*); a.is_marked := false
var b: Ref; b := new(*); b.is_marked := false
a.left := a; a.right := a;
b.left := a; b.right := a;
var nodes: Set[Ref] := Set(a, b)
assert forall n: Ref :: n in nodes ==> !n.is_marked
trav_rec(nodes, a)
/* The assertion is expected to fail because b is in nodes, but b is not reachable from a */
assert forall n: Ref :: n in nodes ==> n.is_marked
}