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: _Method2.__RET__ == NULL
  89         @Commutativity: Enqueue <-> Dequeue: _Method1.q != _Method2.q
  90         @End
  91 */
  92
  93
  94
  95 /**
  96         @Begin
  97         @Interface: Enqueue
  98         @Commit_point_set: Enqueue_Update_Next | Enqueue_Update_Tail
  99         @ID: get_and_inc(tag)
 100         @Action:
 101                 # __ID__ is an internal macro that refers to the id of the current
 102                 # interface call
 103                 tag_elem_t *elem = new_tag_elem(__ID__, val);
 104                 push_back(__queue, elem);
 105                 //model_print("Enqueue: input=%d\n", val);
 106         @End
 107 */
 108 void enqueue(queue_t *q, unsigned int val);
 109
 110 /**
 111         @Begin
 112         @Interface: Dequeue
 113         @Commit_point_set: Dequeue_Read_Head | Dequeue_Read_Tail | Dequeue_Read_Next
 114         @ID: get_id(front(__queue))
 115         @Action:
 116                 unsigned int _Old_Val = 0;
 117                 if (size(__queue) > 0) {
 118                         _Old_Val = get_data(front(__queue));
 119                         pop_front(__queue);
 120                 }
 121         //      model_print("Dequeue: __RET__=%d, retVal=%d, Old_Val=%d\n", __RET__, *retVal, _Old_Val);
 122         @Post_check: _Old_Val == 0 ? !__RET__ : _Old_Val == *retVal
 123         @End
 124 */
 125 bool dequeue(queue_t *q, int *retVal);
 126 int get_thread_num();
 127
 128 #endif