verifythis_2015_parallel_gcd.mlw 4.35 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 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
<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

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