Skip to content

Commit

Permalink
new example leaderElectBroadcast and changes to counter. New solver v…
Browse files Browse the repository at this point in the history 
…ersions used
  • Loading branch information
@jspdium
jspdium committed Jun 11, 2024
1 parent a690a09 commit 36c3942
Show file tree
Hide file tree
Showing 4 changed files with 321 additions and 0 deletions.
180 changes: 180 additions & 0 deletions examples/leaderElection/leaderElectBroadcast.mlw
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,180 @@

(* Very simple maximum algorithm.
Nodes want to agree on the maximum id in a network.
For this they broadcast their ids and keep locally
the maximum received so far.
Apparently it is not an implementation of leaderElectMax,
since there is no way for a node to know that it holds
the maximum id (because it doesn't know when the broadcast
has ended).
However, this *can* be mapped to leaderElectMax, because the
refinement mapping has that information: if no more messages
can be received and the node's maximum is its own id, then
it is the maximum.
The refinement shows that this will be true for at most one node.


*)


module BroadcastLeaderElect

use int.Int
use int.EuclideanDivision
use list.List
use list.Mem
use list.Append
use list.HdTlNoOpt
use map.Map

use leaderElect.LeaderElect
use leaderElectMax.LeaderElectMax

(* Messages
*)
type msg = id

(* System configurations
*)
type world = { value : map node id ;
sent : map node bool ;
inMsgs : map node (list msg) }

let rec lemma list_hd (l : list int)
ensures { not is_nil l -> mem (hd l) l }
= match l with
| Nil -> ()
| Cons _ t -> list_hd t
end



(* System INIT
*)
predicate initWorld_p (w:world) =
forall n :node. 0<=n<n_nodes ->
w.inMsgs[n] = Nil
/\
w.sent[n] = false
/\
w.value[n] = id n


let ghost predicate initWorld (w:world)
= initWorld_p w




(* Refinement mapping
*)
(* Node k will not receive more messages
*)
predicate finalNd (w:world) (k:node) =
(forall n :node. 0<=n<n_nodes -> n<>k -> w.sent[n]) /\ is_nil w.inMsgs[k]

let ghost function refn (w:world) : LeaderElectMax.world
= { isMax = fun (n:node) -> 0<=n<n_nodes && finalNd w n && w.value[n] = id n }




(* Inductive invariant
*)
predicate inv (w:world) =
(forall n :node. 0<=n<n_nodes -> id n <= w.value[n] <= id maxId_global)
/\
(forall n :node, m :msg . 0<=n<n_nodes -> mem m w.inMsgs[n] ->
m <= id maxId_global)
/\
(forall k :node. 0<=k<n_nodes /\ w.sent[maxId_global] ->
w.value[k] = id maxId_global \/ mem (id maxId_global) w.inMsgs[k])


(* System actions
*)
let rec ghost function broadcast (w:world) (n:int) (sndr:node) : map node (list msg)
requires { 0<=n<=n_nodes /\ 0<=sndr<n_nodes }
ensures { forall k:int. 0<=k<n -> k<>sndr -> result[k] = w.inMsgs[k] ++ Cons (id sndr) Nil }
ensures { result[sndr] = w.inMsgs[sndr] }
ensures { forall k:int. k<0 \/ n<=k -> result[k] = w.inMsgs[k] }
variant { n }
= if n=0 then w.inMsgs
else let inb = broadcast w (n-1) sndr
in if sndr = n-1 then inb
else inb[n-1 <- inb[n-1] ++ Cons (id sndr) Nil]



predicate send_enbld (w:world) (h:node) =
0 <= h < n_nodes /\ not w.sent[h]

let ghost function send (w:world) (h:node) : world
requires { send_enbld w h }
ensures { inv w -> inv result }
ensures { inv w -> refn result = refn w }
= { value = w.value ;
sent = w.sent[h<-true] ;
inMsgs = broadcast w n_nodes h }



