Question about "Temporal formula is a tautology" in fairness

92 views
Skip to first unread message

钱晨

unread,
Jun 26, 2022, 4:35:50 AM6/26/22
to tlaplus
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.

TradTwoPhase.tla

Andrew Helwer

unread,
Jun 27, 2022, 10:01:54 AM6/27/22
to tlaplus
How about writing:

2PCLivevess == \A r \in RM: <>(2pcState[r] = "aborted" \/ 2pcState[r] = "committed")

Guessing the liveness interpreter doesn't like the 1 = 1 statement.

Andrew

Stephan Merz

unread,
Jun 28, 2022, 3:07:11 AM6/28/22
to tla...@googlegroups.com
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.

TradTwoPhase.tla

钱晨

unread,
Jun 28, 2022, 11:02:12 AM6/28/22
to tlaplus
Thanks very much for your help! 
I also successfully completed the test with your help. And I will soon refine it in some details such as using weak fairness for the most actions.

One more question, you say "When I comment out this useless fairness condition, TLC throws an exception that appears to indicate that some internal tables become too big.". I also encounter the problem, and I want to know what is meant by "some internal tables become too big". Does it mean that some data structures in TLC can not support the size of the action in the `Next`?

Thanks again for your help!

Stephan Merz

unread,
Jun 28, 2022, 11:55:48 AM6/28/22
to tla...@googlegroups.com
> One more question, you say "When I comment out this useless fairness condition, TLC throws an exception that appears to indicate that some internal tables become too big.". I also encounter the problem, and I want to know what is meant by "some internal tables become too big". Does it mean that some data structures in TLC can not support the size of the action in the `Next`?

It's not the next-state relation that's the problem but the fairness conditions: TLC has to monitor for each fairness condition at which state the underlying action is enabled and which transitions correspond to the action being taken. I do not know how TLC represents this information, but apparently it is not meant to handle a lot of fairness conditions (remember that you have to multiply the RM actions by the number of resource managers in the model).

Stephan

钱晨

unread,
Jun 28, 2022, 12:28:41 PM6/28/22
to tlaplus
Thanks for your nice explanation.

I have another question I want to ask. When I run the case after solving the problem of 'tautology', it happens to be a case that violates the liveness check like below
1. We have [a, b, c] as RM
2. ....
3. TM is in 'aborted' state and all rms are in 'TombstoneNo' (* means forget the result, and 2pc will use Presumed Abort to answer the TM)
4. TM receives one of the abort responses and fills in it in tmConfirmed(* like tmConfirmed = [a] *)
5. Tm occurred tmReboot(* and tmConfirmed will be empty again(* like tmConfirmed = [] *)
Then 4 and 5 will loop forever and cause a liveness problem

I solve the problem by adding the following formulas into the `fairness`(I also add another one that involves "committed" state), and it finally pass the liveness check
```

    /\ SF_vars(

        /\ tmState = "aborted"

        /\ tmConfirmed /= RM

        /\ \A rm \in RM:

            /\ [type |-> "RMABORTED", rm |-> rm] \in msgs

        /\ tmConfirmed' = RM

        /\ UNCHANGED <<rmState, tmState, tmParticipants, tmPrepared, msgs>>          

        ) 

```

It seems we must collect all responses before advancing to the next stage and cannot reboot during the process. In my way, we must write a completely new formula to achieve the goal. Does it exist another better writing style that can achieve the same goal or just use the original formula like `TMRcvAborted`?

Stephan Merz 在 2022年6月28日 星期二晚上11:55:48 [UTC+8] 的信中寫道:

Stephan Merz

unread,
Jun 28, 2022, 12:37:45 PM6/28/22
to tla...@googlegroups.com
It seems to me that you can express this condition by writing

SF_vars(TMRcvAborted /\ tmConfirmed' = RM)

But I don't understand your specification well enough to know if this is a reasonable fairness condition, and why you really need this variant rather than

WF/SF_vars(TMRcvAborted)

which requires TMRcvAborted to occur eventually when it is enabled, eventually ensuring that tmConfirmed = RM.
Given that no action appears to be in conflict with TMRcvAborted, there should be no difference between weak and strong fairness for this action.

Stephan

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/09eb6219-9a8b-4f35-ad5a-e522cf160e05n%40googlegroups.com.

钱晨

unread,
Jun 28, 2022, 10:52:29 PM6/28/22
to tlaplus
I add the following condition into the fairness formulas, while it still reports the error for the liveness problem.
```

    /\ \A rm \in RM: 

        SF_vars(TMRcvAborted(rm) /\ tmConfirmed' = RM)

```

It still appears that `tmReboot` occurred repeatedly before `tmConfirmed` is fully collected, so it loops infinitely and violates the liveness property.

I do not understand what will happen if I declare a formula in liveness except formulas that already occurred in `Next`.

Will it be evaluated as an action or it will do something else?


Stephan Merz 在 2022年6月29日 星期三凌晨12:37:45 [UTC+8] 的信中寫道:

Markus Kuppe

unread,
Jun 29, 2022, 5:37:32 PM6/29/22
to tla...@googlegroups.com
Hi,

can you please create an issue at https://github.com/tlaplus/tlaplus/issues

Thanks,
Markus

Markus Kuppe

unread,
Jul 14, 2022, 11:53:52 PM7/14/22
to tla...@googlegroups.com
The bogus error message has been corrected as part of https://github.com/tlaplus/tlaplus/issues/742

Markus
> --
> 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+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2C070E7E-A900-4476-B102-808738D0A34A%40gmail.com.
> <TradTwoPhase.tla>
>
>
>> On 26 Jun 2022, at 10:35, 钱晨 <allenh...@gmail.com> 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+u...@googlegroups.com.
>> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9e859fd3-6d18-43f6-81b0-ed329f780047n%40googlegroups.com.
>> <TradTwoPhase.tla>
>
>
> --
> 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+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2C070E7E-A900-4476-B102-808738D0A34A%40gmail.com.

Reply all
Reply to author
Forward
0 new messages