pgo/omnilink/concurrentqueue/ConcurrentQueue.tla at main · DistCompiler/pgo · 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
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
---- MODULE ConcurrentQueue ----
EXTENDS Integers, Sequences, SequencesExt, FiniteSets, FiniteSetsExt, TLC

CONSTANTS Elements, Producers, Consumers

VARIABLES queues, enqueueInProgress, dequeueInProgress, sizeApproxMax

vars == <<queues, enqueueInProgress, dequeueInProgress, sizeApproxMax>>

QueueSize ==
    FoldFunction(LAMBDA elem, acc : Len(elem) + acc, 0, queues)

SizeApproxMax ==
    FoldFunction(+, 0, sizeApproxMax)

TypeOK ==
    /\ queues \in [Producers -> Seq(Elements)]
    /\ enqueueInProgress \in [Producers -> Seq(Elements)]
    /\ dequeueInProgress \in [Consumers -> Seq(Elements)]
    /\ sizeApproxMax \in [Producers -> Nat]

RecordDequeue(elem) == TRUE
RecordNoDequeue == TRUE

\* Note: Enqueue with no token uses an implicit thread-local producer token.
\* Therefore, it is just modeled as EnqueueWithToken and a specific
\* producer parameter.

EnqueueWithToken_Step(producer, elements) ==
    /\ IsStrictPrefix(enqueueInProgress[producer], elements)
    /\ LET elem ==
            IF   enqueueInProgress[producer] = <<>>
            THEN Head(elements)
            ELSE elements[Len(enqueueInProgress[producer]) + 1]
       IN  /\ enqueueInProgress' = [enqueueInProgress EXCEPT ![producer] = Append(@, elem)]
           /\ queues' = [queues EXCEPT ![producer] = Append(@, elem)]
           /\ sizeApproxMax' = [sizeApproxMax EXCEPT ![producer] = Max({@, Len(queues'[producer])})]
           /\ RecordNoDequeue
           /\ UNCHANGED dequeueInProgress

EnqueueWithToken_Done(producer, elements) ==
    /\ enqueueInProgress[producer] = elements
    /\ enqueueInProgress' = [enqueueInProgress EXCEPT ![producer] = <<>>]
    /\ RecordNoDequeue
    /\ UNCHANGED <<queues, dequeueInProgress, sizeApproxMax>>

DequeueWithToken_Step(consumer, producer, elements) ==
    /\ IsStrictPrefix(dequeueInProgress[consumer], elements)
    /\ LET elem ==
            IF   dequeueInProgress[consumer] = <<>>
            THEN Head(elements)
            ELSE elements[Len(dequeueInProgress[consumer]) + 1]
       IN  /\ IsPrefix(<<elem>>, queues[producer])
           /\ dequeueInProgress' = [dequeueInProgress EXCEPT ![consumer] = Append(@, elem)]
           /\ queues' = [queues EXCEPT ![producer] = Tail(@)]
           /\ RecordDequeue(elem)
           /\ UNCHANGED <<enqueueInProgress, sizeApproxMax>>

DequeueWithToken_Done(consumer, producer, elements) ==
    /\ dequeueInProgress[consumer] = elements
    /\ dequeueInProgress' = [dequeueInProgress EXCEPT ![consumer] = <<>>]
    /\ RecordNoDequeue
    /\ UNCHANGED <<queues, enqueueInProgress, sizeApproxMax>>

Dequeue_Step(consumer, elements) ==
    \E producer \in Producers :
        DequeueWithToken_Step(consumer, producer, elements)

Dequeue_Done(consumer, elements) ==
    /\ dequeueInProgress[consumer] = elements
    /\ dequeueInProgress' = [dequeueInProgress EXCEPT ![consumer] = <<>>]
    /\ RecordNoDequeue
    /\ UNCHANGED <<queues, enqueueInProgress, sizeApproxMax>>

SizeApprox(size) ==
    /\ size <= SizeApproxMax
    /\ RecordNoDequeue
    /\ UNCHANGED vars

CONSTANT BulkSize
ASSUME BulkSize >= 1

Init ==
    /\ queues = [producer \in Producers |-> <<>>]
    /\ enqueueInProgress = [producer \in Producers |-> <<>>]
    /\ dequeueInProgress = [consumer \in Consumers |-> <<>>]
    /\ sizeApproxMax = [producer \in Producers |-> 0]

Next ==
    \/ \E producer \in Producers, elements \in SeqOf(Elements, BulkSize) :
        \/ EnqueueWithToken_Step(producer, elements)
        \/ EnqueueWithToken_Done(producer, elements)
    \/ \E consumer \in Consumers, elements \in SeqOf(Elements, BulkSize) :
        \/ Dequeue_Step(consumer, elements)
        \/ Dequeue_Done(consumer, elements)
    \/ \E consumer \in Consumers, producer \in Producers, elements \in SeqOf(Elements, BulkSize) :
        \/ DequeueWithToken_Step(consumer, producer, elements)
        \/ DequeueWithToken_Done(consumer, producer, elements)
    \/ \E size \in 0 .. SizeApproxMax :
        SizeApprox(size)

Spec ==
    /\ Init
    /\ [][Next]_vars
    /\ SF_vars(
        \E consumer \in Consumers, elements \in SeqOf(Elements, BulkSize) :
            Dequeue_Step(consumer, elements)
       )
    /\ SF_vars(
        \E consumer \in Consumers, producer \in Producers, elements \in SeqOf(Elements, BulkSize) :
            DequeueWithToken_Step(consumer, producer, elements)
       )

====