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

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

--
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/36E140E9-473B-4E65-AF44-D172D644D7C2%40gmail.com.

Attachment: ReadersWriters.tla
Description: Binary data

On 26 Feb 2021, at 16:44, Younes <younesagma@xxxxxxxxx> wrote:

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.

--
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/bd6a68eb-81a1-4fcf-81fb-d6701289d839n%40googlegroups.com.
<reader_writer_problem_tla.txt>