Skip to content

Commit 36c3942

Browse files
jspdiumjspdium
committed
new example leaderElectBroadcast and changes to counter. New solver versions used
1 parent a690a09 commit 36c3942

File tree

4 files changed

+321
-0
lines changed

4 files changed

+321
-0
lines changed

‎examples/leaderElection/leaderElectBroadcast.mlw

+180
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,180 @@
1+
2+
(* Very simple maximum algorithm.
3+
Nodes want to agree on the maximum id in a network.
4+
For this they broadcast their ids and keep locally
5+
the maximum received so far.
6+
Apparently it is not an implementation of leaderElectMax,
7+
since there is no way for a node to know that it holds
8+
the maximum id (because it doesn't know when the broadcast
9+
has ended).
10+
However, this *can* be mapped to leaderElectMax, because the
11+
refinement mapping has that information: if no more messages
12+
can be received and the node's maximum is its own id, then
13+
it is the maximum.
14+
The refinement shows that this will be true for at most one node.
15+
16+
17+
*)
18+
19+
20+
module BroadcastLeaderElect
21+
22+
use int.Int
23+
use int.EuclideanDivision
24+
use list.List
25+
use list.Mem
26+
use list.Append
27+
use list.HdTlNoOpt
28+
use map.Map
29+
30+
use leaderElect.LeaderElect
31+
use leaderElectMax.LeaderElectMax
32+
33+
(* Messages
34+
*)
35+
type msg = id
36+
37+
(* System configurations
38+
*)
39+
type world = { value : map node id ;
40+
sent : map node bool ;
41+
inMsgs : map node (list msg) }
42+
43+
let rec lemma list_hd (l : list int)
44+
ensures { not is_nil l -> mem (hd l) l }
45+
= match l with
46+
| Nil -> ()
47+
| Cons _ t -> list_hd t
48+
end
49+
50+
51+
52+
(* System INIT
53+
*)
54+
predicate initWorld_p (w:world) =
55+
forall n :node. 0<=n<n_nodes ->
56+
w.inMsgs[n] = Nil
57+
/\
58+
w.sent[n] = false
59+
/\
60+
w.value[n] = id n
61+
62+
63+
let ghost predicate initWorld (w:world)
64+
= initWorld_p w
65+
66+
67+
68+
69+
(* Refinement mapping
70+
*)
71+
(* Node k will not receive more messages
72+
*)
73+
predicate finalNd (w:world) (k:node) =
74+
(forall n :node. 0<=n<n_nodes -> n<>k -> w.sent[n]) /\ is_nil w.inMsgs[k]
75+
76+
let ghost function refn (w:world) : LeaderElectMax.world
77+
= { isMax = fun (n:node) -> 0<=n<n_nodes && finalNd w n && w.value[n] = id n }
78+
79+
80+
81+
82+
(* Inductive invariant
83+
*)
84+
predicate inv (w:world) =
85+
(forall n :node. 0<=n<n_nodes -> id n <= w.value[n] <= id maxId_global)
86+
/\
87+
(forall n :node, m :msg . 0<=n<n_nodes -> mem m w.inMsgs[n] ->
88+
m <= id maxId_global)
89+
/\
90+
(forall k :node. 0<=k<n_nodes /\ w.sent[maxId_global] ->
91+
w.value[k] = id maxId_global \/ mem (id maxId_global) w.inMsgs[k])
92+
93+
94+
(* System actions
95+
*)
96+
let rec ghost function broadcast (w:world) (n:int) (sndr:node) : map node (list msg)
97+
requires { 0<=n<=n_nodes /\ 0<=sndr<n_nodes }
98+
ensures { forall k:int. 0<=k<n -> k<>sndr -> result[k] = w.inMsgs[k] ++ Cons (id sndr) Nil }
99+
ensures { result[sndr] = w.inMsgs[sndr] }
100+
ensures { forall k:int. k<0 \/ n<=k -> result[k] = w.inMsgs[k] }
101+
variant { n }
102+
= if n=0 then w.inMsgs
103+
else let inb = broadcast w (n-1) sndr
104+
in if sndr = n-1 then inb
105+
else inb[n-1 <- inb[n-1] ++ Cons (id sndr) Nil]
106+
107+
108+
109+
predicate send_enbld (w:world) (h:node) =
110+
0 <= h < n_nodes /\ not w.sent[h]
111+
112+
let ghost function send (w:world) (h:node) : world
113+
requires { send_enbld w h }
114+
ensures { inv w -> inv result }
115+
ensures { inv w -> refn result = refn w }
116+
= { value = w.value ;
117+
sent = w.sent[h<-true] ;
118+
inMsgs = broadcast w n_nodes h }
119+
120+
121+
122+
predicate rcv_enbld (w:world) (h:node) =
123+
0 <= h < n_nodes /\ not is_nil w.inMsgs[h]
124+
125+
let ghost function rcv (w:world) (h:node) : world
126+
requires { rcv_enbld w h }
127+
ensures { inv w -> inv result }
128+
ensures { inv w -> finalNd result h /\ h=maxId_global -> refn result = LeaderElectMax.act (refn w) h }
129+
ensures { inv w -> refn result = refn w
130+
\/ LeaderElectMax.stepind (refn w) (refn result) }
131+
= match w.inMsgs[h] with
132+
| Nil -> absurd
133+
| Cons m t ->
134+
let max = if m > w.value[h] then m else w.value[h]
135+
in { value = w.value[h<-max] ;
136+
sent = w.sent ;
137+
inMsgs = w.inMsgs[h<-t] }
138+
end
139+
140+
141+
(* Transition relation
142+
*)
143+
inductive stepind world world =
144+
| send_msg : forall w :world, n :node.
145+
send_enbld w n -> stepind w (send w n)
146+
| rcv_msg : forall w :world, n :node.
147+
rcv_enbld w n -> stepind w (rcv w n)
148+
149+
let ghost predicate step (w1:world) (w2:world) = stepind w1 w2
150+
151+
152+
153+
154+
(* Proof of refinement
155+
*)
156+
clone refinement.Refinement with
157+
type worldC=world, type worldA=LeaderElectMax.world, val refn,
158+
predicate invC=inv, predicate invA=LeaderElectMax.inv,
159+
val initWorldC=initWorld, val initWorldA=LeaderElectMax.initWorld,
160+
val stepC=step, val stepA=LeaderElectMax.step
161+
162+
163+
(* Safety Property
164+
*)
165+
goal uniqueMax : forall w :world, i j :node.
166+
0<=i<n_nodes /\ 0<=j<n_nodes /\ reachableC w
167+
/\ (refn w).isMax[i] /\ (refn w).isMax[j]-> i=j
168+
169+
170+
171+
(* This property does not depend on refinement
172+
*)
173+
goal correctness :
174+
forall w :world. reachableC w ->
175+
forall n :node. 0<=n<n_nodes -> finalNd w n -> w.value[n] = id maxId_global
176+
177+
178+
179+
180+
end

