Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
ChangeLog [ci-skip]
[simgrid.git] / src / simix / simix_network.tla
1 ---- MODULE simix_network ----
2 (* Copyright (c) 2012-2022. The SimGrid Team. All rights reserved.          *)
3
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. *)
6
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.
10
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.
13    *)
14 EXTENDS Naturals, Sequences, FiniteSets
15 CONSTANTS RdV, Addr, Proc, ValTrue, ValFalse, SendIns, RecvIns, WaitIns,
16           TestIns, LocalIns
17 VARIABLES network, memory, pc
18
19 NoProc == CHOOSE p : p \notin Proc
20 NoAddr == CHOOSE a : a \notin Addr
21
22 Partition(S) == \forall x,y \in S : x \cap y /= {} => x = y
23
24 Comm == [id:Nat,
25          rdv:RdV,
26          status:{"send","recv","ready","done"},
27          src:Proc,
28          dst:Proc,
29          data_src:Addr,
30          data_dst:Addr]
31
32 ASSUME ValTrue \in Nat
33 ASSUME ValFalse \in Nat
34
35 (* The set of all the instructions *)
36 ASSUME Partition({SendIns, RecvIns, WaitIns, TestIns, LocalIns})
37 Instr == UNION {SendIns, RecvIns, WaitIns, TestIns, LocalIns}
38
39 ------------------------------------------
40 (* Independence operator *)
41 I(A,B) == ENABLED A /\ ENABLED B => /\ A => (ENABLED B)'
42                                     /\ B => (ENABLED A)'
43                                     /\ A \cdot B \equiv B \cdot A
44
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]
49
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]
54
55 (* The set of all communications waiting at rdv *)
56 mailbox(rdv) == {comm \in network : comm.rdv=rdv /\ comm.status \in {"send","recv"}}
57
58 (* The set of memory addresses of a process being used in a communication *)
59 CommBuffers(pid) ==
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)}}
62
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) ==
69   /\ rdv \in RdV
70   /\ pid \in Proc
71   /\ data_r \in Addr
72   /\ comm_r \in Addr
73   /\ pc[pid] \in SendIns
74
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):
78           /\ c.status="recv"
79           /\ \forall d \in mailbox(rdv): d.status="recv" => c.id <= d.id
80           /\ network' =
81                (network \ {c}) \cup {[c EXCEPT
82                                        !.status = "ready",
83                                        !.src = pid,
84                                        !.data_src = data_r]}
85           (* Use c's existing communication id *)
86           /\ memory' = [memory EXCEPT ![pid][comm_r] = c.id]
87
88
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"
92         /\ LET comm ==
93                  [id |-> Cardinality(network)+1,
94                   rdv |-> rdv,
95                   status |-> "send",
96                   src |-> pid,
97                   dst |-> NoProc,
98                   data_src |-> data_r,
99                   data_dst |-> NoAddr]
100            IN
101              /\ network' = network \cup {comm}
102              /\ memory' = [memory EXCEPT ![pid][comm_r] = comm.id]
103   /\ \E ins \in Instr : pc' = [pc EXCEPT ![pid] = ins]
104
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) ==
111   /\ rdv \in RdV
112   /\ pid \in Proc
113   /\ data_r \in Addr
114   /\ comm_r \in Addr
115   /\ pc[pid] \in RecvIns
116
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):
120           /\ c.status="send"
121           /\ \forall d \in mailbox(rdv): d.status="send" => c.id <= d.id
122           /\ network' =
123                (network \ {c}) \cup {[c EXCEPT
124                                        !.status = "ready",
125                                        !.dst = pid,
126                                        !.data_dst = data_r]}
127           (* Use c's existing communication id *)
128           /\ memory' = [memory EXCEPT ![pid][comm_r] = c.id]
129
130
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"
134         /\ LET comm ==
135                  [id |-> Cardinality(network)+1,
136                   status |-> "recv",
137                   dst |-> pid,
138                   data_dst |-> data_r]
139            IN
140              /\ network' = network \cup {comm}
141              /\ memory' = [memory EXCEPT ![pid][comm_r] = comm.id]
142   /\ \E ins \in Instr : pc' = [pc EXCEPT ![pid] = ins]
143
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 *)
147 Wait(pid, comms) ==
148   /\ comms \subseteq Addr
149   /\ pid \in Proc
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]
158
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
165   /\ ret_r \in Addr
166   /\ pid \in Proc
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]
175            /\ UNCHANGED network
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]
179         /\ UNCHANGED network
180   /\ \E ins \in Instr : pc' = [pc EXCEPT ![pid] = ins]
181
182 (* Local instruction execution *)
183 Local(pid) ==
184     /\ pid \in Proc
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]
190     /\ UNCHANGED network
191
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)
196           \/ Wait(p, comm_r)
197           \/ Test(p, comm_r, ret_r)
198           \/ Local(p)
199
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:
205         /\ p1 /= p2
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))
209
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:
213         /\ p1 /= p2
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))
220
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:
224         /\ p1 /= p2
225         /\ rdv1 /= rdv2
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))
230
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:
234         /\ p1 /= p2
235         /\ rdv1 /= rdv2
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))
240
241 (* Independence of Wait of different processes on the same comm *)
242 THEOREM \forall p1, p2 \in Proc: \forall comm1, comm2 \in Addr:
243         /\ p1 /= p2
244         /\ comm1 = comm2
245         /\ ENABLED Wait(p1, comm1)
246         /\ ENABLED Wait(p2, comm2)
247         => I(Wait(p1, comm1), Wait(p2, comm2))
248 ====
249 \* Generated at Thu Feb 18 13:49:35 CET 2010