TLA_PLUS_SeqLock

gistfile1.txt

--------------------------- MODULE concurrent_map ---------------------------

EXTENDS TLC, Integers, FiniteSets, Sequences

ReaderCount == 2


Readers == 1..ReaderCount





(* --algorithm map
variables 
    Slots = 1..1;
    InitialSeq = {x \in 1..10: x % 2 = 0 };
    keyVersions \in [Slots -> InitialSeq];
    keys = [i \in DOMAIN keyVersions |-> keyVersions[i] ];
    readDone = [r \in Readers |-> FALSE];
    reads = [i \in Readers |-> [version |-> 0, value |-> 0]];
define 
    ReadsDone == \A t \in Readers : pc[t] = "Done"
    
    Correct ==  ReadsDone => \A i \in DOMAIN reads: ((reads[i].version % 2) = 0)  /\ (reads[i].version = reads[i].value)
    
end define 

process writer = 1
variables
  writeIndex \in Slots;
  nextVersion \in InitialSeq
begin
  Prepare:
       nextVersion := nextVersion + 1;
       keyVersions[writeIndex] := nextVersion;
     
    
  Write:
       keys[writeIndex] := nextVersion + 1;
       keyVersions[writeIndex] := nextVersion + 1;
    
  
     
end process;


process reader \in Readers
variables
    
    readIndex \in Slots;
    version = 0;
    checkVersion = 0;
    localValue = 0;
   
 
 begin
    ReadVersion:
       version := keyVersions[readIndex];
       reads[self].version :=  IF version % 2 = 0 THEN version ELSE  0; 
       
       
    ReadData:
        localValue := IF (version # 0) /\ version % 2 = 0 THEN keys[readIndex] ELSE 0;
        checkVersion := keyVersions[readIndex];
        reads[self].value := localValue;
     
 end process     




end algorithm; *)
\* BEGIN TRANSLATION (chksum(pcal) = "b3c78e51" /\ chksum(tla) = "38e1332c")
VARIABLES Slots, InitialSeq, keyVersions, keys, readDone, reads, pc

(* define statement *)
ReadsDone == \A t \in Readers : pc[t] = "Done"

Correct ==  ReadsDone => \A i \in DOMAIN reads: ((reads[i].version % 2) = 0)  /\ (reads[i].version = reads[i].value)

VARIABLES writeIndex, nextVersion, readIndex, version, checkVersion, 
          localValue

vars == << Slots, InitialSeq, keyVersions, keys, readDone, reads, pc, 
           writeIndex, nextVersion, readIndex, version, checkVersion, 
           localValue >>

ProcSet == {1} \cup (Readers)

Init == (* Global variables *)
        /\ Slots = 1..1
        /\ InitialSeq = {x \in 1..10: x % 2 = 0 }
        /\ keyVersions \in [Slots -> InitialSeq]
        /\ keys = [i \in DOMAIN keyVersions |-> keyVersions[i] ]
        /\ readDone = [r \in Readers |-> FALSE]
        /\ reads = [i \in Readers |-> [version |-> 0, value |-> 0]]
        (* Process writer *)
        /\ writeIndex \in Slots
        /\ nextVersion \in InitialSeq
        (* Process reader *)
        /\ readIndex \in [Readers -> Slots]
        /\ version = [self \in Readers |-> 0]
        /\ checkVersion = [self \in Readers |-> 0]
        /\ localValue = [self \in Readers |-> 0]
        /\ pc = [self \in ProcSet |-> CASE self = 1 -> "Prepare"
                                        [] self \in Readers -> "ReadVersion"]

Prepare == /\ pc[1] = "Prepare"
           /\ nextVersion' = nextVersion + 1
           /\ keyVersions' = [keyVersions EXCEPT ![writeIndex] = nextVersion']
           /\ pc' = [pc EXCEPT ![1] = "Write"]
           /\ UNCHANGED << Slots, InitialSeq, keys, readDone, reads, 
                           writeIndex, readIndex, version, checkVersion, 
                           localValue >>

Write == /\ pc[1] = "Write"
         /\ keys' = [keys EXCEPT ![writeIndex] = nextVersion + 1]
         /\ keyVersions' = [keyVersions EXCEPT ![writeIndex] = nextVersion + 1]
         /\ pc' = [pc EXCEPT ![1] = "Done"]
         /\ UNCHANGED << Slots, InitialSeq, readDone, reads, writeIndex, 
                         nextVersion, readIndex, version, checkVersion, 
                         localValue >>

writer == Prepare \/ Write

ReadVersion(self) == /\ pc[self] = "ReadVersion"
                     /\ version' = [version EXCEPT ![self] = keyVersions[readIndex[self]]]
                     /\ reads' = [reads EXCEPT ![self].version = IF version'[self] % 2 = 0 THEN version'[self] ELSE  0]
                     /\ pc' = [pc EXCEPT ![self] = "ReadData"]
                     /\ UNCHANGED << Slots, InitialSeq, keyVersions, keys, 
                                     readDone, writeIndex, nextVersion, 
                                     readIndex, checkVersion, localValue >>

ReadData(self) == /\ pc[self] = "ReadData"
                  /\ localValue' = [localValue EXCEPT ![self] = IF (version[self] # 0) /\ version[self] % 2 = 0 THEN keys[readIndex[self]] ELSE 0]
                  /\ checkVersion' = [checkVersion EXCEPT ![self] = keyVersions[readIndex[self]]]
                  /\ reads' = [reads EXCEPT ![self].value = localValue'[self]]
                  /\ pc' = [pc EXCEPT ![self] = "Done"]
                  /\ UNCHANGED << Slots, InitialSeq, keyVersions, keys, 
                                  readDone, writeIndex, nextVersion, readIndex, 
                                  version >>

reader(self) == ReadVersion(self) \/ ReadData(self)

(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
               /\ UNCHANGED vars

Next == writer
           \/ (\E self \in Readers: reader(self))
           \/ Terminating

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

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION 

====