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

Re: [tlaplus] Reader Writer Problem specs : Liveness & TLC



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.
Y> TLC is checking the liveness property ReaderShouldBeReading and the Reading(actor) action has a weak fairness; which means that if the action Reading(actor) is enabled continuously it will eventually occur. TLC finds a path where:
* the action Writing(actor) is enabled and executed forever : this doesn't enable the action Reading(actor),
* the action Reading(actor) is enabled, but disabled again : so it’s not enabled continuously
==>  Therefore, the property ReaderShouldBeReading doesn’t hold.

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.
Y> When we change the fairness condition for Reading(Actor) from WF to SF, we tell TLC that if the action Reading(actor) is enabled repeatedly, it should eventually occur, and that’s why the property ReaderShouldBeReading holds after we do this change. 

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.
Y> Checking the property WriterShouldBeWriting :
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.
Y> Alright, but I'm a bit confused. Normally, a temporal spec is expressed like this (at least in my case):

Spec == Init /\ [][Next]_vars /\ Fairness

The  Init /\ [][Next]_vars part is the safety part : it guarantees that the system avoids deadlocks and starvation for instance. This part can be reinforced by Invariants (which are a special case of safety properties) to make sure we don't have undesirable behaviors.
The Fairness part is the liveness part : it guarantees that the system can make progress, that actions occur in a "fair" way, and that we don't have some action "taking the monopoly", leaving other actions behind.

So, when you say that I'll have to "come up with a mechanism that ensures liveness for writers, and this will require more than adding fairness conditions", I understand that, to ensure liveness, amending the fairness conditions isn't enough; we need a mechanism, which will probably be in the safety part. Hence, my question is : why should safety ensure liveness?

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 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.

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.