X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/e4abd3f271729beeff499da36267bfb274dd1f6d..9fd6cbc6c3b06f4b09e3c3339ffb3cc8a68f9bfa:/src/simix/simix_network.tla diff --git a/src/simix/simix_network.tla b/src/simix/simix_network.tla index 9ff81f2656..476628d195 100644 --- a/src/simix/simix_network.tla +++ b/src/simix/simix_network.tla @@ -1,13 +1,13 @@ ---- 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 @@ -51,8 +51,8 @@ TypeInv == /\ network \subseteq Comm 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 *) @@ -60,41 +60,41 @@ CommBuffers(pid) == (* 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 *) @@ -102,38 +102,38 @@ Send(pid, rdv, data_r, comm_r) == (* 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 *) @@ -171,7 +171,7 @@ Test(pid, comms, ret_r) == \/ ~ \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 *) @@ -191,11 +191,11 @@ Next == \exists p \in Proc, data_r \in Addr, comm_r \in Addr, rdv \in RdV, \/ Wait(p, comm_r) \/ Test(p, comm_r, ret_r) \/ Local(p) - + Spec == Init /\ [][Next]_<> ------------------------------- (* 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) @@ -211,10 +211,10 @@ THEOREM \forall p1, p2 \in Proc: \forall data, comm1, comm2 \in Addr: \/ (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 @@ -224,7 +224,7 @@ THEOREM \forall p1, p2 \in Proc: \forall rdv1, rdv2 \in RdV: 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