predicate rcv_enbld (w:world) (h:node) =
0 <= h < n_nodes /\ not is_nil w.inMsgs[h]

let ghost function rcv (w:world) (h:node) : world
requires { rcv_enbld w h }
ensures { inv w -> inv result }
ensures { inv w -> finalNd result h /\ h=maxId_global -> refn result = LeaderElectMax.act (refn w) h }
ensures { inv w -> refn result = refn w
\/ LeaderElectMax.stepind (refn w) (refn result) }
= match w.inMsgs[h] with
| Nil -> absurd
| Cons m t ->
let max = if m > w.value[h] then m else w.value[h]
in { value = w.value[h<-max] ;
sent = w.sent ;
inMsgs = w.inMsgs[h<-t] }
end


(* Transition relation
*)
inductive stepind world world =
| send_msg : forall w :world, n :node.
send_enbld w n -> stepind w (send w n)
| rcv_msg : forall w :world, n :node.
rcv_enbld w n -> stepind w (rcv w n)

let ghost predicate step (w1:world) (w2:world) = stepind w1 w2




(* Proof of refinement
*)
clone refinement.Refinement with
type worldC=world, type worldA=LeaderElectMax.world, val refn,
predicate invC=inv, predicate invA=LeaderElectMax.inv,
val initWorldC=initWorld, val initWorldA=LeaderElectMax.initWorld,
val stepC=step, val stepA=LeaderElectMax.step


(* Safety Property
*)
goal uniqueMax : forall w :world, i j :node.
0<=i<n_nodes /\ 0<=j<n_nodes /\ reachableC w
/\ (refn w).isMax[i] /\ (refn w).isMax[j]-> i=j



(* This property does not depend on refinement
*)
goal correctness :
forall w :world. reachableC w ->
forall n :node. 0<=n<n_nodes -> finalNd w n -> w.value[n] = id maxId_global




