tla-specs/aiorwlock/aiorwlock.tla at main · Alexander-N/tla-specs · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
----------------------------- MODULE aiorwlock ------------------------------
EXTENDS Naturals, Sequences, Integers, FiniteSets
CONSTANTS Task
ASSUME /\ Task # {}

VARIABLES RState,
          WState,
          Lock

vars == <<RState, WState, Lock>>

-----------------------------------------------------------------------------
TypeOK == /\ Lock \in [Task -> {"Read", "Write", "WriteRead", "Waiting", "Finished"}]
          /\ RState >= 0
          /\ WState >= 0 /\ WState <= 2
LockInit == Lock = [t \in Task |-> "Waiting"] /\ RState = 0 /\ WState = 0
-----------------------------------------------------------------------------


Rlocked == RState > 0
Wlocked == WState > 0
Unlocked == RState = 0 /\ WState = 0

WOwn(t) == Lock[t] \in {"Write"}

RAquire(t) == \/ /\ ~Wlocked
                 /\ Lock[t] \in {"Waiting"}
                 /\ Lock' = [Lock EXCEPT ![t] = "Read"]
                 /\ RState' = RState + 1
                 /\ UNCHANGED WState
              \/ /\ WOwn(t)
                 /\ Lock' = [Lock EXCEPT ![t] = "WriteRead"]
                 /\ RState' = RState + 1
                 /\ UNCHANGED WState

WAquire(t) == /\ Unlocked
              /\ Lock[t] \in {"Waiting"}
              /\ Lock' = [Lock EXCEPT ![t] = "Write"]
              /\ WState' = WState + 1
              /\ UNCHANGED RState


RRelease(t) == \/ /\ Rlocked /\ Lock[t] = "Read"
                  /\ RState' = RState - 1 /\ Lock' = [Lock EXCEPT ![t] = "Finished"]
                  /\ UNCHANGED WState
               \/ /\ Rlocked /\ Lock[t] = "WriteRead"
                  /\ RState' = RState - 1 /\ Lock' = [Lock EXCEPT ![t] = "Write"]
                  /\ UNCHANGED WState

WRelease(t) == \/ /\ Wlocked /\ Lock[t] = "Write"
                  /\ WState' = WState - 1 /\ Lock' = [Lock EXCEPT ![t] = "Finished"]
                  /\ UNCHANGED RState
               \/ /\ Wlocked /\ Lock[t] = "WriteRead"
                  /\ WState' = WState - 1 /\ Lock' = [Lock EXCEPT ![t] = "Read"]
                  /\ UNCHANGED RState


(* Allow infinite stuttering to prevent deadlock. *)
Finished == /\ \A t \in Task: Lock[t] = "Finished"
            /\ UNCHANGED vars
-----------------------------------------------------------------------------

Next == \E t \in Task: RAquire(t) \/ WAquire(t) \/ RRelease(t) \/ WRelease(t) \/ Finished

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


LockInv ==
    \A t1 \in Task : \A t2 \in (Task \ {t1}):
      Lock[t1] \in {"Write", "WriteRead"} => Lock[t2] \in {"Waiting", "Finished"}
-----------------------------------------------------------------------------

THEOREM Spec => [](TypeOK /\ LockInv)

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