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         @Commutativity: Steal <-> Steal: _Method1.__RET__ == ABORT || _Method2.__RET__ == ABORT
  46
  47     @End
  48 */
  49
  50
  51 Deque * create();
  52 void resize(Deque *q);
  53
  54 /**
  55     @Begin
  56     @Interface: Take
  57     @Commit_point_set: TakeReadBottom | TakeReadBuffer | TakeReadTop
  58     @ID: succ(__RET__) ? __RET__ : DEFAULT_CALL_ID
  59     @Action:
  60                 int elem = 0;
  61         if (succ(__RET__)) {
  62                         elem = back(__deque);
  63                         pop_back(__deque);
  64                         //model_print("take: elem=%d, __RET__=%d\n", elem, __RET__);
  65                 }
  66     @Post_check: succ(__RET__) ? __RET__ == elem : true
  67     @End
  68 */
  69 int take(Deque *q);
  70
  71 /**
  72     @Begin
  73     @Interface: Push
  74     @Commit_point_set: PushUpdateBuffer
  75     @ID: x
  76     @Action:
  77                 push_back(__deque, x);
  78                 //model_print("push: elem=%d\n", x);
  79     @End
  80 */
  81 void push(Deque *q, int x);
  82
  83 /**
  84     @Begin
  85     @Interface: Steal
  86     @Commit_point_set: StealReadTop1 | StealReadTop2 | StealReadBuffer
  87     @ID: succ(__RET__) ? __RET__ : DEFAULT_CALL_ID
  88     @Action:
  89         int elem = 0;
  90         if (succ(__RET__)) {
  91                         elem = front(__deque);
  92                         pop_front(__deque);
  93                         //model_print("steal: elem=%d, __RET__=%d\n", elem, __RET__);
  94                 }
  95     @Post_check: succ(__RET__) ? __RET__ == elem : true
  96     @End
  97 */
  98 int steal(Deque *q);
  99
 100 #endif