fixed command line

[cdsspec-compiler.git] / benchmark / chase-lev-deque-bugfix / deque.c

diff --git a/benchmark/chase-lev-deque-bugfix/deque.c b/benchmark/chase-lev-deque-bugfix/deque.c
deleted file mode 100644 (file)
index ff28527..0000000
--- a/benchmark/chase-lev-deque-bugfix/deque.c
+++ /dev/null
@@ -1,178 +0,0 @@
-#include <stdatomic.h>
-#include <inttypes.h>
-#include "deque.h"
-#include <stdlib.h>
-#include <stdio.h>
-
-inline bool fail(int ret) {
-       return ret == ABORT || ret == EMPTY;
-}
-
-Deque * create() {
-       Deque * q = (Deque *) calloc(1, sizeof(Deque));
-       Array * a = (Array *) calloc(1, sizeof(Array)+2*sizeof(atomic_int));
-       atomic_store_explicit(&q->array, a, memory_order_relaxed);
-       atomic_store_explicit(&q->top, 0, memory_order_relaxed);
-       atomic_store_explicit(&q->bottom, 0, memory_order_relaxed);
-       atomic_store_explicit(&a->size, 2, memory_order_relaxed);
-       return q;
-}
-
-
-/**
-       @Begin
-       @Interface_define: Take 
-       @End
-*/
-int take(Deque *q) {
-       size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed) - 1;
-       Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
-       atomic_store_explicit(&q->bottom, b, memory_order_relaxed);
-       /**** SPEC (sequential) (testcase1.c) ****/
-       atomic_thread_fence(memory_order_seq_cst);
-       size_t t = atomic_load_explicit(&q->top, memory_order_relaxed);
-       int x;
-       if (t <= b) {
-               /* Non-empty queue. */
-               int size = atomic_load_explicit(&a->size,memory_order_relaxed);
-               x = atomic_load_explicit(&a->buffer[b % size], memory_order_relaxed);
-               /**
-                       @Begin
-                       @Commit_point_define_check: true 
-                       @Label: TakeReadBuffer
-                       @End
-               */
-               if (t == b) {
-                       /* Single last element in queue. */
-                       //FIXME: weaken the following seq_cst causes no spec problem
-                       bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t +
-                               1, memory_order_seq_cst, memory_order_relaxed);
-                       if (!succ) {
-                               /* Failed race. */
-                               x = EMPTY;
-                       }
-                       atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
-               }
-       } else { /* Empty queue. */
-               x = EMPTY;
-               atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
-       }
-       return x;
-}
-
-void resize(Deque *q) {
-       Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
-       size_t size=atomic_load_explicit(&a->size, memory_order_relaxed);
-       size_t new_size=size << 1;
-       Array *new_a = (Array *) calloc(1, new_size * sizeof(atomic_int) + sizeof(Array));
-       size_t top=atomic_load_explicit(&q->top, memory_order_relaxed);
-       size_t bottom=atomic_load_explicit(&q->bottom, memory_order_relaxed);
-       atomic_store_explicit(&new_a->size, new_size, memory_order_relaxed);
-       size_t i;
-
-       // Initialize the whole new array to turn off the CDSChecker UL error
-       // Check if CDSSpec checker can catch this bug
-       /*
-       for(i=0; i < new_size; i++) {
-               atomic_store_explicit(&new_a->buffer[i % new_size], atomic_load_explicit(&a->buffer[i % size], memory_order_relaxed), memory_order_relaxed);
-       }
-       */
-       for(i=top; i < bottom; i++) {
-               atomic_store_explicit(&new_a->buffer[i % new_size], atomic_load_explicit(&a->buffer[i % size], memory_order_relaxed), memory_order_relaxed);
-       }
-       /**** detected UL ****/
-       atomic_store_explicit(&q->array, new_a, memory_order_release);
-       //printf("resize\n");
-}
-
-/**
-       @Begin
-       @Interface_define: Push
-       @End
-*/
-void push(Deque *q, int x) {
-       size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed);
-       /**** SPEC (sequential) ****/
-       size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
-       Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
-       if (b - t > atomic_load_explicit(&a->size, memory_order_relaxed) - 1) /* Full queue. */ {
-               resize(q);
-               // CDSSpec can actually detect the same bug if we avoid the UL error
-               //Bug in paper...should have next line...
-               a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
-       }
-       int size = atomic_load_explicit(&a->size, memory_order_relaxed);
-
-       atomic_store_explicit(&a->buffer[b % size], x, memory_order_relaxed);
-       /** @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);
-       
-}
-
-/**
-       @Begin
-       @Interface_define: Steal 
-       @End
-*/
-int steal(Deque *q) {
-       //Watch out: actually on need to be an acquire (don't count it)
-       // An old bug
-       size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
-       /**
-               @Begin
-               @Commit_point_define_check: true
-               @Label: StealReadTop1
-               @End
-       */
-       /********** SPEC error (testcase3.c) **********/
-       atomic_thread_fence(memory_order_seq_cst);
-       /**** SPEC & UL ****/
-       size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire);
-       
-       int x = EMPTY;
-       if (t < b) {
-               /**
-                       @Begin
-                       @Commit_point_clear: true
-                       @Label: StealClear1
-                       @End
-               */
-
-               /* Non-empty queue. */
-               /**** detected UL ****/
-               Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_acquire);
-               int size = atomic_load_explicit(&a->size, memory_order_relaxed);
-               x = atomic_load_explicit(&a->buffer[t % size], memory_order_relaxed);
-               /**
-                       @Begin
-                       @Commit_point_define_check: true
-                       @Label: StealReadBuffer
-                       @End
-               */
-               /**** SPEC (sequential) ****/ 
-               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: StealClear2
-                               @End
-                       */
-
-                       /**
-                               @Begin
-                               @Commit_point_define_check: true
-                               @Label: StealReadTop2
-                               @End
-                       */
-
-                       /* Failed race. */
-                       return ABORT;
-               }
-       }
-       return x;
-}