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.
9 EXTENDS Naturals, Sequences, FiniteSets
10 CONSTANTS RdV, Addr, Proc, ValTrue, ValFalse, SendIns, RecvIns, WaitIns,
12 VARIABLES network, memory, pc
14 NoProc == CHOOSE p : p \notin Proc
15 NoAddr == CHOOSE a : a \notin Addr
17 Partition(S) == \forall x,y \in S : x \cap y /= {} => x = y
21 status:{"send","recv","ready","done"},
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)'
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 *)
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) ==
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):
74 /\ \forall d \in mailbox(rdv): d.status="recv" => c.id <= d.id
76 (network \ {c}) \cup {[c EXCEPT
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"
88 [id |-> Cardinality(network)+1,
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) ==
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):
116 /\ \forall d \in mailbox(rdv): d.status="send" => c.id <= d.id
118 (network \ {c}) \cup {[c EXCEPT
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"
130 [id |-> Cardinality(network)+1,
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 *)
143 /\ comms \subseteq Addr
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) ==
159 /\ comms \subseteq Addr
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]
171 \/ ~ \exists comm_r \in comms, c \in network: c.id = memory[pid][comm_r]
172 /\ c.status \in {"ready","done"}
173 /\ memory' = [memory EXCEPT ![pid][ret_r] = ValFalse]
175 /\ \E ins \in Instr : pc' = [pc EXCEPT ![pid] = ins]
177 (* Local instruction execution *)
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]
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)
192 \/ Test(p, comm_r, ret_r)
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:
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:
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:
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:
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:
240 /\ ENABLED Wait(p1, comm1)
241 /\ ENABLED Wait(p2, comm2)
242 => I(Wait(p1, comm1), Wait(p2, comm2))
244 \* Generated at Thu Feb 18 13:49:35 CET 2010