verifythis_2015_parallel_gcd: threads interleaving by Rustan

in comments for the moment, until I find time to prove it
parent d01e5acf
......@@ -105,3 +105,77 @@ module ParallelGCD
!a
end
(** Threads interleaving.
Code and invariants by Rustan Leino. *)
(***
module Interleaving
use import int.Int
use import number.Gcd
use import ref.Ref
lemma gcd_sub: forall a b: int. gcd a b = gcd a (b - a)
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;
}
predicate inv (th: thread) (a0 b0 a b: int) =
0 < a /\ 0 < b /\ gcd a b = gcd a0 b0 /\
match th.state with
| ReadA -> true
| ReadB -> th.local_a = a
| Compare -> th.local_a = a && b <= th.local_b &&
(th.local_b <= th.local_a -> th.local_b = b)
| Halt -> th.local_a = a = b
end
val create_thread () : thread
ensures { result.state = ReadA }
let step (th: thread) (ghost a0 b0: int) (a b: ref int)
requires { inv th a0 b0 !a !b }
writes { th, a }
ensures { inv th a0 b0 !a !b }
ensures { 0 < !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 parallel_gcd (a0 b0: int) : int
requires { 0 < a0 /\ 0 < b0 }
diverges
ensures { result = gcd a0 b0 }
=
(* shared variables *)
let a = ref a0 in
let b = ref b0 in
(* two threads *)
let th1 = create_thread () in
let th2 = create_thread () in
while th1.state <> Halt || th2.state <> Halt do
invariant { inv th1 a0 b0 !a !b /\ inv th2 b0 a0 !b !a }
if any bool then step th1 a0 b0 a b else step th2 b0 a0 b a
done;
!a
end
***)
......@@ -8,20 +8,20 @@
<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">
<theory name="ParallelGCD" sum="8319d7f76f67ab787192d931e1a55949">
<goal name="gcd_sub">
<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" expl="VC for parallel_gcd">
<transf name="split_goal_wp">
<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">
<goal name="WP_parameter parallel_gcd.3" expl="3. loop invariant preservation">
<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>
......@@ -36,7 +36,7 @@
<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">
<goal name="WP_parameter parallel_gcd.7" expl="7. loop invariant preservation">
<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>
......@@ -52,7 +52,7 @@
<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">
<goal name="WP_parameter parallel_gcd.10" expl="10. postcondition">
<proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
......
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