RedisMutex

I tried to proof my thoughts about the Mutex with tlaplus.

----------------------------- MODULE TypeRedis -----------------------------

EXTENDS Integers, Sequences
CONSTANT Data

VARIABLES AVar, BVar, SVar

vars == << AVar, BVar, SVar >>

RNG == 1..10

RData == Data \X (0..10)

(* General Idea:
Acquire a lock with Redis means, that you have a random number generated and placed in Redis.
If you want to set the locked value in Redis, you need to send the number generated before.
The number will be dropped randomly, because you cannot know, when you were put to sleep.
*)

TypeOK == /\ AVar \in RData
          /\ BVar \in RData
          /\ SVar \in RData
          
Inv == /\ (AVar[1] = SVar[1] \/ BVar[1] = SVar[1])
       /\ (AVar[2] = SVar[2] \/ BVar[2] = SVar[2] \/ SVar[2] = 0)
       
          
Init == /\ AVar = CHOOSE x \in RData: x[2] = 0
        /\ BVar = CHOOSE x \in RData: x[2] = 0
        /\ SVar = CHOOSE x \in RData: x[2] = 0
        
ALkAcq == LET x == CHOOSE x \in RNG : x # SVar[2] /\ x # BVar[2]
          IN /\ IF SVar[2] = 0
                 THEN /\ SVar' = << SVar[1], x >>
                      /\ AVar' = << AVar[1], x >>
                      /\ UNCHANGED << BVar >>
                 ELSE /\ UNCHANGED << vars >>

ALkRel == /\ IF AVar[2] = SVar[2]
              THEN /\ AVar' = << AVar[1], 0 >>
                   /\ SVar' = << SVar[1], 0 >>
                   /\ BVar' = BVar
              ELSE UNCHANGED << vars >>
          
ANewData == /\ IF AVar[2] # 0 /\ AVar[2] = SVar[2]
                THEN /\ AVar' = CHOOSE x \in RData: x[2] = AVar[2] /\ x[1] # AVar[1]
                     /\ SVar' = AVar'
                     /\ BVar' = BVar
                ELSE UNCHANGED vars
                
AFix == IF AVar[2] > 0 /\ SVar[2] = 0
         THEN /\ AVar' = << AVar[1], 0 >>
              /\ UNCHANGED << BVar, SVar >>
         ELSE UNCHANGED << vars >>
          
BLkAcq == LET x == CHOOSE x \in RNG : x # SVar[2] /\ x # AVar[2]
          IN /\ IF SVar[2] = 0
                 THEN /\ SVar' = << SVar[1], x >>
                      /\ BVar' = << BVar[1], x >>
                      /\ UNCHANGED << AVar >>
                 ELSE /\ UNCHANGED << vars >>

BLkRel == /\ IF BVar[2] = SVar[2]
              THEN /\ BVar' = << BVar[1], 0 >>
                   /\ SVar' = << SVar[1], 0 >>
                   /\ AVar' = AVar
              ELSE UNCHANGED << vars >>


BNewData == /\ IF BVar[2] # 0 /\ BVar[2] = SVar[2]
                THEN /\ BVar' = CHOOSE x \in RData: x[2] = BVar[2] /\ x[1] # AVar[1]
                     /\ SVar' = BVar'
                     /\ AVar' = AVar
                ELSE UNCHANGED vars
                
BFix == IF BVar[2] > 0 /\ SVar[2] = 0
         THEN /\ BVar' = << BVar[1], 0 >>
              /\ UNCHANGED << AVar, SVar >>
         ELSE UNCHANGED << vars >>

                   
RnDrop == /\ SVar' = <<SVar[1], 0>>
          /\ UNCHANGED << AVar, BVar >>

Next == \/ ALkAcq
        \/ ALkRel
        \/ ANewData
        \/ BLkAcq
        \/ BLkRel
        \/ BNewData
        \/ RnDrop
        \/ AFix
        \/ BFix
        
FairSpec == /\ Init
            /\ [][Next]_vars
            /\ WF_vars(ALkAcq) /\ SF_vars(ALkRel)
            /\ WF_vars(BLkAcq) /\ SF_vars(BLkRel)
            /\ WF_vars(ANewData) /\ WF_vars(BNewData)
            /\ WF_vars(RnDrop)
            /\ WF_vars(AFix) /\ WF_vars(BFix)

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