 Algorithmique Numérique Distribuée Public GIT Repository
1 ---- MODULE simix_network ----
2 (* This is a TLA module specifying the networking layer of SIMIX.
3    It is used to verify the soundness of the DPOR reduction algorithm
4    used in the model-checker.
6    If you think you found a new independence lemma, add it to this
7    file and relaunch TLC to check whether your lemma actually holds.
8    *)
9 EXTENDS Naturals, Sequences, FiniteSets
10 CONSTANTS RdV, Addr, Proc, ValTrue, ValFalse, SendIns, RecvIns, WaitIns,
11           TestIns, LocalIns
12 VARIABLES network, memory, pc
14 NoProc == CHOOSE p : p \notin Proc
17 Partition(S) == \forall x,y \in S : x \cap y /= {} => x = y
19 Comm == [id:Nat,
20          rdv:RdV,
22          src:Proc,
23          dst:Proc,
27 ASSUME ValTrue \in Nat
28 ASSUME ValFalse \in Nat
30 (* The set of all the instructions *)
31 ASSUME Partition({SendIns, RecvIns, WaitIns, TestIns, LocalIns})
32 Instr == UNION {SendIns, RecvIns, WaitIns, TestIns, LocalIns}
34 ------------------------------------------
35 (* Independence operator *)
36 I(A,B) == ENABLED A /\ ENABLED B => /\ A => (ENABLED B)'
37                                     /\ B => (ENABLED A)'
38                                     /\ A \cdot B \equiv B \cdot A
40 (* Initially there are no messages in the network and the memory can have anything in their memories *)
41 Init == /\ network = {}
42         /\ memory \in [Proc -> [Addr -> Nat]]
43         /\ pc = CHOOSE f : f \in [Proc -> Instr]
45 (* Let's keep everything in the right domains *)
46 TypeInv == /\ network \subseteq Comm
47            /\ memory \in [Proc -> [Addr -> Nat]]
48            /\ pc \in [Proc -> Instr]
50 (* The set of all communications waiting at rdv *)
51 mailbox(rdv) == {comm \in network : comm.rdv=rdv /\ comm.status \in {"send","recv"}}
53 (* The set of memory addresses of a process being used in a communication *)
54 CommBuffers(pid) ==
55   {c.data_src: c \in { y \in network: y.status /= "done" /\ (y.src = pid \/ y.dst = pid)}}
56 \cup {c.data_dst: c \in { y \in network: y.status /= "done" /\ (y.src = pid \/ y.dst = pid)}}
58 (* This is a send step of the system *)
59 (* pid: the process ID of the sender *)
60 (* rdv: the rendez-vous point where the "send" communication request is going to be pushed *)
61 (* data_r: the address in the sender's memory where the data is stored *)
62 (* comm_r: the address in the sender's memory where to store the communication id *)
63 Send(pid, rdv, data_r, comm_r) ==
64   /\ rdv \in RdV
65   /\ pid \in Proc
68   /\ pc[pid] \in SendIns
70      (* A matching recv request exists in the rendez-vous *)
71      (* Complete the sender fields and set the communication to the ready state *)
72   /\ \/ \exists c \in mailbox(rdv):
73           /\ c.status="recv"
74           /\ \forall d \in mailbox(rdv): d.status="recv" => c.id <= d.id
75           /\ network' =
76                (network \ {c}) \cup {[c EXCEPT
78                                        !.src = pid,
79                                        !.data_src = data_r]}
80           (* Use c's existing communication id *)
81           /\ memory' = [memory EXCEPT ![pid][comm_r] = c.id]
84      (* No matching recv communication request exists. *)
85      (* Create a send request and push it in the network. *)
86      \/ /\ ~ \exists c \in mailbox(rdv): c.status = "recv"
87         /\ LET comm ==
88                  [id |-> Cardinality(network)+1,
89                   rdv |-> rdv,
90                   status |-> "send",
91                   src |-> pid,
92                   dst |-> NoProc,
93                   data_src |-> data_r,
95            IN
96              /\ network' = network \cup {comm}
97              /\ memory' = [memory EXCEPT ![pid][comm_r] = comm.id]
98   /\ \E ins \in Instr : pc' = [pc EXCEPT ![pid] = ins]
100 (* This is a receive step of the system *)
101 (* pid: the process ID of the receiver *)
102 (* rdv: the Rendez-vous where the "receive" communication request is going to be pushed *)
103 (* data_r: the address in the receivers's memory where the data is going to be stored *)
104 (* comm_r: the address in the receivers's memory where to store the communication id *)
105 Recv(pid, rdv, data_r, comm_r) ==
106   /\ rdv \in RdV
107   /\ pid \in Proc
110   /\ pc[pid] \in RecvIns
112      (* A matching send request exists in the rendez-vous *)
113      (* Complete the receiver fields and set the communication to the ready state *)
114   /\ \/ \exists c \in mailbox(rdv):
115           /\ c.status="send"
116           /\ \forall d \in mailbox(rdv): d.status="send" => c.id <= d.id
117           /\ network' =
118                (network \ {c}) \cup {[c EXCEPT
120                                        !.dst = pid,
121                                        !.data_dst = data_r]}
122           (* Use c's existing communication id *)
123           /\ memory' = [memory EXCEPT ![pid][comm_r] = c.id]
126      (* No matching send communication request exists. *)
127      (* Create a recv request and push it in the network. *)
128      \/ /\ ~ \exists c \in mailbox(rdv): c.status = "send"
129         /\ LET comm ==
130                  [id |-> Cardinality(network)+1,
131                   status |-> "recv",
132                   dst |-> pid,
133                   data_dst |-> data_r]
134            IN
135              /\ network' = network \cup {comm}
136              /\ memory' = [memory EXCEPT ![pid][comm_r] = comm.id]
137   /\ \E ins \in Instr : pc' = [pc EXCEPT ![pid] = ins]
139 (* Wait for at least one communication from a given list to complete *)
140 (* pid: the process ID issuing the wait *)
141 (* comms: the list of addresses in the process's memory where the communication ids are stored *)
142 Wait(pid, comms) ==
144   /\ pid \in Proc
145   /\ pc[pid] \in WaitIns
146   /\ \E comm_r \in comms, c \in network: c.id = memory[pid][comm_r] /\
147      \/ /\ c.status = "ready"
148         /\ memory' = [memory EXCEPT ![c.dst][c.data_dst] = memory[c.src][c.data_src]]
149         /\ network' = (network \ {c}) \cup {[c EXCEPT !.status = "done"]}
150      \/ /\ c.status = "done"
151         /\ UNCHANGED <<memory,network>>
152   /\ \E ins \in Instr : pc' = [pc EXCEPT ![pid] = ins]
154 (* Test if at least one communication from a given list has completed *)
155 (* pid: the process ID issuing the wait *)
156 (* comms: the list of addresses in the process's memory where the communication ids are stored *)
157 (* ret_r: the address in the process's memory where the result is going to be stored *)
158 Test(pid, comms, ret_r) ==
161   /\ pid \in Proc
162   /\ pc[pid] \in TestIns
163   /\ \/ \E comm_r \in comms, c\in network: c.id = memory[pid][comm_r] /\
164         \/ /\ c.status = "ready"
165            /\ memory' = [memory EXCEPT ![c.dst][c.data_dst] = memory[c.src][c.data_src],
166                                         ![pid][ret_r] = ValTrue]
167            /\ network' = (network \ {c}) \cup {[c EXCEPT !.status = "done"]}
168         \/ /\ c.status = "done"
169            /\ memory' = [memory EXCEPT ![pid][ret_r] = ValTrue]
170            /\ UNCHANGED network
171      \/ ~ \exists comm_r \in comms, c \in network: c.id = memory[pid][comm_r]
173         /\ memory' = [memory EXCEPT ![pid][ret_r] = ValFalse]
174         /\ UNCHANGED network
175   /\ \E ins \in Instr : pc' = [pc EXCEPT ![pid] = ins]
177 (* Local instruction execution *)
178 Local(pid) ==
179     /\ pid \in Proc
180     /\ pc[pid] \in LocalIns
181     /\ memory' \in [Proc -> [Addr -> Nat]]
182     /\ \forall p \in Proc, a \in Addr: memory'[p][a] /= memory[p][a]
183        => p = pid /\ a \notin CommBuffers(pid)
184     /\ \E ins \in Instr : pc' = [pc EXCEPT ![pid] = ins]
185     /\ UNCHANGED network
187 Next == \exists p \in Proc, data_r \in Addr, comm_r \in Addr, rdv \in RdV,
188                 ret_r \in Addr, ids \in SUBSET network:
189           \/ Send(p, rdv, data_r, comm_r)
190           \/ Recv(p, rdv, data_r, comm_r)
191           \/ Wait(p, comm_r)
192           \/ Test(p, comm_r, ret_r)
193           \/ Local(p)
195 Spec == Init /\ [][Next]_<<network,memory>>
196 -------------------------------
197 (* Independence of iSend / iRecv steps *)
198 THEOREM \forall p1, p2 \in Proc: \forall rdv1, rdv2 \in RdV:
199         \forall data1, data2, comm1, comm2 \in Addr:
200         /\ p1 /= p2
201         /\ ENABLED Send(p1, rdv1, data1, comm1)
202         /\ ENABLED Recv(p2, rdv2, data2, comm2)
203         => I(Send(p1, rdv1, data1, comm1), Recv(p2, rdv2, data2, comm2))
205 (* Independence of iSend and Wait *)
206 THEOREM \forall p1, p2 \in Proc: \forall data, comm1, comm2 \in Addr:
207         \forall rdv \in RdV: \exists c \in network:
208         /\ p1 /= p2
209         /\ c.id = memory[p2][comm2]
210         /\ \/ (p1 /= c.dst /\ p1 /= c.src)
211            \/ (comm1 /= c.data_src /\ comm1 /= c.data_dst)
212         /\ ENABLED Send(p1, rdv, data, comm1)
213         /\ ENABLED Wait(p2, comm2)
214         => I(Send(p1, rdv, data, comm1), Wait(p2, comm2))
216 (* Independence of iSend's in different rendez-vous *)
217 THEOREM \forall p1, p2 \in Proc: \forall rdv1, rdv2 \in RdV:
218         \forall data1, data2, comm1, comm2 \in Addr:
219         /\ p1 /= p2
220         /\ rdv1 /= rdv2
221         /\ ENABLED Send(p1, rdv1, data1, comm1)
222         /\ ENABLED Send(p2, rdv2, data2, comm2)
223         => I(Send(p1, rdv1, data1, comm1),
224              Send(p2, rdv2, data2, comm2))
226 (* Independence of iRecv's in different rendez-vous *)
227 THEOREM \forall p1, p2 \in Proc: \forall rdv1, rdv2 \in RdV:
228         \forall data1, data2, comm1, comm2 \in Addr:
229         /\ p1 /= p2
230         /\ rdv1 /= rdv2
231         /\ ENABLED Recv(p1, rdv1, data1, comm1)
232         /\ ENABLED Recv(p2, rdv2, data2, comm2)
233         => I(Recv(p1, rdv1, data1, comm1),
234              Recv(p2, rdv2, data2, comm2))
236 (* Independence of Wait of different processes on the same comm *)
237 THEOREM \forall p1, p2 \in Proc: \forall comm1, comm2 \in Addr:
238         /\ p1 /= p2
239         /\ comm1 = comm2
240         /\ ENABLED Wait(p1, comm1)
241         /\ ENABLED Wait(p2, comm2)
242         => I(Wait(p1, comm1), Wait(p2, comm2))
243 ====
244 \* Generated at Thu Feb 18 13:49:35 CET 2010