verifythis_2015_parallel_gcd.mlw 4.35 KB
 Jean-Christophe Filliâtre 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 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 `````` (** {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 use import int.Int use import number.Gcd use import ref.Ref (** 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 Filliâtre committed Apr 17, 2015 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 `````` (** Threads interleaving. Code and invariants by Rustan Leino. *) (*** module Interleaving use import int.Int use import number.Gcd use import ref.Ref lemma gcd_sub: forall a b: int. gcd a b = gcd a (b - a) 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; } predicate inv (th: thread) (a0 b0 a b: int) = 0 < a /\ 0 < b /\ gcd a b = gcd a0 b0 /\ match th.state with | ReadA -> true | ReadB -> th.local_a = a | Compare -> th.local_a = a && b <= th.local_b && (th.local_b <= th.local_a -> th.local_b = b) | Halt -> th.local_a = a = b end val create_thread () : thread ensures { result.state = ReadA } let step (th: thread) (ghost a0 b0: int) (a b: ref int) requires { inv th a0 b0 !a !b } writes { th, a } ensures { inv th a0 b0 !a !b } ensures { 0 < !a <= old !a } = 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 let parallel_gcd (a0 b0: int) : int requires { 0 < a0 /\ 0 < b0 } diverges ensures { result = gcd a0 b0 } = (* shared variables *) let a = ref a0 in let b = ref b0 in (* two threads *) let th1 = create_thread () in let th2 = create_thread () in while th1.state <> Halt || th2.state <> Halt do invariant { inv th1 a0 b0 !a !b /\ inv th2 b0 a0 !b !a } if any bool then step th1 a0 b0 a b else step th2 b0 a0 b a done; !a end ***)``````