Re: [tlaplus] Question regarding Two Phase Commit spec and the enabling condition of one of its definitions

I have not checked if the spec from the video course is exactly the same one as the one on GitHub [1] but if it is then your proposed change would not be sound. In the GitHub spec, a resource manager is in state "prepared" when it agrees to commit and has previously sent a "Prepared" message to the transaction manager. (In other words, "prepared" means "prepared to commit".) If you allow a resource manager to enter the state "aborted" later then the transaction manager may issue "Commit" although some resource manager does not agree to commit, which contradicts the specification of two-phase commit.

[1] https://github.com/tlaplus/Examples/tree/master/specifications/transaction_commit

On 4 Jan 2020, at 10:53, Curious Student <vedantpimpley7@xxxxxxxxx> wrote:

In Two Phase Commit, the formula RMChooseToAbort(r) has rmState[r]="working" as the enabling condition. Shouldn't "prepared" be a permissible enabling condition for a resource manager(RM) wanting to abort?

This is the definition given in the spec from the video course.

RMChooseToAbort(r) == (*************************************************************************) (* Resource manager r spontaneously decides to abort. As noted above, r *) (* does not send any message in our simplified spec. *) (*************************************************************************) /\ rmState[r] = "working" /\ rmState' = [rmState EXCEPT ![r] = "aborted"] /\ UNCHANGED <<tmState, tmPrepared, msgs>>

The state diagram shown in the transaction commit clearly shows the "aborted" can be reached from both "working" and "prepared" states. Two Phase commit seems to be similar.

Shouldn't the enabling condition instead be this? :

rmState[r] \in {"working", "prepared"}

I'm only curious if there is something deeper within this. I'll be glad to hear your response.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9e5128eb-18fb-426b-9185-c0d7f65a47aa%40googlegroups.com.