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