projects
/
model-checker-benchmarks.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
bench.sh: run dekker-fences
[model-checker-benchmarks.git]
/
ms-queue
/
my_queue.h
diff --git
a/ms-queue/my_queue.h
b/ms-queue/my_queue.h
index 519e9e3a7bd17882f78a30724eec1da2a353b8db..c92e420657c1847ec3575156be8e6a7b133e2dae 100644
(file)
--- a/
ms-queue/my_queue.h
+++ b/
ms-queue/my_queue.h
@@
-1,10
+1,6
@@
#include <stdatomic.h>
#include <stdatomic.h>
-#define TRUE 1
-#define FALSE 0
-
#define MAX_NODES 0xf
#define MAX_NODES 0xf
-#define MAX_SERIAL 10000
typedef unsigned long long pointer;
typedef atomic_ullong pointer_t;
typedef unsigned long long pointer;
typedef atomic_ullong pointer_t;
@@
-15,31
+11,21
@@
typedef atomic_ullong 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 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 & PTR_MASK
; }
-static inline unsigned int get_ptr(pointer p) { return
(p & COUNT_MASK) >> 32
; }
+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 int value;
pointer_t next;
typedef struct node {
unsigned int value;
pointer_t next;
- unsigned int foo[30];
} node_t;
} node_t;
-typedef struct private {
- unsigned int node;
- unsigned int value;
- unsigned int serial[MAX_SERIAL];
-} private_t;
-
-typedef struct shared_mem {
+typedef struct {
pointer_t head;
pointer_t head;
- unsigned int foo1[31];
pointer_t tail;
pointer_t tail;
- unsigned int foo2[31];
- node_t nodes[MAX_NODES+1];
- unsigned int serial;
-} shared_mem_t;
+ node_t nodes[MAX_NODES + 1];
+} queue_t;
-void init_
private(int pid
);
-void
init_memory(
);
-
void init_queue(
);
-
unsigned int 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
();