1 ---- MODULE simix_network ----
2 (* Copyright (c) 2012-2022. The SimGrid Team. All rights reserved. *)
4 (* This program is free software; you can redistribute it and/or modify it
5 * under the terms of the license (GNU LGPL) which comes with this package. *)
7 (* This is a TLA module specifying the networking layer of SIMIX.
8 It is used to verify the soundness of the DPOR reduction algorithm
9 used in the model-checker.
11 If you think you found a new independence lemma, add it to this
12 file and relaunch TLC to check whether your lemma actually holds.
14 EXTENDS Naturals, Sequences, FiniteSets
15 CONSTANTS RdV, Addr, Proc, ValTrue, ValFalse, SendIns, RecvIns, WaitIns,
17 VARIABLES network, memory, pc
19 NoProc == CHOOSE p : p \notin Proc
20 NoAddr == CHOOSE a : a \notin Addr
22 Partition(S) == \forall x,y \in S : x \cap y /= {} => x = y
26 status:{"send","recv","ready","done"},
32 ASSUME ValTrue \in Nat
33 ASSUME ValFalse \in Nat
35 (* The set of all the instructions *)
36 ASSUME Partition({SendIns, RecvIns, WaitIns, TestIns, LocalIns})
37 Instr == UNION {SendIns, RecvIns, WaitIns, TestIns, LocalIns}
39 ------------------------------------------
40 (* Independence operator *)
41 I(A,B) == ENABLED A /\ ENABLED B => /\ A => (ENABLED B)'
43 /\ A \cdot B \equiv B \cdot A
45 (* Initially there are no messages in the network and the memory can have anything in their memories *)
46 Init == /\ network = {}
47 /\ memory \in [Proc -> [Addr -> Nat]]
48 /\ pc = CHOOSE f : f \in [Proc -> Instr]
50 (* Let's keep everything in the right domains *)
51 TypeInv == /\ network \subseteq Comm
52 /\ memory \in [Proc -> [Addr -> Nat]]
53 /\ pc \in [Proc -> Instr]
55 (* The set of all communications waiting at rdv *)
56 mailbox(rdv) == {comm \in network : comm.rdv=rdv /\ comm.status \in {"send","recv"}}
58 (* The set of memory addresses of a process being used in a communication *)
60 {c.data_src: c \in { y \in network: y.status /= "done" /\ (y.src = pid \/ y.dst = pid)}}
61 \cup {c.data_dst: c \in { y \in network: y.status /= "done" /\ (y.src = pid \/ y.dst = pid)}}
63 (* This is a send step of the system *)
64 (* pid: the process ID of the sender *)
65 (* rdv: the rendez-vous point where the "send" communication request is going to be pushed *)
66 (* data_r: the address in the sender's memory where the data is stored *)
67 (* comm_r: the address in the sender's memory where to store the communication id *)
68 Send(pid, rdv, data_r, comm_r) ==
73 /\ pc[pid] \in SendIns
75 (* A matching recv request exists in the rendez-vous *)
76 (* Complete the sender fields and set the communication to the ready state *)
77 /\ \/ \exists c \in mailbox(rdv):
79 /\ \forall d \in mailbox(rdv): d.status="recv" => c.id <= d.id
81 (network \ {c}) \cup {[c EXCEPT
85 (* Use c's existing communication id *)
86 /\ memory' = [memory EXCEPT ![pid][comm_r] = c.id]
89 (* No matching recv communication request exists. *)
90 (* Create a send request and push it in the network. *)
91 \/ /\ ~ \exists c \in mailbox(rdv): c.status = "recv"
93 [id |-> Cardinality(network)+1,
101 /\ network' = network \cup {comm}
102 /\ memory' = [memory EXCEPT ![pid][comm_r] = comm.id]
103 /\ \E ins \in Instr : pc' = [pc EXCEPT ![pid] = ins]
105 (* This is a receive step of the system *)
106 (* pid: the process ID of the receiver *)
107 (* rdv: the Rendez-vous where the "receive" communication request is going to be pushed *)
108 (* data_r: the address in the receivers's memory where the data is going to be stored *)
109 (* comm_r: the address in the receivers's memory where to store the communication id *)
110 Recv(pid, rdv, data_r, comm_r) ==
115 /\ pc[pid] \in RecvIns
117 (* A matching send request exists in the rendez-vous *)
118 (* Complete the receiver fields and set the communication to the ready state *)
119 /\ \/ \exists c \in mailbox(rdv):
121 /\ \forall d \in mailbox(rdv): d.status="send" => c.id <= d.id
123 (network \ {c}) \cup {[c EXCEPT
126 !.data_dst = data_r]}
127 (* Use c's existing communication id *)
128 /\ memory' = [memory EXCEPT ![pid][comm_r] = c.id]
131 (* No matching send communication request exists. *)
132 (* Create a recv request and push it in the network. *)
133 \/ /\ ~ \exists c \in mailbox(rdv): c.status = "send"
135 [id |-> Cardinality(network)+1,
140 /\ network' = network \cup {comm}
141 /\ memory' = [memory EXCEPT ![pid][comm_r] = comm.id]
142 /\ \E ins \in Instr : pc' = [pc EXCEPT ![pid] = ins]
144 (* Wait for at least one communication from a given list to complete *)
145 (* pid: the process ID issuing the wait *)
146 (* comms: the list of addresses in the process's memory where the communication ids are stored *)
148 /\ comms \subseteq Addr
150 /\ pc[pid] \in WaitIns
151 /\ \E comm_r \in comms, c \in network: c.id = memory[pid][comm_r] /\
152 \/ /\ c.status = "ready"
153 /\ memory' = [memory EXCEPT ![c.dst][c.data_dst] = memory[c.src][c.data_src]]
154 /\ network' = (network \ {c}) \cup {[c EXCEPT !.status = "done"]}
155 \/ /\ c.status = "done"
156 /\ UNCHANGED <<memory,network>>
157 /\ \E ins \in Instr : pc' = [pc EXCEPT ![pid] = ins]
159 (* Test if at least one communication from a given list has completed *)
160 (* pid: the process ID issuing the wait *)
161 (* comms: the list of addresses in the process's memory where the communication ids are stored *)
162 (* ret_r: the address in the process's memory where the result is going to be stored *)
163 Test(pid, comms, ret_r) ==
164 /\ comms \subseteq Addr
167 /\ pc[pid] \in TestIns
168 /\ \/ \E comm_r \in comms, c\in network: c.id = memory[pid][comm_r] /\
169 \/ /\ c.status = "ready"
170 /\ memory' = [memory EXCEPT ![c.dst][c.data_dst] = memory[c.src][c.data_src],
171 ![pid][ret_r] = ValTrue]
172 /\ network' = (network \ {c}) \cup {[c EXCEPT !.status = "done"]}
173 \/ /\ c.status = "done"
174 /\ memory' = [memory EXCEPT ![pid][ret_r] = ValTrue]
176 \/ ~ \exists comm_r \in comms, c \in network: c.id = memory[pid][comm_r]
177 /\ c.status \in {"ready","done"}
178 /\ memory' = [memory EXCEPT ![pid][ret_r] = ValFalse]
180 /\ \E ins \in Instr : pc' = [pc EXCEPT ![pid] = ins]
182 (* Local instruction execution *)
185 /\ pc[pid] \in LocalIns
186 /\ memory' \in [Proc -> [Addr -> Nat]]
187 /\ \forall p \in Proc, a \in Addr: memory'[p][a] /= memory[p][a]
188 => p = pid /\ a \notin CommBuffers(pid)
189 /\ \E ins \in Instr : pc' = [pc EXCEPT ![pid] = ins]
192 Next == \exists p \in Proc, data_r \in Addr, comm_r \in Addr, rdv \in RdV,
193 ret_r \in Addr, ids \in SUBSET network:
194 \/ Send(p, rdv, data_r, comm_r)
195 \/ Recv(p, rdv, data_r, comm_r)
197 \/ Test(p, comm_r, ret_r)
200 Spec == Init /\ [][Next]_<<network,memory>>
201 -------------------------------
202 (* Independence of iSend / iRecv steps *)
203 THEOREM \forall p1, p2 \in Proc: \forall rdv1, rdv2 \in RdV:
204 \forall data1, data2, comm1, comm2 \in Addr:
206 /\ ENABLED Send(p1, rdv1, data1, comm1)
207 /\ ENABLED Recv(p2, rdv2, data2, comm2)
208 => I(Send(p1, rdv1, data1, comm1), Recv(p2, rdv2, data2, comm2))
210 (* Independence of iSend and Wait *)
211 THEOREM \forall p1, p2 \in Proc: \forall data, comm1, comm2 \in Addr:
212 \forall rdv \in RdV: \exists c \in network:
214 /\ c.id = memory[p2][comm2]
215 /\ \/ (p1 /= c.dst /\ p1 /= c.src)
216 \/ (comm1 /= c.data_src /\ comm1 /= c.data_dst)
217 /\ ENABLED Send(p1, rdv, data, comm1)
218 /\ ENABLED Wait(p2, comm2)
219 => I(Send(p1, rdv, data, comm1), Wait(p2, comm2))
221 (* Independence of iSend's in different rendez-vous *)
222 THEOREM \forall p1, p2 \in Proc: \forall rdv1, rdv2 \in RdV:
223 \forall data1, data2, comm1, comm2 \in Addr:
226 /\ ENABLED Send(p1, rdv1, data1, comm1)
227 /\ ENABLED Send(p2, rdv2, data2, comm2)
228 => I(Send(p1, rdv1, data1, comm1),
229 Send(p2, rdv2, data2, comm2))
231 (* Independence of iRecv's in different rendez-vous *)
232 THEOREM \forall p1, p2 \in Proc: \forall rdv1, rdv2 \in RdV:
233 \forall data1, data2, comm1, comm2 \in Addr:
236 /\ ENABLED Recv(p1, rdv1, data1, comm1)
237 /\ ENABLED Recv(p2, rdv2, data2, comm2)
238 => I(Recv(p1, rdv1, data1, comm1),
239 Recv(p2, rdv2, data2, comm2))
241 (* Independence of Wait of different processes on the same comm *)
242 THEOREM \forall p1, p2 \in Proc: \forall comm1, comm2 \in Addr:
245 /\ ENABLED Wait(p1, comm1)
246 /\ ENABLED Wait(p2, comm2)
247 => I(Wait(p1, comm1), Wait(p2, comm2))
249 \* Generated at Thu Feb 18 13:49:35 CET 2010