Skip to content

Commit d2926ff

Browse files
ahelwerahelwer
committed
Basic network modeling prototypes
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
1 parent dc6470a commit d2926ff

5 files changed

Lines changed: 304 additions & 0 deletions

File tree

‎specifications/NetworkModeling/ByzantineGenerals.tla‎

Lines changed: 104 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,104 @@
1+
------------------------ MODULE ByzantineGenerals ---------------------------
2+
CONSTANTS Generals
3+
4+
VARIABLES network, confirmations
5+
6+
Vars ≜ ⟨network, connection⟩
7+
8+
CommandMessageType ≜ "Command"
9+
CommandMessage ≜ [
10+
type : {CommandMessageType},
11+
sender : Node
12+
]
13+
14+
ConfirmMessageType ≜ "Confirm"
15+
ConfirmMessage ≜ [
16+
type : {ConfirmMessageType},
17+
sender : Node
18+
]
19+
20+
MessageType ≜ {CommandMessageType, ConfirmMessageType}
21+
Message ≜ CommandMessage ∪ ConfirmMessage
22+
23+
INSTANCE Network WITH Ordered ← FALSE, Duplicates ← TRUE, Loss ← TRUE
24+
25+
TypeOK ≜
26+
∧ network ∈ [Node → PendingMessage]
27+
∧ connection ∈ [Node → SUBSET Node]
28+
29+
Termination ≜ ∀ src, dst ∈ Node : dst ∈ connection[src]
30+
31+
Liveness ≜ □◇Termination
32+
33+
SendSynMessage(src, dst) ≜
34+
∧ dst ∉ connection[src]
35+
∧ ∃ success ∈ BOOLEAN :
36+
network' = [
37+
network EXCEPT
38+
![dst] = SendMessage(@, src, success, [
39+
type ↦ SynMessageType,
40+
sender ↦ src
41+
])
42+
]
43+
∧ UNCHANGED connection
44+
45+
ProcessSynMessage(recipient, sender, msg, success) ≜
46+
∧ msg.type = SynMessageType
47+
∧ ∃ duplicate ∈ BOOLEAN :
48+
network' = [
49+
network EXCEPT
50+
![recipient] = ReceiveMessage(@, sender, duplicate, msg),
51+
![sender] = SendMessage(@, recipient, success, [
52+
type ↦ AckMessageType,
53+
sender ↦ recipient
54+
])
55+
]
56+
∧ UNCHANGED connection
57+
58+
ProcessAckMessage(recipient, sender, msg) ≜
59+
∧ msg.type = AckMessageType
60+
∧ ∃ duplicate ∈ BOOLEAN :
61+
network' = [
62+
network EXCEPT
63+
![recipient] = ReceiveMessage(@, sender, duplicate, msg)
64+
]
65+
∧ connection' = [connection EXCEPT ![recipient] = @ ∪ {sender}]
66+
67+
ProcessMessage(recipient, sender, message_type, success) ≜
68+
∃ msg ∈ PeekMessage(network[recipient]) :
69+
∧ msg.type = message_type
70+
∧ msg.sender = sender
71+
∧ ∨ ProcessSynMessage(recipient, sender, msg, success)
72+
∨ ProcessAckMessage(recipient, sender, msg)
73+
74+
Terminate ≜
75+
∧ Termination
76+
∧ UNCHANGED ⟨network, connection⟩
77+
78+
Init ≜
79+
∧ network = [n ∈ Node ↦ NoPendingMessages]
80+
∧ connection = [n ∈ Node ↦ {}]
81+
82+
Next ≜
83+
∨ ∃ src, dst ∈ Node : SendSynMessage(src, dst)
84+
∨ ∃ recipient, sender ∈ Node :
85+
∃ message_type ∈ MessageType :
86+
∃ success ∈ BOOLEAN :
87+
ProcessMessage(recipient, sender, message_type, success)
88+
∨ Terminate
89+
90+
Fairness ≜
91+
∧ ∀ src, dst ∈ Node : WF_Vars(SendSynMessage(src, dst))
92+
∧ ∀ recipient, sender ∈ Node :
93+
SF_Vars(ProcessMessage(recipient, sender, SynMessageType, TRUE))
94+
∧ ∀ recipient, sender ∈ Node :
95+
∀ success ∈ BOOLEAN :
96+
WF_Vars(ProcessMessage(recipient, sender, AckMessageType, success))
97+
98+
Spec ≜
99+
∧ Init
100+
∧ □[Next]_Vars
101+
∧ Fairness
102+
103+
=============================================================================
104+

