VerifyThis @ ETAPS 2015 competition, Challenge 2: Parallel GCD

The following is the original description of the verification task, reproduced verbatim from the competition web site.

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 int.Int
  use number.Gcd
  use ref.Ref

  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

module Interleaving

  use int.Int
  use number.Gcd
  use ref.Ref

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

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

     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:

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

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

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

  (* Decreasing ordering on program counter *)
  function state_index (s: state) : int = match s with
    | ReadA -> 7
    | ReadB -> 5
    | Compare -> 3
    | Halt -> 2
    end

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

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

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

  (* 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. *)
  val ghost scheduled : ref bool
  val ghost timer : ref int

  val schedule () : bool
    writes  { scheduled, timer }
    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 }
    writes   { th, a }
    ensures  { inv th d !a !b }
    ensures  { 0 < !a <= old !a }
    ensures  { old !a > !a -> old !a >= !a + !b }
    ensures  { progress_thread th !a !b ->
      prog_index (old th) !b > prog_index th !b \/ !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 can_progress (s : state)
    ensures { result = True <-> s <> Halt }
  = match s with Halt -> False | _ -> True end

  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
    let ghost d = gcd a0 b0 in
    (* two threads *)
    let th1 = create_thread () in
    let th2 = create_thread () in
    while can_progress th1.state || can_progress th2.state do
      invariant { inv th1 d !a !b /\ inv th2 d !b !a }
      variant { (* global progress in the algorithm *)
                !a + !b
                ,
                (* progress in one of the two threads *)
                begin if !a = !b
                then prog_index th2 !a + prog_index th1 !b
                else if !a < !b
                then prog_index th2 !a
                else prog_index th1 !b end
                ,
                (* no progress in both threads, but the scheduler
                   switches to the non-progressing thread *)
                begin if progress_thread th1 !a !b
                then if !scheduled then 1 else 0
                else if progress_thread th2 !b !a
                then if !scheduled then 0 else 1
                else 0 end
                ,
                (* the scheduler is still running the non-progressing thread *)
                !timer }
      if schedule () then step th1 d a b else step th2 d b a
    done;
    !a

end