examples/schorr_waite_via_recursion.mlw

   1
   2 (** Schorr-Waite algorithm for general-size records.
   3
   4     Author: Martin Clochard (Université Paris Sud)
   5
   6     Here the proof is carried out by proving an equivalent
   7     recursive program. The recursive program can be justified
   8     to be equivalent to the looping one:
   9     all side-effects/exception throwing are done by running the loop body
  10     (which features a minor modification to exit by exception),
  11     so the recursive programs amounts to execute an arbitrary number
  12     of time the loop body. It is immediately followed by an absurd statement
  13     to enforce the equivalence with the loop which runs its body an
  14     infinite number of times.
  15     Although the added recursive structure can be seen to be computationally
  16     irrelevant, it allows to discharge details about Schorr-Waite
  17     stack management through a recursive procedure proof. The method
  18     basically make explicit the derecursification used to obtain
  19     Schorr-Waite algorithm.
  20
  21     See example verifythis_2016_tree_traversal for details about
  22     the technique, applied to a similar algorithm for trees.
  23
  24 *)
  25
  26 (** Component-as-array memory model, with null pointers
  27     and arbitrary-sized memory blocks. *)
  28 module Memory
  29
  30   use int.Int
  31   use option.Option
  32   use map.Map
  33   (** Memory locations *)
  34   type loc
  35   (** Null pointer *)
  36   constant null : loc
  37   (** Marks used by Schorr-Waite *)
  38   type color =
  39     | White
  40     | Black (option int)
  41   type pmem = map loc (map int loc)
  42   (** Memory blocks have two parts: a marking part containing in particular
  43       Schorr-Waite internal management data, and a sequence of pointers
  44       to other memory blocks. *)
  45   type memory = abstract {
  46     (** Associate block size to location. *)
  47     block_size : map loc int;
  48     (** Pointers to other memory blocks. *)
  49     mutable accessor : pmem;
  50     (** Marks. *)
  51     mutable colors : map loc color;
  52   }
  53   (** Global instance for memory *)
  54   val memo : memory
  55   (** null creation *)
  56   val null () : loc ensures { result = null }
  57   (** null test *)
  58   val is_null (l:loc) : bool ensures { result <-> l = null }
  59   (** Get block size associated to a given location *)
  60   val get_block_size (l:loc) : int
  61     requires { l <> null }
  62     reads { memo }
  63     ensures { result = memo.block_size[l] /\ result >= 0 }
  64   (** Access to a mark *)
  65   val get_color (l:loc) : color
  66     requires { l <> null }
  67     reads { memo }
  68     ensures { result = memo.colors[l] }
  69   (** Set a mark. We also impose the restriction that when a block is
  70       marked black, the given index must be coherent with the block size.
  71       This impose special treatment for 0-sized memory blocks. *)
  72   val set_color (l:loc) (c:color) : unit
  73     requires { l <> null }
  74     requires { match c with
  75       | White -> true
  76       | Black None -> memo.block_size[l] = 0
  77       | Black (Some ind) -> 0 <= ind < memo.block_size[l]
  78       end }
  79     writes { memo.colors }
  80     ensures { memo.colors = old (memo.colors[l <- c]) }
  81   (** Getter/Setter for pointer buffer *)
  82   val get_acc (l:loc) (k:int) : loc
  83     requires { l <> null /\ 0 <= k < memo.block_size[l] }
  84     reads { memo }
  85     ensures { result = memo.accessor[l][k] }
  86   val set_acc (l:loc) (k:int) (d:loc) : unit
  87     requires { l <> null /\ 0 <= k < memo.block_size[l] }
  88     writes { memo.accessor }
  89     ensures { memo.accessor =
  90       old (memo.accessor[l <- memo.accessor[l][k <- d]]) }
  91   (** Take ghost snapshots of memory. *)
  92   val ghost snapshot_acc () : pmem
  93     reads { memo }
  94     ensures { result = memo.accessor }
  95   val ghost snapshot_colors () : map loc color
  96     reads { memo }
  97     ensures { result = memo.colors }
  98
  99 end
 100
 101 (** Define notions about the memory graph *)
 102 module GraphShape
 103
 104   use int.Int
 105   use set.Fset
 106   use map.Map
 107   use Memory
 108
 109   predicate black (c:color) = c <> White
 110
 111   (** Edges *)
 112   predicate edge (m:memory) (x y:loc) =
 113     x <> null /\ (exists n. 0 <= n < m.block_size[x] /\ m.accessor[x][n] = y)
 114   (** Paths *)
 115   inductive path memory (x y:loc) =
 116     | path_nil : forall m x. path m x x
 117     | path_cons : forall m x y z. edge m x y /\ path m y z -> path m x z
 118   (** DFS invariant. For technical reason, it must refer to different parts
 119      of the memory at different time. The graph structure is given
 120      via the initial memory, but the coloring is given via the current one. *)
 121   predicate well_colored_on (graph gray:fset loc) (m:memory) (cl:map loc color) =
 122     subset gray graph /\
 123     (forall x y. mem x graph /\ edge m x y /\ y <> null /\ black cl[x] ->
 124       mem x gray \/ black cl[y]) /\
 125     (forall x. mem x gray -> black cl[x])
 126   (** Unchanged only concerns the graph shape, not the marks *)
 127   predicate unchanged (m1 m2:memory) =
 128     forall x n. x <> null /\ 0 <= n < m1.block_size[x] ->
 129       m2.accessor[x][n] = m1.accessor[x][n]
 130
 131 end
 132
 133 (** Proof of Schorr-Waite algorithm *)
 134 module SchorrWaite
 135
 136   use int.Int
 137   use option.Option
 138   use set.Fset
 139   use map.Map
 140   use map.Const
 141   use ref.Ref
 142   use Memory
 143   use GraphShape
 144
 145   let black (l: loc) : bool
 146     requires { l <> null }
 147     reads { memo }
 148     ensures { result <-> black memo.colors[l] }
 149   = match get_color l with White -> false | _ -> true end
 150
 151   exception Stop
 152
 153   let schorr_waite (root: loc) (ghost graph: fset loc) : unit
 154     (** Root belong to graph (note: for simplicity, the graph set
 155         may (and likely does) contain the null pointer. *)
 156     requires { mem root graph }
 157     (** Graph is closed by following edges *)
 158     requires { forall l n.
 159       mem l graph /\ l <> null /\ 0 <= n < memo.block_size[l] ->
 160       mem memo.accessor[l][n] graph }
 161     writes { memo.accessor, memo.colors }
 162     (** The graph starts fully unmarked. *)
 163     requires { forall x. mem x graph -> not black memo.colors[x] }
 164     (** The graph structure is left unchanged. *)
 165     ensures { unchanged (old memo) memo }
 166     (** Every non-null location reachable from the root is marked black. *)
 167     ensures { forall x. path (old memo) root x /\ x <> null ->
 168       black memo.colors[x] }
 169     (** Every other location is left with its previous color. *)
 170     ensures { forall x. not path (old memo) root x /\ x <> null ->
 171       memo.colors[x] = (old memo).colors[x] }
 172   =
 173     label I in
 174     let t = ref root in
 175     let p = ref (null ()) in
 176     (** Schorr-Waite loop body. *)
 177     let body () : unit
 178       (** Loop body specification: mindlessly repeat the underlying code. *)
 179       requires { !p <> null /\ (!t = null \/ black memo.colors[!t]) ->
 180         match memo.colors[!p] with
 181         | Black (Some m) -> 0 <= m < memo.block_size[!p]
 182         | _ -> false
 183         end }
 184       ensures { old (!p <> null \/ (!t <> null /\ not black memo.colors[!t])) }
 185       ensures { old (!t <> null /\ not black memo.colors[!t] /\
 186                      memo.block_size[!t] = 0) ->
 187         memo.colors = old memo.colors[!t <- Black None] /\
 188         !t = old !t /\ !p = old (!p) /\ memo.accessor = old memo.accessor
 189       }
 190       ensures { old (!t <> null /\ not black memo.colors[!t] /\
 191                      memo.block_size[!t] > 0) ->
 192         memo.colors = old memo.colors[!t <- Black (Some 0)] /\
 193         !t = old memo.accessor[!t][0] /\ !p = old (!t) /\
 194         memo.accessor = old memo.accessor[!t <- memo.accessor[!t][0 <- !p]] }
 195       ensures { old (!t = null \/ black memo.colors[!t]) ->
 196         match old (memo.colors[!p]) with
 197         | Black (Some m) ->
 198             let n = m + 1 in
 199             if n = old (memo.block_size[!p])
 200             then
 201               !t = old (!p) /\ !p = (old memo.accessor[!p])[m] /\
 202               memo.colors = old (memo.colors) /\
 203               memo.accessor =
 204                 (old memo.accessor)[old !p <-
 205                                     (old memo.accessor[!p])[m <- old !t]]
 206             else !p = old !p /\ !t = (old memo.accessor[!p])[n] /\
 207               memo.colors = (old memo.colors)[old !p <- Black (Some n)] /\
 208               let pi = (old memo.accessor[!p])[m] in
 209               memo.accessor =
 210                 (old memo.accessor)[old !p <-
 211                          (old memo.accessor[!p])[n <- pi][m <- old !t]]
 212         | _ -> false
 213         end }
 214       raises { Stop -> old(!p = null /\ (!t = null \/ black memo.colors[!t])) /\
 215         memo.colors = old memo.colors /\ memo.accessor = old memo.accessor }
 216     = (** Minor modification to the loop: it exits by exception.  *)
 217       if is_null !p && (is_null !t || black !t) then raise Stop;
 218       if is_null !t || black !t then begin
 219         match get_color !p with
 220         | Black (Some m) ->
 221             let s = get_block_size !p in
 222             let n = m + 1 in
 223             if n = s then begin (* Pop *)
 224               let q = !t in
 225               t := !p;
 226               p := get_acc !p m;
 227               set_acc !t m q
 228             end else begin (* Swing *)
 229               let q = !t in
 230               t := get_acc !p n;
 231               set_acc !p n (get_acc !p m);
 232               set_acc !p m q;
 233               set_color !p (Black (Some n))
 234             end
 235         | _ -> absurd
 236         end
 237       end else
 238         let s = get_block_size !t in
 239         if s = 0 then (* Mark & continue *) set_color !t (Black None)
 240         else begin (* Mark & Push *)
 241           let q = !p in
 242           p := !t;
 243           t := get_acc !t 0;
 244           set_acc !p 0 q;
 245           set_color !p (Black (Some 0))
 246         end
 247     in
 248     let rec aux (ghost gray:fset loc) : unit
 249       (* DFS invariant *)
 250       requires { well_colored_on graph gray (memo at I) memo.colors }
 251       requires { mem !t graph }
 252       (* Non-marked nodes have unchanged structure with
 253           respect to the initial one. *)
 254       requires { forall x n.
 255         x <> null /\ not black memo.colors[x] /\ 0 <= n < memo.block_size[x] ->
 256         memo.accessor[x][n] = (memo.accessor at I)[x][n] }
 257       (* 'stack frames' are maintained correctly *)
 258       ensures { !t = old !t /\ !p = old !p }
 259       (* Pointer buffer is left unchanged *)
 260       ensures { unchanged (old memo) memo }
 261       (* Maintain DFS invariant *)
 262       ensures { well_colored_on graph gray (memo at I) memo.colors }
 263       (* The top node get marked *)
 264       ensures { black memo.colors[!t] \/ !t = null }
 265       (* May not mark unreachable node, neither change marked node. *)
 266       ensures { forall x.
 267         x <> null -> not path (memo at I) !t x \/ black (old memo.colors)[x] ->
 268         memo.colors[x] = (old memo.colors)[x] }
 269       (* Never 'exit' the loop during the recursive calls *)
 270       raises { Stop -> false }
 271       (* Terminates because there is a limited number of 'grayable' nodes. *)
 272       variant { cardinal graph - cardinal gray }
 273     = label J in
 274       if is_null !t || black !t then () else begin
 275         let s = get_block_size !t in
 276         let ghost g2 = add !t gray in
 277         assert { path (memo at I) !t !t };
 278         body (); (* Either push or mark & continue. *)
 279         if s <> 0 then begin
 280           for i = 0 to s - 2 do (* Over all sub-blocs... *)
 281             (* DFS invariant. *)
 282             invariant { well_colored_on graph g2 (memo at I) memo.colors }
 283             (* Current stack frame invariants *)
 284             invariant { !p = !t at J }
 285             invariant { !t = (memo.accessor at I)[!p][i] }
 286             invariant { memo.colors[!p] = Black (Some i) }
 287             invariant { forall j. 0 <= j < s /\ j <> i ->
 288               memo.accessor[!p][j] = (memo.accessor at J)[!p][j] }
 289             invariant { memo.accessor[!p][i] = !p at J }
 290             (* Outside structure is unchanged. *)
 291             invariant { forall l n.
 292               l <> null /\ l <> !p /\ 0 <= n < memo.block_size[l] ->
 293               memo.accessor[l][n] = (memo.accessor at J)[l][n] }
 294             (* All nodes under !p & before i are either null or marked black. *)
 295             invariant { forall j. 0 <= j < i ->
 296               let l = memo.accessor[!p][j] in l = null \/ black memo.colors[l] }
 297             (* Unreachable/pre-marked blocks do not change. *)
 298             invariant { forall l. l <> null ->
 299               not path (memo at I) !p l \/ black (memo.colors at J)[l] ->
 300                 memo.colors[l] = (memo.colors at J)[l] }
 301             label K in
 302             aux g2; (* Explore sub-bloc. *)
 303             body (); (* Swing to next sub-bloc. *)
 304             assert { !t = (memo.accessor at K)[!p][i+1]
 305               = (memo.accessor at J)[!p][i+1] }
 306           done;
 307           aux g2; (* Explore last sub-bloc. *)
 308           body (); (* Pop. *)
 309         end
 310       end in
 311     try aux (ghost empty); (* Explore main bloc *)
 312         body (); (* Exit *)
 313         absurd; (* Done. *)
 314     with Stop ->
 315       (* Need induction to recover path-based specification. *)
 316       assert { forall x y m. m = memo at I /\ x <> null /\ y <> null /\
 317         mem x graph /\ black memo.colors[x] ->
 318         ([@induction] path m x y) -> black memo.colors[y] }
 319     end
 320
 321 end