Wiki Agenda Contact Version française

Schorr-Waite algorithm, proof using a ghost monitor

Schorr-Waite's graph marking algorithm, an alternative proof using a ghost monitor


Authors: Martin Clochard / Claude Marché

Topics: Ghost code / Graph Algorithms / Pointer Programs

Tools: Why3

see also the index (by topic, by tool, by reference, by year)


proof of Schorr-Waite algorithm using a ghost monitor

The C code for Schorr-Waite is the following:

typedef struct struct_node { unsigned int m :1, c :1; struct struct_node *l, *r; } * node;

void schorr_waite(node root) { node t = root; node p = NULL; while (p != NULL || (t != NULL && ! t->m)) { if (t == NULL || t->m) { if (p->c) { /* pop */ node q = t; t = p; p = p->r; t->r = q; } else { /* swing */ node q = t; t = p->r; p->r = p->l; p->l = q; p->c = 1; } } else { /* push */ node q = p; p = t; t = t->l; p->l = q; p->m = 1; p->c = 0; } } }

The informal specification is

- the graph structure induced by pointer l and r is restored into its original shape - assuming that initially all the nodes reachable from root are unmarked (m is 0) then at exit all those nodes are marked. - the nodes initially unreachable from root have their mark unchanged

module Memory

Component-as-array memory model, with null pointers

  use int.Int
  use option.Option

  type loc

Memory locations

  val constant null : loc

null pointer

  val (=) (l1 l2:loc) : bool
    ensures { result <-> l1 = l2 }

pointer equality

  type memory = abstract {
    mutable left  : loc -> loc;
    mutable right : loc -> loc;
    mutable mark  : loc -> bool;
    mutable color : loc -> bool;
  }

  predicate update (m1 m2:loc -> 'a) (l:loc) (v:'a) =
    m1 l = v /\ forall x. x<>l -> m1 x = m2 x

  val heap : memory

Global instance for memory

  val get_l (l:loc) : loc
    requires { l <> null }
    reads { heap }
    ensures { result = heap.left l }
  val get_r (l:loc) : loc
    requires { l <> null }
    reads { heap }
    ensures { result = heap.right l }
  val get_m (l:loc) : bool
    requires { l <> null }
    reads { heap }
    ensures { result = heap.mark l }
  val get_c (l:loc) : bool
    requires { l <> null }
    reads { heap }
    ensures { result = heap.color l  }
  val set_l (l:loc) (d:loc) : unit
    requires { l <> null }
    writes { heap.left }
    ensures { update heap.left (old heap.left) l d }
  val set_r (l:loc) (d:loc) : unit
    requires { l <> null }
    writes { heap.right }
    ensures { update heap.right (old heap.right) l d }
  val set_m (l:loc) (m:bool) : unit
    requires { l <> null }
    writes { heap.mark }
    ensures { update heap.mark (old heap.mark) l m }
  val set_c (l:loc) (c:bool) : unit
    requires { l <> null }
    writes { heap.color }
    ensures { update heap.color (old heap.color) l c }

Getters/setters for pointers

end

module GraphShape

Define notions about the memory graph

  use int.Int
  use set.Fset
  use Memory

  predicate edge (m:memory) (x y:loc) =
    x <> null /\ (m.left x = y \/ m.right x = y)

Edges

  inductive path memory (x y:loc) =
    | path_nil : forall m x. path m x x
    | path_cons : forall m x y z. edge m x y /\ path m y z -> path m x z

Paths

  predicate well_colored_on (graph gray:fset loc) (m:memory) (mark:loc -> bool) =
    subset gray graph /\
    (forall x. mem x gray -> mark x) /\
    (forall x y. mem x graph /\ edge m x y /\ y <> null /\ mark x ->
      mem x gray \/ mark y)

DFS invariant. For technical reason, it must refer to different parts of the memory at different time. The graph structure is given via the initial memory m, but the coloring is given via the current one mark.

  predicate unchanged_structure (m1 m2:memory) =
    forall x. x <> null ->
      m2.left x = m1.left x /\ m2.right x = m1.right x

Unchanged_structure only concerns the graph shape, not the marks