‎specifications/NetworkModeling/CommunicatingSequentialProcesses.cfg‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
CONSTANT Node = {n1, n2}
2+
INVARIANT TypeOK
3+
PROPERTY Liveness
4+
SPECIFICATION Spec
5+

‎specifications/NetworkModeling/CommunicatingSequentialProcesses.tla‎

Lines changed: 104 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,104 @@
1+
----------------- MODULE CommunicatingSequentialProcesses -------------------
2+
CONSTANTS Node
3+
4+
VARIABLES network, connection
5+
6+
Vars ≜ ⟨network, connection⟩
7+
8+
SynMessageType ≜ "SYN"
9+
SynMessage ≜ [
10+
type : {SynMessageType},
11+
sender : Node
12+
]
13+
14+
AckMessageType ≜ "ACK"
15+
AckMessage ≜ [
16+
type : {AckMessageType},
17+
sender : Node
18+
]
19+
20+
MessageType ≜ {SynMessageType, AckMessageType}
21+
Message ≜ SynMessage ∪ AckMessage
22+
23+
INSTANCE Network WITH Ordered ← FALSE, Duplicates ← TRUE, Loss ← TRUE
24+
25+
TypeOK ≜
26+
∧ network ∈ [Node → PendingMessage]
27+
∧ connection ∈ [Node → SUBSET Node]
28+
29+
Termination ≜ ∀ src, dst ∈ Node : dst ∈ connection[src]
30+
31+
Liveness ≜ □◇Termination
32+
33+
SendSynMessage(src, dst) ≜
34+
∧ dst ∉ connection[src]
35+
∧ ∃ success ∈ BOOLEAN :
36+
network' = [
37+
network EXCEPT
38+
![dst] = SendMessage(@, src, success, [
39+
type ↦ SynMessageType,
40+
sender ↦ src
41+
])
42+
]
43+
∧ UNCHANGED connection
44+
45+
ProcessSynMessage(recipient, sender, msg, success) ≜
46+
∧ msg.type = SynMessageType
47+
∧ ∃ duplicate ∈ BOOLEAN :
48+
network' = [
49+
network EXCEPT
50+
![recipient] = ReceiveMessage(@, sender, duplicate, msg),
51+
![sender] = SendMessage(@, recipient, success, [
52+
type ↦ AckMessageType,
53+
sender ↦ recipient
54+
])
55+
]
56+
∧ UNCHANGED connection
57+
58+
ProcessAckMessage(recipient, sender, msg) ≜
59+
∧ msg.type = AckMessageType
60+
∧ ∃ duplicate ∈ BOOLEAN :
61+
network' = [
62+
network EXCEPT
63+
![recipient] = ReceiveMessage(@, sender, duplicate, msg)
64+
]
65+
∧ connection' = [connection EXCEPT ![recipient] = @ ∪ {sender}]
66+
67+
ProcessMessage(recipient, sender, message_type, success) ≜
68+
∃ msg ∈ PeekMessage(network[recipient]) :
69+
∧ msg.type = message_type
70+
∧ msg.sender = sender
71+
∧ ∨ ProcessSynMessage(recipient, sender, msg, success)
72+
∨ ProcessAckMessage(recipient, sender, msg)
73+
74+
Terminate ≜
75+
∧ Termination
76+
∧ UNCHANGED ⟨network, connection⟩
77+
78+
Init ≜
79+
∧ network = [n ∈ Node ↦ NoPendingMessages]
80+
∧ connection = [n ∈ Node ↦ {}]
81+
82+
Next ≜
83+
∨ ∃ src, dst ∈ Node : SendSynMessage(src, dst)
84+
∨ ∃ recipient, sender ∈ Node :
85+
∃ message_type ∈ MessageType :
86+
∃ success ∈ BOOLEAN :
87+
ProcessMessage(recipient, sender, message_type, success)
88+
∨ Terminate
89+
90+
Fairness ≜
91+
∧ ∀ src, dst ∈ Node : WF_Vars(SendSynMessage(src, dst))
92+
∧ ∀ recipient, sender ∈ Node :
93+
SF_Vars(ProcessMessage(recipient, sender, SynMessageType, TRUE))
94+
∧ ∀ recipient, sender ∈ Node :
95+
∀ success ∈ BOOLEAN :
96+
WF_Vars(ProcessMessage(recipient, sender, AckMessageType, success))
97+
98+
Spec ≜
99+
∧ Init
100+
∧ □[Next]_Vars
101+
∧ Fairness
102+
103+
=============================================================================
104+

