verifythis_2015_parallel_gcd.mlw 7.67 KB
Newer Older
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
<a href="http://etaps2015.verifythis.org/challenges">the competition web site</a>.

<pre>
PARALLEL GCD (60 minutes)
=========================

Algorithm description
---------------------

Various parallel GCD algorithms exist. In this challenge, we consider a
simple Euclid-like algorithm with two parallel threads. One thread
subtracts in one direction, the other thread subtracts in the other
direction, and eventually this procedure converges on GCD.


Implementation
--------------

In pseudocode, the algorithm is described as follows:

(
  WHILE a != b DO
      IF a>b THEN a:=a-b ELSE SKIP FI
  OD
||
  WHILE a != b DO
       IF b>a THEN b:=b-a ELSE SKIP FI
  OD
);
OUTPUT a


Verification tasks
------------------

Specify and verify the following behaviour of this parallel GCD algorithm:

Input:  two positive integers a and b
Output: a positive number that is the greatest common divisor of a and b

Feel free to add synchronisation where appropriate, but try to avoid
blocking of the parallel threads.


Sequentialization
-----------------

If your tool does not support reasoning about parallel threads, you may
verify the following pseudocode algorithm:

WHILE a != b DO
    CHOOSE(
         IF a > b THEN a := a - b ELSE SKIP FI,
         IF b > a THEN b := b - a ELSE SKIP FI
    )
OD;
OUTPUT a

</pre>}

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

82 83 84
  use int.Int
  use number.Gcd
  use ref.Ref
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
108 109

(** Threads interleaving.
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.
    *)
114 115
module Interleaving

116 117 118
  use int.Int
  use number.Gcd
  use ref.Ref
119 120 121

  lemma gcd_sub: forall a b: int. gcd a b = gcd a (b - a)

122 123
  (* Representation of a thread: two local variables
    (register copies of the globals) and a program counter:
124

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:
134

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)
   *)
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;
  }

147 148 149
  (* Thread invariant. *)
  predicate inv (th: thread) (d a b: int) =
    0 < a /\ 0 < b /\ gcd a b = d /\
150 151
    match th.state with
    | ReadA -> true
152
    | ReadB -> th.local_a = a (* No other thread can write in a. *)
153 154
    | Compare -> th.local_a = a && b <= th.local_b &&
                  (th.local_b <= th.local_a -> th.local_b = b)
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. *)
158 159
    end

160 161
  (* Does running this thread make any progress toward the result? *)
  predicate progress_thread (th: thread) (a b: int) =
162 163 164
    a > b \/ (a = b /\ th.state <> Halt)

  (* Decreasing ordering on program counter *)
165
  function state_index (s: state) : int = match s with
166 167 168 169 170 171 172
    | ReadA -> 7
    | ReadB -> 5
    | Compare -> 3
    | Halt -> 2
    end

  (* Synchronisation status. *)
173
  predicate sync (th: thread) (b: int) =
174 175 176
    match th.state with Compare -> th.local_b = b | _ -> true end

  (* Convert status into an index. *)
177
  function sync_index (th: thread) (b: int) : int =
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 *)
184
  function prog_index (th: thread) (b: int) : int =
185 186
    sync_index th b + state_index th.state

187 188 189
  val create_thread () : thread
    ensures { result.state = ReadA }

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. *)
194 195 196 197
  val ghost scheduled : ref bool
  val ghost timer : ref int

  val schedule () : bool
198
    writes  { scheduled, timer }
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 }
205
    writes   { th, a }
206
    ensures  { inv th d !a !b }
207
    ensures  { 0 < !a <= old !a }
208 209
    ensures  { old !a > !a -> old !a >= !a + !b }
    ensures  { progress_thread th !a !b ->
210
      prog_index (old th) !b > prog_index th !b \/ !a < old !a }
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

228 229 230 231
  let can_progress (s : state)
    ensures { result = True <-> s <> Halt }
  = match s with Halt -> False | _ -> True end

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
239
    let ghost d = gcd a0 b0 in
240 241 242
    (* two threads *)
    let th1 = create_thread () in
    let th2 = create_thread () in
243
    while can_progress th1.state || can_progress th2.state do
244
      invariant { inv th1 d !a !b /\ inv th2 d !b !a }
245 246 247 248
      variant { (* global progress in the algorithm *)
                !a + !b
                ,
                (* progress in one of the two threads *)
249
                begin if !a = !b
250 251 252
                then prog_index th2 !a + prog_index th1 !b
                else if !a < !b
                then prog_index th2 !a
253
                else prog_index th1 !b end
254 255 256
                ,
                (* no progress in both threads, but the scheduler
                   switches to the non-progressing thread *)
257
                begin if progress_thread th1 !a !b
258 259 260
                then if !scheduled then 1 else 0
                else if progress_thread th2 !b !a
                then if !scheduled then 0 else 1
261
                else 0 end
262 263 264
                ,
                (* the scheduler is still running the non-progressing thread *)
                !timer }
265
      if schedule () then step th1 d a b else step th2 d b a
266 267 268 269
    done;
    !a

end