end

module SchorrWaite

  use int.Int
  use set.Fset
  use ref.Ref
  use Memory
  use GraphShape

  let schorr_waite (root : loc) (ghost graph : fset loc) : unit
    requires {

Root belong to graph

      mem root graph }
    requires {

Graph is closed by following edges

      forall l. mem l graph /\ l <> null ->
        mem (heap.left l) graph /\ mem (heap.right l) graph }
    writes { heap }
    requires {

The graph starts fully unmarked.

      forall x. mem x graph -> not heap.mark x }
    ensures  {

The graph structure is left unchanged.

      unchanged_structure (old heap) heap }
    ensures  {

Every non-null location reachable from the root is marked.

      forall x. path (old heap) root x /\ x <> null ->
        heap.mark x }
    ensures {

Every other location is left with its previous marking.

      forall x. not path (old heap) root x /\ x <> null ->
        heap.mark x = (old heap.mark) x }

=
  (* Non-memory internal state *)
  let pc = ref 0 in
  let t = ref null in
  let p = ref null in

  let step () : unit
    requires { 0 <= !pc < 2 }
    writes   { pc,t,p,heap }
    ensures  { old (!pc = 0) -> !pc = 1 /\ !t = root /\ !p = null /\ heap = old heap }
    ensures  { old (!pc = 1 /\ not(!p <> null \/ (!t <> null /\ not heap.mark !t))) ->
      !pc = 2 /\ !t = old !t /\ !p = old !p /\ heap = old heap }
    ensures  { old (!pc = 1 /\ (!p <> null \/ (!t <> null /\ not heap.mark !t))) ->
      !pc = 1 /\
      ( old ((!t = null \/ heap.mark !t) /\ heap.color !p) -> (* Pop *)
         (* q = t *) let q = old !t in
         (* t = p *) !t = old !p /\
         (* p = p->r *) !p = old (heap.right !p) /\
         (* t->r = q (t is old p here!) *) update heap.right (old heap.right) (old !p) q /\
         heap.left = old (heap.left) /\
         heap.mark = old (heap.mark) /\
         heap.color = old (heap.color) )
       /\
       ( old ((!t = null \/ heap.mark !t) /\ not heap.color !p) -> (* Swing *)
         (* q = t *) let q = old !t in
         (* p unchanged *) !p = old !p /\
         (* t = p->r *) !t = old (heap.right !p) /\
         (* p->r = p->l *) update heap.right (old heap.right) !p (old (heap.left !p)) /\
         (* p->l = q *) update heap.left (old heap.left) !p q /\
         (* p->c = 1 *) update heap.color (old heap.color) !p true /\
         heap.mark = old (heap.mark) )
       /\
       ( old (not (!t = null \/ heap.mark !t)) -> (* Push *)
         (* q = p *) let q = old !p in
         (* p = t *) !p = old !t /\
         (* t = t -> l *) !t = old (heap.left !t) /\
         (* p->l = q (p is old t here!) *) update heap.left (old heap.left) (old !t) q /\
         (* p->m = 1 *) update heap.mark (old heap.mark) !p true /\
         (* p->c = 0 *) update heap.color (old heap.color) !p false /\
         heap.right = old (heap.right) )
      }
  =
    if !pc = 0 then (t := root; p := null; pc := 1)
    else if !pc = 1 then
      if !p <> null || (!t <> null && not(get_m(!t)))
      then begin
        if !t = null || get_m(!t) then
        if get_c !p then (* Pop *)
          let q = !t in t := !p;  p := get_r !p; set_r !t q; pc := 1
        else (* Swing *)
          let q = !t in t := get_r !p; set_r !p (get_l !p); set_l !p q; set_c !p true; pc := 1
        else (* Push *)
          let q = !p in p := !t; t := get_l !t; set_l !p q; set_m !p true; set_c !p false; pc := 1
       end
      else pc := 2
    else absurd
  in
  let ghost initial_heap = pure {heap} in (* Copy of initial memory *)
  let rec recursive_monitor (ghost gray_nodes: fset loc) : unit
      requires { !pc = 1 }
      requires { mem !t graph }
      requires { (* assume DFS invariant *)
        well_colored_on graph gray_nodes initial_heap heap.mark }
      requires { (* Non-marked nodes have unchanged structure with respect
                    to the initial one *)
        forall x. x <> null /\ not heap.mark x ->
          heap.left x = initial_heap.left x /\ heap.right x = initial_heap.right x }

