edits: add comments to demonstrate the found bugs and bug injections

[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
index bc670e7ef1e540d56b2e043fe1b11b48f396b91a..9927f9df5a5a9075bc7fc232ade5f51a8a400176 100644 (file)
--- a/chase-lev-deque-bugfix/deque.h
+++ b/chase-lev-deque-bugfix/deque.h
@@ -1,6 +1,9 @@
 #ifndef DEQUE_H
 #define DEQUE_H
 
+#include <stdatomic.h>
+#include <inttypes.h>
+
 typedef struct {
        atomic_size_t size;
        atomic_int buffer[];
@@ -9,14 +12,35 @@ typedef struct {
 typedef struct {
        atomic_size_t top, bottom;
        atomic_uintptr_t array; /* Atomic(Array *) */
+
+    // This is just used to mask the uninitialized loads in the known bugs to
+    // show that even without the CDSChecker's internal check, CDSSpec can
+    // also
+    // detects the known bug.
+    void *newArray;
 } Deque;
 
+Deque * create_size(int size);
 Deque * create();
 int take(Deque *q);
 void resize(Deque *q);
 void push(Deque *q, int x);
+int steal(Deque *q);
 
 #define EMPTY 0xffffffff
 #define ABORT 0xfffffffe
 
+/** @Define:
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+bool succ(int res);
+bool fail(int res);
+
+#ifdef __cplusplus
+};
+#endif
+*/
+
 #endif