1\*
2\* %CopyrightBegin%
3\*
4\* Copyright Ericsson AB 2021. All Rights Reserved.
5\*
6\* Licensed under the Apache License, Version 2.0 (the "License");
7\* you may not use this file except in compliance with the License.
8\* You may obtain a copy of the License at
9\*
10\*     http://www.apache.org/licenses/LICENSE-2.0
11\*
12\* Unless required by applicable law or agreed to in writing, software
13\* distributed under the License is distributed on an "AS IS" BASIS,
14\* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15\* See the License for the specific language governing permissions and
16\* limitations under the License.
17\*
18\* %CopyrightEnd%
19\*
20
21(*
22    --- Model of the new link protocol introduced in Erlang/OTP 23.3 ---
23
24    The protocol is documented in the ERTS User's Guide ->
25    Distribution Protocol -> Protocol Between Connected Nodes ->
26    Link Protocol -> New Link Protocol
27
28    This model only models a link between two processes. This since a link
29    between one pair of processes is completely independent of links between
30    other pairs of processes. This model also assumes that the connection
31    between the processes does not fail. In the real world a connection can
32    of course fail. This is however taken care of by clearing the link
33    information on both ends when a connection fails, and tracking which
34    instantiation of a connection between the nodes signals arrive on and
35    ignoring signals from old instantiations of connections. That is,
36    connection loss is trivially taken care of since we just start over
37    again from scratch if the connection is lost.
38
39    The documentation of the protocol talks about "process local information
40    about links". This information is stored in the process state record below.
41    The 'other' field contains the identifier of the other process. The 'type'
42    field acts as "active flag". The link is active when 'type' equals
43    "linked" and not active when 'type' equals "unlinked". If the
44    'wait_unlink_ack' field contains a value larger than or equal to zero
45    it is the "unlink id" of an unlink request we have issued and are waiting
46    for to get acknowledged. If the 'wait_unlink_ack' field contains -1 we
47    are not waiting for an acknowledgment. When 'type' equals "unlinked" and
48    'wait_unlink_ack' equals -1, we would in the documented protocol have
49    removed the "process local information about the link". In this model we,
50    however, keep the state, but in this state instead of removing it.
51    Messages are tagged with a message number in order to model the signal
52    order of Erlang. The message number of the unlink signal is also used as
53    "unlink id".
54
55    The model has been checked with the following parameters:
56
57      Declared constants:
58        PROCS <- {"a", "b"}
59
60      Temporal formula:
61        FairSpec
62
63      Deadlock:
64        disabled
65
66      Invariants:
67        TypeOK
68        ValidState
69
70      State Constraint:
71        /\ \E proc \in PROCS : procState[proc].next_send =< 15
72        /\ Cardinality(msgs) =< 10
73
74    That is, we have checked all states where processes send up to 15 signals
75    with at most 10 outstanding signals.
76
77    Deadlock checking has been disabled since we intentionally stop when
78    we have no outstanding signals (in 'Next') in order to avoid checking
79    signal sequences equivalent to sequences we already have checked.
80
81*)
82------------------------------ MODULE NewLinking ------------------------------
83EXTENDS Integers, TLC, FiniteSets
84CONSTANTS PROCS \* PROCS should be a set of exactly two process names
85
86VARIABLES
87    procState, \* Set of process states; procState[proc] is state of proc
88    msgs \* Set of messages sent
89
90vars == <<procState, msgs>>
91
92\* Set of possible process states...
93procStateRec ==
94    [self : PROCS,
95     other: PROCS,
96     type : {"linked", "unlinked"},
97     wait_unlink_ack : Nat \cup {-1},
98     next_send : Nat,
99     next_recv : Nat]
100
101\* Set of possible messages...
102Messages ==
103  [type : {"link", "unlink", "unlink_ack"}, from : PROCS, to : PROCS, msg_no : Nat, ack : Nat \cup {-1}]
104
105TypeOK ==
106   /\ procState \in [PROCS -> procStateRec]
107   /\ msgs \subseteq Messages
108
109Init ==
110    /\ msgs = {}
111    /\ procState = [p \in PROCS |-> [self |-> p,
112                                     other |-> CHOOSE p2 \in PROCS : p2 /= p,
113                                     type |-> "unlinked",
114                                     next_send |-> 0,
115                                     next_recv |-> 0,
116                                     wait_unlink_ack |-> -1]]
117
118MkMsg(self, mtype, accnr) ==
119  [type |-> mtype,
120   from |-> procState[self].self,
121   to |-> procState[self].other,
122   msg_no |-> procState[self].next_send,
123   ack |-> accnr]
124
125Link(self) ==
126  /\ procState[self].type = "unlinked"
127  /\ msgs' = msgs \cup {MkMsg(self, "link", -1)}
128  /\ procState' = [procState EXCEPT ![self].type = "linked",
129                                    ![self].next_send = @ + 1,
130                                    ![self].wait_unlink_ack = -1]
131
132Unlink(self) ==
133  /\ procState[self].type = "linked"
134  /\ msgs' = msgs \cup {MkMsg(self, "unlink", -1)}
135  /\ procState' = [procState EXCEPT ![self].type = "unlinked",
136                                    ![self].next_send = @ + 1,
137                                    ![self].wait_unlink_ack = procState[self].next_send]
138
139RecvLink(self, msg) ==
140   LET type == IF procState[self].wait_unlink_ack /= -1
141               THEN "unlinked"
142               ELSE "linked"
143   IN /\ msgs' = msgs \ {msg}
144      /\ procState' = [procState EXCEPT ![self].type = type,
145                                        ![self].next_recv = @ + 1]
146
147RecvUnlink(self, msg) ==
148  /\ msgs' = (msgs \ {msg}) \cup {MkMsg(self,
149                                        "unlink_ack",
150                                        procState[self].next_recv)}
151  /\ procState' = [procState EXCEPT ![self].type = "unlinked",
152                                    ![self].next_recv = @ + 1,
153                                    ![self].next_send = @ + 1]
154
155RecvUnlinkAck(self, msg) ==
156   LET wack == IF procState[self].wait_unlink_ack = msg.ack
157               THEN -1
158               ELSE procState[self].wait_unlink_ack
159   IN /\ msgs' = msgs \ {msg}
160      /\ procState' = [procState EXCEPT ![self].next_recv = @ + 1,
161                                        ![self].wait_unlink_ack = wack]
162
163Recv(self) ==
164  /\ \E m \in msgs : /\ m.to = self
165                     /\ m.msg_no = procState[self].next_recv
166  /\ LET msg == CHOOSE m \in msgs : /\ m.to = self
167                                    /\ m.msg_no = procState[self].next_recv
168     IN CASE msg.type = "link" -> RecvLink(self, msg)
169          [] msg.type = "unlink" -> RecvUnlink(self, msg)
170          [] msg.type = "unlink_ack" -> RecvUnlinkAck(self, msg)
171
172(*
173   If we have no outstanding messages; both processes should
174   have the same view about whether they are linked or not...
175*)
176ValidState ==
177  IF msgs /= {}
178  THEN TRUE
179  ELSE \A p \in PROCS : \A p2 \in PROCS : procState[p].type = procState[p2].type
180
181Next ==
182    /\ (msgs /= {} \/ \A p \in PROCS : procState[p].next_send = 0)
183    /\ \E p \in PROCS : \/ Recv(p)
184                        \/ Link(p)
185                        \/ Unlink(p)
186
187Spec == Init /\ [][Next]_vars
188
189FairSpec == Spec /\ WF_vars(Next)
190
191=============================================================================
192\* Modification History
193\* Last modified Mon Jan 25 11:26:06 CET 2021 by rickard.green
194\* Created Wed Jan 20 13:11:46 CET 2021 by rickard.green
195