## VerifyThis 2015: solution to problem 2

**Authors:** Jean-Christophe Filliâtre / Guillaume Melquiond / Martin Clochard / Léon Gondelman

**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 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 | Alt-Ergo 2.0.0 | Spass 3.9 | Vampire 0.6 | |

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.02 | --- | --- | |

loop invariant preservation | 0.01 | --- | --- | |

loop invariant preservation | 0.01 | --- | --- | |

postcondition | 0.26 | --- | --- |

## Theory "verifythis_2015_parallel_gcd.Interleaving": fully verified

Obligations | Alt-Ergo 2.0.0 | CVC4 1.5 | Eprover 2.0 | Z3 4.6.0 | ||

gcd_sub | --- | --- | 0.04 | --- | ||

VC for step | --- | --- | --- | --- | ||

split_goal_right | ||||||

postcondition | 0.01 | --- | --- | --- | ||

postcondition | 0.00 | --- | --- | --- | ||

postcondition | 0.00 | --- | --- | --- | ||

postcondition | --- | --- | --- | 0.03 | ||

postcondition | 0.01 | --- | --- | --- | ||

postcondition | 0.01 | --- | --- | --- | ||

postcondition | 0.00 | --- | --- | --- | ||

postcondition | 0.24 | --- | --- | --- | ||

postcondition | 0.01 | --- | --- | --- | ||

postcondition | 0.00 | --- | --- | --- | ||

postcondition | 0.01 | --- | --- | --- | ||

postcondition | 0.01 | --- | --- | --- | ||

postcondition | --- | --- | --- | 0.03 | ||

postcondition | 0.01 | --- | --- | --- | ||

postcondition | 0.01 | --- | --- | --- | ||

postcondition | 0.01 | --- | --- | --- | ||

postcondition | 0.01 | --- | --- | --- | ||

postcondition | 0.01 | --- | --- | --- | ||

postcondition | 0.01 | --- | --- | --- | ||

postcondition | --- | 0.04 | --- | --- | ||

postcondition | 0.01 | --- | --- | --- | ||

postcondition | 0.01 | --- | --- | --- | ||

postcondition | 0.01 | --- | --- | --- | ||

postcondition | 0.00 | --- | --- | --- | ||

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.02 | --- | --- | --- | ||

precondition | 0.00 | --- | --- | --- | ||

loop variant decrease | --- | --- | --- | --- | ||

inline_all | ||||||

loop variant decrease | --- | 0.20 | --- | --- | ||

loop invariant preservation | 0.02 | --- | --- | --- | ||

postcondition | 0.56 | --- | --- | --- |