examples/schorr_waite.mlw

   1
   2 (** Schorr-Waite algorithm
   3
   4     The Schorr-Waite algorithm is the first mountain that any
   5     formalism for pointer aliasing should climb.
   6                                       -- Richard Bornat, 2000
   7
   8   Author: Mário Pereira (UBI, then Université Paris Sud)
   9
  10   The code, specification, and invariants below follow those of
  11   the following two proofs:
  12
  13   - Thierry Hubert and Claude Marché, using Caduceus and Coq
  14
  15     A case study of C source code verification: the Schorr-Waite algorithm.
  16     SEFM 2005. http://www.lri.fr/~marche/hubert05sefm.ps
  17
  18   - Rustan Leino, using Dafny
  19
  20     Dafny: An Automatic Program Verifier for Functional Correctness.
  21     LPAR-16.
  22     http://research.microsoft.com/en-us/um/people/leino/papers/krml203.pdf
  23 *)
  24
  25 module SchorrWaite
  26
  27   use seq.Seq
  28   use map.Map
  29   use ref.Ref
  30   use int.Int
  31   use list.List
  32   use list.Length
  33   use list.Append
  34   use set.Fset as S
  35
  36   (** Why3 has no support for arbitrary pointers,
  37       so we introduce a small component-as-array memory model *)
  38
  39   (** the type of pointers and the null pointer *)
  40   type loc
  41   val constant null: loc
  42
  43   val (=) (a b: loc) : bool
  44     ensures { result = (a = b) }
  45
  46   (** each (non-null) location holds four fields: two Boolean marks m and c
  47       and two pointers left and right *)
  48   val m: ref (map loc bool)
  49   val c: ref (map loc bool)
  50   val left: ref (map loc loc)
  51   val right: ref (map loc loc)
  52
  53   val get_left (p: loc) : loc
  54     requires { p <> null }
  55     ensures  { result = !left[p] }
  56
  57   val set_left (p: loc) (v: loc) : unit
  58     requires { p <> null }
  59     writes   { left }
  60     ensures  { !left = set (old !left) p v }
  61
  62   val get_right (p: loc) : loc
  63     requires { p <> null }
  64     ensures  { result = !right[p] }
  65
  66   val set_right (p: loc) (v: loc) : unit
  67     requires { p <> null }
  68     writes   { right }
  69     ensures  { !right = set (old !right) p v }
  70
  71   val get_m (p: loc) : bool
  72     requires { p <> null }
  73     ensures  { result = !m[p] }
  74
  75   val set_m (p: loc) (v: bool) : unit
  76     requires { p <> null }
  77     writes   { m }
  78     ensures  { !m = set (old !m) p v }
  79
  80   val get_c (p: loc) : bool
  81     requires { p <> null }
  82     ensures  { result = !c[p] }
  83
  84   val set_c (p: loc) (v: bool) : unit
  85     requires { p <> null }
  86     writes   { c }
  87     ensures  { !c = set (old !c) p v }
  88
  89   (** for the purpose of the proof, we add a fifth, ghost, field,
  90       which records the path from the root (when relevant) *)
  91   val ghost path_from_root : ref (map loc (list loc))
  92
  93   val ghost get_path_from_root (p : loc) : list loc
  94     ensures  { result = !path_from_root[p] }
  95
  96   val ghost set_path_from_root (p: loc) (l : list loc) : unit
  97     requires { p <> null }
  98     writes   { path_from_root }
  99     ensures  { !path_from_root = set (old !path_from_root) p l }
 100
 101   (** Stack of nodes, from the root to the current location, in
 102       reverse order (i.e. the current location is the first element
 103       in the stack) *)
 104
 105   type stacknodes = Seq.seq loc
 106
 107   predicate not_in_stack (n: loc) (s: stacknodes) =
 108     forall i: int. 0 <= i < Seq.length s -> n <> Seq.get s i
 109
 110   let ghost tl_stackNodes (stack: stacknodes) : stacknodes
 111     requires { Seq.length stack > 0 }
 112     ensures  { result = stack[1..] }
 113     ensures  { forall n. not_in_stack n stack -> not_in_stack n result }
 114   = stack[1..]
 115
 116   (** two lemmas about stacks *)
 117
 118   let lemma cons_not_in (s: stacknodes) (n t: loc)
 119     requires { not_in_stack n (cons t s) }
 120     ensures  { not_in_stack n s }
 121   =
 122     assert { forall i: int. 0 <= i < Seq.length s ->
 123              Seq.get s i = Seq.get (cons t s) (i+1) }
 124
 125   let lemma tl_cons (s1 s2: stacknodes) (p: loc)
 126     requires { Seq.length s2 > 0 }
 127     requires { s1 = s2[1..] }
 128     requires { p = Seq.get s2 0 }
 129     ensures  { s2 = cons p s1 }
 130   = assert { Seq.(==) s2 (cons p s1) }
 131
 132   function last (s: stacknodes) : loc =
 133     Seq.get s (Seq.length s - 1)
 134
 135   predicate distinct (s: stacknodes) =
 136     forall i j. 0 <= i < Seq.length s -> 0 <= j < Seq.length s -> i <> j ->
 137     Seq.get s i <> Seq.get s j
 138
 139   (** Paths *)
 140
 141   predicate edge (x y : loc) (left right : map loc loc) =
 142     x <> null /\ (left[x] = y \/ right[x] = y)
 143
 144   inductive path (left right : map loc loc) (x y : loc) (p : list loc) =
 145   | path_nil   : forall x : loc, l r : map loc loc. path l r x x Nil
 146   | path_cons  : forall x y z : loc,
 147                  l r : (map loc loc),
 148                  p : list loc.
 149                  edge x z l r -> path l r z y p ->
 150                  path l r x y (Cons x p)
 151
 152   let rec lemma trans_path (x y z : loc) (l r : map loc loc) (p1 p2 : list loc)
 153     variant  { length p1 }
 154     requires { path l r x y p1 }
 155     requires { path l r y z p2 }
 156     ensures  { path l r x z (p1 ++ p2) }
 157   = match p1 with
 158     | Cons _ (Cons b _ as p') -> trans_path b y z l r p' p2
 159     | _                       -> ()
 160     end
 161
 162   lemma path_edge : forall x y : loc, left right : map loc loc.
 163     edge x y left right -> path left right x y (Cons x Nil)
 164
 165   lemma path_edge_cons:
 166     forall n x y : loc, left right : map loc loc, pth : list loc.
 167     path left right n x pth -> edge x y left right ->
 168     path left right n y (pth ++ (Cons x Nil))
 169
 170   predicate reachable (left right: map loc loc) (x y : loc) =
 171     exists p : list loc. path left right x y p
 172
 173   (** Schorr-Waite algorithm *)
 174
 175   let schorr_waite (root: loc) (ghost graph : S.fset loc) : unit
 176     requires { root <> null /\ S.mem root graph }
 177     (* graph is closed under left and right *)
 178     requires { forall n : loc. S.mem n graph ->
 179                n <> null /\
 180                (!left[n] = null \/ S.mem !left[n] graph) /\
 181                (!right[n] = null \/ S.mem !right[n] graph) }
 182     (* graph starts with nothing marked *)
 183     requires { forall x : loc. S.mem x graph -> not !m[x] }
 184     (* the structure of the graph is not changed *)
 185     ensures  { forall n : loc. S.mem n graph ->
 186                (old !left)[n] = !left[n] /\
 187                (old !right)[n] = !right[n] }
 188     (* all the non-null vertices reachable from root
 189        are marked at the end of the algorithm, and only these *)
 190     ensures  { forall n : loc. S.mem n graph -> !m[n] ->
 191                reachable (old !left) (old !right) root n }
 192     ensures  { !m[root] }
 193     ensures  { forall n : loc. S.mem n graph -> !m[n] ->
 194           (forall ch : loc. edge n ch !left !right -> ch <> null -> !m[ch]) }
 195   = let t = ref root in
 196     let p = ref null in
 197     let ghost stackNodes = ref Seq.empty in
 198     let ghost pth = ref Nil in
 199     ghost set_path_from_root !t !pth;
 200     let ghost unmarked_nodes = ref graph in
 201     let ghost c_false_nodes = ref graph in
 202     while !p <> null || (!t <> null && not get_m !t) do
 203       invariant { forall n. S.mem n graph -> not_in_stack n !stackNodes \/
 204                   exists i : int. Seq.get !stackNodes i = n }
 205       invariant { not_in_stack null !stackNodes }
 206       invariant { Seq.length !stackNodes = 0 <-> !p = null }
 207       invariant { !p <> null -> S.mem !p graph }
 208       invariant { Seq.length !stackNodes <> 0 -> Seq.get !stackNodes 0 = !p }
 209       invariant { forall n : loc. S.mem n graph -> not !m[n] ->
 210                   S.mem n !unmarked_nodes }
 211       invariant { forall n : loc. S.mem n graph -> not !c[n] ->
 212                   S.mem n !c_false_nodes }
 213       invariant { forall i. 0 <= i < Seq.length !stackNodes ->
 214                   S.mem (Seq.get !stackNodes i) graph }
 215       invariant { forall i.  0 <= i < Seq.length !stackNodes - 1 ->
 216                   let p1 = Seq.get !stackNodes i in
 217                   let p2 = Seq.get !stackNodes (i+1) in
 218                   (!c[p2] -> old !left[p2] = !left[p2] /\
 219                              old !right[p2] = p1) /\
 220                   (not !c[p2] -> old !left[p2] = p1 /\
 221                                  old !right[p2] = !right[p2]) }
 222       invariant { !path_from_root[root] = Nil }
 223       invariant { forall n : loc. S.mem n graph ->
 224                   not_in_stack n !stackNodes ->
 225                   !left[n] = old !left[n] /\
 226                   !right[n] = old !right[n] }
 227       (* something like Leino's line 74; this is useful to prove that
 228        * the stack is empty iff p = null *)
 229       invariant { Seq.length !stackNodes <> 0 ->
 230                   let first = last !stackNodes in
 231                   if !c[first] then !right[first] = null
 232                   else !left[first] = null }
 233       invariant { Seq.length !stackNodes <> 0 -> last !stackNodes = root }
 234       (* something like lines 75-76 from Leino's paper *)
 235       invariant { forall k : int. 0 <= k < Seq.length !stackNodes - 1 ->
 236                if !c[Seq.get !stackNodes k]
 237                then !right[Seq.get !stackNodes k] = Seq.get !stackNodes (k+1)
 238                else !left [Seq.get !stackNodes k] = Seq.get !stackNodes (k+1) }
 239       (* all nodes in the stack are marked
 240        * (I4a in Hubert and Marché and something alike line 57 in Leino) *)
 241       invariant { forall i. 0 <= i < Seq.length !stackNodes ->
 242                   !m[Seq.get !stackNodes i] }
 243       (* stack has no duplicates ---> line 55 from Leino's paper *)
 244       invariant { distinct !stackNodes }
 245       (* something like Leino's line 68 *)
 246       invariant { forall i. 0 <= i < Seq.length !stackNodes ->
 247                   let n = Seq.get !stackNodes i in
 248                   if !c[n] then !left[n] = old !left[n]
 249                   else !right[n] = old !right[n] }
 250       (* lines 80-81 from Leino's paper *)
 251       invariant { Seq.length !stackNodes <> 0 ->
 252                   if !c[!p] then old !right[!p] = !t
 253                   else old !left[!p] = !t }
 254       (* lines 78-79 from Leino's paper *)
 255       invariant { forall k : int. 0 < k < Seq.length !stackNodes ->
 256                   let n = Seq.get !stackNodes k in
 257                   if !c[n]
 258                   then Seq.get !stackNodes (k - 1) = old !right[n]
 259                   else Seq.get !stackNodes (k - 1) = old !left[n] }
 260       (* line 70 from Leino's paper *)
 261       invariant { !p <> null ->
 262                   path (old !left) (old !right) root !p !pth }
 263       (* line 72 from Leino's paper *)
 264       invariant { forall n : loc. S.mem n graph -> !m[n] ->
 265                   reachable (old !left) (old !right) root n }
 266       invariant { !p = null -> !t = root }
 267       (* line 70 from Leino's paper *)
 268       invariant { forall n : loc, pth : list loc.
 269                   S.mem n graph -> !m[n] ->
 270                   pth = !path_from_root[n] ->
 271                   path (old !left) (old !right) root n pth }
 272       (* lines 61-62 from Leinos' paper *)
 273       invariant { forall n : loc. S.mem n graph -> n <> null -> !m[n] ->
 274                   not_in_stack n !stackNodes ->
 275                   (!left[n] <> null -> !m[!left[n]]) /\
 276                   (!right[n] <> null -> !m[!right[n]]) }
 277       (* something like Leino's lines 57-59 *)
 278       invariant { forall i. 0 <= i < Seq.length !stackNodes ->
 279                   let n = Seq.get !stackNodes i in
 280                   !c[n] ->
 281                   (!left[n] <> null -> !m[!left[n]]) /\
 282                   (!right[n] <> null -> !m[!right[n]]) }
 283       (* termination proved using lexicographic order over a triple *)
 284       variant   { S.cardinal !unmarked_nodes,
 285                   S.cardinal !c_false_nodes,
 286                   Seq.length !stackNodes }
 287       if !t = null || get_m !t then begin
 288         if get_c !p then begin (* pop *)
 289           let q = !t in
 290           t := !p;
 291           ghost stackNodes := tl_stackNodes !stackNodes;
 292            p := get_right !p;
 293            set_right !t q;
 294           ghost pth := get_path_from_root !p;
 295         end else begin (* swing *)
 296           let q = !t in
 297           t := get_right !p;
 298           set_right !p (get_left !p);
 299           set_left !p q;
 300           ghost c_false_nodes := S.remove !p !c_false_nodes;
 301           set_c !p true;
 302         end
 303       end else begin (* push *)
 304         let q = !p in
 305         p := !t;
 306         ghost stackNodes := Seq.cons !p !stackNodes;
 307         t := get_left !t;
 308         set_left !p q;
 309         set_m !p true;
 310         ghost if !p <> root then pth := !pth ++ (Cons q Nil) else pth := Nil;
 311         ghost set_path_from_root !p !pth;
 312         assert { !p = Seq.get !stackNodes 0 };
 313         assert { path (old !left) (old !right) root !p !pth };
 314         set_c !p false;
 315         ghost c_false_nodes := S.add !p !c_false_nodes;
 316         ghost unmarked_nodes := S.remove !p !unmarked_nodes
 317       end
 318     done
 319
 320
 321 end