Skip to content

Commit 95b04ec

Browse files
fhackettfhackett
authored
Merge pull request #271 from AnzheXue/main
Allowing Enqueue operation specification function correctly
2 parents 0c9771a + 9f258a4 commit 95b04ec

File tree

3 files changed

+50
-42
lines changed

3 files changed

+50
-42
lines changed

‎omnilink/concurrentqueue/ConcurrentQueueAPI.tla‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -35,14 +35,14 @@ MinCount(a, b) ==
3535

3636
PayloadForElement(element) == <<element>>
3737

38-
BulkBufferSet == [1..MaxBulkSize -> Elements]
38+
BulkBufferSet == { seq \in Seq(Elements) : Len(seq) <= MaxBulkSize }
3939
BulkBuffer(elements) == elements \in BulkBufferSet
4040
BulkPayload(elements, count) == Take(elements, count)
4141

4242
BulkArgsOk(elements, count) ==
4343
/\ BulkBuffer(elements)
4444
/\ count \in 1..MaxBulkSize
45-
/\ Len(BulkPayload(elements, count)) = count
45+
/\ Len(elements) >= count
4646
/\ IsPrefix(BulkPayload(elements, count), elements)
4747

4848
EnqueueOutcome(canEnqueue, thread, payload, delta, success) ==
@@ -166,14 +166,14 @@ Next ==
166166
QueueTryEnqueue(element, success, thread)
167167
\/ \E thread \in Threads, elements \in BulkBufferSet, count \in 1..MaxBulkSize, success \in BOOLEAN :
168168
QueueTryEnqueueBulk(elements, count, success, thread)
169-
\/ \E thread \in Threads, element \in Elements, success \in BOOLEAN :
170-
QueueTryDequeue(element, success, thread)
171-
\/ \E thread \in Threads, elements \in BulkBufferSet, max \in 1..MaxBulkSize, count \in 0..MaxBulkSize :
172-
QueueTryDequeueBulk(elements, max, count, thread)
173-
\/ \E thread \in Threads, element \in Elements, success \in BOOLEAN :
174-
QueueTryDequeueFromProducer(thread, element, success, thread)
175-
\/ \E thread \in Threads, elements \in BulkBufferSet, max \in 1..MaxBulkSize, count \in 0..MaxBulkSize :
176-
QueueTryDequeueBulkFromProducer(thread, elements, max, count, thread)
169+
\* \/ \E thread \in Threads, element \in Elements, success \in BOOLEAN :
170+
\* QueueTryDequeue(element, success, thread)
171+
\* \/ \E thread \in Threads, elements \in BulkBufferSet, max \in 1..MaxBulkSize, count \in 0..MaxBulkSize :
172+
\* QueueTryDequeueBulk(elements, max, count, thread)
173+
\* \/ \E thread \in Threads, element \in Elements, success \in BOOLEAN :
174+
\* QueueTryDequeueFromProducer(thread, element, success, thread)
175+
\* \/ \E thread \in Threads, elements \in BulkBufferSet, max \in 1..MaxBulkSize, count \in 0..MaxBulkSize :
176+
\* QueueTryDequeueBulkFromProducer(thread, elements, max, count, thread)
177177
\/ \E size \in 0..MaxElements :
178178
QueueSizeApprox(size)
179179

‎omnilink/concurrentqueue/MCConcurrentQueueAPIValidate.tla‎

