-
Notifications
You must be signed in to change notification settings - Fork 4
/
TestLinQueue.tla
101 lines (91 loc) · 3.24 KB
/
TestLinQueue.tla
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
---------------------------- MODULE TestLinQueue ----------------------------
EXTENDS LinQueue
Hmk == <<
\* A enqueues x.
[op|->"E", val|->"x", proc|->"A"],
[op|->"Ok", proc|->"A"]
>>
ASSUME L!Complete(Hmk) = Hmk
ASSUME L!InvocationsWithoutResponses(Hmk) = {}
ASSUME L!Extensions(Hmk) = {{}}
ASSUME L!ExtendedHistories(Hmk) = {Hmk}
ASSUME IsLinearizableHistory(Hmk)
---------
Enq == [op|->"E", val|->"y", proc|->"B"]
Ok == [op|->"Ok", proc|->"B"]
Hmk2 == Hmk \o <<Enq>>
ASSUME L!InvocationsWithoutResponses(Hmk2) = {Enq}
ASSUME L!Extensions(Hmk2) = {{Ok}}
ASSUME L!ExtendedHistories(Hmk2) = {Hmk2 \o <<Ok>>}
ASSUME IsLinearizableHistory(Hmk2)
ASSUME L!Complete(Hmk2) = Hmk
ASSUME L!Complete(Hmk2 \o <<Ok>>) = Hmk2 \o <<Ok>>
Hmk3 == <<
\* A and B concurrently enqueue x and y.
[op|->"E", val|->"x", proc|->"A"],
[op|->"E", val|->"y", proc|->"B"],
[op|->"Ok", proc|->"B"],
[op|->"Ok", proc|->"A"],
\* B dequeues x.
[op|->"D", proc|->"B"],
[op|->"Ok", val|->"x", proc|->"B"],
\* \* A dequeues y.
[op|->"D", proc|->"A"],
[op|->"Ok", val|->"y", proc|->"A"]
>>
ASSUME L!InvocationsWithoutResponses(Hmk3) = {}
ASSUME L!Extensions(Hmk3) = {{}}
ASSUME L!ExtendedHistories(Hmk3) = {Hmk3}
ASSUME L!Complete(Hmk3) = Hmk3
ASSUME IsLinearizableHistory(Hmk3)
---------
H1 == <<
\* A and B concurrently enqueue x and y.
[op|->"E", val|->"x", proc|->"A"],
[op|->"E", val|->"y", proc|->"B"],
[op|->"Ok", proc|->"B"],
[op|->"Ok", proc|->"A"],
\* B dequeues x.
[op|->"D", proc|->"B"],
[op|->"Ok", val|->"x", proc|->"B"],
\* \* A dequeues y.
[op|->"D", proc|->"A"],
[op|->"Ok", val|->"y", proc|->"A"],
\* InL!Complete enqueue of z by A.
[op|->"E", val|->"z", proc|->"A"]>>
ASSUME L!InvocationsWithoutResponses(H1) = {[op|->"E", val|->"z", proc|->"A"]}
ASSUME L!Extensions(H1) = {{[op|->"Ok", proc|->"A"]}}
ASSUME L!ExtendedHistories(H1) = {H1 \o <<[op|->"Ok", proc|->"A"]>>}
\* Strip inL!Complete enqueue of z by A.
ASSUME L!Complete(H1) = SubSeq(H1, 1, Len(H1) - 1)
ASSUME L!Complete(H1 \o <<[op|->"Ok", proc|->"A"]>>) = H1 \o <<[op|->"Ok", proc|->"A"]>>
ASSUME IsLinearizableHistory(H1)
H2 == <<
[op|->"E", val|->"x", proc|->"A"],
[op|->"Ok", proc|->"A"],
[op|->"E", val|->"y", proc|->"B"],
[op|->"D", proc|->"A"],
[op|->"Ok", proc|->"B"],
[op|->"Ok", val|->"y", proc|->"A"]
>>
ASSUME ~IsLinearizableHistory(H2)
H3 == <<
[op|->"E", val|->"x", proc|->"A"],
[op|->"D", proc|-> "B"],
[op|->"Ok", val|->"x", proc|->"B"]>>
ASSUME IsLinearizableHistory(H3)
H4 == <<
[op|->"E", val|->"x", proc|->"A"],
[op|->"E", val|->"y", proc|->"B"],
[op|->"Ok", proc|->"A"],
[op|->"Ok", proc|->"B"],
[op|->"D", proc|-> "A"],
[op|->"D", proc|-> "C"],
[op|->"Ok", val|->"y", proc|->"A"],
[op|->"Ok", val|->"y", proc|->"C"]
>>
ASSUME ~IsLinearizableHistory(H4)
=============================================================================
\* Modification History
\* Last modified Sun Oct 21 15:21:29 PDT 2018 by lhochstein
\* Created Sun Oct 21 10:56:40 PDT 2018 by lhochstein