Reader Writer Problem specs : Liveness & TLC

[Younes]

Hello,

1 - I've written the specs below for the Reader-Writer Problem, and I'm wondering if the Liveness conditions I have set are right. I considered that the liveness conditions are :

• Every reader in the community of Readers will eventually be reading
• Every writer in the community of Writer will eventually be writing

-------------------------- MODULE Readers_Writers --------------------------

\*  https://en.wikipedia.org/wiki/Readers%E2%80%93writers_problem

EXTENDS FiniteSets

CONSTANTS Readers, Writers

VARIABLES Resource

vars == Resource

Init == Resource = [ Readers |-> {}, Writers |-> {} ]

Actors == Readers \union Writers

BusyActors == Resource.Readers \union Resource.Writers

FreeActors == Actors \ BusyActors

Reading(actor) == /\ actor \in Readers

                  /\ actor \notin BusyActors

                  /\ Cardinality(Resource.Writers) = 0

                  /\ Resource' = [Resource EXCEPT !.Readers = @ \union {actor} ]

                  

Writing(actor) == /\ actor \in Writers

                  /\ actor \notin BusyActors

                  /\ Cardinality(BusyActors) = 0

                  /\ Resource' = [Resource EXCEPT !.Writers = @ \union {actor }]

StopActivity(actor) == /\ actor \in BusyActors

                       /\ \/ actor \in Resource.Readers /\ Resource' = [Resource EXCEPT !.Readers = @ \ {actor} ]

                          \/ actor \in Resource.Writers /\ Resource' = [Resource EXCEPT !.Writers = @ \ {actor} ]

ReaderShouldBeReading == \A reader \in Readers : [] <> (reader \in Resource.Readers)

WriterShouldBeWriting == \A writer \in Writers : [] <> (writer \in Resource.Writers)

Liveness == ReaderShouldBeReading /\ WriterShouldBeWriting

Next == \E actor \in Actors : Reading(actor) \/ Writing(actor) \/ StopActivity(actor)

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

=============================================================================

2 - I have also realized that whether I include the Liveness conditions or not in my Spec, the results, after the model checking, are the same. Why?

3 - Why does the action StopActivity has 0 distinct state? Does that mean TLC doesn't explore it at all? Why is that?

I will also gladly take any comments about the specs for improvement.

Thank you!

[Younes]

2 - Maybe, because Spec is machine closed?

[Stephan Merz]

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

[Younes]

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,

[Stephan Merz]

Hello,

your explanations for the various results are correct. As for designing a solution that ensures freedom of starvation for both readers and writers, you'll find a discussion on the Wikipedia page about the readers/writers problem. It uses semaphores, but you can transpose the idea to your TLA+ spec.

why should safety ensure liveness?

Of course you'll need a combination of algorithmic design (in the safety part of the spec) and suitable fairness conditions.

Regards,

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/e08490d0-4d3a-40af-9429-549b83355e4en%40googlegroups.com.

[Younes]

Hello Stephan,

I have attached an updated version of the spec. I represented the semaphore system with a queue in my spec. Please let me know if the spec is missing any of the semaphore/mutex characteristics, or if that is just a workaround.

Although, with this spec, whether I am on weak or strong fairness conditions, I get the same outcome. It looks like the fairness conditions don't change much in the progress / liveness of the system. It's like if the progress is guaranteed by the safety part more than the liveness part. This sounds extreme, but what I mean is that the model seems insensitive to a change from weak to strong fairness conditions, and vice versa. That's what I deduced from the runs I launched. Could you please let me know why?

Looking forward to getting your feedback.

Thank you again,

Younes.

[Stephan Merz]

Hello,

the previous specification already ensured the required safety properties, as well as liveness for readers. The remaining issue was that readers could arrive in rapid succession, thereby locking our writers. If we want to make sure this cannot happen, a waiting writer must be able to block new readers from being served.

Your solution does this by imposing a FIFO treatment of all requests. This serializes all (read and write) requests at the waiting queue, and that's why you don't observe any difference between weak or strong fairness: there is only one request that can possibly be served, and once it is enabled, it remains enabled until it is served.

Attached is a different, more relaxed solution where requests may be served in different orders. I obtained it from the previous spec by adding a "waiting room" that can hold at most one writer that arrives when there are active readers. As soon as the waiting room is non-empty, new readers are blocked. You can play with different combinations of WF and SF, and TLC will show you different counter-examples.

Which specification you prefer depends on the system you are aiming at.

I suggest we leave it at that: a mailing list is not the right place for a conversation between two persons.

Stephan

[Younes]

Very clear.

Thank you,  Stephan.