src/simix/simix_network.tla

   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.
   5
   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
  13
  14 NoProc == CHOOSE p : p \notin Proc
  15 NoAddr == CHOOSE a : a \notin Addr
  16
  17 Partition(S) == \forall x,y \in S : x \cap y /= {} => x = y
  18
  19 Comm == [id:Nat,
  20          rdv:RdV,
  21          status:{"send","recv","ready","done"},
  22          src:Proc,
  23          dst:Proc,
  24          data_src:Addr,
  25          data_dst:Addr]
  26
  27 ASSUME ValTrue \in Nat
  28 ASSUME ValFalse \in Nat
  29
  30 (* The set of all the instructions *)
  31 ASSUME Partition({SendIns, RecvIns, WaitIns, TestIns, LocalIns})
  32 Instr == UNION {SendIns, RecvIns, WaitIns, TestIns, LocalIns}
  33
  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
  39
  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]
  44
  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]
  49
  50 (* The set of all communications waiting at rdv *)
  51 mailbox(rdv) == {comm \in network : comm.rdv=rdv /\ comm.status \in {"send","recv"}}
  52
  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)}}
  57
  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
  66   /\ data_r \in Addr
  67   /\ comm_r \in Addr
  68   /\ pc[pid] \in SendIns
  69
  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
  77                                        !.status = "ready",
  78                                        !.src = pid,
  79                                        !.data_src = data_r]}
  80           (* Use c's existing communication id *)
  81           /\ memory' = [memory EXCEPT ![pid][comm_r] = c.id]
  82
  83
  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,
  94                   data_dst |-> NoAddr]
  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]
  99
 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
 108   /\ data_r \in Addr
 109   /\ comm_r \in Addr
 110   /\ pc[pid] \in RecvIns
 111
 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
 119                                        !.status = "ready",
 120                                        !.dst = pid,
 121                                        !.data_dst = data_r]}
 122           (* Use c's existing communication id *)
 123           /\ memory' = [memory EXCEPT ![pid][comm_r] = c.id]
 124
 125
 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]
 138
 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) ==
 143   /\ comms \subseteq Addr
 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]
 153
 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
 160   /\ ret_r \in Addr
 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]
 172         /\ c.status \in {"ready","done"}
 173         /\ memory' = [memory EXCEPT ![pid][ret_r] = ValFalse]
 174         /\ UNCHANGED network
 175   /\ \E ins \in Instr : pc' = [pc EXCEPT ![pid] = ins]
 176
 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
 186
 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)
 194
 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))
 204
 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))
 215
 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))
 225
 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))
 235
 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