---- MODULE simix_network ----
-(* This is a TLA module specifying the networking layer of SIMIX.
+(* This is a TLA module specifying the networking layer of SIMIX.
It is used to verify the soundness of the DPOR reduction algorithm
- used in the model-checker.
+ used in the model-checker.
If you think you found a new independence lemma, add it to this
file and relaunch TLC to check whether your lemma actually holds.
*)
EXTENDS Naturals, Sequences, FiniteSets
-CONSTANTS RdV, Addr, Proc, ValTrue, ValFalse, SendIns, RecvIns, WaitIns,
+CONSTANTS RdV, Addr, Proc, ValTrue, ValFalse, SendIns, RecvIns, WaitIns,
TestIns, LocalIns
VARIABLES network, memory, pc
mailbox(rdv) == {comm \in network : comm.rdv=rdv /\ comm.status \in {"send","recv"}}
(* The set of memory addresses of a process being used in a communication *)
-CommBuffers(pid) ==
- {c.data_src: c \in { y \in network: y.status /= "done" /\ (y.src = pid \/ y.dst = pid)}}
+CommBuffers(pid) ==
+ {c.data_src: c \in { y \in network: y.status /= "done" /\ (y.src = pid \/ y.dst = pid)}}
\cup {c.data_dst: c \in { y \in network: y.status /= "done" /\ (y.src = pid \/ y.dst = pid)}}
(* This is a send step of the system *)
(* rdv: the rendez-vous point where the "send" communication request is going to be pushed *)
(* data_r: the address in the sender's memory where the data is stored *)
(* comm_r: the address in the sender's memory where to store the communication id *)
-Send(pid, rdv, data_r, comm_r) ==
+Send(pid, rdv, data_r, comm_r) ==
/\ rdv \in RdV
/\ pid \in Proc
/\ data_r \in Addr
/\ comm_r \in Addr
/\ pc[pid] \in SendIns
-
+
(* A matching recv request exists in the rendez-vous *)
(* Complete the sender fields and set the communication to the ready state *)
/\ \/ \exists c \in mailbox(rdv):
/\ c.status="recv"
/\ \forall d \in mailbox(rdv): d.status="recv" => c.id <= d.id
- /\ network' =
+ /\ network' =
(network \ {c}) \cup {[c EXCEPT
!.status = "ready",
!.src = pid,
!.data_src = data_r]}
(* Use c's existing communication id *)
/\ memory' = [memory EXCEPT ![pid][comm_r] = c.id]
-
-
+
+
(* No matching recv communication request exists. *)
(* Create a send request and push it in the network. *)
- \/ /\ ~ \exists c \in mailbox(rdv): c.status = "recv"
- /\ LET comm ==
- [id |-> Cardinality(network)+1,
+ \/ /\ ~ \exists c \in mailbox(rdv): c.status = "recv"
+ /\ LET comm ==
+ [id |-> Cardinality(network)+1,
rdv |-> rdv,
- status |-> "send",
+ status |-> "send",
src |-> pid,
- dst |-> NoProc,
+ dst |-> NoProc,
data_src |-> data_r,
data_dst |-> NoAddr]
IN
/\ network' = network \cup {comm}
- /\ memory' = [memory EXCEPT ![pid][comm_r] = comm.id]
+ /\ memory' = [memory EXCEPT ![pid][comm_r] = comm.id]
/\ \E ins \in Instr : pc' = [pc EXCEPT ![pid] = ins]
(* This is a receive step of the system *)
(* rdv: the Rendez-vous where the "receive" communication request is going to be pushed *)
(* data_r: the address in the receivers's memory where the data is going to be stored *)
(* comm_r: the address in the receivers's memory where to store the communication id *)
-Recv(pid, rdv, data_r, comm_r) ==
+Recv(pid, rdv, data_r, comm_r) ==
/\ rdv \in RdV
/\ pid \in Proc
/\ data_r \in Addr
/\ comm_r \in Addr
/\ pc[pid] \in RecvIns
-
+
(* A matching send request exists in the rendez-vous *)
(* Complete the receiver fields and set the communication to the ready state *)
/\ \/ \exists c \in mailbox(rdv):
/\ c.status="send"
/\ \forall d \in mailbox(rdv): d.status="send" => c.id <= d.id
- /\ network' =
+ /\ network' =
(network \ {c}) \cup {[c EXCEPT
!.status = "ready",
!.dst = pid,
!.data_dst = data_r]}
(* Use c's existing communication id *)
/\ memory' = [memory EXCEPT ![pid][comm_r] = c.id]
-
-
+
+
(* No matching send communication request exists. *)
(* Create a recv request and push it in the network. *)
- \/ /\ ~ \exists c \in mailbox(rdv): c.status = "send"
- /\ LET comm ==
+ \/ /\ ~ \exists c \in mailbox(rdv): c.status = "send"
+ /\ LET comm ==
[id |-> Cardinality(network)+1,
- status |-> "recv",
- dst |-> pid,
+ status |-> "recv",
+ dst |-> pid,
data_dst |-> data_r]
IN
/\ network' = network \cup {comm}
- /\ memory' = [memory EXCEPT ![pid][comm_r] = comm.id]
+ /\ memory' = [memory EXCEPT ![pid][comm_r] = comm.id]
/\ \E ins \in Instr : pc' = [pc EXCEPT ![pid] = ins]
(* Wait for at least one communication from a given list to complete *)
\/ ~ \exists comm_r \in comms, c \in network: c.id = memory[pid][comm_r]
/\ c.status \in {"ready","done"}
/\ memory' = [memory EXCEPT ![pid][ret_r] = ValFalse]
- /\ UNCHANGED network
+ /\ UNCHANGED network
/\ \E ins \in Instr : pc' = [pc EXCEPT ![pid] = ins]
(* Local instruction execution *)
\/ Wait(p, comm_r)
\/ Test(p, comm_r, ret_r)
\/ Local(p)
-
+
Spec == Init /\ [][Next]_<<network,memory>>
-------------------------------
(* Independence of iSend / iRecv steps *)
-THEOREM \forall p1, p2 \in Proc: \forall rdv1, rdv2 \in RdV:
+THEOREM \forall p1, p2 \in Proc: \forall rdv1, rdv2 \in RdV:
\forall data1, data2, comm1, comm2 \in Addr:
/\ p1 /= p2
/\ ENABLED Send(p1, rdv1, data1, comm1)
\/ (comm1 /= c.data_src /\ comm1 /= c.data_dst)
/\ ENABLED Send(p1, rdv, data, comm1)
/\ ENABLED Wait(p2, comm2)
- => I(Send(p1, rdv, data, comm1), Wait(p2, comm2))
+ => I(Send(p1, rdv, data, comm1), Wait(p2, comm2))
(* Independence of iSend's in different rendez-vous *)
-THEOREM \forall p1, p2 \in Proc: \forall rdv1, rdv2 \in RdV:
+THEOREM \forall p1, p2 \in Proc: \forall rdv1, rdv2 \in RdV:
\forall data1, data2, comm1, comm2 \in Addr:
/\ p1 /= p2
/\ rdv1 /= rdv2
Send(p2, rdv2, data2, comm2))
(* Independence of iRecv's in different rendez-vous *)
-THEOREM \forall p1, p2 \in Proc: \forall rdv1, rdv2 \in RdV:
+THEOREM \forall p1, p2 \in Proc: \forall rdv1, rdv2 \in RdV:
\forall data1, data2, comm1, comm2 \in Addr:
/\ p1 /= p2
/\ rdv1 /= rdv2
