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 inline bool fail(int ret);
  25 /**
  26     @Begin
  27     @Options:
  28         LANG = C;
  29     @Global_define:
  30         @DeclareVar:
  31                         IntegerList *__deque;
  32         @InitVar:
  33                         __deque = createIntegerList();
  34                 @Finalize:
  35                         if (__deque)
  36                                 destroyIntegerList(__deque);
  37                         return true;
  38                 @DefineFunc:
  39                         bool succ(int res) {
  40                                 return res != EMPTY && res != ABORT;
  41                         }
  42     @Happens_before:
  43         Push -> Steal
  44         @Commutativity: Push <-> Steal: true
  45         @Commutativity: Take <-> Steal: true
  46         @Commutativity: Steal <-> Steal: fail(_Method1.__RET__) || fail(_Method2.__RET__)
  47
  48     @End
  49 */
  50
  51
  52 Deque * create();
  53 void resize(Deque *q);
  54
  55 /**
  56     @Begin
  57     @Interface: Take
  58     @Commit_point_set: TakeReadBottom | TakeReadBuffer | TakeReadTop
  59     @ID: succ(__RET__) ? __RET__ : DEFAULT_CALL_ID
  60     @Action:
  61                 int elem = 0;
  62         if (succ(__RET__)) {
  63                         elem = back(__deque);
  64                         pop_back(__deque);
  65                         //model_print("take: elem=%d, __RET__=%d\n", elem, __RET__);
  66                 }
  67     @Post_check: succ(__RET__) ? __RET__ == elem : true
  68     @End
  69 */
  70 int take(Deque *q);
  71
  72 /**
  73     @Begin
  74     @Interface: Push
  75     @Commit_point_set: PushUpdateBuffer
  76     @ID: x
  77     @Action:
  78                 push_back(__deque, x);
  79                 //model_print("push: elem=%d\n", x);
  80     @End
  81 */
  82 void push(Deque *q, int x);
  83
  84 /**
  85     @Begin
  86     @Interface: Steal
  87     @Commit_point_set: StealReadTop1 | StealReadTop2 | StealReadBuffer
  88     @ID: succ(__RET__) ? __RET__ : DEFAULT_CALL_ID
  89     @Action:
  90         int elem = 0;
  91         if (succ(__RET__)) {
  92                         elem = front(__deque);
  93                         pop_front(__deque);
  94                         //model_print("steal: elem=%d, __RET__=%d\n", elem, __RET__);
  95                 }
  96     @Post_check: succ(__RET__) ? __RET__ == elem : true
  97     @End
  98 */
  99 int steal(Deque *q);
 100
 101 #endif