edits
[cdsspec-compiler.git] / benchmark / ms-queue / my_queue.h
1 #ifndef _MY_QUEUE_H
2 #define _MY_QUEUE_H
3
4 #include <stdatomic.h>
5
6 #include <spec_lib.h>
7 #include <stdlib.h>
8 #include <cdsannotate.h>
9 #include <specannotation.h>
10 #include <model_memory.h>
11 #include "common.h" 
12
13 #define MAX_NODES                       0xf
14
15 typedef unsigned long long pointer;
16 typedef atomic_ullong pointer_t;
17
18 #define MAKE_POINTER(ptr, count)        ((((pointer)count) << 32) | ptr)
19 #define PTR_MASK 0xffffffffLL
20 #define COUNT_MASK (0xffffffffLL << 32)
21
22 static inline void set_count(pointer *p, unsigned int val) { *p = (*p & ~COUNT_MASK) | ((pointer)val << 32); }
23 static inline void set_ptr(pointer *p, unsigned int val) { *p = (*p & ~PTR_MASK) | val; }
24 static inline unsigned int get_count(pointer p) { return (p & COUNT_MASK) >> 32; }
25 static inline unsigned int get_ptr(pointer p) { return p & PTR_MASK; }
26
27 typedef struct node {
28         unsigned int value;
29         pointer_t next;
30 } node_t;
31
32 typedef struct {
33         pointer_t head;
34         pointer_t tail;
35         node_t nodes[MAX_NODES + 1];
36 } queue_t;
37
38 void init_queue(queue_t *q, int num_threads);
39
40 /**
41         @Begin
42         @Options:
43                 LANG = C;
44         @Global_define:
45                 @DeclareStruct:
46                 typedef struct tag_elem {
47                         call_id_t id;
48                         unsigned int data;
49                 } tag_elem_t;
50                 
51                 @DeclareVar:
52                         spec_list *__queue;
53                         id_tag_t *tag;
54                 @InitVar:
55                         __queue = new_spec_list();
56                         tag = new_id_tag(); // Beginning of available id
57                 //@Cleanup:
58                 //      if (__queue)
59                 //              free_spec_list(__queue);
60                 //      if (tag)
61                 //              free_id_tag(tag);
62                 @DefineFunc:
63                         tag_elem_t* new_tag_elem(call_id_t id, unsigned int data) {
64                                 tag_elem_t *e = (tag_elem_t*) CMODEL_MALLOC(sizeof(tag_elem_t));
65                                 e->id = id;
66                                 e->data = data;
67                                 return e;
68                         }
69                 //@DefineFunc:
70                 //      void free_tag_elem(tag_elem_t *e) {
71                 //              free(e);
72                 //      }
73                 @DefineFunc:
74                         call_id_t get_id(void *wrapper) {
75                 //              if (wrapper == NULL)
76                 //                      return 0;
77                 //              return ((tag_elem_t*) wrapper)->id;
78                                 return wrapper == NULL ? 0 : ((tag_elem_t*) wrapper)->id;
79                         }
80                 @DefineFunc:
81                         unsigned int get_data(void *wrapper) {
82                                 return ((tag_elem_t*) wrapper)->data;
83                         }
84         @Happens_before: Enqueue -> Dequeue
85                 # Only check the happens-before relationship according to the id of the
86                 # commit_point_set. For commit_point_set that has same ID, A -> B means
87                 # B happens after the previous A.
88         @Commutativity: Enqueue <-> Dequeue: true
89         @Commutativity: Enqueue <-> Enqueue: _Method1.q != _Method2.q
90         @Commutativity: Dequeue <-> Dequeue: _Method1.q != _Method2.q
91         @End
92 */
93
94
95
96 /**
97         @Begin
98         @Interface: Enqueue
99         @Commit_point_set: EnqueueUpdateNext
100         @ID: get_and_inc(tag)
101         @Action:
102                 # __ID__ is an internal macro that refers to the id of the current
103                 # interface call
104                 tag_elem_t *elem = new_tag_elem(__ID__, val);
105                 push_back(__queue, elem);
106                 //model_print("Enqueue: input=%d\n", val);
107         @End
108 */
109 void enqueue(queue_t *q, unsigned int val);
110
111 /**
112         @Begin
113         @Interface: Dequeue
114         @Commit_point_set: DequeueUpdateHead | DequeueReadNextVerify
115         @ID: get_id(front(__queue))
116         @Action:
117                 unsigned int _Old_Val = 0;
118                 if (size(__queue) > 0) {
119                         _Old_Val = get_data(front(__queue));
120                         pop_front(__queue);
121                 }
122         //      model_print("Dequeue: __RET__=%d, retVal=%d, Old_Val=%d\n", __RET__, *retVal, _Old_Val);
123         @Post_check: _Old_Val == 0 ? !__RET__ : _Old_Val == *retVal
124         @End
125 */
126 bool dequeue(queue_t *q, int *retVal);
127 int get_thread_num();
128
129 #endif