‎examples/leaderElection/leaderElectBroadcast/why3session.xml

+139
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,139 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
3+
"https://www.why3.org/why3session.dtd">
4+
<why3session shape_version="6">
5+
<prover id="0" name="Z3" version="4.11.2" timelimit="2000" steplimit="0" memlimit="5000"/>
6+
<prover id="1" name="CVC5" version="1.0.3" timelimit="2000" steplimit="0" memlimit="5000"/>
7+
<prover id="2" name="CVC4" version="1.8" timelimit="5" steplimit="0" memlimit="1000"/>
8+
<prover id="3" name="Alt-Ergo" version="2.5.3" timelimit="5" steplimit="0" memlimit="1000"/>
9+
<prover id="5" name="Alt-Ergo" version="2.4.2" timelimit="1" steplimit="0" memlimit="1000"/>
10+
<file format="whyml" proved="true">
11+
<path name=".."/><path name="leaderElectBroadcast.mlw"/>
12+
<theory name="BroadcastLeaderElect" proved="true">
13+
<goal name="list_hd&#39;vc" expl="VC for list_hd" proved="true">
14+
<proof prover="2"><result status="valid" time="0.025132" steps="14399"/></proof>
15+
</goal>
16+
<goal name="refn&#39;vc" expl="VC for refn" proved="true">
17+
<proof prover="5"><result status="valid" time="0.008401" steps="4"/></proof>
18+
</goal>
19+
<goal name="broadcast&#39;vc" expl="VC for broadcast" proved="true">
20+
<proof prover="5"><result status="valid" time="0.061115" steps="990"/></proof>
21+
</goal>
22+
<goal name="send&#39;vc" expl="VC for send" proved="true">
23+
<transf name="unfold" proved="true" arg1="inv">
24+
<goal name="send&#39;vc.0" expl="VC for send" proved="true">
25+
<transf name="split_vc" proved="true" >
26+
<goal name="send&#39;vc.0.0" expl="precondition" proved="true">
27+
<proof prover="5"><result status="valid" time="0.009863" steps="18"/></proof>
28+
</goal>
29+
<goal name="send&#39;vc.0.1" expl="postcondition" proved="true">
30+
<proof prover="2"><result status="valid" time="0.980557" steps="155076"/></proof>
31+
</goal>
32+
<goal name="send&#39;vc.0.2" expl="postcondition" proved="true">
33+
<transf name="split_vc" proved="true" >
34+
<goal name="send&#39;vc.0.2.0" expl="postcondition" proved="true">
35+
<transf name="inline_goal" proved="true" >
36+
<goal name="send&#39;vc.0.2.0.0" expl="postcondition" proved="true">
37+
<transf name="split_all_full" proved="true" >
38+
<goal name="send&#39;vc.0.2.0.0.0" expl="postcondition" proved="true">
39+
<transf name="split_vc" proved="true" >
40+
<goal name="send&#39;vc.0.2.0.0.0.0" expl="postcondition" proved="true">
41+
<proof prover="1"><result status="valid" time="1.412037" steps="159045"/></proof>
42+
</goal>
43+
</transf>
44+
</goal>
45+
</transf>
46+
</goal>
47+
</transf>
48+
</goal>
49+
</transf>
50+
</goal>
51+
</transf>
52+
</goal>
53+
</transf>
54+
</goal>
55+
<goal name="rcv&#39;vc" expl="VC for rcv" proved="true">
56+
<transf name="unfold" proved="true" arg1="inv">
57+
<goal name="rcv&#39;vc.0" expl="VC for rcv" proved="true">
58+
<transf name="split_vc" proved="true" >
59+
<goal name="rcv&#39;vc.0.0" expl="unreachable point" proved="true">
60+
<proof prover="5"><result status="valid" time="0.012493" steps="58"/></proof>
61+
</goal>
62+
<goal name="rcv&#39;vc.0.1" expl="postcondition" proved="true">
63+
<transf name="split_vc" proved="true" >
64+
<goal name="rcv&#39;vc.0.1.0" expl="postcondition" proved="true">
65+
<proof prover="5"><result status="valid" time="0.271970" steps="2341"/></proof>
66+
</goal>
67+
<goal name="rcv&#39;vc.0.1.1" expl="postcondition" proved="true">
68+
<proof prover="5" timelimit="5"><result status="valid" time="1.190913" steps="9639"/></proof>
69+
</goal>
70+
<goal name="rcv&#39;vc.0.1.2" expl="postcondition" proved="true">
71+
<proof prover="2" timelimit="1"><result status="valid" time="0.420299" steps="76659"/></proof>
72+
</goal>
73+
<goal name="rcv&#39;vc.0.1.3" expl="postcondition" proved="true">
74+
<proof prover="2"><result status="valid" time="0.244719" steps="53447"/></proof>
75+
</goal>
76+
</transf>
77+
</goal>
78+
<goal name="rcv&#39;vc.0.2" expl="postcondition" proved="true">
79+
<proof prover="2"><result status="valid" time="0.684776" steps="131442"/></proof>
80+
</goal>
81+
<goal name="rcv&#39;vc.0.3" expl="postcondition" proved="true">
82+
<transf name="split_vc" proved="true" >
83+
<goal name="rcv&#39;vc.0.3.0" expl="postcondition" proved="true">
84+
<transf name="split_vc" proved="true" >
85+
<goal name="rcv&#39;vc.0.3.0.0" expl="postcondition" proved="true">
86+
<transf name="inline_goal" proved="true" >
87+
<goal name="rcv&#39;vc.0.3.0.0.0" expl="postcondition" proved="true">
88+
<transf name="split_all_full" proved="true" >
89+
<goal name="rcv&#39;vc.0.3.0.0.0.0" expl="postcondition" proved="true">
90+
<transf name="split_vc" proved="true" >
91+
<goal name="rcv&#39;vc.0.3.0.0.0.0.0" expl="postcondition" proved="true">
92+
<proof prover="2"><result status="valid" time="0.203600" steps="53216"/></proof>
93+
</goal>
94+
</transf>
95+
</goal>
96+
</transf>
97+
</goal>
98+
</transf>
99+
</goal>
100+
<goal name="rcv&#39;vc.0.3.0.1" expl="postcondition" proved="true">
101+
<transf name="inline_goal" proved="true" >
102+
<goal name="rcv&#39;vc.0.3.0.1.0" expl="postcondition" proved="true">
103+
<transf name="split_all_full" proved="true" >
104+
<goal name="rcv&#39;vc.0.3.0.1.0.0" expl="postcondition" proved="true">
105+
<proof prover="2" timelimit="2000" memlimit="5000"><result status="valid" time="0.274309" steps="65001"/></proof>
106+
</goal>
107+
</transf>
108+
</goal>
109+
</transf>
110+
</goal>
111+
</transf>
112+
</goal>
113+
</transf>
114+
</goal>
115+
</transf>
116+
</goal>
117+
</transf>
118+
</goal>
119+
<goal name="Refinement.initWorldA&#39;refn&#39;vc" expl="VC for initWorldA&#39;refn" proved="true">
120+
<proof prover="3"><result status="valid" time="0.027047" steps="75"/></proof>
121+
</goal>
122+
<goal name="Refinement.initWorldC&#39;refn&#39;vc" expl="VC for initWorldC&#39;refn" proved="true">
123+
<proof prover="5" timelimit="2000" memlimit="5000"><result status="valid" time="2.316975" steps="21473"/></proof>
124+
</goal>
125+
<goal name="Refinement.stepA&#39;refn&#39;vc" expl="VC for stepA&#39;refn" proved="true">
126+
<proof prover="5" timelimit="2000" memlimit="5000"><result status="valid" time="0.015098" steps="85"/></proof>
127+
</goal>
128+
<goal name="Refinement.stepC&#39;refn&#39;vc" expl="VC for stepC&#39;refn" proved="true">
129+
<proof prover="0"><result status="valid" time="0.023008" steps="58153"/></proof>
130+
</goal>
131+
<goal name="uniqueMax" proved="true">
132+
<proof prover="5" timelimit="5"><result status="valid" time="0.025206" steps="252"/></proof>
133+
</goal>
134+
<goal name="correctness" proved="true">
135+
<proof prover="5" timelimit="2000" memlimit="5000"><result status="valid" time="0.237209" steps="2742"/></proof>
136+
</goal>
137+
</theory>
138+
</file>
139+
</why3session>

‎examples/leaderElection/leaderElectBroadcast/why3shapes.gz

5.11 KB
Binary file not shown.

‎replay.sh

+2
Original file line numberDiff line numberDiff line change
@@ -60,6 +60,8 @@ echo "## ChangRoberts"
6060
why3 replay examples/leaderElection/ChangRoberts -L stateMachineModels -L examples/leaderElection
6161
echo "## ChangRobertsNetwork"
6262
why3 replay examples/leaderElection/ChangRobertsNetwork -L stateMachineModels -L examples/leaderElection
63+
echo "## leaderElectBroadcast"
64+
why3 replay examples/leaderElection/leaderElectBroadcast -L stateMachineModels -L examples/leaderElection
6365
echo "--------------------------------"
6466

6567
echo "# examples/mutualExclusionToken"

0 commit comments

Comments
 (0)