examples/verifythis_2018_register_allocation.mlw

   1 (** {1 VerifyThis @ ETAPS 2018 competition extra challenge : Register allocation }
   2
   3 Author: Quentin Garchery (LRI, Université Paris-Sud)
   4
   5 *)
   6
   7 (** {2 Import sets and maps } *)
   8
   9 use int.Int
  10 use option.Option
  11
  12 (** Assume there is a type of variables with decidable equality. *)
  13
  14 type var
  15 val eq (x y : var) : bool
  16     ensures { result <-> x = y }
  17
  18 use set.Fset
  19 clone set.SetApp as Svar with type elt = var, val eq = eq
  20
  21 (** We represent dictionaries as maps:
  22
  23        • the interference relation G between variables will be of type <Dvar.t Svar.set>
  24
  25        • the result dictionary A will be of type <Dvar.t var>
  26 *)
  27
  28 use fmap.Fmap as D
  29 clone fmap.MapApp as Dvar with type key = var, val eq = eq
  30
  31
  32 (** {2 Define functions on relations and dictionaries } *)
  33
  34 (** Define the remove (rem) operation on the interference relation.  *)
  35
  36 val map_remove (v : var) (g : Dvar.t Svar.set) : Dvar.t Svar.set
  37     ensures MapRemDomain { forall k. D.mem k result <-> D.mem k g }
  38     ensures MapRemValue { forall k. D.mem k result ->
  39                           D.find k result == Svar.remove v (D.find k g) }
  40     ensures MapRemSize { Dvar.size result = Dvar.size g }
  41
  42 let function rem (v : var) (g : Dvar.t Svar.set) : Dvar.t Svar.set
  43     requires RemReq { D.mem v g }
  44     ensures RemRemove { not D.mem v result }
  45     ensures RemDomain { forall k. D.mem k result <-> k <> v /\ D.mem k g }
  46     ensures RemValue { forall k. D.mem k result -> D.find k result == Svar.remove v (D.find k g) }
  47     ensures RemSize { Dvar.size result = Dvar.size g - 1 }
  48 =
  49     let remv = Dvar.remove v g in
  50     map_remove v remv
  51
  52 (** Define the merge operation on the interference relation. *)
  53
  54 let function replace (v u : var) (s : Svar.set) : Svar.set
  55     requires ReplaceDiff { v <> u }
  56     ensures ReplaceTarget { mem u result = (mem u s \/ mem v s) }
  57     ensures ReplaceRemove { not mem v result }
  58     ensures ReplaceOther { forall w. w <> u -> w <> v -> mem w result = mem w s }
  59   =
  60     if Svar.mem v s
  61     then Svar.add u (Svar.remove v s)
  62     else s
  63
  64 val map_replace (v u : var) (g : Dvar.t Svar.set) : Dvar.t Svar.set
  65     ensures ReplaceDomain { forall k. D.mem k result <-> D.mem k g }
  66     ensures ReplaceValue { forall k. D.mem k result ->
  67                                      D.find k result == replace v u (D.find k g) }
  68     ensures ReplaceSize { Dvar.size result = Dvar.size g }
  69
  70
  71 let function merge (v u : var) (g : Dvar.t Svar.set) : Dvar.t Svar.set
  72     requires MergeReq1 { v <> u }
  73     requires MergeReq2 { D.mem v g /\ D.mem u g }
  74     ensures MergeDomain { forall k. D.mem k result <-> k <> v /\ D.mem k g }
  75     ensures MergeValue { D.find u result == union (replace v u (D.find u g))
  76                                                   (replace v u (D.find v g)) }
  77     ensures MergeValueDiff { forall k. D.mem k result -> k <> u ->
  78                              D.find k result == replace v u (D.find k g) }
  79     ensures MergeSize { Dvar.size result = Dvar.size g - 1 }
  80 =
  81     let g1 = map_replace v u g in
  82     let gu = if Dvar.mem u g1 then Dvar.find u g1 else Svar.empty () in
  83     let gv = if Dvar.mem v g1 then Dvar.find v g1 else Svar.empty () in
  84     let g2 = Dvar.add u (Svar.union gu gv) g1 in
  85     assert { Dvar.size g2 = Dvar.size g };
  86     Dvar.remove v g2
  87
  88
  89 (** Define the available operation on the result dictionary. *)
  90
  91 let rec function all_from (s : Svar.set) (a : Dvar.t var) : Svar.set
  92     variant { cardinal s }
  93     ensures AllFrom { forall v. mem v result <->
  94                                 exists k. mem k s /\ D.mapsto k v a }
  95 =
  96    if Svar.is_empty s
  97    then Svar.empty ()
  98    else let k = Svar.choose s in
  99         let sk = Svar.remove k s in
 100         let allk = all_from sk a in
 101         if Dvar.mem k a
 102         then Svar.add (Dvar.find k a) allk
 103         else allk
 104
 105 let available (s : Svar.set) (a : Dvar.t var) (r : Svar.set) : option var
 106     ensures Available
 107             { match result with
 108               | None -> forall u. mem u r ->
 109                                   exists v. mem v s /\ D.mapsto v u a
 110               | Some res -> mem res r /\
 111                             forall v. mem v s -> D.mem v a ->
 112                                       res <> D.find v a
 113               end }
 114 =
 115     let free_r = Svar.diff r (all_from s a) in
 116     if Svar.is_empty free_r
 117     then None
 118     else Some (Svar.choose free_r)
 119
 120
 121 (** We also define the identity dictionary built from a given set. *)
 122
 123 let rec init (r : Svar.set) : Dvar.t var
 124     variant { cardinal r }
 125     ensures InitDomain { forall u. Dvar.mem u result <-> mem u r }
 126     ensures InitValue  { forall u. Dvar.mem u result -> Dvar.find u result = u }
 127 =
 128    if Svar.is_empty r
 129    then Dvar.create ()
 130    else let u = Svar.choose r in
 131         let initu = init (Svar.remove u r) in
 132         Dvar.add u u initu
 133
 134
 135 (** {2 Functions given : pick and coalesce } *)
 136
 137 val pick (g : Dvar.t Svar.set ) (r : Svar.set) : option var
 138     ensures Pick { match result with
 139                    | None -> forall v. D.mem v g -> mem v r
 140                    | Some v -> D.mem v g /\ not mem v r
 141                    end }
 142
 143 val coalesce (g : Dvar.t Svar.set) (v : var) : option var
 144     ensures Coalesce { match result with
 145                        | None -> true
 146                        | Some u -> u <> v /\ Dvar.mem u g /\ not mem v (Dvar.find u g)
 147                        end }
 148
 149 (** {2 Define properties of our data structures } *)
 150
 151 predicate no_collision (g : Dvar.t Svar.set) (a : Dvar.t var) =
 152     forall u v. Dvar.mem u g -> Dvar.mem v g -> Dvar.mem u a -> Dvar.mem v a ->
 153                 mem v (Dvar.find u g) ->
 154                 Dvar.find u a <> Dvar.find v a
 155
 156 predicate irrefl (g : Dvar.t Svar.set) =
 157      forall u. Dvar.mem u g -> not mem u (Dvar.find u g)
 158
 159 predicate sym (g : Dvar.t Svar.set) =
 160      forall u v. Dvar.mem u g -> Dvar.mem v g ->
 161                  mem v (Dvar.find u g) -> mem u (Dvar.find v g)
 162
 163 (** Symmetry is preserved by merge in our use case. *)
 164
 165 lemma sym_merge :
 166       forall v u g. sym g -> irrefl g -> Dvar.mem u g -> Dvar.mem v g ->
 167                     v <> u -> not mem v (Dvar.find u g) ->
 168                     sym (merge v u g)
 169       by forall x y. let mg = merge v u g in
 170          Dvar.mem x mg -> Dvar.mem y mg ->
 171          mem x (Dvar.find y mg) -> not (mem y (Dvar.find x mg)) -> false
 172          by if x = u then if y = u then false else false
 173             else if y = u then false else false
 174
 175
 176 (** {2 Iterated Register Coalescing algorithm } *)
 177
 178 (** We assume that the variables in the A dictionary have already been replaced
 179     by their corresponding register so that we don't need a parameter for A.
 180     This is the same as assuming that A is injective. We show that this is a
 181     needed property by giving a counterexample. Assume that variables v₁, v₂ and
 182     v₃ are such that v₁ and v₂ are mapped to register r₁ in A. Also assume that
 183     variable v₃ is not yet assigned a register and that v₂ and v₃ interfere.
 184     Then, by coalescing v₁ and v₃, we see that v₃ is assigned r₁, hence the
 185     contradiction. *)
 186
 187 let rec irc (g : Dvar.t Svar.set) (r : Svar.set) : Dvar.t var
 188     requires InclReg { forall v. mem v r -> Dvar.mem v g }
 189     requires Irrefl { irrefl g }
 190     requires Sym { sym g }
 191     variant { Dvar.size g }
 192     ensures ResDomain { forall u. Dvar.mem u result <-> Dvar.mem u g }
 193     ensures ResImage { forall u v. Dvar.mapsto u v result -> Dvar.mem v g }
 194     ensures ResInit { forall k. mem k r -> Dvar.mapsto k k result }
 195     ensures NoCollision { no_collision g result
 196     by forall u v. Dvar.mem u g -> Dvar.mem v g -> Dvar.mem u result -> Dvar.mem v result ->
 197                    mem v (Dvar.find u g) ->
 198                    Dvar.find u result = Dvar.find v result -> false
 199            }
 200 =
 201     let ghost ref gr = 0 in
 202     match pick g r with
 203     | None -> init r
 204     | Some v -> match coalesce g v with
 205                 | None ->
 206                     let s = Dvar.find v g in
 207                     let a = irc (rem v g) r in
 208                     match available s a r with
 209                     | Some av -> Dvar.add v av a
 210                     | None -> gr <- 1; Dvar.add v v a end
 211                 | Some u ->
 212                     let a = irc (merge v u g) r in
 213                     Dvar.add v (Dvar.find u a) a
 214                 end
 215     end
 216