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