verifythis_2015_parallel_gcd.mlw 7.67 KB
 Jean-Christophe Filliatre committed Apr 13, 2015 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 `````` (** {1 VerifyThis @ ETAPS 2015 competition, Challenge 2: Parallel GCD} {h The following is the original description of the verification task, reproduced verbatim from the competition web site.
} The following is the solution by Jean-Christophe Filliâtre (CNRS) and Guillaume Melquiond (Inria) who entered the competition as "team Why3". Since Why3 has no support for threads, we prove the sequential implementation. We do not prove termination, which would require some fairness hypothesis (in that case, you can prove that the code terminates with probability 1). *) module ParallelGCD `````` Andrei Paskevich committed Jun 15, 2018 82 83 84 `````` use int.Int use number.Gcd use ref.Ref `````` Jean-Christophe Filliatre committed Apr 13, 2015 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 `````` (** the following lemma is easily derived from a more general lemma in library [number.Gcd], namely [gcd_euclid].*) lemma gcd_sub: forall a b: int. gcd a b = gcd a (b - a) let parallel_gcd (a0 b0: int) : int requires { 0 < a0 /\ 0 < b0 } diverges ensures { result = gcd a0 b0 } = let a = ref a0 in let b = ref b0 in while !a <> !b do invariant { 0 < !a <= a0 /\ 0 < !b <= b0 } invariant { gcd !a !b = gcd a0 b0 } if any bool then if !a > !b then a := !a - !b else () else if !b > !a then b := !b - !a else () done; !a end `````` Jean-Christophe Filliatre committed Apr 17, 2015 108 109 `````` (** Threads interleaving. `````` Jean-Christophe Filliatre committed Apr 22, 2015 110 111 112 113 `````` Code and invariants by Rustan Leino. Termination argument by Martin Clochard and Léon Gondelman. Proof by Martin Clochard and Léon Gondelman. *) `````` Jean-Christophe Filliatre committed Apr 17, 2015 114 115 ``````module Interleaving `````` Andrei Paskevich committed Jun 15, 2018 116 117 118 `````` use int.Int use number.Gcd use ref.Ref `````` Jean-Christophe Filliatre committed Apr 17, 2015 119 120 121 `````` lemma gcd_sub: forall a b: int. gcd a b = gcd a (b - a) `````` Martin Clochard committed Apr 22, 2015 122 123 `````` (* Representation of a thread: two local variables (register copies of the globals) and a program counter: `````` Jean-Christophe Filliatre committed Apr 22, 2015 124 `````` `````` Martin Clochard committed Apr 22, 2015 125 126 127 128 129 130 131 132 133 `````` ReadA: local_a <- a ReadB: local_b <- b Compare: if local_a = local_b goto Halt; if local_a > local_b a := local_a - local_b; goto ReadA; Halt: `````` Jean-Christophe Filliatre committed Apr 22, 2015 134 `````` `````` Martin Clochard committed Apr 22, 2015 135 136 137 138 `````` For the sake of simplicity, every section is considered atomic. (strictly speaking, section Compare is not, but it interacts atomically with memory so it would be equivalent) *) `````` Jean-Christophe Filliatre committed Apr 17, 2015 139 140 141 142 143 144 145 146 `````` type state = ReadA | ReadB | Compare | Halt type thread = { mutable local_a: int; (* local copy of a *) mutable local_b: int; (* local copy of b *) mutable state : state; } `````` Martin Clochard committed Apr 22, 2015 147 148 149 `````` (* Thread invariant. *) predicate inv (th: thread) (d a b: int) = 0 < a /\ 0 < b /\ gcd a b = d /\ `````` Jean-Christophe Filliatre committed Apr 17, 2015 150 151 `````` match th.state with | ReadA -> true `````` Martin Clochard committed Apr 22, 2015 152 `````` | ReadB -> th.local_a = a (* No other thread can write in a. *) `````` Jean-Christophe Filliatre committed Apr 17, 2015 153 154 `````` | Compare -> th.local_a = a && b <= th.local_b && (th.local_b <= th.local_a -> th.local_b = b) `````` Martin Clochard committed Apr 22, 2015 155 156 157 `````` (* Other thread may have overwritten b, but only in a decreasing decreasing fashion, and only once under a. *) | Halt -> th.local_a = a = b (* Final state is stable. *) `````` Jean-Christophe Filliatre committed Apr 17, 2015 158 159 `````` end `````` Jean-Christophe Filliatre committed Apr 22, 2015 160 161 `````` (* Does running this thread make any progress toward the result? *) predicate progress_thread (th: thread) (a b: int) = `````` Martin Clochard committed Apr 22, 2015 162 163 164 `````` a > b \/ (a = b /\ th.state <> Halt) (* Decreasing ordering on program counter *) `````` Jean-Christophe Filliatre committed Apr 22, 2015 165 `````` function state_index (s: state) : int = match s with `````` Martin Clochard committed Apr 22, 2015 166 167 168 169 170 171 172 `````` | ReadA -> 7 | ReadB -> 5 | Compare -> 3 | Halt -> 2 end (* Synchronisation status. *) `````` Jean-Christophe Filliatre committed Apr 22, 2015 173 `````` predicate sync (th: thread) (b: int) = `````` Martin Clochard committed Apr 22, 2015 174 175 176 `````` match th.state with Compare -> th.local_b = b | _ -> true end (* Convert status into an index. *) `````` Jean-Christophe Filliatre committed Apr 22, 2015 177 `````` function sync_index (th: thread) (b: int) : int = `````` Martin Clochard committed Apr 22, 2015 178 179 180 181 182 183 `````` if sync th b then 0 else 42 (* Thread progression index: if running this thread should make any progression toward the result, then it will have the following shape: - A first (optional) loop run for synchronization. - A second synchronized run until effective progress *) `````` Jean-Christophe Filliatre committed Apr 22, 2015 184 `````` function prog_index (th: thread) (b: int) : int = `````` Martin Clochard committed Apr 22, 2015 185 186 `````` sync_index th b + state_index th.state `````` Jean-Christophe Filliatre committed Apr 17, 2015 187 188 189 `````` val create_thread () : thread ensures { result.state = ReadA } `````` Jean-Christophe Filliatre committed Apr 22, 2015 190 191 192 193 `````` (* Fair scheduler modelisation: Each time it switches between threads, it also writes down the maximal time remaining before it will switch to the other. If it does not switch, this timeout decreases. *) `````` Martin Clochard committed Apr 22, 2015 194 195 196 197 `````` val ghost scheduled : ref bool val ghost timer : ref int val schedule () : bool `````` Jean-Christophe Filliatre committed Apr 22, 2015 198 `````` writes { scheduled, timer } `````` Martin Clochard committed Apr 22, 2015 199 200 201 202 203 204 `````` ensures { !scheduled = old !scheduled -> 0 <= !timer < old !timer } ensures { result = !scheduled } (* Execution of one thread step. *) let step (th: thread) (ghost d: int) (a b: ref int) requires { inv th d !a !b } `````` Jean-Christophe Filliatre committed Apr 17, 2015 205 `````` writes { th, a } `````` Martin Clochard committed Apr 22, 2015 206 `````` ensures { inv th d !a !b } `````` Jean-Christophe Filliatre committed Apr 17, 2015 207 `````` ensures { 0 < !a <= old !a } `````` Jean-Christophe Filliatre committed Apr 22, 2015 208 209 `````` ensures { old !a > !a -> old !a >= !a + !b } ensures { progress_thread th !a !b -> `````` Martin Clochard committed Apr 22, 2015 210 `````` prog_index (old th) !b > prog_index th !b \/ !a < old !a } `````` Jean-Christophe Filliatre committed Apr 17, 2015 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 `````` = match th.state with | ReadA -> th.local_a <- !a; th.state <- ReadB | ReadB -> th.local_b <- !b; th.state <- Compare | Compare -> if th.local_a = th.local_b then th.state <- Halt else begin if th.local_a > th.local_b then a := th.local_a - th.local_b; th.state <- ReadA end | Halt -> () end `````` Guillaume Melquiond committed Mar 16, 2016 228 229 230 231 `````` let can_progress (s : state) ensures { result = True <-> s <> Halt } = match s with Halt -> False | _ -> True end `````` Jean-Christophe Filliatre committed Apr 17, 2015 232 233 234 235 236 237 238 `````` let parallel_gcd (a0 b0: int) : int requires { 0 < a0 /\ 0 < b0 } ensures { result = gcd a0 b0 } = (* shared variables *) let a = ref a0 in let b = ref b0 in `````` Andrei Paskevich committed Jun 10, 2017 239 `````` let ghost d = gcd a0 b0 in `````` Jean-Christophe Filliatre committed Apr 17, 2015 240 241 242 `````` (* two threads *) let th1 = create_thread () in let th2 = create_thread () in `````` Guillaume Melquiond committed Mar 16, 2016 243 `````` while can_progress th1.state || can_progress th2.state do `````` Martin Clochard committed Apr 22, 2015 244 `````` invariant { inv th1 d !a !b /\ inv th2 d !b !a } `````` Jean-Christophe Filliatre committed Apr 22, 2015 245 246 247 248 `````` variant { (* global progress in the algorithm *) !a + !b , (* progress in one of the two threads *) `````` Andrei Paskevich committed Jun 11, 2017 249 `````` begin if !a = !b `````` Martin Clochard committed Apr 22, 2015 250 251 252 `````` then prog_index th2 !a + prog_index th1 !b else if !a < !b then prog_index th2 !a `````` Andrei Paskevich committed Jun 11, 2017 253 `````` else prog_index th1 !b end `````` Jean-Christophe Filliatre committed Apr 22, 2015 254 255 256 `````` , (* no progress in both threads, but the scheduler switches to the non-progressing thread *) `````` Andrei Paskevich committed Jun 11, 2017 257 `````` begin if progress_thread th1 !a !b `````` Martin Clochard committed Apr 22, 2015 258 259 260 `````` then if !scheduled then 1 else 0 else if progress_thread th2 !b !a then if !scheduled then 0 else 1 `````` Andrei Paskevich committed Jun 11, 2017 261 `````` else 0 end `````` Jean-Christophe Filliatre committed Apr 22, 2015 262 263 264 `````` , (* the scheduler is still running the non-progressing thread *) !timer } `````` Martin Clochard committed Apr 22, 2015 265 `````` if schedule () then step th1 d a b else step th2 d b a `````` Jean-Christophe Filliatre committed Apr 17, 2015 266 267 268 269 `````` done; !a end``````