examples/verifythis_2015_parallel_gcd.mlw

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