examples/schorr_waite_with_ghost_monitor.mlw

   1
   2 (** proof of Schorr-Waite algorithm using a ghost monitor
   3
   4 The C code for Schorr-Waite is the following:
   5
   6 typedef struct struct_node {
   7   unsigned int m :1, c :1;
   8   struct struct_node *l, *r;
   9 } * node;
  10
  11 void schorr_waite(node root) {
  12   node t = root;
  13   node p = NULL;
  14   while (p != NULL || (t != NULL && ! t->m)) {
  15     if (t == NULL || t->m) {
  16       if (p->c) { /* pop */
  17         node q = t; t = p; p = p->r; t->r = q;
  18       }
  19       else { /* swing */
  20         node q = t; t = p->r; p->r = p->l; p->l = q; p->c = 1;
  21       }
  22     }
  23     else { /* push */
  24       node q = p; p = t; t = t->l; p->l = q; p->m = 1; p->c = 0;
  25     }
  26   }
  27 }
  28
  29 The informal specification is
  30
  31 - the graph structure induced by pointer `l` and `r` is restored into its original shape
  32 - assuming that initially all the nodes reachable from `root` are unmarked (m is 0) then
  33   at exit all those nodes are marked.
  34 - the nodes initially unreachable from `root` have their mark unchanged
  35
  36 *)
  37
  38 (** Component-as-array memory model, with null pointers *)
  39 module Memory
  40
  41   use int.Int
  42   use option.Option
  43
  44   (** Memory locations *)
  45   type loc
  46
  47   (** null pointer *)
  48   val constant null : loc
  49
  50   (** pointer equality *)
  51   val (=) (l1 l2:loc) : bool
  52     ensures { result <-> l1 = l2 }
  53
  54   type memory = abstract {
  55     mutable left  : loc -> loc;
  56     mutable right : loc -> loc;
  57     mutable mark  : loc -> bool;
  58     mutable color : loc -> bool;
  59   }
  60
  61   predicate update (m1 m2:loc -> 'a) (l:loc) (v:'a) =
  62     m1 l = v /\ forall x. x<>l -> m1 x = m2 x
  63
  64   (** Global instance for memory *)
  65   val heap : memory
  66
  67   (** Getters/setters for pointers *)
  68   val get_l (l:loc) : loc
  69     requires { l <> null }
  70     reads { heap }
  71     ensures { result = heap.left l }
  72   val get_r (l:loc) : loc
  73     requires { l <> null }
  74     reads { heap }
  75     ensures { result = heap.right l }
  76   val get_m (l:loc) : bool
  77     requires { l <> null }
  78     reads { heap }
  79     ensures { result = heap.mark l }
  80   val get_c (l:loc) : bool
  81     requires { l <> null }
  82     reads { heap }
  83     ensures { result = heap.color l  }
  84   val set_l (l:loc) (d:loc) : unit
  85     requires { l <> null }
  86     writes { heap.left }
  87     ensures { update heap.left (old heap.left) l d }
  88   val set_r (l:loc) (d:loc) : unit
  89     requires { l <> null }
  90     writes { heap.right }
  91     ensures { update heap.right (old heap.right) l d }
  92   val set_m (l:loc) (m:bool) : unit
  93     requires { l <> null }
  94     writes { heap.mark }
  95     ensures { update heap.mark (old heap.mark) l m }
  96   val set_c (l:loc) (c:bool) : unit
  97     requires { l <> null }
  98     writes { heap.color }
  99     ensures { update heap.color (old heap.color) l c }
 100
 101 end
 102
 103
 104
 105 (** Define notions about the memory graph *)
 106 module GraphShape
 107
 108   use int.Int
 109   use set.Fset
 110   use Memory
 111
 112   (** Edges *)
 113   predicate edge (m:memory) (x y:loc) =
 114     x <> null /\ (m.left x = y \/ m.right x = y)
 115
 116   (** Paths *)
 117   inductive path memory (x y:loc) =
 118     | path_nil : forall m x. path m x x
 119     | path_cons : forall m x y z. edge m x y /\ path m y z -> path m x z
 120
 121   (** DFS invariant. For technical reason, it must refer to different parts
 122      of the memory at different time. The graph structure is given
 123      via the initial memory `m`, but the coloring is given via the current one `mark`. *)
 124   predicate well_colored_on (graph gray:fset loc) (m:memory) (mark:loc -> bool) =
 125     subset gray graph /\
 126     (forall x. mem x gray -> mark x) /\
 127     (forall x y. mem x graph /\ edge m x y /\ y <> null /\ mark x ->
 128       mem x gray \/ mark y)
 129
 130   (** Unchanged_structure only concerns the graph shape, not the marks *)
 131   predicate unchanged_structure (m1 m2:memory) =
 132     forall x. x <> null ->
 133       m2.left x = m1.left x /\ m2.right x = m1.right x
 134
 135 end
 136
 137
 138
 139
 140 module SchorrWaite
 141
 142   use int.Int
 143   use set.Fset
 144   use ref.Ref
 145   use Memory
 146   use GraphShape
 147
 148   let schorr_waite (root : loc) (ghost graph : fset loc) : unit
 149     requires { (** Root belong to graph *)
 150       mem root graph }
 151     requires { (** Graph is closed by following edges *)
 152       forall l. mem l graph /\ l <> null ->
 153         mem (heap.left l) graph /\ mem (heap.right l) graph }
 154     writes { heap }
 155     requires { (** The graph starts fully unmarked. *)
 156       forall x. mem x graph -> not heap.mark x }
 157     ensures  { (** The graph structure is left unchanged. *)
 158       unchanged_structure (old heap) heap }
 159     ensures  { (** Every non-null location reachable from the root is marked. *)
 160       forall x. path (old heap) root x /\ x <> null ->
 161         heap.mark x }
 162     ensures { (** Every other location is left with its previous marking. *)
 163       forall x. not path (old heap) root x /\ x <> null ->
 164         heap.mark x = (old heap.mark) x }
 165
 166 =
 167   (* Non-memory internal state *)
 168   let pc = ref 0 in
 169   let t = ref null in
 170   let p = ref null in
 171
 172   (** step function for low-level Schorr-Waite algorithm
 173   L0:
 174   node t = root;
 175   node p = NULL;
 176   while L1: (p != NULL || (t != NULL && ! t->m)) {
 177     if (t == NULL || t->m) {
 178       if (p->c) { /* Pop */
 179         node q = t; t = p; p = p->r; t->r = q;
 180       }
 181       else { /* Swing */
 182         node q = t; t = p->r; p->r = p->l; p->l = q; p->c = 1;
 183       }
 184     }
 185     else { /* Push */
 186       node q = p; p = t; t = t->l; p->l = q; p->m = 1; p->c = 0;
 187     }
 188   }
 189   L2:
 190   *)
 191   let step () : unit
 192     requires { 0 <= !pc < 2 }
 193     writes   { pc,t,p,heap }
 194     ensures  { old (!pc = 0) -> !pc = 1 /\ !t = root /\ !p = null /\ heap = old heap }
 195     ensures  { old (!pc = 1 /\ not(!p <> null \/ (!t <> null /\ not heap.mark !t))) ->
 196       !pc = 2 /\ !t = old !t /\ !p = old !p /\ heap = old heap }
 197     ensures  { old (!pc = 1 /\ (!p <> null \/ (!t <> null /\ not heap.mark !t))) ->
 198       !pc = 1 /\
 199       ( old ((!t = null \/ heap.mark !t) /\ heap.color !p) -> (* Pop *)
 200          (* q = t *) let q = old !t in
 201          (* t = p *) !t = old !p /\
 202          (* p = p->r *) !p = old (heap.right !p) /\
 203          (* t->r = q (t is old p here!) *) update heap.right (old heap.right) (old !p) q /\
 204          heap.left = old (heap.left) /\
 205          heap.mark = old (heap.mark) /\
 206          heap.color = old (heap.color) )
 207        /\
 208        ( old ((!t = null \/ heap.mark !t) /\ not heap.color !p) -> (* Swing *)
 209          (* q = t *) let q = old !t in
 210          (* p unchanged *) !p = old !p /\
 211          (* t = p->r *) !t = old (heap.right !p) /\
 212          (* p->r = p->l *) update heap.right (old heap.right) !p (old (heap.left !p)) /\
 213          (* p->l = q *) update heap.left (old heap.left) !p q /\
 214          (* p->c = 1 *) update heap.color (old heap.color) !p true /\
 215          heap.mark = old (heap.mark) )
 216        /\
 217        ( old (not (!t = null \/ heap.mark !t)) -> (* Push *)
 218          (* q = p *) let q = old !p in
 219          (* p = t *) !p = old !t /\
 220          (* t = t -> l *) !t = old (heap.left !t) /\
 221          (* p->l = q (p is old t here!) *) update heap.left (old heap.left) (old !t) q /\
 222          (* p->m = 1 *) update heap.mark (old heap.mark) !p true /\
 223          (* p->c = 0 *) update heap.color (old heap.color) !p false /\
 224          heap.right = old (heap.right) )
 225       }
 226   =
 227     if !pc = 0 then (t := root; p := null; pc := 1)
 228     else if !pc = 1 then
 229       if !p <> null || (!t <> null && not(get_m(!t)))
 230       then begin
 231         if !t = null || get_m(!t) then
 232         if get_c !p then (* Pop *)
 233           let q = !t in t := !p;  p := get_r !p; set_r !t q; pc := 1
 234         else (* Swing *)
 235           let q = !t in t := get_r !p; set_r !p (get_l !p); set_l !p q; set_c !p true; pc := 1
 236         else (* Push *)
 237           let q = !p in p := !t; t := get_l !t; set_l !p q; set_m !p true; set_c !p false; pc := 1
 238        end
 239       else pc := 2
 240     else absurd
 241   in
 242   let ghost initial_heap = pure {heap} in (* Copy of initial memory *)
 243   let rec recursive_monitor (ghost gray_nodes: fset loc) : unit
 244       requires { !pc = 1 }
 245       requires { mem !t graph }
 246       requires { (* assume DFS invariant *)
 247         well_colored_on graph gray_nodes initial_heap heap.mark }
 248       requires { (* Non-marked nodes have unchanged structure with respect
 249                     to the initial one *)
 250         forall x. x <> null /\ not heap.mark x ->
 251           heap.left x = initial_heap.left x /\ heap.right x = initial_heap.right x }
 252
 253       ensures { !pc = 1 }
 254       ensures { !t = old !t /\ !p = old !p }
 255       ensures { (* Pointer buffer is overall left unchanged *)
 256         unchanged_structure (old heap) heap }
 257       ensures { (* Maintain DFS invariant *)
 258         well_colored_on graph gray_nodes initial_heap heap.mark }
 259       ensures { (* The top node get marked *)
 260         !t <> null -> heap.mark !t }
 261       ensures { (* May not mark unreachable nodes,
 262                    neither change marked nodes. *)
 263         forall x. x <> null ->
 264           not path initial_heap !t x \/ old heap.mark x ->
 265           heap.mark x = (old heap.mark) x /\
 266           heap.color x = (old heap.color) x
 267       }
 268       (* Terminates because there is a finite number of 'grayable' nodes. *)
 269       variant { cardinal graph - cardinal gray_nodes }
 270     = if !t = null || get_m !t then () else
 271       let ghost new_gray = add !t gray_nodes in
 272       step (); (* Push *)
 273       recursive_monitor new_gray; (* Traverse the left child *)
 274       step (); (* Swing *)
 275       recursive_monitor new_gray; (* Traverse the right child *)
 276       step () (* Pop *)
 277     in
 278     step (); (* Initialize *)
 279     recursive_monitor empty;
 280     step (); (* Exit. *)
 281     assert { !pc = 2 };
 282     (* Need induction to recover path-based specification. *)
 283     assert { forall x y. ([@induction] path initial_heap x y) ->
 284         x <> null /\ y <> null /\ mem x graph /\ heap.mark x ->
 285         heap.mark y }
 286
 287 end