*/
int take(Deque *q) {
size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed) - 1;
- /**
- @Begin
- @Commit_point_define_check: true
- @Label: TakeReadBottom
- @End
- */
Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
atomic_store_explicit(&q->bottom, b, memory_order_relaxed);
/**** SPEC (sequential) (testcase1.c) ****/
size_t t = atomic_load_explicit(&q->top, memory_order_relaxed);
int x;
if (t <= b) {
- /**
- @Begin
- @Commit_point_clear: true
- @Label: TakeClear1
- @End
- */
-
/* Non-empty queue. */
int size = atomic_load_explicit(&a->size,memory_order_relaxed);
x = atomic_load_explicit(&a->buffer[b % size], memory_order_relaxed);
bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t +
1, memory_order_seq_cst, memory_order_relaxed);
if (!succ) {
- /**
- @Begin
- @Commit_point_clear: true
- @Label: TakeClear2
- @End
- */
-
- /**
- @Begin
- @Commit_point_define_check: true
- @Label: TakeReadTop
- @End
- */
-
/* Failed race. */
x = EMPTY;
}
int size = atomic_load_explicit(&a->size, memory_order_relaxed);
atomic_store_explicit(&a->buffer[b % size], x, memory_order_relaxed);
- /**
- @Begin
- @Commit_point_define_check: true
- @Label: PushUpdateBuffer
- @End
- */
+ /** @OPDefine: true */
+
/**** UL & SPEC (Sync) (run with -u100 to avoid the uninitialized bug) ****/
atomic_thread_fence(memory_order_release);
atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
}
static public void main(String[] args) {
- String[] dirNames = { Environment.REGISTER, Environment.MS_QUEUE,
- Environment.LINUXRWLOCKS, Environment.MCS_LOCK,
- Environment.DEQUE };
+// String[] dirNames = { Environment.REGISTER, Environment.MS_QUEUE,
+// Environment.LINUXRWLOCKS, Environment.MCS_LOCK,
+// Environment.DEQUE };
+ String[] dirNames = args;
for (int i = 0; i < dirNames.length; i++) {
String dirName = dirNames[i];