diff --git a/verification/spec/connection-handshake/updateclient-deadlock/ConnectionHandshakeModule.tla b/verification/spec/connection-handshake/updateclient-deadlock/ConnectionHandshakeModule.tla new file mode 100644 index 0000000000..22cd0d19dc --- /dev/null +++ b/verification/spec/connection-handshake/updateclient-deadlock/ConnectionHandshakeModule.tla @@ -0,0 +1,383 @@ +--------------------- MODULE ConnectionHandshakeModule --------------------- + +(*************************************************************************** + + This module is part of the TLA+ specification for the + IBC Connection Handshake protocol (ICS3). + + This module captures the actions and operators of the ICS3 protocol. + Typically, it is an IBC module running on a chain that would implement + the logic in this TLA+ module, hence the name "ConnectionHandshakeModule" + sometimes abbreviated to "chModule" or "chm". + + This module deals with a high-level spec of the ICS3 protocol, so it is + a simplification with respect to ICS3 proper in several regards: + + - the modules assumes to run on a chain which we model as a simple + advancing height, plus a few more critical fields (see the 'store'), + but without any state (e.g., blockchain, transactions, consensus core); + + - we model a single connection; establishing multiple connections is not + possible; + + - we do not perform any cryptographic proof verifications; + + - the abstractions we use are higher-level, and slightly different from + the ones in ICS3 (see e.g., ConnectionEnd and Connection records). + + - the client colocated with the module is simplified, comprising only + a set of heights (not the actual blockchain headers). + + ***************************************************************************) + +EXTENDS Naturals, FiniteSets, Sequences, ICS3Types + + +CONSTANTS MaxChainHeight, \* Maximum height of the local chain. + ConnectionIDs, \* The set of valid connection IDs. + ClientIDs, \* The set of valid client IDs. + MaxBufLen \* Maximum length of the input and output buffers. + + +ASSUME Cardinality(ConnectionIDs) >= 1 +ASSUME Cardinality(ClientIDs) >= 1 + + +VARIABLES +(******************************* Store ***************************** + + The store record of a chain contains the following fields: + + - chainID -- a string + Stores the identifier of the chain where this module executes. + + - latestHeight -- a natural number in the range 1..MaxHeight + Describes the current height of the chain. + + - connection -- a connection record. + Captures all the details of the connection on this chain. + For a full description of a connection record, see the + 'Environment.Connections' set. + + - client -- a client record. + Specifies the state of the client running on this chain. + + A client record contains the following fields: + + - consensusHeights -- a set of heights + Stores the set of all heights (i.e., consensus states) that this + client observed. + + - clientID -- a string + The identifier of the client. + + - latestHeight -- a natural number in the range 1..MaxHeight + Stores the latest height among all the heights in consensusHeights. + + For more details on how clients are initialized, see the operator + ICS3Types.InitClients. + + ***************************************************************************) + store, + (* A buffer (Sequence) holding any message(s) incoming to this module. *) + inBuf, + (* A buffer (Sequence) holding outbound message(s) from this module. *) + outBuf + + +moduleVars == + <> + + +(*************************************************************************** + Helper operators. + ***************************************************************************) + + +(* Simple computation returning the maximum out of two numbers 'a' and 'b'. + *) +MAX(a, b) == + IF a > b THEN a ELSE b + + +(* Validates a connection parameter. + + Returns true if 'para' matches the parameters in the local connection, + and returns false otherwise. + + *) +ValidConnectionParameters(para) == + LET local == store.connection.parameters.localEnd + remote == store.connection.parameters.remoteEnd + IN /\ local.connectionID = para.localEnd.connectionID + /\ remote.connectionID = para.remoteEnd.connectionID + /\ local.clientID = para.localEnd.clientID + /\ remote.clientID = para.remoteEnd.clientID + + +(* Validates a connection parameter local end. + + Expects as input a ConnectionParameter 'para' and returns true or false. + This is a basic validation step, making sure that the local end in 'para' + is valid with respect to module-level constants ConnectionIDs and ClientIDs. + +*) +ValidLocalEnd(para) == + /\ para.localEnd.connectionID \in ConnectionIDs + /\ para.localEnd.clientID \in ClientIDs + + +(* Operator for reversing the connection ends. + + Given a ConnectionParameters record 'para', returns a new set + of parameters where the local and remote ends are + flipped (i.e., reversed). + *) +FlipConnectionParameters(para) == + [localEnd |-> para.remoteEnd, + remoteEnd |-> para.localEnd] + + +(* Operator for constructing a connection proof. + + The connection proof is used to demonstrate to another chain that the + local store on this chain comprises a connection in a certain state. + *) +GetConnProof(myConnection) == + [connection |-> myConnection] + + +(* Operator for constructing a client proof. + *) +GetClientProof == + [latestHeight |-> store.client.latestHeight, + consensusHeights |-> store.client.consensusHeights] + + +(* Verification of a connection proof. + + This is a state predicate returning true if the following holds: + - the state of connection in this proof should match with input parameter + 'expectedState'; and + - the connection parameters in this proof should match with the flipped version + of the input 'expectedParams'. + + *) +VerifyConnProof(cp, expectedState, expectedParams) == + /\ cp.connection.state = expectedState + /\ cp.connection.parameters = FlipConnectionParameters(expectedParams) + + +(* Verification of a client proof. + + This is a state predicate returning true if the following holds: the height + reported in the client proof must not exceed the current (latestHeight) of + this chain. + *) +VerifyClientProof(cp) == + /\ cp.latestHeight <= store.latestHeight (* Consistency height check. *) + /\ cp.latestHeight \in cp.consensusHeights (* Client verification step. *) + + +(*************************************************************************** + Connection Handshake Module actions & operators. + ***************************************************************************) + + +(* Modifies the local store. + + Replaces the connection in the store with the argument 'newCon'. + This action also advances the chain height. + *) +NewStore(newCon) == + [store EXCEPT !.connection = newCon, + !.latestHeight = @ + 1] + + +(* Handles a "ICS3MsgInit" message 'm'. + + Primes the store.connection to become initialized with the parameters + specified in 'm'. Also creates a reply message, enqueued on the outgoing + buffer. + *) +HandleInitMsg(m) == + LET newCon == [parameters |-> m.parameters, + state |-> "INIT"] + myConnProof == GetConnProof(newCon) + myClientProof == GetClientProof + replyMsg == [parameters |-> FlipConnectionParameters(m.parameters), + type |-> "ICS3MsgTry", + proofHeight |-> store.latestHeight, + connProof |-> myConnProof, + clientProof |-> myClientProof] IN + IF /\ ValidLocalEnd(m.parameters) (* Basic validation of localEnd in parameters. *) + /\ store.connection.state = "UNINIT" + THEN [out |-> Append(outBuf, replyMsg), + store |-> NewStore(newCon)] + ELSE [out |-> outBuf, + store |-> store] + + +(* State predicate, guarding the handler for the Try msg. + + If any of these preconditions does not hold, the message + is dropped. + *) +PreconditionsTryMsg(m) == + /\ \/ /\ store.connection.state = "UNINIT" + /\ ValidLocalEnd(m.parameters) + \/ /\ store.connection.state = "INIT" + /\ ValidConnectionParameters(m.parameters) + /\ m.proofHeight \in store.client.consensusHeights (* Consistency height check. *) + /\ VerifyConnProof(m.connProof, "INIT", m.parameters) + /\ VerifyClientProof(m.clientProof) + + +(* Handles a "ICS3MsgTry" message. + *) +HandleTryMsg(m) == + LET newCon == [parameters |-> m.parameters, + state |-> "TRYOPEN"] + myConnProof == GetConnProof(newCon) + myClientProof == GetClientProof + replyMsg == [parameters |-> FlipConnectionParameters(m.parameters), + type |-> "ICS3MsgAck", + proofHeight |-> store.latestHeight, + connProof |-> myConnProof, + clientProof |-> myClientProof] IN + IF PreconditionsTryMsg(m) + THEN [out |-> Append(outBuf, replyMsg), + store |-> NewStore(newCon)] + ELSE [out |-> outBuf, + store |-> store] + + +(* State predicate, guarding the handler for the Ack msg. + *) +PreconditionsAckMsg(m) == + /\ \/ store.connection.state = "INIT" + \/ store.connection.state = "TRYOPEN" + /\ ValidConnectionParameters(m.parameters) + /\ m.proofHeight \in store.client.consensusHeights (* Consistency height check. *) + /\ VerifyConnProof(m.connProof, "TRYOPEN", m.parameters) + /\ VerifyClientProof(m.clientProof) + + +(* Handles a "ICS3MsgAck" message. + *) +HandleAckMsg(m) == + LET newCon == [parameters |-> m.parameters, + state |-> "OPEN"] + myConnProof == GetConnProof(newCon) + replyMsg == [parameters |-> FlipConnectionParameters(m.parameters), + proofHeight |-> store.latestHeight, + type |-> "ICS3MsgConfirm", + connProof |-> myConnProof] IN + IF PreconditionsAckMsg(m) + THEN [out |-> Append(outBuf, replyMsg), + store |-> NewStore(newCon)] + ELSE [out |-> outBuf, + store |-> store] + + +(* State predicate, guarding the handler for the Confirm msg. + *) +PreconditionsConfirmMsg(m) == + /\ store.connection.state = "TRYOPEN" + /\ ValidConnectionParameters(m.parameters) + /\ m.proofHeight \in store.client.consensusHeights (* Consistency height check. *) + /\ VerifyConnProof(m.connProof, "OPEN", m.parameters) + + +(* Handles a "ICS3MsgConfirm" message. + *) +HandleConfirmMsg(m) == + LET newCon == [parameters |-> m.parameters, + state |-> "OPEN"] IN + IF PreconditionsConfirmMsg(m) + THEN [out |-> outBuf, (* Never need to reply to a confirm msg. *) + store |-> NewStore(newCon)] + ELSE [out |-> outBuf, + store |-> store] + + +(* Action for advancing the current height (latestHeight) of the chain. + + The environment triggers this as part of the GoodNextEnv action. + *) +AdvanceChainHeight == + store' = [store EXCEPT !.latestHeight = @ + 1] + + +(* State predicate returning true if MaxChainHeight not yet attained. + *) +CanAdvance == + store.latestHeight < MaxChainHeight + + +(* Action for updating the local client on this chain with a new height. + + The environment triggers this as part of the GoodNextEnv action. + This primes the store; leaves the chain buffers unchanged. + This will also advance the chain height. + *) +UpdateClient(height) == + /\ store' = [store EXCEPT !.latestHeight = @ + 1, + !.client.consensusHeights = @ \cup {height}, + !.client.latestHeight = MAX(height, store.client.latestHeight)] + +CanUpdateClient(height) == + /\ CanAdvance + /\ height \notin store.client.consensusHeights + (* Warning: following line could provoke a deadlock in ICS3 protocol. *) + /\ height >= store.client.latestHeight + + +(* Generic action for handling any type of inbound message. + + Expects as parameter a message. + Takes care of invoking priming the 'store' and any reply msg in 'outBuf'. + This action assumes the message type is valid, therefore one of the + disjunctions will always enable. + *) +ProcessMsg(m) == + LET res == CASE m.type = "ICS3MsgInit" -> HandleInitMsg(m) + [] m.type = "ICS3MsgTry" -> HandleTryMsg(m) + [] m.type = "ICS3MsgAck" -> HandleAckMsg(m) + [] m.type = "ICS3MsgConfirm" -> HandleConfirmMsg(m) IN + /\ outBuf' = res.out + /\ store' = res.store + + +(*************************************************************************** + Connection Handshake Module (ICS3) main spec. + ***************************************************************************) + + +Init(chainID, client) == + /\ store = [chainID |-> chainID, + latestHeight |-> 1, + connection |-> NullConnection, + client |-> client] + + +Next == + \/ /\ inBuf # <<>> \* Enabled if we have an inbound msg. + /\ CanAdvance + /\ ProcessMsg(Head(inBuf)) \* Generic action for handling a msg. + /\ inBuf' = Tail(inBuf) \* Strip the head of our inbound msg. buffer. + \/ /\ inBuf = <<>> + /\ ~ CanAdvance + /\ UNCHANGED<> + + +TypeInvariant == + /\ inBuf \in Seq(ConnectionHandshakeMessages) \union {<<>>} + /\ outBuf \in Seq(ConnectionHandshakeMessages) \union {<<>>} + /\ store \in Stores + + +============================================================================= +\* Modification History +\* Last modified Thu May 21 08:16:28 CEST 2020 by adi +\* Created Fri Apr 24 19:08:19 CEST 2020 by adi diff --git a/verification/spec/connection-handshake/updateclient-deadlock/Environment.tla b/verification/spec/connection-handshake/updateclient-deadlock/Environment.tla new file mode 100644 index 0000000000..ff3ae4a5f5 --- /dev/null +++ b/verification/spec/connection-handshake/updateclient-deadlock/Environment.tla @@ -0,0 +1,337 @@ +---------------------------- MODULE Environment ---------------------------- + +(*************************************************************************** + + This module is part of the TLA+ specification for the IBC Connection + Handshake protocol (identifier 'ICS3'). This is a high-level spec of ICS3. + + This module captures the operators and actions outside of the CH protocol + itself (i.e., the environment). + Among others, the environment does the following: + - creates two instances of ConnectionHandshakeModule, + - wires these instances together, + - simulates some malicious behavior by injecting incorrect messages + - provides the initialization step for ICS3 protocol, concretely a + "ICS3MsgInit" message, so that the two instances can perform the protocol. + - updates the clients on each instance periodically, or advances the chain + of each instance. + + ***************************************************************************) + +EXTENDS Naturals, FiniteSets, Sequences + + +CONSTANT MaxHeight, \* Maximum height of any chain in the system. + MaxBufLen \* Length (size) of message buffers. + + +ASSUME MaxHeight > 1 +ASSUME MaxBufLen >= 1 + + +VARIABLES + inBufChainA, \* A buffer (sequence) for messages inbound to chain A. + inBufChainB, \* A buffer for messages inbound to chain B. + outBufChainA, \* A buffer for messages outgoing from chain A. + outBufChainB, \* A buffer for messages outgoing from chain B. + storeChainA, \* The local store of chain A. + storeChainB, \* The local store of chain B. + relayToA, \* Flag, signaling that the env. can relay a msg. to A. + relayToB \* Flag, signaling that the env. can relay a msg. to B. + +(************* ChainAConnectionEnds & ChainBConnectionEnds ***************** + + The set of records that each chain can use as a valid local connection + end. For each chain, this set contains one record, since we are + modeling a single connection in this specification. + + ***************************************************************************) +ChainAConnectionEnds == + [ + connectionID : { "connAtoB" }, + clientID : { "clientOnAToB" } + ] +ChainBConnectionEnds == + [ + connectionID : { "connBtoA" }, + clientID : { "clientOnBToA" } + ] + +AllConnectionEnds == + ChainAConnectionEnds \union ChainBConnectionEnds + +AllClientIDs == + { x.clientID : x \in AllConnectionEnds } + +AllConnectionIDs == + { x.connectionID : x \in AllConnectionEnds } + +AllChainIDs == + { "chainA", "chainB" } + +ChainAClientIDs == + { x.clientID : x \in ChainAConnectionEnds } + +ChainBClientIDs == + { x.clientID : x \in ChainBConnectionEnds } + +ChainAConnectionIDs == + { x.connectionID : x \in ChainAConnectionEnds } + +ChainBConnectionIDs == + { x.connectionID : x \in ChainBConnectionEnds } + + +(* Bundle with variables that chain A has access to. *) +chainAVars == <> (* The local chain store. *) + +(* Bundle with variables that chain B has access to. *) +chainBVars == <> (* Local chain store. *) + +(* All variables specific to both chains. *) +chainStoreVars == <> + +allVars == <> + + +(* Separate module with the common type definitions. *) +INSTANCE ICS3Types + +chmA == INSTANCE ConnectionHandshakeModule + WITH MaxChainHeight <- MaxHeight, + inBuf <- inBufChainA, + outBuf <- outBufChainA, + store <- storeChainA, + ConnectionIDs <- ChainAConnectionIDs, + ClientIDs <- ChainAClientIDs + + +chmB == INSTANCE ConnectionHandshakeModule + WITH MaxChainHeight <- MaxHeight, + inBuf <- inBufChainB, + outBuf <- outBufChainB, + store <- storeChainB, + ConnectionIDs <- ChainBConnectionIDs, + ClientIDs <- ChainBClientIDs + + +(*************************************************************************** + Environment actions. + ***************************************************************************) + + +(* Environment initialization. + + This action kick-starts the ICS3 protocol by assigning an ICS3MsgInit + msg to either of the two chains (or both). + + *) +InitEnv == + /\ relayToA = FALSE /\ relayToB = FALSE + /\ \/ /\ inBufChainA \in {<> : (* ICS3MsgInit to chain A. *) + msg \in InitMsgs(ChainAConnectionEnds, ChainBConnectionEnds)} + /\ inBufChainB = <<>> + \/ /\ inBufChainB \in {<> : (* ICS3MsgInit to chain B. *) + msg \in InitMsgs(ChainBConnectionEnds, ChainAConnectionEnds)} + /\ inBufChainA = <<>> + \/ /\ inBufChainA \in {<> : (* ICS3MsgInit to both chains. *) + msg \in InitMsgs(ChainAConnectionEnds, ChainBConnectionEnds)} + /\ inBufChainB \in {<> : + msg \in InitMsgs(ChainBConnectionEnds, ChainAConnectionEnds)} + /\ outBufChainA = <<>> (* Output buffers should be empty initially. *) + /\ outBufChainB = <<>> + + +(* Relay sub-action of the environment. + + This performs a basic relaying step, that is, passing a message from the + output buffer of one of the chains (paramter 'from') into the input buffer + of another chain (parameter 'to'). + + *) +RelayMessage(from, to) == + /\ from # <<>> + /\ Len(to) < MaxBufLen - 1 + /\ to' = Append(to, Head(from)) + /\ from' = Tail(from) + + +(* Updates the client on one of the chains, and updates the relay flag for that + chain (signaling that the env. is ready to relay a message to that chain). + + *) +UpdateChainClient == + \/ /\ chmA!CanUpdateClient(storeChainB.latestHeight) + /\ chmA!UpdateClient(storeChainB.latestHeight) + /\ ~ relayToA + /\ relayToA' = TRUE (* We can now relay to A. *) + /\ UNCHANGED<> + \/ /\ chmB!CanUpdateClient(storeChainA.latestHeight) + /\ chmB!UpdateClient(storeChainA.latestHeight) + /\ ~ relayToB + /\ relayToB' = TRUE (* We can now relay to B. *) + /\ UNCHANGED<> + + +(* Relaying action for the environment. + + This action performs a relaying step: moving a message between the output + buffer of a chain to the input buffer of the other chain, and updating accordingly + the client on the latter chain. + + *) +RelayNextEnv == + \/ LET msg == Head(outBufChainA) + targetHeight == IF MessageTypeIncludesConnProof(msg.type) + THEN msg.proofHeight + ELSE storeChainA.latestHeight + IN /\ RelayMessage(outBufChainA, inBufChainB) + /\ relayToB + /\ relayToB' = FALSE + /\ \/ chmB!CanUpdateClient(targetHeight) + /\ chmB!UpdateClient(targetHeight) + \/ ~ chmB!CanUpdateClient(targetHeight) + /\ UNCHANGED storeChainB + /\ UNCHANGED<> + \/ LET msg == Head(outBufChainB) + targetHeight == IF MessageTypeIncludesConnProof(msg.type) + THEN msg.proofHeight + ELSE storeChainB.latestHeight + IN /\ RelayMessage(outBufChainB, inBufChainA) + /\ relayToA + /\ relayToA' = FALSE + /\ \/ chmA!CanUpdateClient(targetHeight) + /\ chmA!UpdateClient(targetHeight) + \/ ~ chmA!CanUpdateClient(targetHeight) + /\ UNCHANGED storeChainA + /\ UNCHANGED<> + + +(* Environment next action. + + There are two possible actions that the environment may perform: + + 1. An update client step: the environment updates the client on + one of the two chains, if that chain is expecting to receive a message + (i.e., if there is a message in the ougoing buffer of the other chain). + + 2. Otherwise, the environment performs a relaying step. + + *) +NextEnv == + (* Update the clients on the corresponding chain. *) + \/ /\ (outBufChainA # <<>> \/ outBufChainB # <<>>) + /\ UpdateChainClient + (* Clients are already updated, we relay the message. *) + \/ RelayNextEnv + + +(* Enables when the connection is open on both chains. + + State predicate signaling that the protocol terminated correctly. + + *) +ICS3ReachedOpenConnection == + /\ storeChainA.connection.state = "OPEN" + /\ storeChainB.connection.state = "OPEN" + /\ UNCHANGED allVars + + +(* Enables when both chains are stuck, i.e., unable to progress while + their connection is not opened. + + State predicate signaling that the protocol terminated unsucessfully. + + *) +ICS3ImpossibleToAdvance == + /\ \/ (~ chmA!CanAdvance /\ storeChainA.connection.state # "OPEN") + \/ (~ chmB!CanAdvance /\ storeChainB.connection.state # "OPEN") + /\ UNCHANGED allVars + + +(****************************************************************************** + + Main spec. The system comprises the environment plus the two instances of + ICS3 modules. + + *****************************************************************************) + + +(* Initializes both chains, attributing to each a chainID and a client. *) +Init == + /\ \E clientA \in InitClients(ChainAClientIDs) : + chmA!Init("chainA", clientA) + /\ \E clientB \in InitClients(ChainBClientIDs) : + chmB!Init("chainB", clientB) + /\ InitEnv + + +(* The two ICS3 modules and the environment alternate their steps + non-deterministically. Eventually, the execution ends with either + successful (ICS3ReachedOpenConnection sub-action) or unsuccesfull + (ICS3ImpossibleToAdvance sub-action) termination. +*) +Next == + \/ ICS3ReachedOpenConnection + \/ ICS3ImpossibleToAdvance + \/ NextEnv + \/ chmA!Next /\ UNCHANGED <> + \/ chmB!Next /\ UNCHANGED <> + + +FairProgress == + /\ WF_chainAVars(chmA!Next) + /\ WF_chainBVars(chmB!Next) + /\ WF_<>(RelayNextEnv) + + +Spec == + /\ Init + /\ [][Next]_<> + /\ FairProgress + + +TypeInvariant == + /\ chmA!TypeInvariant + /\ chmB!TypeInvariant + + +(* Liveness property. + + We expect to always reach an OPEN connection on both chains if the following + condition holds: + both chains can advance with at least 4 more steps (4 is the minimum + number of steps that are necessary for the chains to reach OPEN). +*) +Termination == + <> [](/\ storeChainA.connection.state = "OPEN" + /\ storeChainB.connection.state = "OPEN") + + +(* Safety property. + + If the connections in the two chains are not null, then the + connection parameters must always match. + *) +ConsistencyProperty == + /\ storeChainA.connection.state # "UNINIT" + /\ storeChainB.connection.state # "UNINIT" + => storeChainA.connection.parameters + = chmB!FlipConnectionParameters(storeChainB.connection.parameters) + + +Consistency == + [] ConsistencyProperty + + +============================================================================= +\* Modification History +\* Last modified Thu May 21 08:44:06 CEST 2020 by adi +\* Created Fri Apr 24 18:51:07 CEST 2020 by adi diff --git a/verification/spec/connection-handshake/updateclient-deadlock/ICS3Types.tla b/verification/spec/connection-handshake/updateclient-deadlock/ICS3Types.tla new file mode 100644 index 0000000000..308bcc597a --- /dev/null +++ b/verification/spec/connection-handshake/updateclient-deadlock/ICS3Types.tla @@ -0,0 +1,357 @@ +----------------------------- MODULE ICS3Types ----------------------------- + +(*************************************************************************** + + This module is part of the TLA+ high-level specification for the + IBC Connection Handshake protocol (ICS3). + + This module includes common domain definitions that other modules will + extend. + + ***************************************************************************) + +EXTENDS Naturals + +CONSTANTS MaxHeight, + AllConnectionIDs, + AllClientIDs, + AllChainIDs + + +(******************************* InitClients ******************************** + + A set of records describing the possible initial values for the + clients on a chain. + + A client record contains the following fields: + + - consensusHeights -- a set of heights + Stores the set of all heights (i.e., consensus states) that this + client observed. At initialization time, the client only observes + the first height, so the only possible value for this record is + {1}. + + - clientID -- a string + The identifier of the client. This is expected as a parameter, since + it is a chain-specific field at initialization time. + + - latestHeight -- a number representing a (consensus) height + Stores the latest height among all the heights in consensusHeights. + Initialized to 1. + + ***************************************************************************) +InitClients(specificClientIDs) == + [ + consensusHeights : {{1}}, + clientID : specificClientIDs, + latestHeight : {1} + ] + + +(***************************** InitMsgs *********************************** + + The set of ConnectionHandshakeMessage records where message type is + ICS3MsgInit. + + This operator returns the set of all initialization messages, such that + the local end is the set 'le', and the remote end is set 're'. + + ***************************************************************************) +InitMsgs(le, re) == + [ + type : {"ICS3MsgInit"}, + parameters : [ + localEnd : le, + remoteEnd : re + ] + ] + + +(******************************* ICS3MessageTypes ***************************** + + The set of valid message types that the ConnectionHandshakeModule can + handle, e.g., as incoming or outgoing messages. + + In the low-level connection handshake protocol, the four messages have + types: ConnOpenInit, ConnOpenTry, ConnOpenAck, ConnOpenConfirm. + In this high-level specification, we choose slightly different names, to + make an explicit distinction to the low-level protocol. Message types + are as follows: + ICS3MsgInit, ICS3MsgTry, ICS3MsgAck, and ICS3MsgConfirm. + For a complete description of the message record, see + ConnectionHandshakeMessage below. + + ***************************************************************************) +ICS3MessageTypes == + { + "ICS3MsgInit", + "ICS3MsgTry", + "ICS3MsgAck", + "ICS3MsgConfirm" + } + + +(******************************* ICS3ConnectionStates ********************** + + The set of valid states that a connection can be in. + + ***************************************************************************) +ICS3ConnectionStates == + { + "UNINIT", + "INIT", + "TRYOPEN", + "OPEN" + } + + +NullClientID == + "NULLClientID" + +NullConnectionID == + "NULLConnectionID" + + +(******************************* NullConnectionEnd ************************* + + A special record defining an uninitialized connection end record. + + ***************************************************************************) +NullConnectionEnd == + [ + connectionID |-> NullConnectionID, + clientID |-> NullClientID + ] + + +(******************************* NullConnectionParameters ****************** + + A record defining the special null connection parameters record. + + ***************************************************************************) +NullConnectionParameters == + [ + localEnd |-> NullConnectionEnd, + remoteEnd |-> NullConnectionEnd + ] + + +(******************************* ConnectionEnds ***************************** + + A set of connection end records. + A connection end record contains the following fields: + + - connectionID -- a string + Stores the identifier of this connection, specific to a chain. + + - clientID -- a string + Stores the identifier of the client running on this chain. + + ***************************************************************************) +ConnectionEnds == + [ + connectionID : AllConnectionIDs, + clientID : AllClientIDs + ] + + +(******************************* ConnectionParameters ********************** + + A set of connection parameter records. + A connection parameter record contains the following fields: + + - localEnd -- a connection end + Specifies the local connection details (i.e., connection ID and + client ID). + + - remoteEnd -- a connection end + Specifies the remote connection details. + + ***************************************************************************) +ConnectionParameters == + [ + localEnd : ConnectionEnds, + remoteEnd : ConnectionEnds + ] + \union + { + NullConnectionParameters + } + + +(******************************* NullConnection **************************** + + Initially, the connection on both chains is uninitialized, defined as + this special record. + + ***************************************************************************) +NullConnection == [ + parameters |-> NullConnectionParameters, + state |-> "UNINIT" +] + + +(******************************* Connections ******************************* + + The set of possible connection records. + A connection record contains the following fields: + + - parameters -- a connection parameters record + Specifies the local plus remote ends. + + - state -- a connection state (see ConnectionStates set). + + ***************************************************************************) +Connections == + [ + parameters : ConnectionParameters, + state : ICS3ConnectionStates + ] + + +(******************************* ConnProof ********************************* + + A set of records describing the possible values for connection proofs. + + A connection proof record contains a single field: + + - connection -- a connection record + This is the connection (in the local store of a chain) at the moment + when the module created this proof. + + ***************************************************************************) +ConnProofs == + [ + connection : Connections + ] + + +(******************************* Heights *********************************** + + The set of all possible heights that a chain can assume throughout any + execution. + + ***************************************************************************) +Heights == + 1..MaxHeight + + +(******************************* ClientProofs ******************************* + + A set of records describing the possible values for client proofs. + + A client proof record contains two fields: + + - latestHeight -- a number representing a height + The current height (latestHeight) of the client (in the local store of a + chain) at the moment when the ICS3 module created this proof. + + - consensusHeights -- a set of heights + The set of heights of the client colocated with module which created + this proof. + + ***************************************************************************) +ClientProofs == + [ + latestHeight : Heights, + consensusHeights : SUBSET Heights + ] + + +(*********************** ConnectionHandshakeMessages *********************** + + The set of ConnectionHandshakeMessage records. + These are connection handshake specific messages that two chains exchange + while executing the ICS3 protocol. + + ***************************************************************************) +ConnectionHandshakeMessages == + [ + type : {"ICS3MsgInit"}, + parameters : ConnectionParameters + ] + \union + [ + type : {"ICS3MsgTry"}, + parameters : ConnectionParameters, + proofHeight : Heights, + connProof : ConnProofs, + clientProof : ClientProofs + ] + \union + [ + type : {"ICS3MsgAck"}, + parameters : ConnectionParameters, + proofHeight : Heights, + connProof : ConnProofs, + clientProof : ClientProofs + ] + \union + [ + type : {"ICS3MsgConfirm"}, + parameters : ConnectionParameters, + proofHeight : Heights, + connProof : ConnProofs + ] + + + +(********************** MessageTypeIncludesConnProof *********************** + + Operator that evaluates to true if the message type (input parameter + 'type') refers to a message that includes a connection proof. + + ***************************************************************************) +MessageTypeIncludesConnProof(type) == + type \in {"ICS3MsgTry", "ICS3MsgAck", "ICS3MsgConfirm"} + + +(******************************* Clients *********************************** + + A set of records describing all the possible values for the + clients on a chain. + + See client record description above (within the InitClients operator). + + ***************************************************************************) +Clients == + [ + consensusHeights : SUBSET Heights, + clientID : AllClientIDs \union { NullClientID }, + latestHeight : Heights + ] + +(******************************* Stores ************************************* + + The set of store records. + A store record represents the local storage of a chain. This record + contains the following fields: + + - chainID -- a string + Stores the identifier of the chain where this module executes. + + - latestHeight -- a number representing a height + Describes the current height of the chain. + + - connection -- a connection record + Captures all the details of the connection on this chain. + For a full description of a connection record, see the + 'Environment.Connections' set. + + - client -- a client record. + Specifies the state of the client running on this chain. + + ***************************************************************************) +Stores == + [ + chainID : AllChainIDs, + latestHeight : Heights, + connection : Connections \union { NullConnection }, + client : Clients + ] + + +============================================================================= +\* Modification History +\* Last modified Wed May 20 16:53:21 CEST 2020 by adi +\* Created Mon May 18 17:53:08 CEST 2020 by adi diff --git a/verification/spec/connection-handshake/updateclient-deadlock/MC.cfg b/verification/spec/connection-handshake/updateclient-deadlock/MC.cfg new file mode 100644 index 0000000000..628b65844b --- /dev/null +++ b/verification/spec/connection-handshake/updateclient-deadlock/MC.cfg @@ -0,0 +1,17 @@ +\* CONSTANT definitions +CONSTANT +MaxBufLen <- const_1590044123036426000 +\* CONSTANT definitions +CONSTANT +MaxHeight <- const_1590044123036427000 +\* SPECIFICATION definition +SPECIFICATION +Spec +\* INVARIANT definition +INVARIANT +TypeInvariant +ConsistencyProperty +\* PROPERTY definition +PROPERTY +Termination +\* Generated on Thu May 21 08:55:23 CEST 2020 \ No newline at end of file diff --git a/verification/spec/connection-handshake/updateclient-deadlock/MC.out b/verification/spec/connection-handshake/updateclient-deadlock/MC.out new file mode 100644 index 0000000000..ff539ed5b6 --- /dev/null +++ b/verification/spec/connection-handshake/updateclient-deadlock/MC.out @@ -0,0 +1,480 @@ +@!@!@STARTMSG 2262:0 @!@!@ +TLC2 Version 2.15 of Day Month 20?? (rev: eb3ff99) +@!@!@ENDMSG 2262 @!@!@ +@!@!@STARTMSG 2187:0 @!@!@ +Running breadth-first search Model-Checking with fp 17 and seed -8638731545884049323 with 3 workers on 4 cores with 1943MB heap and 4368MB offheap memory [pid: 26881] (Mac OS X 10.15.4 x86_64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue). +@!@!@ENDMSG 2187 @!@!@ +@!@!@STARTMSG 2220:0 @!@!@ +Starting SANY... +@!@!@ENDMSG 2220 @!@!@ +Parsing file /Users/adi/Kraftwerk/Specs/tla-playground/CHModular/CHModular.toolbox/Model_1/MC.tla +Parsing file /Users/adi/Kraftwerk/Specs/tla-playground/CHModular/CHModular.toolbox/Model_1/Environment.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202004251858/tla2sany/StandardModules/TLC.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202004251858/tla2sany/StandardModules/Naturals.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202004251858/tla2sany/StandardModules/FiniteSets.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202004251858/tla2sany/StandardModules/Sequences.tla +Parsing file /Users/adi/Kraftwerk/Specs/tla-playground/CHModular/CHModular.toolbox/Model_1/ICS3Types.tla +Parsing file /Users/adi/Kraftwerk/Specs/tla-playground/CHModular/CHModular.toolbox/Model_1/ConnectionHandshakeModule.tla +Semantic processing of module Naturals +Semantic processing of module Sequences +Semantic processing of module FiniteSets +Semantic processing of module ICS3Types +Semantic processing of module ConnectionHandshakeModule +Semantic processing of module Environment +Semantic processing of module TLC +Semantic processing of module MC +@!@!@STARTMSG 2219:0 @!@!@ +SANY finished. +@!@!@ENDMSG 2219 @!@!@ +@!@!@STARTMSG 2185:0 @!@!@ +Starting... (2020-05-21 08:55:24) +@!@!@ENDMSG 2185 @!@!@ +@!@!@STARTMSG 2212:0 @!@!@ +Implied-temporal checking--satisfiability problem has 1 branches. +@!@!@ENDMSG 2212 @!@!@ +@!@!@STARTMSG 2189:0 @!@!@ +Computing initial states... +@!@!@ENDMSG 2189 @!@!@ +@!@!@STARTMSG 2269:0 @!@!@ +Computed 2 initial states... +@!@!@ENDMSG 2269 @!@!@ +@!@!@STARTMSG 2190:0 @!@!@ +Finished computing initial states: 3 distinct states generated at 2020-05-21 08:55:26. +@!@!@ENDMSG 2190 @!@!@ +@!@!@STARTMSG 2114:1 @!@!@ +Deadlock reached. +@!@!@ENDMSG 2114 @!@!@ +@!@!@STARTMSG 2121:1 @!@!@ +The behavior up to this point is: +@!@!@ENDMSG 2121 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +1: +/\ storeChainA = [ latestHeight |-> 1, + connection |-> + [ state |-> "UNINIT", + parameters |-> + [ localEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ], + remoteEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ] ] ], + chainID |-> "chainA", + client |-> + [ clientID |-> "clientOnAToB", + latestHeight |-> 1, + consensusHeights |-> {1} ] ] +/\ storeChainB = [ latestHeight |-> 1, + connection |-> + [ state |-> "UNINIT", + parameters |-> + [ localEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ], + remoteEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ] ] ], + chainID |-> "chainB", + client |-> + [ clientID |-> "clientOnBToA", + latestHeight |-> 1, + consensusHeights |-> {1} ] ] +/\ outBufChainA = <<>> +/\ outBufChainB = <<>> +/\ inBufChainA = << [ type |-> "ICS3MsgInit", + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"] ] ] >> +/\ inBufChainB = <<>> +/\ relayToA = FALSE +/\ relayToB = FALSE + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +2: +/\ storeChainA = [ latestHeight |-> 2, + connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ], + chainID |-> "chainA", + client |-> + [ clientID |-> "clientOnAToB", + latestHeight |-> 1, + consensusHeights |-> {1} ] ] +/\ storeChainB = [ latestHeight |-> 1, + connection |-> + [ state |-> "UNINIT", + parameters |-> + [ localEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ], + remoteEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ] ] ], + chainID |-> "chainB", + client |-> + [ clientID |-> "clientOnBToA", + latestHeight |-> 1, + consensusHeights |-> {1} ] ] +/\ outBufChainA = << [ type |-> "ICS3MsgTry", + proofHeight |-> 1, + parameters |-> + [ localEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"], + remoteEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"] ], + connProof |-> + [ connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ] ], + clientProof |-> [latestHeight |-> 1, consensusHeights |-> {1}] ] >> +/\ outBufChainB = <<>> +/\ inBufChainA = <<>> +/\ inBufChainB = <<>> +/\ relayToA = FALSE +/\ relayToB = FALSE + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +3: +/\ storeChainA = [ latestHeight |-> 2, + connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ], + chainID |-> "chainA", + client |-> + [ clientID |-> "clientOnAToB", + latestHeight |-> 1, + consensusHeights |-> {1} ] ] +/\ storeChainB = [ latestHeight |-> 2, + connection |-> + [ state |-> "UNINIT", + parameters |-> + [ localEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ], + remoteEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ] ] ], + chainID |-> "chainB", + client |-> + [ clientID |-> "clientOnBToA", + latestHeight |-> 2, + consensusHeights |-> {1, 2} ] ] +/\ outBufChainA = << [ type |-> "ICS3MsgTry", + proofHeight |-> 1, + parameters |-> + [ localEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"], + remoteEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"] ], + connProof |-> + [ connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ] ], + clientProof |-> [latestHeight |-> 1, consensusHeights |-> {1}] ] >> +/\ outBufChainB = <<>> +/\ inBufChainA = <<>> +/\ inBufChainB = <<>> +/\ relayToA = FALSE +/\ relayToB = TRUE + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +4: +/\ storeChainA = [ latestHeight |-> 2, + connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ], + chainID |-> "chainA", + client |-> + [ clientID |-> "clientOnAToB", + latestHeight |-> 1, + consensusHeights |-> {1} ] ] +/\ storeChainB = [ latestHeight |-> 2, + connection |-> + [ state |-> "UNINIT", + parameters |-> + [ localEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ], + remoteEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ] ] ], + chainID |-> "chainB", + client |-> + [ clientID |-> "clientOnBToA", + latestHeight |-> 2, + consensusHeights |-> {1, 2} ] ] +/\ outBufChainA = <<>> +/\ outBufChainB = <<>> +/\ inBufChainA = <<>> +/\ inBufChainB = << [ type |-> "ICS3MsgTry", + proofHeight |-> 1, + parameters |-> + [ localEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"], + remoteEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"] ], + connProof |-> + [ connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ] ], + clientProof |-> [latestHeight |-> 1, consensusHeights |-> {1}] ] >> +/\ relayToA = FALSE +/\ relayToB = FALSE + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +5: +/\ storeChainA = [ latestHeight |-> 2, + connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ], + chainID |-> "chainA", + client |-> + [ clientID |-> "clientOnAToB", + latestHeight |-> 1, + consensusHeights |-> {1} ] ] +/\ storeChainB = [ latestHeight |-> 3, + connection |-> + [ state |-> "TRYOPEN", + parameters |-> + [ localEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"], + remoteEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ] ] ], + chainID |-> "chainB", + client |-> + [ clientID |-> "clientOnBToA", + latestHeight |-> 2, + consensusHeights |-> {1, 2} ] ] +/\ outBufChainA = <<>> +/\ outBufChainB = << [ type |-> "ICS3MsgAck", + proofHeight |-> 2, + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"] ], + connProof |-> + [ connection |-> + [ state |-> "TRYOPEN", + parameters |-> + [ localEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ], + remoteEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ] ] ] ], + clientProof |-> [latestHeight |-> 2, consensusHeights |-> {1, 2}] ] >> +/\ inBufChainA = <<>> +/\ inBufChainB = <<>> +/\ relayToA = FALSE +/\ relayToB = FALSE + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +6: +/\ storeChainA = [ latestHeight |-> 3, + connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ], + chainID |-> "chainA", + client |-> + [ clientID |-> "clientOnAToB", + latestHeight |-> 3, + consensusHeights |-> {1, 3} ] ] +/\ storeChainB = [ latestHeight |-> 3, + connection |-> + [ state |-> "TRYOPEN", + parameters |-> + [ localEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"], + remoteEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ] ] ], + chainID |-> "chainB", + client |-> + [ clientID |-> "clientOnBToA", + latestHeight |-> 2, + consensusHeights |-> {1, 2} ] ] +/\ outBufChainA = <<>> +/\ outBufChainB = << [ type |-> "ICS3MsgAck", + proofHeight |-> 2, + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"] ], + connProof |-> + [ connection |-> + [ state |-> "TRYOPEN", + parameters |-> + [ localEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ], + remoteEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ] ] ] ], + clientProof |-> [latestHeight |-> 2, consensusHeights |-> {1, 2}] ] >> +/\ inBufChainA = <<>> +/\ inBufChainB = <<>> +/\ relayToA = TRUE +/\ relayToB = FALSE + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +7: +/\ storeChainA = [ latestHeight |-> 3, + connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ], + chainID |-> "chainA", + client |-> + [ clientID |-> "clientOnAToB", + latestHeight |-> 3, + consensusHeights |-> {1, 3} ] ] +/\ storeChainB = [ latestHeight |-> 3, + connection |-> + [ state |-> "TRYOPEN", + parameters |-> + [ localEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"], + remoteEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ] ] ], + chainID |-> "chainB", + client |-> + [ clientID |-> "clientOnBToA", + latestHeight |-> 2, + consensusHeights |-> {1, 2} ] ] +/\ outBufChainA = <<>> +/\ outBufChainB = <<>> +/\ inBufChainA = << [ type |-> "ICS3MsgAck", + proofHeight |-> 2, + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"] ], + connProof |-> + [ connection |-> + [ state |-> "TRYOPEN", + parameters |-> + [ localEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ], + remoteEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ] ] ] ], + clientProof |-> [latestHeight |-> 2, consensusHeights |-> {1, 2}] ] >> +/\ inBufChainB = <<>> +/\ relayToA = FALSE +/\ relayToB = FALSE + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +8: +/\ storeChainA = [ latestHeight |-> 3, + connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ], + chainID |-> "chainA", + client |-> + [ clientID |-> "clientOnAToB", + latestHeight |-> 3, + consensusHeights |-> {1, 3} ] ] +/\ storeChainB = [ latestHeight |-> 3, + connection |-> + [ state |-> "TRYOPEN", + parameters |-> + [ localEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"], + remoteEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ] ] ], + chainID |-> "chainB", + client |-> + [ clientID |-> "clientOnBToA", + latestHeight |-> 2, + consensusHeights |-> {1, 2} ] ] +/\ outBufChainA = <<>> +/\ outBufChainB = <<>> +/\ inBufChainA = <<>> +/\ inBufChainB = <<>> +/\ relayToA = FALSE +/\ relayToB = FALSE + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2200:0 @!@!@ +Progress(9) at 2020-05-21 08:55:27: 212 states generated (3,160 s/min), 169 distinct states found (2,519 ds/min), 57 states left on queue. +@!@!@ENDMSG 2200 @!@!@ +@!@!@STARTMSG 2199:0 @!@!@ +212 states generated, 169 distinct states found, 57 states left on queue. +@!@!@ENDMSG 2199 @!@!@ +@!@!@STARTMSG 2194:0 @!@!@ +The depth of the complete state graph search is 9. +@!@!@ENDMSG 2194 @!@!@ +@!@!@STARTMSG 2268:0 @!@!@ +The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 3 and the 95th percentile is 2). +@!@!@ENDMSG 2268 @!@!@ +@!@!@STARTMSG 2186:0 @!@!@ +Finished in 4033ms at (2020-05-21 08:55:27) +@!@!@ENDMSG 2186 @!@!@ diff --git a/verification/spec/connection-handshake/updateclient-deadlock/MC.tla b/verification/spec/connection-handshake/updateclient-deadlock/MC.tla new file mode 100644 index 0000000000..1b56e1f9f4 --- /dev/null +++ b/verification/spec/connection-handshake/updateclient-deadlock/MC.tla @@ -0,0 +1,16 @@ +---- MODULE MC ---- +EXTENDS Environment, TLC + +\* CONSTANT definitions @modelParameterConstants:0MaxBufLen +const_1590044123036426000 == +2 +---- + +\* CONSTANT definitions @modelParameterConstants:1MaxHeight +const_1590044123036427000 == +5 +---- + +============================================================================= +\* Modification History +\* Created Thu May 21 08:55:23 CEST 2020 by adi diff --git a/verification/spec/connection-handshake/updateclient-deadlock/MC_TE.out b/verification/spec/connection-handshake/updateclient-deadlock/MC_TE.out new file mode 100644 index 0000000000..ff539ed5b6 --- /dev/null +++ b/verification/spec/connection-handshake/updateclient-deadlock/MC_TE.out @@ -0,0 +1,480 @@ +@!@!@STARTMSG 2262:0 @!@!@ +TLC2 Version 2.15 of Day Month 20?? (rev: eb3ff99) +@!@!@ENDMSG 2262 @!@!@ +@!@!@STARTMSG 2187:0 @!@!@ +Running breadth-first search Model-Checking with fp 17 and seed -8638731545884049323 with 3 workers on 4 cores with 1943MB heap and 4368MB offheap memory [pid: 26881] (Mac OS X 10.15.4 x86_64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue). +@!@!@ENDMSG 2187 @!@!@ +@!@!@STARTMSG 2220:0 @!@!@ +Starting SANY... +@!@!@ENDMSG 2220 @!@!@ +Parsing file /Users/adi/Kraftwerk/Specs/tla-playground/CHModular/CHModular.toolbox/Model_1/MC.tla +Parsing file /Users/adi/Kraftwerk/Specs/tla-playground/CHModular/CHModular.toolbox/Model_1/Environment.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202004251858/tla2sany/StandardModules/TLC.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202004251858/tla2sany/StandardModules/Naturals.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202004251858/tla2sany/StandardModules/FiniteSets.tla +Parsing file /Applications/TLA+ Toolbox.app/Contents/Eclipse/plugins/org.lamport.tlatools_1.0.0.202004251858/tla2sany/StandardModules/Sequences.tla +Parsing file /Users/adi/Kraftwerk/Specs/tla-playground/CHModular/CHModular.toolbox/Model_1/ICS3Types.tla +Parsing file /Users/adi/Kraftwerk/Specs/tla-playground/CHModular/CHModular.toolbox/Model_1/ConnectionHandshakeModule.tla +Semantic processing of module Naturals +Semantic processing of module Sequences +Semantic processing of module FiniteSets +Semantic processing of module ICS3Types +Semantic processing of module ConnectionHandshakeModule +Semantic processing of module Environment +Semantic processing of module TLC +Semantic processing of module MC +@!@!@STARTMSG 2219:0 @!@!@ +SANY finished. +@!@!@ENDMSG 2219 @!@!@ +@!@!@STARTMSG 2185:0 @!@!@ +Starting... (2020-05-21 08:55:24) +@!@!@ENDMSG 2185 @!@!@ +@!@!@STARTMSG 2212:0 @!@!@ +Implied-temporal checking--satisfiability problem has 1 branches. +@!@!@ENDMSG 2212 @!@!@ +@!@!@STARTMSG 2189:0 @!@!@ +Computing initial states... +@!@!@ENDMSG 2189 @!@!@ +@!@!@STARTMSG 2269:0 @!@!@ +Computed 2 initial states... +@!@!@ENDMSG 2269 @!@!@ +@!@!@STARTMSG 2190:0 @!@!@ +Finished computing initial states: 3 distinct states generated at 2020-05-21 08:55:26. +@!@!@ENDMSG 2190 @!@!@ +@!@!@STARTMSG 2114:1 @!@!@ +Deadlock reached. +@!@!@ENDMSG 2114 @!@!@ +@!@!@STARTMSG 2121:1 @!@!@ +The behavior up to this point is: +@!@!@ENDMSG 2121 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +1: +/\ storeChainA = [ latestHeight |-> 1, + connection |-> + [ state |-> "UNINIT", + parameters |-> + [ localEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ], + remoteEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ] ] ], + chainID |-> "chainA", + client |-> + [ clientID |-> "clientOnAToB", + latestHeight |-> 1, + consensusHeights |-> {1} ] ] +/\ storeChainB = [ latestHeight |-> 1, + connection |-> + [ state |-> "UNINIT", + parameters |-> + [ localEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ], + remoteEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ] ] ], + chainID |-> "chainB", + client |-> + [ clientID |-> "clientOnBToA", + latestHeight |-> 1, + consensusHeights |-> {1} ] ] +/\ outBufChainA = <<>> +/\ outBufChainB = <<>> +/\ inBufChainA = << [ type |-> "ICS3MsgInit", + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"] ] ] >> +/\ inBufChainB = <<>> +/\ relayToA = FALSE +/\ relayToB = FALSE + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +2: +/\ storeChainA = [ latestHeight |-> 2, + connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ], + chainID |-> "chainA", + client |-> + [ clientID |-> "clientOnAToB", + latestHeight |-> 1, + consensusHeights |-> {1} ] ] +/\ storeChainB = [ latestHeight |-> 1, + connection |-> + [ state |-> "UNINIT", + parameters |-> + [ localEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ], + remoteEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ] ] ], + chainID |-> "chainB", + client |-> + [ clientID |-> "clientOnBToA", + latestHeight |-> 1, + consensusHeights |-> {1} ] ] +/\ outBufChainA = << [ type |-> "ICS3MsgTry", + proofHeight |-> 1, + parameters |-> + [ localEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"], + remoteEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"] ], + connProof |-> + [ connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ] ], + clientProof |-> [latestHeight |-> 1, consensusHeights |-> {1}] ] >> +/\ outBufChainB = <<>> +/\ inBufChainA = <<>> +/\ inBufChainB = <<>> +/\ relayToA = FALSE +/\ relayToB = FALSE + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +3: +/\ storeChainA = [ latestHeight |-> 2, + connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ], + chainID |-> "chainA", + client |-> + [ clientID |-> "clientOnAToB", + latestHeight |-> 1, + consensusHeights |-> {1} ] ] +/\ storeChainB = [ latestHeight |-> 2, + connection |-> + [ state |-> "UNINIT", + parameters |-> + [ localEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ], + remoteEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ] ] ], + chainID |-> "chainB", + client |-> + [ clientID |-> "clientOnBToA", + latestHeight |-> 2, + consensusHeights |-> {1, 2} ] ] +/\ outBufChainA = << [ type |-> "ICS3MsgTry", + proofHeight |-> 1, + parameters |-> + [ localEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"], + remoteEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"] ], + connProof |-> + [ connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ] ], + clientProof |-> [latestHeight |-> 1, consensusHeights |-> {1}] ] >> +/\ outBufChainB = <<>> +/\ inBufChainA = <<>> +/\ inBufChainB = <<>> +/\ relayToA = FALSE +/\ relayToB = TRUE + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +4: +/\ storeChainA = [ latestHeight |-> 2, + connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ], + chainID |-> "chainA", + client |-> + [ clientID |-> "clientOnAToB", + latestHeight |-> 1, + consensusHeights |-> {1} ] ] +/\ storeChainB = [ latestHeight |-> 2, + connection |-> + [ state |-> "UNINIT", + parameters |-> + [ localEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ], + remoteEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ] ] ], + chainID |-> "chainB", + client |-> + [ clientID |-> "clientOnBToA", + latestHeight |-> 2, + consensusHeights |-> {1, 2} ] ] +/\ outBufChainA = <<>> +/\ outBufChainB = <<>> +/\ inBufChainA = <<>> +/\ inBufChainB = << [ type |-> "ICS3MsgTry", + proofHeight |-> 1, + parameters |-> + [ localEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"], + remoteEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"] ], + connProof |-> + [ connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ] ], + clientProof |-> [latestHeight |-> 1, consensusHeights |-> {1}] ] >> +/\ relayToA = FALSE +/\ relayToB = FALSE + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +5: +/\ storeChainA = [ latestHeight |-> 2, + connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ], + chainID |-> "chainA", + client |-> + [ clientID |-> "clientOnAToB", + latestHeight |-> 1, + consensusHeights |-> {1} ] ] +/\ storeChainB = [ latestHeight |-> 3, + connection |-> + [ state |-> "TRYOPEN", + parameters |-> + [ localEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"], + remoteEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ] ] ], + chainID |-> "chainB", + client |-> + [ clientID |-> "clientOnBToA", + latestHeight |-> 2, + consensusHeights |-> {1, 2} ] ] +/\ outBufChainA = <<>> +/\ outBufChainB = << [ type |-> "ICS3MsgAck", + proofHeight |-> 2, + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"] ], + connProof |-> + [ connection |-> + [ state |-> "TRYOPEN", + parameters |-> + [ localEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ], + remoteEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ] ] ] ], + clientProof |-> [latestHeight |-> 2, consensusHeights |-> {1, 2}] ] >> +/\ inBufChainA = <<>> +/\ inBufChainB = <<>> +/\ relayToA = FALSE +/\ relayToB = FALSE + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +6: +/\ storeChainA = [ latestHeight |-> 3, + connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ], + chainID |-> "chainA", + client |-> + [ clientID |-> "clientOnAToB", + latestHeight |-> 3, + consensusHeights |-> {1, 3} ] ] +/\ storeChainB = [ latestHeight |-> 3, + connection |-> + [ state |-> "TRYOPEN", + parameters |-> + [ localEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"], + remoteEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ] ] ], + chainID |-> "chainB", + client |-> + [ clientID |-> "clientOnBToA", + latestHeight |-> 2, + consensusHeights |-> {1, 2} ] ] +/\ outBufChainA = <<>> +/\ outBufChainB = << [ type |-> "ICS3MsgAck", + proofHeight |-> 2, + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"] ], + connProof |-> + [ connection |-> + [ state |-> "TRYOPEN", + parameters |-> + [ localEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ], + remoteEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ] ] ] ], + clientProof |-> [latestHeight |-> 2, consensusHeights |-> {1, 2}] ] >> +/\ inBufChainA = <<>> +/\ inBufChainB = <<>> +/\ relayToA = TRUE +/\ relayToB = FALSE + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +7: +/\ storeChainA = [ latestHeight |-> 3, + connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ], + chainID |-> "chainA", + client |-> + [ clientID |-> "clientOnAToB", + latestHeight |-> 3, + consensusHeights |-> {1, 3} ] ] +/\ storeChainB = [ latestHeight |-> 3, + connection |-> + [ state |-> "TRYOPEN", + parameters |-> + [ localEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"], + remoteEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ] ] ], + chainID |-> "chainB", + client |-> + [ clientID |-> "clientOnBToA", + latestHeight |-> 2, + consensusHeights |-> {1, 2} ] ] +/\ outBufChainA = <<>> +/\ outBufChainB = <<>> +/\ inBufChainA = << [ type |-> "ICS3MsgAck", + proofHeight |-> 2, + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"] ], + connProof |-> + [ connection |-> + [ state |-> "TRYOPEN", + parameters |-> + [ localEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ], + remoteEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ] ] ] ], + clientProof |-> [latestHeight |-> 2, consensusHeights |-> {1, 2}] ] >> +/\ inBufChainB = <<>> +/\ relayToA = FALSE +/\ relayToB = FALSE + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2217:4 @!@!@ +8: +/\ storeChainA = [ latestHeight |-> 3, + connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ], + chainID |-> "chainA", + client |-> + [ clientID |-> "clientOnAToB", + latestHeight |-> 3, + consensusHeights |-> {1, 3} ] ] +/\ storeChainB = [ latestHeight |-> 3, + connection |-> + [ state |-> "TRYOPEN", + parameters |-> + [ localEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"], + remoteEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ] ] ], + chainID |-> "chainB", + client |-> + [ clientID |-> "clientOnBToA", + latestHeight |-> 2, + consensusHeights |-> {1, 2} ] ] +/\ outBufChainA = <<>> +/\ outBufChainB = <<>> +/\ inBufChainA = <<>> +/\ inBufChainB = <<>> +/\ relayToA = FALSE +/\ relayToB = FALSE + +@!@!@ENDMSG 2217 @!@!@ +@!@!@STARTMSG 2200:0 @!@!@ +Progress(9) at 2020-05-21 08:55:27: 212 states generated (3,160 s/min), 169 distinct states found (2,519 ds/min), 57 states left on queue. +@!@!@ENDMSG 2200 @!@!@ +@!@!@STARTMSG 2199:0 @!@!@ +212 states generated, 169 distinct states found, 57 states left on queue. +@!@!@ENDMSG 2199 @!@!@ +@!@!@STARTMSG 2194:0 @!@!@ +The depth of the complete state graph search is 9. +@!@!@ENDMSG 2194 @!@!@ +@!@!@STARTMSG 2268:0 @!@!@ +The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 3 and the 95th percentile is 2). +@!@!@ENDMSG 2268 @!@!@ +@!@!@STARTMSG 2186:0 @!@!@ +Finished in 4033ms at (2020-05-21 08:55:27) +@!@!@ENDMSG 2186 @!@!@ diff --git a/verification/spec/connection-handshake/updateclient-deadlock/README.md b/verification/spec/connection-handshake/updateclient-deadlock/README.md new file mode 100644 index 0000000000..a72575e289 --- /dev/null +++ b/verification/spec/connection-handshake/updateclient-deadlock/README.md @@ -0,0 +1,537 @@ +# ICS3 Protocol Deadlock Scenario + +In this folder we describe a version of the ICS3 TLA+ specification that exhibits a deadlock, caused by a race condition in the way `UpdateClient` action is used. + +There are three parts to this document: + +- [A brief description of the ICS3 spec that can deadlock](#specification-details), + +- [An annotated trace of a deadlocking execution](#trace). + +### Specification details + +This specification resembles closely the default spec, so it includes three modules: `Environment`, `ConnectionHandshakeModule`, and `ICS3Types`. + +There are two main difference between this "deadlocking" version of the ICS3 protocol and the default specification: +1. The default spec allows a client on a chain to be updated with arbitrary heights, whereas this deadlocking version enforces that client updates must be monotonic. +`UpdateClient` is the action that specifies a client update, and the specific precondition for this action in the "deadlocking version" is as follows: + +``` +CanUpdateClient(height) == + /\ CanAdvance + /\ height \notin store.client.consensusHeights + (* Warning: following line could provoke a deadlock in ICS3 protocol. *) + /\ height >= store.client.latestHeight +``` + +The relevant part is the last line of this state predicate, requiring that the new height must be larger or equal than the latest height on the client. + +2. The Environment in the default spec is non-deterministic, by comprising a sub-action `DefaultNextEnv` that can simply advance the height or update the client of one of the chains non-deterministically. +In contrast, the "deadlocking" version replaces this non-determinism in the Environment with a deterministic `UpdateChainClient` sub-action; this sub-action always update the client on one of the chains if that chain is expecting an incoming message, and otherwise the sub-action is not enabled. + +The rationale behind the `UpdateChainClient` is that this sub-action should trigger before any relaying is performed, which can lead to the following problematic execution trace: + +0. Chain A creates a message `M` that has a proof for height `h`, chain A also advances its height to `h+1`. + +1. We update the client on chain B with the latest height of chain A, namely `h+1`; this is the `UpdateChainClient` deterministic sub-action. + +2. We relay message `M` that chain A created (at step 0) to chain B, and also attempt to update the client on chain B with height `h` (the height in the proof of this message), but are unable to do so because `h` is smaller than `h +1` (the latest height of client on chain B). + +3. Chain B will be unable to verify message `M` since it lacks the adequate height information `h`, so chain B will drop this message, hence a deadlock occurs. + + +#### On the termination property + +As a technical side-note, we simplify the termination property for this variant of the specification. +In the default spec, the non-determinism of `DefaultNextEnv` can make each chain advance their respective heights until they reach `MaxHeight`, and thereby becoming unable to progress any further and eventually open a connection. +For this reason, the termination property in the default spec has a precondition that each chain has not exhausted their steps, and are at least 4 steps away from `MaxHeight` (4 steps are minimum for completing the connection handshake). + +In the deadlocking version, we can expect termination to always happen. +No preconditions are necessary for the termination property, since the environment non-determinism no longer exists. +We capture the termination conditions as follows: + +``` +<> [](/\ storeChainA.connection.state = "OPEN" + /\ storeChainB.connection.state = "OPEN")) +``` + +### Trace + + +The following is an annotated trace of an execution that exhibits the deadlock. +To recreate this trace, simply import the three modules in your TLA+ toolbox and use the model as described in [MC.cfg](./MC.cfg) and [MC.tla](./MC.tla). + +#### Annotated execution trace + + << + [ + _TEAction |-> [ + position |-> 1, + name |-> "Initial predicate", + location |-> "Unknown location" + ], + inBufChainA |-> << [ type |-> "ICS3MsgInit", + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"] ] ] >>, + inBufChainB |-> <<>>, + outBufChainA |-> <<>>, + outBufChainB |-> <<>>, + relayToA |-> FALSE, + relayToB |-> FALSE, + storeChainA |-> [ latestHeight |-> 1, + connection |-> + [ state |-> "UNINIT", + parameters |-> + [ localEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ], + remoteEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ] ] ], + chainID |-> "chainA", + client |-> + [ clientID |-> "clientOnAToB", + latestHeight |-> 1, + consensusHeights |-> {1} ] ], + storeChainB |-> [ latestHeight |-> 1, + connection |-> + [ state |-> "UNINIT", + parameters |-> + [ localEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ], + remoteEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ] ] ], + chainID |-> "chainB", + client |-> + [ clientID |-> "clientOnBToA", + latestHeight |-> 1, + consensusHeights |-> {1} ] ] + ], + +In this first step of the execution trace, the connection on both chains is in "UNINIT" state, and chain A is assigned the initialization message: see `inBufChainA` variable and the record with type `ICS3MsgInit` therein. + + [ + _TEAction |-> [ + position |-> 2, + name |-> "Next", + location |-> "line 285, col 8 to line 285, col 62 of module Environment" + ], + inBufChainA |-> <<>>, + inBufChainB |-> <<>>, + outBufChainA |-> << [ type |-> "ICS3MsgTry", + proofHeight |-> 1, + parameters |-> + [ localEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"], + remoteEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"] ], + connProof |-> + [ connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ] ], + clientProof |-> [latestHeight |-> 1, consensusHeights |-> {1}] ] >>, + outBufChainB |-> <<>>, + relayToA |-> FALSE, + relayToB |-> FALSE, + storeChainA |-> [ latestHeight |-> 2, + connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ], + chainID |-> "chainA", + client |-> + [ clientID |-> "clientOnAToB", + latestHeight |-> 1, + consensusHeights |-> {1} ] ], + storeChainB |-> [ latestHeight |-> 1, + connection |-> + [ state |-> "UNINIT", + parameters |-> + [ localEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ], + remoteEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ] ] ], + chainID |-> "chainB", + client |-> + [ clientID |-> "clientOnBToA", + latestHeight |-> 1, + consensusHeights |-> {1} ] ] + ], + +In the second step, chain A finished processing the Init message and produces as output a `ICS3MsgTry` message. +As part of this step, chain A also advances its height to `2`. + + [ + _TEAction |-> [ + position |-> 3, + name |-> "NextEnv", + location |-> "line 230, col 8 to line 231, col 27 of module Environment" + ], + inBufChainA |-> <<>>, + inBufChainB |-> <<>>, + outBufChainA |-> << [ type |-> "ICS3MsgTry", + proofHeight |-> 1, + parameters |-> + [ localEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"], + remoteEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"] ], + connProof |-> + [ connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ] ], + clientProof |-> [latestHeight |-> 1, consensusHeights |-> {1}] ] >>, + outBufChainB |-> <<>>, + relayToA |-> FALSE, + relayToB |-> TRUE, + storeChainA |-> [ latestHeight |-> 2, + connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ], + chainID |-> "chainA", + client |-> + [ clientID |-> "clientOnAToB", + latestHeight |-> 1, + consensusHeights |-> {1} ] ], + storeChainB |-> [ latestHeight |-> 2, + connection |-> + [ state |-> "UNINIT", + parameters |-> + [ localEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ], + remoteEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ] ] ], + chainID |-> "chainB", + client |-> + [ clientID |-> "clientOnBToA", + latestHeight |-> 2, + consensusHeights |-> {1, 2} ] ] + ], + +At the end of step 3 of this execution, the client on chain B is updated with the latest height of chain A (namely, height `2`). +See `client` record as part of the `storeChainB` variable. +At the same time, the height of chain B also advances from `1` to `2` (see `storeChainB |-> [ latestHeight |-> 2`). + + [ + _TEAction |-> [ + position |-> 4, + name |-> "RelayNextEnv", + location |-> "line 195, col 11 to line 202, col 73 of module Environment" + ], + inBufChainA |-> <<>>, + inBufChainB |-> << [ type |-> "ICS3MsgTry", + proofHeight |-> 1, + parameters |-> + [ localEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"], + remoteEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"] ], + connProof |-> + [ connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ] ], + clientProof |-> [latestHeight |-> 1, consensusHeights |-> {1}] ] >>, + outBufChainA |-> <<>>, + outBufChainB |-> <<>>, + relayToA |-> FALSE, + relayToB |-> FALSE, + storeChainA |-> [ latestHeight |-> 2, + connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ], + chainID |-> "chainA", + client |-> + [ clientID |-> "clientOnAToB", + latestHeight |-> 1, + consensusHeights |-> {1} ] ], + storeChainB |-> [ latestHeight |-> 2, + connection |-> + [ state |-> "UNINIT", + parameters |-> + [ localEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ], + remoteEnd |-> + [ connectionID |-> "NULLConnectionID", + clientID |-> "NULLClientID" ] ] ], + chainID |-> "chainB", + client |-> + [ clientID |-> "clientOnBToA", + latestHeight |-> 2, + consensusHeights |-> {1, 2} ] ] + ], + +At step 4, a relay sub-action is performed: the `ICS3MsgTry` message that chain A has produced earlier is moved into the input buffer of chain B. + + [ + _TEAction |-> [ + position |-> 5, + name |-> "Next", + location |-> "line 286, col 8 to line 286, col 62 of module Environment" + ], + inBufChainA |-> <<>>, + inBufChainB |-> <<>>, + outBufChainA |-> <<>>, + outBufChainB |-> << [ type |-> "ICS3MsgAck", + proofHeight |-> 2, + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"] ], + connProof |-> + [ connection |-> + [ state |-> "TRYOPEN", + parameters |-> + [ localEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ], + remoteEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ] ] ] ], + clientProof |-> [latestHeight |-> 2, consensusHeights |-> {1, 2}] ] >>, + relayToA |-> FALSE, + relayToB |-> FALSE, + storeChainA |-> [ latestHeight |-> 2, + connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ], + chainID |-> "chainA", + client |-> + [ clientID |-> "clientOnAToB", + latestHeight |-> 1, + consensusHeights |-> {1} ] ], + storeChainB |-> [ latestHeight |-> 3, + connection |-> + [ state |-> "TRYOPEN", + parameters |-> + [ localEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"], + remoteEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ] ] ], + chainID |-> "chainB", + client |-> + [ clientID |-> "clientOnBToA", + latestHeight |-> 2, + consensusHeights |-> {1, 2} ] ] + ], + +At the end of this step, chain B finished processing the `ICS3MsgTry` message and produced a `ICS3MsgAck` message. +It is important to note that the height of the proof in this Ack message is `2` (see `proofHeight |-> 2`). +Additionally, chain B also advanced from height `2` to `3`. + + [ + _TEAction |-> [ + position |-> 6, + name |-> "NextEnv", + location |-> "line 230, col 8 to line 231, col 27 of module Environment" + ], + inBufChainA |-> <<>>, + inBufChainB |-> <<>>, + outBufChainA |-> <<>>, + outBufChainB |-> << [ type |-> "ICS3MsgAck", + proofHeight |-> 2, + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"] ], + connProof |-> + [ connection |-> + [ state |-> "TRYOPEN", + parameters |-> + [ localEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ], + remoteEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ] ] ] ], + clientProof |-> [latestHeight |-> 2, consensusHeights |-> {1, 2}] ] >>, + relayToA |-> TRUE, + relayToB |-> FALSE, + storeChainA |-> [ latestHeight |-> 3, + connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ], + chainID |-> "chainA", + client |-> + [ clientID |-> "clientOnAToB", + latestHeight |-> 3, + consensusHeights |-> {1, 3} ] ], + storeChainB |-> [ latestHeight |-> 3, + connection |-> + [ state |-> "TRYOPEN", + parameters |-> + [ localEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"], + remoteEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ] ] ], + chainID |-> "chainB", + client |-> + [ clientID |-> "clientOnBToA", + latestHeight |-> 2, + consensusHeights |-> {1, 2} ] ] + ], + +At the end of step 6, the client on chain A is updated with the latest height of chain B, consequently, this client will store the set of heights: `consensusHeights |-> {1, 3}`. + + [ + _TEAction |-> [ + position |-> 7, + name |-> "RelayNextEnv", + location |-> "line 207, col 11 to line 214, col 73 of module Environment" + ], + inBufChainA |-> << [ type |-> "ICS3MsgAck", + proofHeight |-> 2, + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"] ], + connProof |-> + [ connection |-> + [ state |-> "TRYOPEN", + parameters |-> + [ localEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ], + remoteEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ] ] ] ], + clientProof |-> [latestHeight |-> 2, consensusHeights |-> {1, 2}] ] >>, + inBufChainB |-> <<>>, + outBufChainA |-> <<>>, + outBufChainB |-> <<>>, + relayToA |-> FALSE, + relayToB |-> FALSE, + storeChainA |-> [ latestHeight |-> 3, + connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ], + chainID |-> "chainA", + client |-> + [ clientID |-> "clientOnAToB", + latestHeight |-> 3, + consensusHeights |-> {1, 3} ] ], + storeChainB |-> [ latestHeight |-> 3, + connection |-> + [ state |-> "TRYOPEN", + parameters |-> + [ localEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"], + remoteEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ] ] ], + chainID |-> "chainB", + client |-> + [ clientID |-> "clientOnBToA", + latestHeight |-> 2, + consensusHeights |-> {1, 2} ] ] + ], + +We now perform a relay step, moving the `ICS3MsgAck` from the output buffer of chain B into the input buffer of chain A. +As part of relaying, the client on chain A is also updated (if possible) with the height that is reported in the proof from this messages, namely, height `2`. +This update is skipped, however, since the client on chain A already stores a higher height `3` (the update for this height occured earlier at step 6). + + [ + _TEAction |-> [ + position |-> 8, + name |-> "Next", + location |-> "line 285, col 8 to line 285, col 62 of module Environment" + ], + inBufChainA |-> <<>>, + inBufChainB |-> <<>>, + outBufChainA |-> <<>>, + outBufChainB |-> <<>>, + relayToA |-> FALSE, + relayToB |-> FALSE, + storeChainA |-> [ latestHeight |-> 3, + connection |-> + [ state |-> "INIT", + parameters |-> + [ localEnd |-> + [connectionID |-> "connAtoB", clientID |-> "clientOnAToB"], + remoteEnd |-> + [ connectionID |-> "connBtoA", + clientID |-> "clientOnBToA" ] ] ], + chainID |-> "chainA", + client |-> + [ clientID |-> "clientOnAToB", + latestHeight |-> 3, + consensusHeights |-> {1, 3} ] ], + storeChainB |-> [ latestHeight |-> 3, + connection |-> + [ state |-> "TRYOPEN", + parameters |-> + [ localEnd |-> + [connectionID |-> "connBtoA", clientID |-> "clientOnBToA"], + remoteEnd |-> + [ connectionID |-> "connAtoB", + clientID |-> "clientOnAToB" ] ] ], + chainID |-> "chainB", + client |-> + [ clientID |-> "clientOnBToA", + latestHeight |-> 2, + consensusHeights |-> {1, 2} ] ] + ] + >> + +At the final step, chain A effectively drops the `ICS3MsgAck` message since it cannot verify the proof (`proofHeight |-> 2,`) in this message. \ No newline at end of file