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