VerifyThis @ ETAPS 2015: solution to challenge 2

parent 1128d7bb
(**
{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
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="6" memlimit="1000"/>
<prover id="1" name="Z3" version="4.3.1" timelimit="6" memlimit="1000"/>
<prover id="2" name="Spass" version="3.7" timelimit="6" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
<prover id="4" name="Vampire" version="0.6" timelimit="6" memlimit="1000"/>
<file name="../verifythis_2015_parallel_gcd.mlw" expanded="true">
<theory name="ParallelGCD" sum="8319d7f76f67ab787192d931e1a55949" expanded="true">
<goal name="gcd_sub" expanded="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="WP_parameter parallel_gcd" expl="VC for parallel_gcd" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="WP_parameter parallel_gcd.1" expl="1. loop invariant init">
<proof prover="3"><result status="valid" time="0.01" steps="2"/></proof>
</goal>
<goal name="WP_parameter parallel_gcd.2" expl="2. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter parallel_gcd.3" expl="3. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.03" steps="21"/></proof>
<proof prover="4"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="WP_parameter parallel_gcd.4" expl="4. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter parallel_gcd.5" expl="5. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.02" steps="10"/></proof>
</goal>
<goal name="WP_parameter parallel_gcd.6" expl="6. loop invariant preservation">
<proof prover="3"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter parallel_gcd.7" expl="7. loop invariant preservation" expanded="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<proof prover="2" timelimit="30"><result status="valid" time="0.09"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="13"/></proof>
<proof prover="4" timelimit="30"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="WP_parameter parallel_gcd.8" expl="8. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="WP_parameter parallel_gcd.9" expl="9. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01"/></proof>
<proof prover="1"><result status="valid" time="0.00"/></proof>
<proof prover="3"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="WP_parameter parallel_gcd.10" expl="10. postcondition" expanded="true">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment