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

[Younes <younesagma@xxxxxxxxx>]

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.
-------------------------- MODULE Readers_Writers --------------------------
EXTENDS Sequences, Naturals, FiniteSets
CONSTANTS Readers, Writers

VARIABLES Resource, Waiting
vars == <<Resource, Waiting>>

Init == /\ Resource = [ Readers |-> {}, Writers |-> {} ]
        /\ Waiting = <<>>

TypeOK == /\ {Resource.Readers} \subseteq SUBSET Readers
          /\ {Resource.Writers} \subseteq SUBSET Writers

Actors == Readers \union Writers
BusyActors == Resource.Readers \union Resource.Writers

Range(S) == { S[i] : i \in DOMAIN S}

\* Actions 
Request(actor) == /\ Len(Waiting) < Cardinality(Actors)
                  /\ actor \notin BusyActors \union Range(Waiting)
                  /\ Waiting' = Append(Waiting, actor)
                  /\ UNCHANGED <<Resource>>

AddToSet(el, Set) == /\ Resource' = [ Resource EXCEPT ![Set] = @ \union {el} ]
                     /\ Waiting' = Tail(Waiting)

Reading == /\ Waiting # <<>>
           /\ Head(Waiting) \in Readers
           /\ Resource.Writers = {}
           /\ AddToSet(Head(Waiting), "Readers")

Writing == /\ Waiting # <<>>
           /\ Head(Waiting) \in Writers
           /\ BusyActors = {}
           /\ AddToSet(Head(Waiting), "Writers")

Stop == LET actor == CHOOSE el \in BusyActors : TRUE
        IN /\ BusyActors # {}
           /\ \/ actor \in Resource.Readers /\ Resource' = [Resource EXCEPT !.Readers = @ \ {actor} ]
              \/ actor \in Resource.Writers /\ Resource' = [Resource EXCEPT !.Writers = @ \ {actor} ]
           /\ UNCHANGED Waiting

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

FairRequest == \A actor \in Actors: SF_vars(Request(actor))
FairReading == \A reader \in Readers: SF_vars(Reading)
FairWriting == \A writer \in Readers: SF_vars(Writing)
FairStop == \A actor \in Actors: SF_vars(Stop)

Fairness == FairReading /\ FairWriting /\ FairStop /\ FairRequest

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

\* Safety properties : something bad never happens
Invariants ==
           /\ TypeOK
           \* There can never be an active writer and an active reader at the same time  
           /\ ~( Resource.Writers # {} /\ Resource.Readers # {} ) 
           \* There should be at most one writer
           /\ \A a,b \in Actors : a \in Resource.Writers /\ b \in Resource.Writers => a = b

ReaderShouldBeReading == \A reader \in Readers : [] <> (reader \in Resource.Readers)
WriterShouldBeWriting == \A writer \in Writers : [] <> (writer \in Resource.Writers)
ReadersShouldStop == \A reader \in Readers : reader \in Resource.Readers ~> <> ( reader \notin Resource.Readers )
WritersShouldStop == \A writer \in Writers : writer \in Resource.Writers ~> <> ( writer \notin Resource.Writers )
=============================================================================