[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Younes <younesagma@xxxxxxxxx>*Date*: Wed, 24 Feb 2021 02:58:28 -0800 (PST)*References*: <c3e5a888-34f3-4445-af2d-a6de32e8c20cn@googlegroups.com> <2C3CE438-E2BE-48AE-9204-F509B90BC0DA@gmail.com>

Thank you, Stephan, for your feedback.

Below are my comments in bold based on my understanding (and please, do not hesitate to correct me if I'm mistaken).

S> \* assume that for every actor, if some action is forever enabled, it must eventually be taken

FairRead == \A a \in Readers : WF_vars(Reading(a))

FairWrite == \A a \in Writers : WF_vars(Writing(a))

FairStop == \A a \in Actors : WF_vars(StopActivity(a))

Fairness == FairRead /\ FairWrite /\ FairStop

and add Fairness to your Spec, instead of Liveness. When you now attempt to verify the liveness property for readers (formula ReaderShouldBeReading), TLC will produce a counter-example where some writer repeatedly accesses the resource but no reader ever reads.

Take the time that is needed to understand why this execution satisfies the above fairness conditions.

S> We can ensure the liveness condition for readers by changing WF to SF in the definition of FairRead, and TLC will confirm this. Again make sure you understand why this is the case.

S> Turning to checking liveness for writers (formula WriterShouldBeWriting), TLC will produce a more elaborate counter-example that shows you why this property does not hold, even if you replace WF by SF in the definition of FairWrite.

**WF_vars(Writing(writer)) => We tell TLC that if the action Writing is enabled continuously, it should eventually occur.****TLC's counter-example : Readers are reading repeatedly => enabling condition of the Writing action may be true (when all readers stop reading), but not continuously, so the Action Writing never occurs!****SF_vars(Writing(writer)) => We tell TLC that if the action Writing is enabled repeatedly, it should eventually occur.****TLC's counter-example : Readers are reading and only some of them stop, so the enabling condition of the Writing action (****BusyActors = {}****) is never true => the property WriterShouldBeWriting never holds.**

S> Take the time necessary to understand why this counter-example is fair. Now you'll have to come up with a mechanism that ensures liveness for writers, and this will require more than adding fairness conditions.

Thank you again,

On Tuesday, February 23, 2021 at 3:52:42 PM UTC+1 Stephan Merz wrote:

Hello,before attempting to verify liveness properties, always verify some safety properties. In your case, the canonical property to verify is that there can always be at most one writer and that there can never be active readers and writers at the same time. In order to make sure that your specification is not vacuous, it is also recommended to verify as many non-properties as you can think of and make sure that the counter-examples that TLC returns conform to your intuition. For example, claim that no reader can ever be active or that no writer can ever be active.In order to answer your questions:(1) I presume your formula "Liveness" defines the property that you expect your specification to ensure. But then you shouldn't make it part of the definition of Spec, otherwise you just verify a triviality. And you haven't made it clear how you intend to implement the liveness property in your system.Typically, one assumes being able to ensure (weak or strong) fairness conditions on actions, based on appropriate schedulers. So you could define\* assume that for every actor, if some action is forever enabled, it must eventually be takenFairRead == \A a \in Readers : WF_vars(Reading(a))

FairWrite == \A a \in Writers : WF_vars(Writing(a))

FairStop == \A a \in Actors : WF_vars(StopActivity(a))

Fairness == FairRead /\ FairWrite /\ FairStop

and add Fairness to your Spec, instead of Liveness. When you now attempt to verify the liveness property for readers (formula ReaderShouldBeReading), TLC will produce a counter-example where some writer repeatedly accesses the resource but no reader ever reads.Take the time that is needed to understand why this execution satisfies the above fairness conditions.We can ensure the liveness condition for readers by changing WF to SF in the definition of FairRead, and TLC will confirm this. Again make sure you understand why this is the case.Turning to checking liveness for writers (formula WriterShouldBeWriting), TLC will produce a more elaborate counter-example that shows you why this property does not hold, even if you replace WF by SF in the definition of FairWrite.Take the time necessary to understand why this counter-example is fair. Now you'll have to come up with a mechanism that ensures liveness for writers, and this will require more than adding fairness conditions.The attached module contains the above definitions.(2) The statistics that TLC outputs at the end of a run reflect properties of the state graph such as the numbers of states and distinct states. The graph is the same whether you check safety or liveness properties, so these numbers are the same as well.(3) In the breadth-first exploration that TLC performs, the action StopActivity always loops back to a state that TLC has encountered before, that's why it doesn't produce new "distinct states".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+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/e08490d0-4d3a-40af-9429-549b83355e4en%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Reader Writer Problem specs : Liveness & TLC***From:*Stephan Merz

**References**:**[tlaplus] Reader Writer Problem specs : Liveness & TLC***From:*Younes

**Re: [tlaplus] Reader Writer Problem specs : Liveness & TLC***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Reader Writer Problem specs : Liveness & TLC** - Next by Date:
**Re: [tlaplus] Reader Writer Problem specs : Liveness & TLC** - Previous by thread:
**Re: [tlaplus] Reader Writer Problem specs : Liveness & TLC** - Next by thread:
**Re: [tlaplus] Reader Writer Problem specs : Liveness & TLC** - Index(es):