## VerifyThis 2015: solution to problem 2

Topics: Arithmetic

Tools: Why3

References: VerifyThis @ ETAPS 2015

see also the index (by topic, by tool, by reference, by year)

# 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
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

------------------

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

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

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

the following lemma is easily derived from a more general lemma in library [number.Gcd], namely [gcd_euclid].

```  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
```

Threads interleaving. Code and invariants by Rustan Leino. Termination argument by Martin Clochard and Léon Gondelman. Proof by Martin Clochard and Léon Gondelman.

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

local_a <- a
local_b <- b
Compare:
if local_a = local_b goto Halt;
if local_a > local_b a := local_a - local_b;
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)
*)

mutable local_a: int; (* local copy of a *)
mutable local_b: int; (* local copy of b *)
mutable state  : state;
}

predicate inv (th: thread) (d a b: int) =
0 < a /\ 0 < b /\ gcd a b = d /\
match th.state with
| 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? *)
a > b \/ (a = b /\ th.state <> Halt)

(* Decreasing ordering on program counter *)
function state_index (s: state) : int = match s with
| 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

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

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
th.local_a <- !a; th.state <- 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;
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
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
```