## VerifyThis 2015: solution to problem 2

Catégories: Arithmetic

Outils: Why3

Références: 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
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)
```

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:

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

download ZIP archive

# Why3 Proof Results for Project "verifythis_2015_parallel_gcd"

## Theory "verifythis_2015_parallel_gcd.ParallelGCD": fully verified

 Obligations CVC5 1.0.5 Spass 3.9 Vampire 0.6 Z3 4.8.4 gcd_sub --- 0.05 0.02 --- VC for parallel_gcd --- --- --- --- split_goal_right loop invariant init --- --- --- 0.00 loop invariant init --- --- --- 0.00 loop invariant preservation --- --- --- 0.01 loop invariant preservation --- --- --- 0.02 loop invariant preservation --- --- --- 0.01 loop invariant preservation --- --- --- 0.00 loop invariant preservation --- --- --- 0.01 loop invariant preservation 0.07 --- --- --- loop invariant preservation --- --- --- 0.01 loop invariant preservation --- --- --- 0.01 postcondition --- --- --- 0.11

## Theory "verifythis_2015_parallel_gcd.Interleaving": fully verified

 Obligations CVC4 1.5 CVC5 1.0.5 Eprover 2.0 Z3 4.8.4 gcd_sub --- --- 0.04 --- VC for step --- --- --- --- split_goal_right postcondition --- --- --- 0.01 postcondition --- --- --- 0.00 postcondition --- --- --- 0.00 postcondition --- 0.09 --- --- postcondition --- 0.07 --- --- postcondition --- --- --- 0.01 postcondition --- --- --- 0.00 postcondition --- 0.07 --- --- postcondition --- 0.07 --- --- postcondition --- --- --- 0.00 postcondition --- --- --- 0.01 postcondition --- 0.07 --- --- postcondition --- 0.94 --- --- postcondition --- 0.07 --- --- postcondition --- 0.06 --- --- postcondition --- 0.07 --- --- postcondition --- --- --- 0.01 postcondition --- --- --- 0.01 postcondition --- --- --- 0.01 postcondition 0.04 --- --- --- postcondition --- --- --- 0.01 postcondition --- --- --- 0.01 postcondition --- --- --- 0.01 postcondition --- 0.05 --- --- VC for can_progress --- --- --- 0.01 VC for parallel_gcd --- --- --- --- split_goal_right loop invariant init --- --- --- 0.01 precondition --- --- --- 0.01 loop variant decrease --- --- --- --- inline_all loop variant decrease 0.10 --- --- --- loop invariant preservation --- 0.14 --- --- precondition --- --- --- 0.00 loop variant decrease --- --- --- --- inline_all loop variant decrease 0.20 --- --- --- loop invariant preservation --- 0.12 --- --- postcondition --- --- --- 0.02