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                 @DefineFunc:
  58                         tag_elem_t* new_tag_elem(call_id_t id, unsigned int data) {
  59                                 tag_elem_t *e = (tag_elem_t*) CMODEL_MALLOC(sizeof(tag_elem_t));
  60                                 e->id = id;
  61                                 e->data = data;
  62                                 return e;
  63                         }
  64                 @DefineFunc:
  65                         void free_tag_elem(tag_elem_t *e) {
  66                                 free(e);
  67                         }
  68                 @DefineFunc:
  69                         call_id_t get_id(void *wrapper) {
  70                                 return ((tag_elem_t*) wrapper)->id;
  71                         }
  72                 @DefineFunc:
  73                         unsigned int get_data(void *wrapper) {
  74                                 return ((tag_elem_t*) wrapper)->data;
  75                         }
  76         @Happens_before:
  77                 # Only check the happens-before relationship according to the id of the
  78                 # commit_point_set. For commit_point_set that has same ID, A -> B means
  79                 # B happens after the previous A.
  80                 Enqueue -> Dequeue
  81         @End
  82 */
  83
  84
  85
  86 /**
  87         @Begin
  88         @Interface: Enqueue
  89         @Commit_point_set: Enqueue_Success_Point
  90         @ID: get_and_inc(tag)
  91         @Action:
  92                 # __ID__ is an internal macro that refers to the id of the current
  93                 # interface call
  94                 tag_elem_t *elem = new_tag_elem(__ID__, val);
  95                 push_back(__queue, elem);
  96         @End
  97 */
  98 void enqueue(queue_t *q, unsigned int val);
  99
 100 /**
 101         @Begin
 102         @Interface: Dequeue
 103         @Commit_point_set: Dequeue_Success_Point | Dequeue_Empty_Point
 104         @ID: get_id(front(__queue))
 105         @Action:
 106                 unsigned int _Old_Val = get_data(front(__queue));
 107                 pop_front(__queue);
 108         @Post_check:
 109                 _Old_Val == __RET__
 110         @End
 111 */
 112 unsigned int dequeue(queue_t *q);
 113 int get_thread_num();
 114
 115 #endif