benchmark/chase-lev-deque-bugfix/deque.h

   1 #ifndef DEQUE_H
   2 #define DEQUE_H
   3
   4 #include <spec_lib.h>
   5 #include <stdlib.h>
   6 #include <cdsannotate.h>
   7 #include <specannotation.h>
   8 #include <model_memory.h>
   9 #include "common.h"
  10
  11 typedef struct {
  12         atomic_size_t size;
  13         atomic_int buffer[];
  14 } Array;
  15
  16 typedef struct {
  17         atomic_size_t top, bottom;
  18         atomic_uintptr_t array; /* Atomic(Array *) */
  19 } Deque;
  20
  21 #define EMPTY 0xffffffff
  22 #define ABORT 0xfffffffe
  23
  24 /**
  25     @Begin
  26     @Options:
  27         LANG = C;
  28     @Global_define:
  29         @DeclareVar:
  30                         IntegerList *__deque;
  31         @InitVar:
  32                         __deque = createIntegerList();
  33                 @Finalize:
  34                         if (__deque)
  35                                 destroyIntegerList(__deque);
  36                         return true;
  37                 @DefineFunc:
  38                         bool succ(int res) {
  39                                 return res != EMPTY && res != ABORT;
  40                         }
  41     @Happens_before:
  42         Push -> Steal
  43         @Commutativity: Push <-> Steal: true
  44         @Commutativity: Take <-> Steal: true
  45
  46     @End
  47 */
  48
  49
  50 Deque * create();
  51 void resize(Deque *q);
  52
  53 /**
  54     @Begin
  55     @Interface: Take
  56     @Commit_point_set: Take_Read_Bottom | Take_Additional_Point
  57     @ID: succ(__RET__) ? __RET__ : DEFAULT_CALL_ID
  58     @Action:
  59                 int elem = 0;
  60         if (succ(__RET__)) {
  61                         elem = back(__deque);
  62                         pop_back(__deque);
  63                         //model_print("take: elem=%d, __RET__=%d\n", elem, __RET__);
  64                 }
  65     @Post_check: succ(__RET__) ? __RET__ == elem : true
  66     @End
  67 */
  68 int take(Deque *q);
  69
  70 /**
  71     @Begin
  72     @Interface: Push
  73     @Commit_point_set: Push_Update_Bottom
  74     @ID: x
  75     @Action:
  76                 push_back(__deque, x);
  77                 //model_print("push: elem=%d\n", x);
  78     @End
  79 */
  80 void push(Deque *q, int x);
  81
  82 /**
  83     @Begin
  84     @Interface: Steal
  85     @Commit_point_set: Steal_Read_Bottom | Steal_Additional_Point
  86     @ID: succ(__RET__) ? __RET__ : DEFAULT_CALL_ID
  87     @Action:
  88         int elem = 0;
  89         if (succ(__RET__)) {
  90                         elem = front(__deque);
  91                         pop_front(__deque);
  92                         //model_print("steal: elem=%d, __RET__=%d\n", elem, __RET__);
  93                 }
  94     @Post_check: succ(__RET__) ? __RET__ == elem : true
  95     @End
  96 */
  97 int steal(Deque *q);
  98
  99 #endif