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
  12 #define MAX_NODES                       0xf
  13
  14 typedef unsigned long long pointer;
  15 typedef atomic_ullong pointer_t;
  16
  17 #define MAKE_POINTER(ptr, count)        ((((pointer)count) << 32) | ptr)
  18 #define PTR_MASK 0xffffffffLL
  19 #define COUNT_MASK (0xffffffffLL << 32)
  20
  21 static inline void set_count(pointer *p, unsigned int val) { *p = (*p & ~COUNT_MASK) | ((pointer)val << 32); }
  22 static inline void set_ptr(pointer *p, unsigned int val) { *p = (*p & ~PTR_MASK) | val; }
  23 static inline unsigned int get_count(pointer p) { return (p & COUNT_MASK) >> 32; }
  24 static inline unsigned int get_ptr(pointer p) { return p & PTR_MASK; }
  25
  26 typedef struct node {
  27         unsigned int value;
  28         pointer_t next;
  29 } node_t;
  30
  31 typedef struct {
  32         pointer_t head;
  33         pointer_t tail;
  34         node_t nodes[MAX_NODES + 1];
  35 } queue_t;
  36
  37 void init_queue(queue_t *q, int num_threads);
  38
  39 /**
  40         @Begin
  41         @Options:
  42                 LANG = C;
  43         @Global_define:
  44                 @DeclareStruct:
  45                 typedef struct tag_elem {
  46                         call_id_t id;
  47                         unsigned int data;
  48                 } tag_elem_t;
  49
  50                 @DeclareVar:
  51                 spec_list *__queue;
  52                 id_tag_t *tag;
  53                 @InitVar:
  54                         __queue = new_spec_list();
  55                         tag = new_id_tag(); // Beginning of available id
  56                 @DefineFunc:
  57                         tag_elem_t* new_tag_elem(call_id_t id, unsigned int data) {
  58                                 tag_elem_t *e = (tag_elem_t*) CMODEL_MALLOC(sizeof(tag_elem_t));
  59                                 e->id = id;
  60                                 e->data = data;
  61                                 return e;
  62                         }
  63                 @DefineFunc:
  64                         void free_tag_elem(tag_elem_t *e) {
  65                                 free(e);
  66                         }
  67                 @DefineFunc:
  68                         call_id_t get_id(void *wrapper) {
  69                                 return ((tag_elem_t*) wrapper)->id;
  70                         }
  71                 @DefineFunc:
  72                         unsigned int get_data(void *wrapper) {
  73                                 return ((tag_elem_t*) wrapper)->data;
  74                         }
  75         @Happens_before:
  76                 # Only check the happens-before relationship according to the id of the
  77                 # commit_point_set. For commit_point_set that has same ID, A -> B means
  78                 # B happens after the previous A.
  79                 Enqueue -> Dequeue
  80         @End
  81 */
  82
  83
  84
  85 /**
  86         @Begin
  87         @Interface: Enqueue
  88         @Commit_point_set: Enqueue_Success_Point
  89         @ID: get_and_inc(tag)
  90         @Action:
  91                 # __ID__ is an internal macro that refers to the id of the current
  92                 # interface call
  93                 tag_elem_t *elem = new_tag_elem(__ID__, val);
  94                 push_back(__queue, elem);
  95         @End
  96 */
  97 void enqueue(queue_t *q, unsigned int val);
  98
  99 /**
 100         @Begin
 101         @Interface: Dequeue
 102         @Commit_point_set: Dequeue_Success_Point | Dequeue_Empty_Point
 103         @ID: get_id(front(__queue))
 104         @Action:
 105                 unsigned int _Old_Val = get_data(front(__queue));
 106                 pop_front(__queue);
 107         @Post_check:
 108                 _Old_Val == __RET__
 109         @End
 110 */
 111 unsigned int dequeue(queue_t *q);
 112 int get_thread_num();
 113
 114 #endif