Lines changed: 15 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -13,11 +13,18 @@ ElementsImpl == TLCCache(UNION UNION { {
1313

1414
ThreadsImpl == TLCCache(UNION UNION { {
1515
LET __rec == __traces[t][i]
16-
IN IF "prodToken" \in DOMAIN __rec.operation
17-
THEN {__rec.operation.prodToken}
18-
ELSE IF "consToken" \in DOMAIN __rec.operation
19-
THEN {__rec.operation.consToken}
20-
ELSE {}
16+
__op == __rec.operation
17+
__threads ==
18+
(IF "thread" \in DOMAIN __op /\ __op.thread # "null" /\ __op.thread \in Int
19+
THEN {__op.thread}
20+
ELSE {}) \cup
21+
(IF "prodToken" \in DOMAIN __op /\ __op.prodToken # "null" /\ __op.prodToken \in Int
22+
THEN {__op.prodToken}
23+
ELSE {}) \cup
24+
(IF "consToken" \in DOMAIN __op /\ __op.consToken # "null" /\ __op.consToken \in Int
25+
THEN {__op.consToken}
26+
ELSE {})
27+
IN __threads
2128
: i \in DOMAIN __traces[t] }
2229
: t \in DOMAIN __traces }, {"ThreadsImpl"})
2330

@@ -29,11 +36,12 @@ TypeOK == __Spec!TypeOK
2936
QueueInvariant == __Spec!QueueInvariant
3037
NoLostElements == __Spec!NoLostElements
3138

32-
PragmaticView ==
39+
(* PragmaticView ==
3340
[
34-
__pc |-> __pc,
41+
__pc |-> __pc,
3542
queue_len |-> Len(queue)
3643
]
44+
*)
3745

3846
====
3947

‎omnilink/concurrentqueue/workload/main.cpp‎

Lines changed: 25 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -45,15 +45,16 @@ struct QueueWorkloadContext: public omnilink::WorkloadContext<QueueWorkloadConte
4545
// };
4646
// }
4747

48-
// void perform_operation(Ctx<ConcurrentQueueAPI::QueueEnqueueBulk>& ctx) {
49-
// int32_t count = rand_bulk_size();
50-
// std::vector<int32_t> elements(count);
51-
// for (int32_t i = 0; i < count; i++) {
52-
// elements[i] = rand_element();
53-
// }
54-
// bool success = workload_context.queue.enqueue_bulk(elements.data(), count);
55-
// ctx.op = ConcurrentQueueAPI::QueueEnqueueBulk{elements, count, success};
56-
// }
48+
void perform_operation(Ctx<ConcurrentQueueAPI::QueueEnqueueBulk>& ctx) {
49+
int32_t count = rand_bulk_size();
50+
std::vector<int32_t> elements(count);
51+
for (int32_t i = 0; i < count; i++) {
52+
elements[i] = rand_element();
53+
}
54+
bool success = workload_context.queue.enqueue_bulk(elements.data(), count);
55+
ctx.op = ConcurrentQueueAPI::QueueEnqueueBulk{elements, count, success};
56+
ctx.op.thread = static_cast<int32_t>(thread_idx);
57+
}
5758

5859
// void perform_operation(Ctx<ConcurrentQueueAPI::QueueEnqueueBulkWithToken>& ctx) {
5960
// int32_t count = rand_bulk_size();
@@ -90,15 +91,15 @@ struct QueueWorkloadContext: public omnilink::WorkloadContext<QueueWorkloadConte
9091
// };
9192
// }
9293

93-
// void perform_operation(Ctx<ConcurrentQueueAPI::QueueTryEnqueueBulk>& ctx) {
94-
// int32_t count = rand_bulk_size();
95-
// std::vector<int32_t> elements(count);
96-
// for (int32_t i = 0; i < count; i++) {
97-
// elements[i] = rand_element();
98-
// }
99-
// bool success = workload_context.queue.try_enqueue_bulk(elements.data(), count);
100-
// ctx.op = ConcurrentQueueAPI::QueueTryEnqueueBulk{elements, count, success};
101-
// }
94+
void perform_operation(Ctx<ConcurrentQueueAPI::QueueTryEnqueueBulk>& ctx) {
95+
int32_t count = rand_bulk_size();
96+
std::vector<int32_t> elements(count);
97+
for (int32_t i = 0; i < count; i++) {
98+
elements[i] = rand_element();
99+
}
100+
bool success = workload_context.queue.try_enqueue_bulk(elements.data(), count);
101+
ctx.op = ConcurrentQueueAPI::QueueTryEnqueueBulk{elements, count, success};
102+
}
102103

103104
// void perform_operation(Ctx<ConcurrentQueueAPI::QueueTryEnqueueBulkWithToken>& ctx) {
104105
// int32_t count = rand_bulk_size();
@@ -116,12 +117,12 @@ struct QueueWorkloadContext: public omnilink::WorkloadContext<QueueWorkloadConte
116117
// };
117118
// }
118119

119-
void perform_operation(Ctx<ConcurrentQueueAPI::QueueTryDequeue>& ctx) {
120-
int32_t element = 0;
121-
bool success = workload_context.queue.try_dequeue(element);
122-
ctx.op = ConcurrentQueueAPI::QueueTryDequeue{element, success};
123-
ctx.op.thread = static_cast<int32_t>(thread_idx);
124-
}
120+
// void perform_operation(Ctx<ConcurrentQueueAPI::QueueTryDequeue>& ctx) {
121+
// int32_t element = 0;
122+
// bool success = workload_context.queue.try_dequeue(element);
123+
// ctx.op = ConcurrentQueueAPI::QueueTryDequeue{element, success};
124+
// ctx.op.thread = static_cast<int32_t>(thread_idx);
125+
// }
125126

126127
// void perform_operation(Ctx<ConcurrentQueueAPI::QueueTryDequeueWithToken>& ctx) {
127128
// int32_t element = 0;
@@ -185,7 +186,6 @@ struct QueueWorkloadContext: public omnilink::WorkloadContext<QueueWorkloadConte
185186

186187
void perform_operation(Ctx<ConcurrentQueueAPI::QueueSizeApprox>& ctx) {
187188
ctx.op = ConcurrentQueueAPI::QueueSizeApprox{static_cast<int32_t>(workload_context.queue.size_approx())};
188-
ctx.op.thread = static_cast<int32_t>(thread_idx);
189189
}
190190
};
191191
};

0 commit comments

Comments
 (0)