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                 @DeclareVar:
  46                         IntegerList *__queue;
  47                 @InitVar:
  48                         __queue = createIntegerList();
  49                 @Finalize:
  50                         if (__queue)
  51                                 destroyIntegerList(__queue);
  52                         return true;
  53         @Happens_before: Enqueue -> Dequeue
  54         @Commutativity: Enqueue <-> Dequeue: true
  55         @Commutativity: Dequeue <-> Dequeue: !_Method1.__RET__ || !_Method2.__RET__
  56         //@Commutativity: Enqueue <-> Enqueue: _Method1.q != _Method2.q
  57         //@Commutativity: Dequeue <-> Dequeue: _Method1.q != _Method2.q
  58         @End
  59 */
  60
  61
  62
  63 /**
  64         @Begin
  65         @Interface: Enqueue
  66         @Commit_point_set: EnqueueUpdateNext
  67         @ID: val
  68         @Action:
  69                 # __ID__ is an internal macro that refers to the id of the current
  70                 # interface call
  71                 push_back(__queue, val);
  72                 //model_print("Enqueue: val=%d\n", val);
  73         @End
  74 */
  75 void enqueue(queue_t *q, unsigned int val);
  76
  77 /**
  78         @Begin
  79         @Interface: Dequeue
  80         @Commit_point_set: DequeueReadHead | DequeueUpdateHead | DequeueReadNextVerify
  81         @ID: __RET__ ? *retVal : 0
  82         @Action:
  83                 int elem = 0;
  84                 if (__RET__) {
  85                         elem = front(__queue);
  86                         pop_front(__queue);
  87                 }
  88                 //model_print("Dequeue: __RET__=%d, retVal=%d, elem=%d, \n", __RET__, *retVal, elem);
  89                 //model_print("Result: %d\n", __RET__ ? *retVal == elem : true);
  90         @Post_check: __RET__ ? *retVal == elem : true
  91         @End
  92 */
  93 bool dequeue(queue_t *q, int *retVal);
  94 int get_thread_num();
  95
  96 #endif