end
139 changes: 139 additions & 0 deletions examples/leaderElection/leaderElectBroadcast/why3session.xml
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,139 @@
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"https://www.why3.org/why3session.dtd">
<why3session shape_version="6">
<prover id="0" name="Z3" version="4.11.2" timelimit="2000" steplimit="0" memlimit="5000"/>
<prover id="1" name="CVC5" version="1.0.3" timelimit="2000" steplimit="0" memlimit="5000"/>
<prover id="2" name="CVC4" version="1.8" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="2.5.3" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="2.4.2" timelimit="1" steplimit="0" memlimit="1000"/>
<file format="whyml" proved="true">
<path name=".."/><path name="leaderElectBroadcast.mlw"/>
<theory name="BroadcastLeaderElect" proved="true">
<goal name="list_hd&#39;vc" expl="VC for list_hd" proved="true">
<proof prover="2"><result status="valid" time="0.025132" steps="14399"/></proof>
</goal>
<goal name="refn&#39;vc" expl="VC for refn" proved="true">
<proof prover="5"><result status="valid" time="0.008401" steps="4"/></proof>
</goal>
<goal name="broadcast&#39;vc" expl="VC for broadcast" proved="true">
<proof prover="5"><result status="valid" time="0.061115" steps="990"/></proof>
</goal>
<goal name="send&#39;vc" expl="VC for send" proved="true">
<transf name="unfold" proved="true" arg1="inv">
<goal name="send&#39;vc.0" expl="VC for send" proved="true">
<transf name="split_vc" proved="true" >
<goal name="send&#39;vc.0.0" expl="precondition" proved="true">
<proof prover="5"><result status="valid" time="0.009863" steps="18"/></proof>
</goal>
<goal name="send&#39;vc.0.1" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.980557" steps="155076"/></proof>
</goal>
<goal name="send&#39;vc.0.2" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="send&#39;vc.0.2.0" expl="postcondition" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="send&#39;vc.0.2.0.0" expl="postcondition" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="send&#39;vc.0.2.0.0.0" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="send&#39;vc.0.2.0.0.0.0" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="1.412037" steps="159045"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="rcv&#39;vc" expl="VC for rcv" proved="true">
<transf name="unfold" proved="true" arg1="inv">
<goal name="rcv&#39;vc.0" expl="VC for rcv" proved="true">
<transf name="split_vc" proved="true" >
<goal name="rcv&#39;vc.0.0" expl="unreachable point" proved="true">
<proof prover="5"><result status="valid" time="0.012493" steps="58"/></proof>
</goal>
<goal name="rcv&#39;vc.0.1" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="rcv&#39;vc.0.1.0" expl="postcondition" proved="true">
<proof prover="5"><result status="valid" time="0.271970" steps="2341"/></proof>
</goal>
<goal name="rcv&#39;vc.0.1.1" expl="postcondition" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="1.190913" steps="9639"/></proof>
</goal>
<goal name="rcv&#39;vc.0.1.2" expl="postcondition" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.420299" steps="76659"/></proof>
</goal>
<goal name="rcv&#39;vc.0.1.3" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.244719" steps="53447"/></proof>
</goal>
</transf>
</goal>
<goal name="rcv&#39;vc.0.2" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.684776" steps="131442"/></proof>
</goal>
<goal name="rcv&#39;vc.0.3" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="rcv&#39;vc.0.3.0" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="rcv&#39;vc.0.3.0.0" expl="postcondition" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="rcv&#39;vc.0.3.0.0.0" expl="postcondition" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="rcv&#39;vc.0.3.0.0.0.0" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="rcv&#39;vc.0.3.0.0.0.0.0" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.203600" steps="53216"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="rcv&#39;vc.0.3.0.1" expl="postcondition" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="rcv&#39;vc.0.3.0.1.0" expl="postcondition" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="rcv&#39;vc.0.3.0.1.0.0" expl="postcondition" proved="true">
<proof prover="2" timelimit="2000" memlimit="5000"><result status="valid" time="0.274309" steps="65001"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="Refinement.initWorldA&#39;refn&#39;vc" expl="VC for initWorldA&#39;refn" proved="true">
<proof prover="3"><result status="valid" time="0.027047" steps="75"/></proof>
</goal>
<goal name="Refinement.initWorldC&#39;refn&#39;vc" expl="VC for initWorldC&#39;refn" proved="true">
<proof prover="5" timelimit="2000" memlimit="5000"><result status="valid" time="2.316975" steps="21473"/></proof>
</goal>
<goal name="Refinement.stepA&#39;refn&#39;vc" expl="VC for stepA&#39;refn" proved="true">
<proof prover="5" timelimit="2000" memlimit="5000"><result status="valid" time="0.015098" steps="85"/></proof>
</goal>
<goal name="Refinement.stepC&#39;refn&#39;vc" expl="VC for stepC&#39;refn" proved="true">
<proof prover="0"><result status="valid" time="0.023008" steps="58153"/></proof>
</goal>
<goal name="uniqueMax" proved="true">
<proof prover="5" timelimit="5"><result status="valid" time="0.025206" steps="252"/></proof>
</goal>
<goal name="correctness" proved="true">
<proof prover="5" timelimit="2000" memlimit="5000"><result status="valid" time="0.237209" steps="2742"/></proof>
</goal>
</theory>
</file>
</why3session>
Binary file added examples/leaderElection/leaderElectBroadcast/why3shapes.gz
View file
Binary file not shown.
2 changes: 2 additions & 0 deletions replay.sh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,8 @@ echo "## ChangRoberts"
why3 replay examples/leaderElection/ChangRoberts -L stateMachineModels -L examples/leaderElection
echo "## ChangRobertsNetwork"
why3 replay examples/leaderElection/ChangRobertsNetwork -L stateMachineModels -L examples/leaderElection
echo "## leaderElectBroadcast"
why3 replay examples/leaderElection/leaderElectBroadcast -L stateMachineModels -L examples/leaderElection
echo "--------------------------------"

echo "# examples/mutualExclusionToken"
Expand Down

0 comments on commit 36c3942

Please sign in to comment.