Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker-benchmarks

[model-checker-benchmarks.git] / chase-lev-deque-bugfix / deque.h

diff --git a/chase-lev-deque-bugfix/deque.h b/chase-lev-deque-bugfix/deque.h
new file mode 100644 (file)
index 0000000..bc670e7
--- /dev/null
+++ b/chase-lev-deque-bugfix/deque.h
@@ -0,0 +1,22 @@
+#ifndef DEQUE_H
+#define DEQUE_H
+
+typedef struct {
+       atomic_size_t size;
+       atomic_int buffer[];
+} Array;
+
+typedef struct {
+       atomic_size_t top, bottom;
+       atomic_uintptr_t array; /* Atomic(Array *) */
+} Deque;
+
+Deque * create();
+int take(Deque *q);
+void resize(Deque *q);
+void push(Deque *q, int x);
+
+#define EMPTY 0xffffffff
+#define ABORT 0xfffffffe
+
+#endif