step function for low-level Schorr-Waite algorithm L0: node t = root; node p = NULL; while L1: (p != NULL || (t != NULL && ! t->m)) { if (t == NULL || t->m) { if (p->c) { /* Pop */ node q = t; t = p; p = p->r; t->r = q; } else { /* Swing */ node q = t; t = p->r; p->r = p->l; p->l = q; p->c = 1; } } else { /* Push */ node q = p; p = t; t = t->l; p->l = q; p->m = 1; p->c = 0; } } L2:

      ensures { !pc = 1 }
      ensures { !t = old !t /\ !p = old !p }
      ensures { (* Pointer buffer is overall left unchanged *)
        unchanged_structure (old heap) heap }
      ensures { (* Maintain DFS invariant *)
        well_colored_on graph gray_nodes initial_heap heap.mark }
      ensures { (* The top node get marked *)
        !t <> null -> heap.mark !t }
      ensures { (* May not mark unreachable nodes,
                   neither change marked nodes. *)
        forall x. x <> null ->
          not path initial_heap !t x \/ old heap.mark x ->
          heap.mark x = (old heap.mark) x /\
          heap.color x = (old heap.color) x
      }
      (* Terminates because there is a finite number of 'grayable' nodes. *)
      variant { cardinal graph - cardinal gray_nodes }
    = if !t = null || get_m !t then () else
      let ghost new_gray = add !t gray_nodes in
      step (); (* Push *)
      recursive_monitor new_gray; (* Traverse the left child *)
      step (); (* Swing *)
      recursive_monitor new_gray; (* Traverse the right child *)
      step () (* Pop *)
    in
    step (); (* Initialize *)
    recursive_monitor empty;
    step (); (* Exit. *)
    assert { !pc = 2 };
    (* Need induction to recover path-based specification. *)
    assert { forall x y. ([@induction] path initial_heap x y) ->
        x <> null /\ y <> null /\ mem x graph /\ heap.mark x ->
        heap.mark y }

end

download ZIP archive

Why3 Proof Results for Project "schorr_waite_with_ghost_monitor"

Theory "schorr_waite_with_ghost_monitor.SchorrWaite": fully verified

ObligationsAlt-Ergo 2.2.0CVC4 1.6
VC for schorr_waite------
split_goal_right
postcondition---0.04
postcondition---0.03
postcondition---0.04
precondition---0.06
precondition---0.03
precondition---0.04
precondition---0.03
precondition0.01---
postcondition---0.03
postcondition0.01---
postcondition---0.06
precondition0.01---
precondition---0.04
precondition---0.04
precondition---0.06
precondition0.00---
postcondition---0.03
postcondition---0.06
postcondition---0.05
precondition---0.03
precondition---0.06
precondition---0.04
precondition0.01---
postcondition0.01---
postcondition---0.05
postcondition---0.05
postcondition---0.06
postcondition---0.02
postcondition---0.02
unreachable point---0.04
precondition---0.06
postcondition---0.09
postcondition---0.03
postcondition0.01---
postcondition0.01---
postcondition0.01---
postcondition0.10---
precondition---0.10
variant decrease---0.09
precondition---0.04
precondition---0.05
precondition0.02---
precondition---0.12
precondition---0.02
variant decrease---0.08
precondition---0.06
precondition---0.05
precondition---0.06
precondition---0.05
precondition---0.03
postcondition---0.06
postcondition---0.10
postcondition---0.20
postcondition---0.39
postcondition---0.08
postcondition0.16---
precondition0.01---
precondition---0.06
precondition---0.09
precondition---0.06
precondition---0.03
precondition---0.02
assertion---0.04
assertion------
induction_pr
assertion---0.05
assertion---0.10
postcondition---0.04
postcondition---0.04
postcondition---0.05