‎specifications/NetworkModeling/Network.tla‎

Lines changed: 86 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,86 @@
1+
------------------------------ MODULE Network -------------------------------
2+
(***************************************************************************)
3+
(* NETWORKING OPERATIONS *)
4+
(* *)
5+
(* Various network-related operations (send & receiving messages, etc.) *)
6+
(* and their adaptations for sequential vs. unordered messaging models. *)
7+
(* *)
8+
(***************************************************************************)
9+
10+
LOCAL INSTANCE Naturals
11+
LOCAL INSTANCE Sequences
12+
13+
CONSTANTS
14+
Node,
15+
Message,
16+
Ordered,
17+
Duplicates,
18+
Loss
19+
20+
ASSUME
21+
∧ Node ≠ {}
22+
∧ Message ≠ {}
23+
∧ Ordered ∈ BOOLEAN
24+
∧ Duplicates ∈ BOOLEAN
25+
∧ Loss ∈ BOOLEAN
26+
27+
\* Converts a sequence into an unordered set of unique elements
28+
SeqToSet(seq) ≜ {seq[i] : i ∈ 1 ‥ Len(seq)}
29+
30+
\* Transforms every element of a sequence with some operator
31+
MapSeq(seq, f(_)) ≜ [i ∈ 1 ‥ Len(seq) ↦ f(seq[i])]
32+
33+
\* The set of all possible pending messages; useful for type invariants
34+
PendingMessage ≜
35+
IF Ordered
36+
THEN [Node → Seq(Message)]
37+
ELSE SUBSET Message
38+
39+
\* The set of messages currently pending at a node
40+
CurrentlyPendingMessages(pending) ≜
41+
IF Ordered
42+
THEN UNION {SeqToSet(pending[n]) : n ∈ Node}
43+
ELSE pending
44+
45+
\* Transforms all pending messages with some operator
46+
MapPendingMessages(pending, f(_)) ≜
47+
IF Ordered
48+
THEN [n ∈ Node ↦ MapSeq(pending[n], f)]
49+
ELSE {f(msg) : msg ∈ pending}
50+
51+
\* The state of having no pending messages; useful for initial states
52+
NoPendingMessages ≜
53+
IF Ordered
54+
THEN [n ∈ Node ↦ ⟨⟩]
55+
ELSE {}
56+
57+
\* Add a message to the pending messages at the recipient node
58+
SendMessage(pending, sender, success, msg) ≜
59+
IF Loss ∧ ¬success
60+
THEN pending
61+
ELSE IF Ordered
62+
THEN [pending EXCEPT ![sender] = Append(@, msg)]
63+
ELSE pending ∪ {msg}
64+
65+
\* Get the next message to be received
66+
PeekMessage(pending) ≜
67+
IF Ordered
68+
THEN {Head(pending[n]) : n ∈ {n ∈ Node : pending[n] ≠ ⟨⟩}}
69+
ELSE pending
70+
71+
\* Mark a message as having been received
72+
ReceiveMessage(pending, sender, duplicate, msg) ≜
73+
IF Duplicates ∧ duplicate
74+
THEN pending
75+
ELSE IF Ordered
76+
THEN [pending EXCEPT ![sender] = Tail(@)]
77+
ELSE pending \ {msg}
78+
79+
\* Re-enqueue a message to be processed at a later time
80+
ReEnqueueMessage(pending, sender, msg) ≜
81+
IF Ordered
82+
THEN [pending EXCEPT ![sender] = Append(Tail(@), msg)]
83+
ELSE pending
84+
85+
=============================================================================
86+

‎specifications/NetworkModeling/check/CommunicatingSequentialProcesses.cfg‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
CONSTANT Node = {n1, n2}
2+
INVARIANT TypeOK
3+
PROPERTY Liveness
4+
SPECIFICATION Spec
5+

0 commit comments

Comments
 (0)