Re: [tlaplus] Question about "Temporal formula is a tautology" in fairness

Hello,

I believe that TLC is wrong when it claims that your liveness property is a tautology. Your fairness conditions include

\A rm \in RM : SF_vars(TMRcvPreparedNO(rm))

where TMRcvPreparedNO is a stuttering action (as the comment above the action definition confirms). Therefore,

ENABLED <<TMRcvPreparedNO(rm)>>_vars

is equivalent to FALSE (for any value of rm), and the fairness condition is equivalent to TRUE – but that just means that this condition is trivial, not that the entire liveness property is a tautology.

When I comment out this useless fairness condition, TLC throws an exception that appears to indicate that some internal tables become too big.

Trying to reduce the size of the fairness condition, I defined formulas TMNext and RMNext(rm) corresponding to the disjunctions of all actions of the transaction manager and of the resource managers, respectively [1]. I then replaced your fairness conditions by

/\ WF_vars(TMNext)
/\ \A rm \in RM : WF_vars(RMNext(rm))

Now TLC produces what appears to be a sensible counter-example in which the TM reboots very frequently. I therefore adjusted that condition by removing the TMReboot action from the fairness condition [2], i.e.

Fairness ==
/\ WF_vars(TMRcv2PC \/ TMDecideToCommit \/ TMDecideToAbort \/ TMForgetCtx)
/\ \A rm \in RM : WF_vars(RMNext(rm))

For this specification, TLC says that the liveness property is satisfied. (Note in particular that weak fairness appears to be enough for this specification.) Of course, it is up to you to decide if that corresponds to a reasonable fairness hypothesis for your algorithm.

Lessons learnt:

1. Do not assert fairness conditions for stuttering actions – although I believe that TLC should be able to handle those.

2. Prefer few fairness hypotheses for disjunctions of actions (that correspond to progress of individual actors) over conjuncts of many individual fairness conditions.

Hope this helps,

Stephan

[1] Probably you do not want to include all actions in these disjuncts, but I didn't have time to understand your specification in detail.

[2] I am assuming that rebooting corresponds to an error in the execution, which the algorithm has to be prepared to handle, but which you do not request to occur.

--
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/2C070E7E-A900-4476-B102-808738D0A34A%40gmail.com.

Attachment: TradTwoPhase.tla
Description: Binary data

On 26 Jun 2022, at 10:35, 钱晨 <allenhandora@xxxxxxxxx> wrote:

I have recently written a 2pc protocol with fairness, I first write all request/response handlers as the strong fairness(except reboot and exception events) in order to pass the liveness check:

the liveness check is as below:
2PCLivevess == \A r \in RM: 1 = 1 ~> (2pcState[r] = "aborted" \/ 2pcState[r] = "committed")

the spec is something like below:
================== start====================
Fairness ==
/\ WF_vars(TMRcv2PC)
/\ SF_vars(TMDecideToAbort)
/\ SF_vars(TMDecideToCommit)
/\ \A rm \in RM:
SF_vars(TMRcvPreparedOK(rm))
/\ \A rm \in RM:
SF_vars(TMRcvPreparedNO(rm))
/\ \A rm \in RM:
SF_vars(TMRcvCommitted(rm))
/\ \A rm \in RM:
SF_vars(TMRcvAborted(rm))
/\ \A rm \in RM:
SF_vars(RMRcvPrepareOK(rm))
/\ \A rm \in RM:
SF_vars(RMRcvPrepareNO(rm))
/\ \A rm \in RM:
SF_vars(RMRcvCommit(rm))
/\ \A rm \in RM:
SF_vars(RMRcvAbort(rm))
/\ \A rm \in RM:
SF_vars(OrphanRMRcvMsg(rm))
/\ \A rm \in RM:
SF_vars(RMForgetCtx(rm))
/\ SF_vars(TMForgetCtx)
================== end ====================
While the model check reports "Temporal formula is a tautology (its negation is unsatisfiable).". Can any tell me why my fairness check reports the errors.

--
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/9e859fd3-6d18-43f6-81b0-ed329f780047n%40googlegroups.com.
<TradTwoPhase.tla>