--------------------------- MODULE WSAtomicTransaction----------------------- EXTENDS TLC (***************************************************************************) (* This is a preliminary version of a formal specification of the Web *) (* Services Atomic Transaction protocol, described in the document by *) (* Cabrera et al. We are specifying the safety property of the protocol *) (* (what is allowed to happen), not its liveness property (what must *) (* eventually happen). *) (* *) (* The protocol involves an initiator, a transaction coordinator (TC), and *) (* a set of participants. The TC exchanges messages with the *) (* participants. For convenience, we assume that the initiator and TC are *) (* actually executed on the same processor, so they can be considered to *) (* be a single process. *) (* *) (* The protocol allows messages to be lost, duplicated, or received out *) (* of order. A process is therefore free to resend a message at any *) (* time. An implementation will resend a message if it times out without *) (* receiving a reply. Such resending is not described explicitly in the *) (* specification. Instead, we represent the communication infrastructure *) (* by a set msgs of all messages that have ever been sent. Since *) (* resending a sent message does not change the specification's state, it *) (* is allowed by our specification. *) (* *) (* An action that, in an implementation, would be enabled by the receipt *) (* of certain messages is here enabled by the existence of those messages *) (* in msgs. Loss of a message is represented by simply not executing *) (* that action, even though it is enabled. This works because we are *) (* specifying only safety properties, so there is no requirement that an *) (* enabled action is ever executed. *) (* *) (* Since messages are never removed from msgs, receipt of the same message *) (* twice is allowed. This can happen in an implementation either because *) (* the communication infrastructure delivers a duplicate copy, or because *) (* the sender mistakenly believed the original copy had been lost and *) (* resent the message. In most cases, the specification says that such *) (* duplicate copies are ignored because the response has already been *) (* sent, so msgs already contains the response. However, in an *) (* implementation, receipt of a duplicate message may indicate that the *) (* sender resent the message because it never received the response. *) (* Hence, an implementation would resend the response. The specification *) (* sometimes asserts that such responses are in msgs, indicating that they *) (* would probably be resent in an implementation. *) (***************************************************************************) (***************************************************************************) (* The CONSTANT and VARIABLES sections define constant parameters and *) (* variables. *) (***************************************************************************) CONSTANT Participant \* The set of all participants. VARIABLES iState, \* The state of the initiator. tcData, \* The data maintained by the coordinator. pData, \* pData[p] is the data maintained by participate p. msgs \* The set of all sent messages. Message == (*************************************************************************) (* The set of all possible messages. A message sent from the TC to a *) (* participant has a dest field indicating its destination. A message *) (* from a participant to the TC has a src field indicating its sender. *) (* A participant's "Register" message also has a reg field indicating if *) (* it's registering as volatile or durable. *) (*************************************************************************) [type : {"RegisterResponse", "Prepare", "Commit", "Rollback"}, dest : Participant] \cup [type : {"Prepared", "ReadOnly", "Committed", "Aborted"}, src : Participant] \cup [type : {"Register"}, reg : {"volatile", "durable"}, src : Participant] TypeOK == (*************************************************************************) (* The type-correctness invariant, indicating the possible values that *) (* can be assumed by the variables. *) (*************************************************************************) /\ iState \in {"active", "committed", "aborted", "completing"} (**********************************************************************) (* Because we are assuming that the initiator and the TC are the same *) (* process, there is no need for the initiator to have a separate *) (* "aborting" state. Once the decision to abort has been made by *) (* the TC, the then initiator knows that the transaction is aborted. *) (* *) (* For convenience, we ignore the action in which the initiator *) (* registers the transaction with the TC. Instead, we assume that the *) (* initiator and TC begin in the "active" state. We also assume that *) (* the initiator never forgets the outcome. (In an implementation, *) (* the initiator can forget about the transaction as soon as it knows *) (* the outcome. It is forgetting by the TC that's tricky.) *) (**********************************************************************) /\ tcData \in [st : {"active", "preparingVolatile", "preparingDurable", "aborting", "committing"}, reg : [Participant -> {"unregistered", "volatile", "durable", "prepared", "readOnly", "committed"}]] \cup [st : {"ended"}, res : {"committed", "aborted"}] (********************************************************************) (* tcData has an st component that indicates the TC's state. *) (* While the TC is performing the transaction, tcData also has a *) (* reg field such that tcData.reg[p] indicates the TC's knowledge *) (* of the state of participant p. The TC enters the "ended" state *) (* when it forgets about the transaction. For convenience in *) (* understanding the protocol, when tcData = "ended", we let *) (* tcData have a res component that indicates the outcome (whether *) (* the transaction committed or aborted). No TC actions depend on *) (* the value of tcData.res. *) (* *) (* Note: The document "Web Services Atomic Transaction Commit" *) (* lists a "Preparing" and a "PreparedSuccess" state. We have *) (* split the "Preparing" state into "preparingVolatile", entered *) (* initially, and "preparingDurable", entered after all volatile *) (* participants have prepared. We have eliminated the *) (* "PreparedSuccess" state because that is an internal state, not *) (* visible to other processes. We model the protocol by having the *) (* TC go directly from the "preparingDurable" state into either the *) (* "Committing" or "Aborting" state. (An implementation is free to *) (* split any of our specification's states into substates.) *) (********************************************************************) /\ pData \in [Participant -> [st : {"unregistered", "prepared"}] \cup [st : {"registering", "active", "preparing"}, reg : {"volatile", "durable"}] \cup [st : {"ended"}, res : {"?", "committed", "aborted"}]] (********************************************************************) (* pData[p] is the data maintained by participant p. It contains *) (* an st field indicating the participant's state. When in the *) (* "registering" or "active" state, there is also a reg field *) (* indicating if the participant is volatile or durable. When a *) (* registered participant forgets about the transaction, it enters *) (* the "ended" state. *) (* *) (* To help us understand the protocol, when pData[p].st = "ended", *) (* there is a field pData[p].res that indicates the participant's *) (* knowledge of the outcome when it forgot about the transaction. *) (* The value "?" indicates that the participant was read-only, so *) (* it didn't learn the outcome. *) (* *) (* Note that the document "Web Services Atomic Transaction Commit" *) (* does not distinguish between the "unregistered" and *) (* "registering" state, which it lumps with the "ended" state into *) (* a single "None" state. The document also has "Prepared" and *) (* "PreparedSuccess" states that we have combined into the single *) (* "prepared" state. Those states are not visible externally (that *) (* is, by the TC) as different states. (An implementation is free *) (* to split any of our specification's states into substates.) We *) (* might have lumped the "preparing" and "prepared" states together *) (* as well, but it seems convenient to keep them separated because *) (* of the interaction of preparing and registration of durable *) (* participants. *) (* *) (* We have also eliminated the "committing" and "aborting" states, *) (* having the participant immediately forget the transaction by *) (* going to the "ended" state. In a similar way, we could have *) (* eliminated the "aborting" state of the TC, but didn't for no *) (* good reason. Perhaps we will in the next version. *) (********************************************************************) /\ msgs \subseteq Message (********************************************************************) (* msgs equals a set of messages. *) (********************************************************************) Consistency == (*************************************************************************) (* A predicate that implies that the protocol is not in an inconsistent *) (* final or finishing state--that is, where one process thinks the *) (* protocol committed and another thinks it has aborted. There are two *) (* separate conjuncts, one asserting what's true if the initiator has *) (* reached the "committed" state, and the other asserting what's true if *) (* a participant has reached the "committed" state. These two conjuncts *) (* are not logically independent, but we have not eliminated the *) (* redundancy in order to make it clear what is being asserted. The *) (* invariance of this predicate is the correctness property that we *) (* check. *) (*************************************************************************) /\ (iState = "committed") => \/ /\ tcData.st = "ended" /\ tcData.res = "committed" /\ \A p \in Participant : \/ pData[p].st = "unregistered" \/ /\ pData[p].st = "ended" /\ pData[p].res \in {"?", "committed"} \/ /\ tcData.st = "committing" /\ \A p \in Participant : \/ pData[p].st \in {"unregistered", "prepared"} \/ /\ pData[p].st = "ended" /\ pData[p].res \in {"?", "committed"} /\ \A p \in Participant : /\ pData[p].st = "ended" /\ pData[p].res = "committed" => /\ iState = "committed" /\ \/ /\ tcData.st = "ended" /\ tcData.res = "committed" /\ iState = "committed" \/ tcData.st = "committing" /\ \A pp \in Participant : \/ pData[pp].st \in {"unregistered", "prepared"} \/ /\ pData[pp].st = "ended" /\ pData[pp].res \in {"?", "committed"} Init == (*************************************************************************) (* The initial predicate. *) (*************************************************************************) /\ iState = "active" /\ tcData = [st |-> "active", reg |-> [p \in Participant |-> "unregistered"]] /\ pData = [p \in Participant |-> [st |-> "unregistered"]] /\ msgs = {} ----------------------------------------------------------------------------- (***************************************************************************) (* THE ACTIONS *) (* *) (* The next-state action is the disjunction of the four actions *) (* TCInternal, TCRcvMsg, PInternal, and PRcvMsg. The major part of the *) (* specification consists of the definitions of these four actions, which *) (* follow. *) (***************************************************************************) TCInternal == (*************************************************************************) (* This action describes the actions of the initiator and the internal *) (* actions of the TC--that is, the actions of the initiator prompted by *) (* timeouts or by a spontaneous action of the initiator. It also *) (* describes actions enabled by the TC having received enough messages. *) (* (Those actions could be described as occurring when the the TC *) (* receives the last message needed to enable it, but it's more *) (* convenient to let it be done as a separate internal action.) *) (*************************************************************************) /\ \/ (*******************************************************************) (* The initiator decides to commit the transaction. It sets its *) (* state to "completing". At the same time, the TC sets its state *) (* to "preparingVolatile" and sends "Prepare" messages to every *) (* participant that has registered as volatile. *) (*******************************************************************) /\ iState = "active" /\ \A p \in Participant : (pData[p].st = "registering") => /\ pData[p].reg = "durable" /\ \E pp \in Participant : /\ pData[pp].st \in {"active", "preparing"} /\ pData[pp].reg = "volatile" (****************************************************************) (* The only participants that may be registering are durable *) (* ones that are being installed by a volatile participant that *) (* is not yet prepared. It is up to the application to ensure *) (* that this condition is met. *) (****************************************************************) /\ iState' = "completing" /\ tcData' = [tcData EXCEPT !.st = "preparingVolatile"] /\ msgs' = msgs \cup [type : {"Prepare"}, dest : {p \in Participant : tcData.reg[p] = "volatile"}] \/ (*******************************************************************) (* Either the initiator decides to abort the transaction while in *) (* its "active" state, or else the TC decides to abort it while in *) (* a "preparing" state--presumably because of some timeout. The *) (* initiator's state is set to "aborted", the TC state is set to *) (* "aborting", and "Rollback" messages are sent to every *) (* registered participant from which the TC did not already *) (* receive a "ReadOnly" message. *) (*******************************************************************) /\ \/ iState = "active" \/ tcData.st \in {"preparingVolatile", "preparingDurable"} /\ iState' = "aborted" /\ tcData' = [tcData EXCEPT !.st = "aborting"] /\ msgs' = msgs \cup [type : {"Rollback"}, dest : {p \in Participant : tcData.reg[p] \notin {"unregistered", "readOnly"}}] \/ (*******************************************************************) (* The TC ends the volatile prepare and begins the durable *) (* prepare. It does this when it has received "Prepared" or *) (* "ReadOnly" messages from every participant that registered as *) (* volatile, and it sends "Prepare" message to every participant *) (* that registered as durable. *) (*******************************************************************) /\ tcData.st = "preparingVolatile" /\ \A p \in Participant : tcData.reg[p] # "volatile" /\ tcData' = [tcData EXCEPT !.st = "preparingDurable"] /\ msgs' = msgs \cup [type : {"Prepare"}, dest : {p \in Participant : tcData.reg[p] = "durable"}] /\ UNCHANGED iState \/ (*******************************************************************) (* The TC finishes the durable prepare and decides to commit the *) (* transaction. It can do this when it has received a "Prepared" *) (* or "ReadOnly" message from every durable particpant. It sets *) (* its state to "committing", notifies the initiator that the *) (* transaction has committed, and sends "Commit" messages to every *) (* participant that replied with a "Prepared" message (instead of *) (* a "ReadOnly" message). *) (*******************************************************************) /\ tcData.st = "preparingDurable" /\ \A p \in Participant : tcData.reg[p] # "durable" /\ tcData' = [tcData EXCEPT !.st = "committing"] /\ msgs' = msgs \cup [type : {"Commit"}, dest : {p \in Participant : tcData.reg[p] = "prepared"}] /\ iState' = "committed" \/ (*******************************************************************) (* The action by which the TC forgets the transaction, entering *) (* the "ended" state. It can do this if it is in the "aborting" *) (* state, or if it is in the "committing" state and has received a *) (* "ReadOnly" or "Committed" message from every registered *) (* participant. *) (*******************************************************************) /\ \/ tcData.st = "aborting" \/ /\ tcData.st = "committing" /\ \A p \in Participant : tcData.reg[p] \in {"unregistered", "readOnly", "committed"} /\ tcData' = [st |-> "ended", res |-> IF tcData.st = "aborting" THEN "aborted" ELSE "committed"] /\ UNCHANGED <> /\ UNCHANGED pData (********************************************************************) (* The participants' states are left unchanged. *) (********************************************************************) (***************************************************************************) (* The following action definition uses the TLA+ construct *) (* *) (* CASE B1 -> P1 [] ... [] Bn -> Pn *) (* *) (* This construct is used here (and in most places) when the state *) (* predicates Bi, which are called the `guards', are mutually *) (* disjoint--that is, no two of them can be true in the same state. When *) (* the guards are mutually disjoint, the CASE expression equals `Pi' if *) (* guard Bi is true. If none of the guards are true, then the value of *) (* the expression is undefined. If TLC ever evaluates such an undefined *) (* expression, it reports an error. Thus, this CASE statement is *) (* equivalent to the formula *) (* *) (* (B1 /\ P1) \/ ... \/ (Bn /\ Pn) *) (* *) (* except that when none of the guards are true, the formula equals FALSE *) (* while the value of the CASE statement is undefined. *) (* *) (* In this following action, the guards of each CASE formula describe all *) (* the possible cases in which the TC can receive a particular message. *) (***************************************************************************) TCRcvMsg == (*************************************************************************) (* The action in which the TC receives a message from a participant. *) (*************************************************************************) \E m \in msgs : (**********************************************************************) (* m is the message being received. *) (**********************************************************************) LET Reply(tp) == msgs' = msgs \cup {[type |-> tp, dest |-> m.src]} (******************************************************************) (* Locally defines Reply(tp) to be the action of sending a *) (* message of type tp to the sender of message m. *) (******************************************************************) HaveSent(tp) == \E mm \in msgs : (mm.type = tp) /\ (mm.dest = m.src) (******************************************************************) (* Locally defines HaveSent(tp) to be true iff the TC has sent a *) (* message of type tp to the sender of m. *) (******************************************************************) IN \/ (****************************************************************) (* m is a "Register" message. *) (****************************************************************) /\ m.type = "Register" /\ CASE (********************************************************) (* The normal case, in which the TC state is either *) (* "active", or else this is a durable participant *) (* registering while the TC is performing the volatile *) (* prepare. *) (********************************************************) \/ tcData.st = "active" \/ /\ tcData.st = "preparingVolatile" /\ m.reg = "durable" -> (********************************************************) (* The TC sends a "RegisterResponse" reply to the *) (* sender, and sets the appropriate tcData.reg *) (* component (the one corresponding to the sender) to *) (* the contents of the reg field of m. *) (********************************************************) /\ Reply("RegisterResponse") /\ tcData' = [tcData EXCEPT !.reg[m.src] = m.reg] [] (********************************************************) (* If the TC is in a "preparing" or "committing" state *) (* or has forgotten the transaction, then m is a *) (* duplicate message to which the TC has already *) (* responded and so is ignored. *) (********************************************************) /\ \/ /\ tcData.st = "preparingVolatile" /\ m.reg = "volatile" \/ tcData.st \in {"preparingDurable", "committing"} /\ HaveSent("RegisterResponse") -> UNCHANGED <> [] (********************************************************) (* If the TC is in the "aborting" state, then if the *) (* sender is not already registered, then the decision *) (* to abort was made before the sender could register, *) (* in which case a "Rollback" message is sent. (Is *) (* this correct?) Otherwise, this is a duplicate *) (* message to which the TC has already responded, and *) (* it has already sent a "Rollback" message to the *) (* sender (unless the participant responded "ReadOnly" *) (* to a "Prepare" message). *) (********************************************************) /\ tcData.st = "aborting" /\ \/ tcData.reg[m.src] \in {"unregistered", "readOnly"} \/ /\ tcData.reg[m.src] \in {"volatile", "durable", "prepared"} /\ HaveSent("Rollback") -> /\ IF tcData.reg[m.src] = "unregistered" THEN Reply("Rollback") ELSE UNCHANGED msgs /\ UNCHANGED tcData [] (********************************************************) (* If the TC is in the "ended" state, then either the *) (* transaction has been aborted before the sender had a *) (* chance to register, or else the "Register" message *) (* is old and, if it was committed, then the sender *) (* has already forgotten the transaction and hence will *) (* ignore any message it receives. Therefore, it's *) (* safe to send a "Rollback" message. *) (********************************************************) /\ tcData.st = "ended" /\ \/ tcData.res = "aborted" \/ pData[m.src].st = "ended" -> /\ Reply("Rollback") /\ UNCHANGED tcData /\ UNCHANGED <> (***********************************************************) (* The initiator's state and the participants' data are *) (* not changed. *) (***********************************************************) \/ (****************************************************************) (* m is a "Prepared" message. *) (****************************************************************) /\ m.type = "Prepared" /\ CASE (********************************************************) (* The normal case, in which the TC has sent a *) (* "Prepare" message and is waiting for the sender's *) (* reply. *) (********************************************************) \/ /\ tcData.st = "preparingVolatile" /\ tcData.reg[m.src] = "volatile" \/ /\ tcData.st = "preparingDurable" /\ tcData.reg[m.src] = "durable" -> /\ tcData' = [tcData EXCEPT !.reg[m.src] = "prepared"] /\ UNCHANGED msgs [] (********************************************************) (* The TC has forgotten the transaction. *) (********************************************************) tcData.st = "ended" -> (********************************************************) (* The TC sends a "Rollback" reply to the sender. The *) (* transaction could either have aborted or committed. *) (* However, if the transaction has committed, then the *) (* sender will know that it has and will ignore the *) (* "Rollback" message. *) (********************************************************) /\ Reply("Rollback") /\ UNCHANGED tcData [] (*********************************************************) (* If the TC is either in a "preparing" state, or in *) (* the "aborting" or "committing" state, then it has *) (* already received and acted on a copy of m, so it *) (* does nothing. *) (*********************************************************) \/ /\ tcData.st \in {"preparingVolatile", "preparingDurable"} /\ tcData.reg[m.src] = "prepared" \/ /\ tcData.st = "aborting" /\ HaveSent("Rollback") \/ /\ tcData.st = "committing" /\ HaveSent("Commit") -> UNCHANGED <> /\ UNCHANGED <> (***********************************************************) (* The initiator's state is not changed. *) (***********************************************************) \/ (****************************************************************) (* m is a "ReadOnly" message. *) (****************************************************************) /\ m.type = "ReadOnly" /\ CASE (********************************************************) (* The normal case, in which the TC has sent a *) (* "Prepare" message and is waiting for the sender's *) (* reply. *) (********************************************************) \/ /\ tcData.st = "preparingVolatile" /\ tcData.reg[m.src] = "volatile" \/ /\ tcData.st = "preparingDurable" /\ tcData.reg[m.src] = "durable" -> (********************************************************) (* The TC sets its tcData.reg component corresponding *) (* to the sender to "readOnly". *) (********************************************************) /\ tcData' = [tcData EXCEPT !.reg[m.src] = "readOnly"] /\ UNCHANGED msgs [] (********************************************************) (* If the TC has forgotten the transaction, then either *) (* m is a duplicate message, or else it was decided to *) (* abort the transaction before the TC received the *) (* response to the "Prepare" message it sent to the *) (* sender of m. In either case, the message is *) (* ignored. *) (********************************************************) tcData.st = "ended" -> UNCHANGED <> [] (********************************************************) (* In the following cases, m is a duplicate of a *) (* message that the TC has already received and it is *) (* ignored. *) (********************************************************) \/ /\ tcData.st \in {"preparingVolatile", "preparingDurable"} /\ tcData.reg[m.src] = "readOnly" \/ /\ tcData.st = "aborting" /\ \/ tcData.reg[m.src] = "readOnly" \/ /\ tcData.reg[m.src] \in {"volatile", "durable"} /\ HaveSent("Rollback") \/ tcData.st = "committing" -> UNCHANGED <> /\ UNCHANGED <> (***********************************************************) (* The initiator's state and the participants' data are *) (* not changed. *) (***********************************************************) \/ (****************************************************************) (* m is an "Aborted" message. *) (****************************************************************) /\ m.type = "Aborted" /\ CASE (********************************************************) (* The normal case, in which the TC receives the *) (* message when it is "active" or in a "preparing" *) (* state and the sender has not replied to a *) (* "Prepare" message. In this case, the transaction *) (* is aborted, the TC sends "Rollback" messages to all *) (* registered participants from which it has not *) (* already received a "ReadOnly" message, and the *) (* initiator is notified that the transaction has *) (* been aborted. *) (********************************************************) /\ tcData.st \in {"active", "preparingVolatile", "preparingDurable"} /\ tcData.reg[m.src] \in {"unregistered", "volatile", "durable"} -> /\ iState' = "aborted" /\ tcData' = [tcData EXCEPT !.st = "aborting"] /\ msgs' = msgs \cup [type : {"Rollback"}, dest : {p \in Participant : tcData.reg[p] \notin {"unregistered", "readOnly"}}] \* 11 Dec 2003, changed "ReadOnly" -> "readOnly" \* typo found by Colin Campbell /\ UNCHANGED pData [] (********************************************************) (* If the TC is already in the "aborting" state or it *) (* has forgotten an aborted transaction, then the TC *) (* has already sent a "Rollback" message to the sender *) (* (perhaps because m is a duplicate of a message the *) (* TC already received). If the TC has forgotten a *) (* committed transaction, then this "Aborted" message *) (* was sent because the sender received an obsolete *) (* "Prepare" message after it had forgotten the *) (* transaction. In either case, m is ignored. *) (********************************************************) /\ \/ tcData.st = "aborting" \/ /\ tcData.st = "ended" /\ \/ /\ tcData.res = "aborted" /\ HaveSent("Rollback") \/ /\ tcData.res = "committed" /\ pData[m.src].st = "ended" /\ pData[m.src].res = "committed" -> UNCHANGED <> [] (********************************************************) (* If the TC is in the "committing" or "ended" state, *) (* or it is in a preparing state and the sender has *) (* already responded to the "Prepared" message, then *) (* the message is ignored. (It could have been sent in *) (* response to a duplicate "Prepared" message after the *) (* participant had reached the "ended" state.) *) (********************************************************) /\ \/ tcData.st \in {"committing", "ended"} \/ /\ tcData.st \in {"active", "preparingVolatile", "preparingDurable"} /\ tcData.reg[m.src] \in {"prepared", "readOnly", "committed"} -> UNCHANGED <> \/ (****************************************************************) (* m is a "Committed" message. *) (****************************************************************) /\ m.type = "Committed" /\ CASE (********************************************************) (* The normal case, in which the TC is in the *) (* "committing" state. In this case, it sets the *) (* element of tcData.reg corresponding to the sender to *) (* "committed". *) (********************************************************) tcData.st = "committing" -> tcData' = [tcData EXCEPT !.reg[m.src] = "committed"] [] (********************************************************) (* If the TC has forgotten the transaction, then the *) (* transaction has been committed and m is ignored. *) (********************************************************) /\ tcData.st = "ended" /\ tcData.res = "committed" -> UNCHANGED tcData /\ UNCHANGED <> (***********************************************************) (* The initiator's state and the participants' data are *) (* unchanged, and no messages are sent. *) (***********************************************************) PInternal == (*************************************************************************) (* This action describes the internal actions of the *) (* participants--actions that occur "spontaneously", either prompted by *) (* timeouts or, as in the case of the register action, by some *) (* communication external to the protocol. *) (*************************************************************************) \E p \in Participant : (***********************************************************************) (* p is the participant performing the action. *) (***********************************************************************) LET SendMsg(tp) == msgs' = msgs \cup {[type |-> tp, src |-> p]} SendRegisterMsg(rg) == msgs' = msgs \cup {[type |-> "Register", src |-> p, reg |-> rg]} (*****************************************************************) (* Locally defined action expressions. SendMsg(tp) sends a *) (* message of type tp from participant p to the TC. *) (* SendRegisterMsg(rg) sends a Register rg message, where rg is *) (* either "durable" or "volatile". *) (*****************************************************************) IN \/ (*****************************************************************) (* p registers as a volatile participant. It can do this only *) (* if it is unregistered and the initiator is in the "active" *) (* state. *) (*****************************************************************) /\ pData[p].st = "unregistered" /\ iState = "active" /\ pData' = [pData EXCEPT ![p] = [st |-> "registering", reg |-> "volatile"]] /\ SendRegisterMsg("volatile") /\ UNCHANGED <> \/ (*****************************************************************) (* p registers as a durable participant. It can do this only if *) (* it is unregistered and, if either the initiator is in the *) (* "active" state, or there is some volatile participant that is *) (* willing to wait for p to register before preparing. Since we *) (* don't model "willingness to wait", we allow the participant *) (* to register as long as there is some volatile participant *) (* that can wait for it. *) (*****************************************************************) /\ pData[p].st = "unregistered" /\ \/ iState = "active" \/ \E pp \in Participant : /\ pData[pp].st \in {"active", "preparing"} /\ pData[pp].reg = "volatile" /\ pData' = [pData EXCEPT ![p] = [st |-> "registering", reg |-> "durable"]] /\ SendRegisterMsg("durable") /\ UNCHANGED <> \/ (*****************************************************************) (* p spontaneously aborts and forgets about the transaction. We *) (* do not allow it to abort in the "registering" state. If we *) (* allowed this, then we could wind up with a situation in which *) (* a participant aborted before it registered, and the *) (* transaction committed anyway. In practice, there will have *) (* to be some way for a participant to give up when it hasn't *) (* received a RegisterResponse message. However, to do this, it *) (* must learn from the initiator or a volatile participant that *) (* the transaction aborted so it can forget about it. Since *) (* we are not modeling this kind of inter-participant *) (* communication, we do not model this procedure. *) (*****************************************************************) /\ pData[p].st \in {"active", "preparing"} /\ pData' = [pData EXCEPT ![p] = [st |-> "ended", res |-> "aborted"]] /\ SendMsg("Aborted") /\ UNCHANGED <> \/ (*****************************************************************) (* p either prepares or becomes read-only. If p is volatile, *) (* then it cannot do this if there is a durable participant that *) (* is in the "registering" state, and there is no other volatile *) (* participant to wait for it to register. *) (*****************************************************************) /\ pData[p].st = "preparing" /\ \/ pData[p].reg = "durable" \/ ~ \E dp \in Participant : /\ pData[dp].st = "registering" /\ pData[dp].reg = "durable" \/ \E vp \in Participant \ {p} : /\ pData[vp].st = "active" /\ pData[vp].reg = "volatile" \* 11 Dec 03 : Colin Campbell observes that the \* "\ {p}" is unnecessary. It should probably be removed. /\ \/ /\ pData' = [pData EXCEPT ![p] = [st |-> "prepared"]] /\ SendMsg("Prepared") \/ /\ pData' = [pData EXCEPT ![p] = [st |-> "ended", res |-> "?"]] /\ SendMsg("ReadOnly") /\ UNCHANGED <> PRcvMsg == (*************************************************************************) (* The action in which a participant receives a message from the TC. *) (*************************************************************************) \E m \in msgs : (***********************************************************************) (* m is the message being received. *) (***********************************************************************) LET Reply(tp) == msgs' = msgs \cup {[type |-> tp, src |-> m.dest]} (******************************************************************) (* Locally defines Reply(tp) to be the action of sending a *) (* message of type tp from the sender of message m. *) (******************************************************************) HaveSent(tp) == \E mm \in msgs : (mm.type = tp) /\ (mm.src = m.dest) (******************************************************************) (* Locally defines HaveSent(tp) to be true iff the participant *) (* receiving m has sent a message of type tp to the TC. *) (******************************************************************) IN /\ \/ (*************************************************************) (* m is a "RegisterResponse" message *) (*************************************************************) /\ m.type = "RegisterResponse" /\ CASE (*****************************************************) (* The normal case. *) (*****************************************************) pData[m.dest].st = "registering" -> /\ pData' = [pData EXCEPT ![m.dest].st = "active"] /\ UNCHANGED msgs [] (*****************************************************) (* This is a duplicate of an already-received *) (* message, or else it is ignorable because another *) (* message to the participant arrived ahead of it. *) (*****************************************************) pData[m.dest].st \in {"active", "preparing", "prepared", "ended"} -> UNCHANGED <> \/ (*************************************************************) (* m is a "Prepare" message. *) (*************************************************************) /\ m.type = "Prepare" /\ (**********************************************************) (* This is either the normal case (the participant is in *) (* the "active" state), or else this "Prepare" message *) (* has arrived before the "RegisterResponse" message. *) (**********************************************************) CASE pData[m.dest].st \in {"registering", "active"} -> /\ pData' = [pData EXCEPT ![m.dest].st = "preparing"] /\ UNCHANGED msgs [] (*****************************************************) (* This is a duplicate of a message already *) (* received. *) (*****************************************************) pData[m.dest].st \in {"preparing", "prepared"} -> UNCHANGED <> [] (*****************************************************) (* The transaction has been forgotten. The *) (* participant responds with an "Aborted" *) (* message--even though the transaction might have *) (* committed or be in the process of committing. In *) (* the latter case, the "Aborted" message will be *) (* ignored by the TC. *) (*****************************************************) /\ pData[m.dest].st = "ended" /\ \/ /\ pData[m.dest].res = "committed" /\ HaveSent("Committed") \/ /\ pData[m.dest].res = "aborted" /\ \/ HaveSent("Aborted") \/ /\ tcData.st = "ended" /\ tcData.res = "committed" \/ /\ pData[m.dest].res = "?" /\ HaveSent("ReadOnly") -> /\ Reply("Aborted") /\ UNCHANGED pData \/ (*************************************************************) (* m is a "Commit" message. *) (*************************************************************) /\ m.type = "Commit" /\ (**********************************************************) (* The normal case. *) (**********************************************************) CASE pData[m.dest].st = "prepared" -> /\ pData' = [pData EXCEPT ![m.dest] = [st |-> "ended", res |-> "committed"]] /\ Reply("Committed") [] (******************************************************) (* The transaction has ended, so this must be a *) (* message that was already received. *) (******************************************************) /\ pData[m.dest].st = "ended" /\ pData[m.dest].res \in {"?", "committed"} -> UNCHANGED <> \/ (*************************************************************) (* m is a "Rollback" message. *) (*************************************************************) /\ m.type = "Rollback" /\ (**********************************************************) (* The participant can be in any registered state. If it *) (* hasn't ended, then this causes it to abort. It also *) (* sends an "Aborted" message to the TC. This message *) (* isn't needed, but it is apparently used as an *) (* acknowledgement. *) (**********************************************************) CASE pData[m.dest].st \in {"registering", "active", "preparing", "prepared"} -> /\ pData' = [pData EXCEPT ![m.dest] = [st |-> "ended", res |-> "aborted"]] /\ Reply("Aborted") [] (******************************************************) (* If the participant has already finished, then this *) (* is ignored. It is possible for this message to *) (* arrive even though the participant has ended by *) (* committing the transaction. In this case, the *) (* "Rollback" message was generated by a duplicate *) (* "Register" message arriving at the TC after it had *) (* forgotten the transaction. *) (******************************************************) pData[m.dest].st = "ended" -> UNCHANGED <> /\ UNCHANGED <> Next == TCInternal \/ TCRcvMsg \/ PInternal \/ PRcvMsg (*************************************************************************) (* The specification's next-state action. *) (*************************************************************************) ----------------------------------------------------------------------------- vars == <> (*************************************************************************) (* The tuple of all variables. *) (*************************************************************************) Spec == Init /\ [][Next]_vars (*************************************************************************) (* The complete spec of the two-phase Commit protocol. *) (*************************************************************************) THEOREM Spec => [](TypeOK /\ Consistency) (*************************************************************************) (* This theorem asserts that the predicates TypeOK and Consistency are *) (* invariants of the specification. TLC checked this with 4 *) (* participants. It generated 10269919 states, 504306 of them were *) (* distinct. The longest non-repeating behavior had 45 states. It took *) (* TLC about 4-1/4 minutes on a 2-processor, 2.4GHz machine. *) (*************************************************************************) \* Last modified on Thu Dec 11 13:27:41 PT 2003 by lamport =============================================================================