verifythis_2015_parallel_gcd: documentation and updated session

parent 9369e246
......@@ -107,7 +107,10 @@ module ParallelGCD
end
(** Threads interleaving.
Code and invariants by Rustan Leino. *)
Code and invariants by Rustan Leino.
Termination argument by Martin Clochard and Léon Gondelman.
Proof by Martin Clochard and Léon Gondelman.
*)
module Interleaving
use import int.Int
......@@ -118,7 +121,7 @@ module Interleaving
(* Representation of a thread: two local variables
(register copies of the globals) and a program counter:
ReadA:
local_a <- a
ReadB:
......@@ -128,7 +131,7 @@ module Interleaving
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)
......@@ -154,12 +157,12 @@ module Interleaving
| 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) =
(* 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
function state_index (s: state) : int = match s with
| ReadA -> 7
| ReadB -> 5
| Compare -> 3
......@@ -167,31 +170,32 @@ module Interleaving
end
(* Synchronisation status. *)
predicate sync (th:thread) (b:int) =
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 =
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 =
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 switch to a thread,
it also writes down the time remaining before it switch to the other.
If it does not switch, this timeout decrease. *)
(* 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 }
writes { scheduled, timer }
ensures { !scheduled = old !scheduled -> 0 <= !timer < old !timer }
ensures { result = !scheduled }
......@@ -201,8 +205,8 @@ module Interleaving
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 ->
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
......@@ -234,17 +238,26 @@ module Interleaving
let th2 = create_thread () in
while th1.state <> Halt || th2.state <> Halt do
invariant { inv th1 d !a !b /\ inv th2 d !b !a }
variant { !a + !b ,
variant { (* global progress in the algorithm *)
!a + !b
,
(* progress in one of the two threads *)
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 ,
else prog_index th1 !b
,
(* no progress in both threads, but the scheduler
switches to the non-progressing thread *)
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 , !timer }
else 0
,
(* 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
......
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