A
lgorithmique
N
umérique
D
istribuée
Public GIT Repository
projects
/
simgrid.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
add the Storage::read_async and Storage::write_async methods
[simgrid.git]
/
src
/
simix
/
simix_network.tla
diff --git
a/src/simix/simix_network.tla
b/src/simix/simix_network.tla
index
9ff81f2
..
476628d
100644
(file)
--- a/
src/simix/simix_network.tla
+++ b/
src/simix/simix_network.tla
@@
-1,13
+1,13
@@
---- MODULE simix_network ----
---- 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
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
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
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 *)
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 *)
\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 *)
(* 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
/\ 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
(* 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]
(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. *)
(* 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,
rdv |-> rdv,
- status |-> "send",
+ status |-> "send",
src |-> pid,
src |-> pid,
- dst |-> NoProc,
+ dst |-> NoProc,
data_src |-> data_r,
data_dst |-> NoAddr]
IN
/\ network' = network \cup {comm}
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 *)
/\ \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 *)
(* 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
/\ 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
(* 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]
(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. *)
(* 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,
[id |-> Cardinality(network)+1,
- status |-> "recv",
- dst |-> pid,
+ status |-> "recv",
+ dst |-> pid,
data_dst |-> data_r]
IN
/\ network' = network \cup {comm}
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 *)
/\ \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]
\/ ~ \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 *)
/\ \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)
\/ Wait(p, comm_r)
\/ Test(p, comm_r, ret_r)
\/ Local(p)
-
+
Spec == Init /\ [][Next]_<<network,memory>>
-------------------------------
(* Independence of iSend / iRecv steps *)
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)
\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)
\/ (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 *)
(* 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
\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 *)
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
\forall data1, data2, comm1, comm2 \in Addr:
/\ p1 /= p2
/\ rdv1 /= rdv2
