fix bug
[model-checker-benchmarks.git] / ms-queue / my_queue.h
index 3e3f435b43569eb843932f29122907f6be06967d..c92e420657c1847ec3575156be8e6a7b133e2dae 100644 (file)
@@ -1,43 +1,31 @@
 #include <stdatomic.h>
 
-#define TRUE                           1
-#define FALSE                          0
+#define MAX_NODES                      0xf
 
-#define MAX_NODES                      0xff
-#define MAX_SERIAL                     10000
+typedef unsigned long long pointer;
+typedef atomic_ullong pointer_t;
 
-#define MAKE_LONG(lo, hi)              ((hi)<<16)+(lo)
+#define MAKE_POINTER(ptr, count)       ((((pointer)count) << 32) | ptr)
+#define PTR_MASK 0xffffffffLL
+#define COUNT_MASK (0xffffffffLL << 32)
 
-typedef union pointer {
-       struct {
-               volatile unsigned short count;
-               volatile unsigned short ptr;
-       } sep;
-       atomic_ulong con;
-} pointer_t;
+static inline void set_count(pointer *p, unsigned int val) { *p = (*p & ~COUNT_MASK) | ((pointer)val << 32); }
+static inline void set_ptr(pointer *p, unsigned int val) { *p = (*p & ~PTR_MASK) | val; }
+static inline unsigned int get_count(pointer p) { return (p & COUNT_MASK) >> 32; }
+static inline unsigned int get_ptr(pointer p) { return p & PTR_MASK; }
 
 typedef struct node {
-       unsigned value;
+       unsigned int value;
        pointer_t next;
-       unsigned foo[30];
 } node_t;
 
-typedef struct private {
-       unsigned node;
-       unsigned value;
-       unsigned serial[MAX_SERIAL];
-} private_t;
-
-typedef struct shared_mem {
+typedef struct {
        pointer_t head;
-       unsigned foo1[31];
        pointer_t tail;
-       unsigned foo2[31];
-       node_t nodes[MAX_NODES+1];
-       unsigned serial;
-} shared_mem_t;
+       node_t nodes[MAX_NODES + 1];
+} queue_t;
 
-void init_private();
-void init_memory();
-void init_queue();
-unsigned dequeue();
+void init_queue(queue_t *q, int num_threads);
+void enqueue(queue_t *q, unsigned int val);
+unsigned int dequeue(queue_t *q);
+int get_thread_num();