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                                 if (wrapper == NULL)
  71                                         return 0;
  72                                 return ((tag_elem_t*) wrapper)->id;
  73                         }
  74                 @DefineFunc:
  75                         unsigned int get_data(void *wrapper) {
  76                                 return ((tag_elem_t*) wrapper)->data;
  77                         }
  78         @Happens_before:
  79                 # Only check the happens-before relationship according to the id of the
  80                 # commit_point_set. For commit_point_set that has same ID, A -> B means
  81                 # B happens after the previous A.
  82                 Enqueue -> Dequeue
  83         @End
  84 */
  85
  86
  87
  88 /**
  89         @Begin
  90         @Interface: Enqueue
  91         @Commit_point_set: Enqueue_Read_Tail | Enqueue_UpdateNext
  92         @ID: get_and_inc(tag)
  93         @Action:
  94                 # __ID__ is an internal macro that refers to the id of the current
  95                 # interface call
  96                 tag_elem_t *elem = new_tag_elem(__ID__, val);
  97                 push_back(__queue, elem);
  98                 model_print("Enqueue: input=%d\n", val);
  99         @End
 100 */
 101 void enqueue(queue_t *q, unsigned int val);
 102
 103 /**
 104         @Begin
 105         @Interface: Dequeue
 106         @Commit_point_set: Dequeue_Read_Head | Dequeue_Read_Tail | Dequeue_LoadNext
 107         @ID: get_id(front(__queue))
 108         @Action:
 109                 unsigned int _Old_Val = 0;
 110                 if (size(__queue) > 0) {
 111                         _Old_Val = get_data(front(__queue));
 112                         pop_front(__queue);
 113                 }
 114                 model_print("Dequeue: __RET__=%d, retVal=%d, Old_Val=%d\n", __RET__, *retVal, _Old_Val);
 115         @Post_check:
 116                 _Old_Val == 0 ? !__RET__ : _Old_Val == *retVal
 117         @End
 118 */
 119 bool dequeue(queue_t *q, int *retVal);
 120 int get_thread_num();
 121
 122 #endif