+++ /dev/null
----- MODULE simix_network ----
-(* 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.
-
- 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,
- TestIns, LocalIns
-VARIABLES network, memory, pc
-
-NoProc == CHOOSE p : p \notin Proc
-NoAddr == CHOOSE a : a \notin Addr
-
-Partition(S) == \forall x,y \in S : x \cap y /= {} => x = y
-
-Comm == [id:Nat,
- rdv:RdV,
- status:{"send","recv","ready","done"},
- src:Proc,
- dst:Proc,
- data_src:Addr,
- data_dst:Addr]
-
-ASSUME ValTrue \in Nat
-ASSUME ValFalse \in Nat
-
-(* The set of all the instructions *)
-ASSUME Partition({SendIns, RecvIns, WaitIns, TestIns, LocalIns})
-Instr == UNION {SendIns, RecvIns, WaitIns, TestIns, LocalIns}
-
-------------------------------------------
-(* Independence operator *)
-I(A,B) == ENABLED A /\ ENABLED B => /\ A => (ENABLED B)'
- /\ B => (ENABLED A)'
- /\ A \cdot B \equiv B \cdot A
-
-(* Initially there are no messages in the network and the memory can have anything in their memories *)
-Init == /\ network = {}
- /\ memory \in [Proc -> [Addr -> Nat]]
- /\ pc = CHOOSE f : f \in [Proc -> Instr]
-
-(* Let's keep everything in the right domains *)
-TypeInv == /\ network \subseteq Comm
- /\ memory \in [Proc -> [Addr -> Nat]]
- /\ pc \in [Proc -> Instr]
-
-(* The set of all communications waiting at rdv *)
-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)}}
-\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 *)
-(* pid: the process ID of the sender *)
-(* 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) ==
- /\ 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 \ {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,
- rdv |-> rdv,
- status |-> "send",
- src |-> pid,
- dst |-> NoProc,
- data_src |-> data_r,
- data_dst |-> NoAddr]
- IN
- /\ network' = network \cup {comm}
- /\ 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 *)
-(* pid: the process ID of the receiver *)
-(* 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) ==
- /\ 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 \ {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 ==
- [id |-> Cardinality(network)+1,
- status |-> "recv",
- dst |-> pid,
- data_dst |-> data_r]
- IN
- /\ network' = network \cup {comm}
- /\ 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 *)
-(* pid: the process ID issuing the wait *)
-(* comms: the list of addresses in the process's memory where the communication ids are stored *)
-Wait(pid, comms) ==
- /\ comms \subseteq Addr
- /\ pid \in Proc
- /\ pc[pid] \in WaitIns
- /\ \E comm_r \in comms, c \in network: c.id = memory[pid][comm_r] /\
- \/ /\ c.status = "ready"
- /\ memory' = [memory EXCEPT ![c.dst][c.data_dst] = memory[c.src][c.data_src]]
- /\ network' = (network \ {c}) \cup {[c EXCEPT !.status = "done"]}
- \/ /\ c.status = "done"
- /\ UNCHANGED <<memory,network>>
- /\ \E ins \in Instr : pc' = [pc EXCEPT ![pid] = ins]
-
-(* Test if at least one communication from a given list has completed *)
-(* pid: the process ID issuing the wait *)
-(* comms: the list of addresses in the process's memory where the communication ids are stored *)
-(* ret_r: the address in the process's memory where the result is going to be stored *)
-Test(pid, comms, ret_r) ==
- /\ comms \subseteq Addr
- /\ ret_r \in Addr
- /\ pid \in Proc
- /\ pc[pid] \in TestIns
- /\ \/ \E comm_r \in comms, c\in network: c.id = memory[pid][comm_r] /\
- \/ /\ c.status = "ready"
- /\ memory' = [memory EXCEPT ![c.dst][c.data_dst] = memory[c.src][c.data_src],
- ![pid][ret_r] = ValTrue]
- /\ network' = (network \ {c}) \cup {[c EXCEPT !.status = "done"]}
- \/ /\ c.status = "done"
- /\ memory' = [memory EXCEPT ![pid][ret_r] = ValTrue]
- /\ UNCHANGED network
- \/ ~ \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
- /\ \E ins \in Instr : pc' = [pc EXCEPT ![pid] = ins]
-
-(* Local instruction execution *)
-Local(pid) ==
- /\ pid \in Proc
- /\ pc[pid] \in LocalIns
- /\ memory' \in [Proc -> [Addr -> Nat]]
- /\ \forall p \in Proc, a \in Addr: memory'[p][a] /= memory[p][a]
- => p = pid /\ a \notin CommBuffers(pid)
- /\ \E ins \in Instr : pc' = [pc EXCEPT ![pid] = ins]
- /\ UNCHANGED network
-
-Next == \exists p \in Proc, data_r \in Addr, comm_r \in Addr, rdv \in RdV,
- ret_r \in Addr, ids \in SUBSET network:
- \/ Send(p, rdv, data_r, comm_r)
- \/ Recv(p, rdv, data_r, comm_r)
- \/ 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:
- \forall data1, data2, comm1, comm2 \in Addr:
- /\ p1 /= p2
- /\ ENABLED Send(p1, rdv1, data1, comm1)
- /\ ENABLED Recv(p2, rdv2, data2, comm2)
- => I(Send(p1, rdv1, data1, comm1), Recv(p2, rdv2, data2, comm2))
-
-(* Independence of iSend and Wait *)
-THEOREM \forall p1, p2 \in Proc: \forall data, comm1, comm2 \in Addr:
- \forall rdv \in RdV: \exists c \in network:
- /\ p1 /= p2
- /\ c.id = memory[p2][comm2]
- /\ \/ (p1 /= c.dst /\ p1 /= c.src)
- \/ (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))
-
-(* Independence of iSend's in different rendez-vous *)
-THEOREM \forall p1, p2 \in Proc: \forall rdv1, rdv2 \in RdV:
- \forall data1, data2, comm1, comm2 \in Addr:
- /\ p1 /= p2
- /\ rdv1 /= rdv2
- /\ ENABLED Send(p1, rdv1, data1, comm1)
- /\ ENABLED Send(p2, rdv2, data2, comm2)
- => I(Send(p1, rdv1, data1, comm1),
- Send(p2, rdv2, data2, comm2))
-
-(* Independence of iRecv's in different rendez-vous *)
-THEOREM \forall p1, p2 \in Proc: \forall rdv1, rdv2 \in RdV:
- \forall data1, data2, comm1, comm2 \in Addr:
- /\ p1 /= p2
- /\ rdv1 /= rdv2
- /\ ENABLED Recv(p1, rdv1, data1, comm1)
- /\ ENABLED Recv(p2, rdv2, data2, comm2)
- => I(Recv(p1, rdv1, data1, comm1),
- Recv(p2, rdv2, data2, comm2))
-
-(* Independence of Wait of different processes on the same comm *)
-THEOREM \forall p1, p2 \in Proc: \forall comm1, comm2 \in Addr:
- /\ p1 /= p2
- /\ comm1 = comm2
- /\ ENABLED Wait(p1, comm1)
- /\ ENABLED Wait(p2, comm2)
- => I(Wait(p1, comm1), Wait(p2, comm2))
-====
-\* Generated at Thu Feb 18 13:49:35 CET 2010
