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

   1 #ifndef DEQUE_H
   2 #define DEQUE_H
   3 #include <spec_lib.h>
   4 #include <stdlib.h>
   5 #include <cdsannotate.h>
   6 #include <specannotation.h>
   7 #include <model_memory.h>
   8 #include "common.h"
   9
  10 typedef struct {
  11         atomic_size_t size;
  12         atomic_int buffer[];
  13 } Array;
  14
  15 typedef struct {
  16         atomic_size_t top, bottom;
  17         atomic_uintptr_t array; /* Atomic(Array *) */
  18 } Deque;
  19
  20 #define EMPTY 0xffffffff
  21 #define ABORT 0xfffffffe
  22
  23 /**
  24     @Begin
  25     @Options:
  26         LANG = C;
  27     @Global_define:
  28         @DeclareStruct:
  29         typedef struct tag_elem {
  30             call_id_t id;
  31             int data;
  32         } tag_elem_t;
  33
  34         @DeclareVar:
  35         spec_list *__deque;
  36         id_tag_t *tag;
  37         @InitVar:
  38             __deque= new_spec_list();
  39             tag = new_id_tag(); // Beginning of available id
  40         @DefineFunc:
  41             tag_elem_t* new_tag_elem(call_id_t id, int data) {
  42                 tag_elem_t *e = (tag_elem_t*) CMODEL_MALLOC(sizeof(tag_elem_t));
  43                 e->id = id;
  44                 e->data = data;
  45                 return e;
  46             }
  47         @DefineFunc:
  48             call_id_t get_id(void *wrapper) {
  49                 return ((tag_elem_t*) wrapper)->id;
  50             }
  51         @DefineFunc:
  52             int get_data(void *wrapper) {
  53                 return ((tag_elem_t*) wrapper)->data;
  54             }
  55     @Happens_before:
  56         Push -> Steal
  57                 Push -> Take
  58     @End
  59 */
  60
  61
  62 Deque * create();
  63 void resize(Deque *q);
  64
  65 /**
  66     @Begin
  67     @Interface: Take
  68     @Commit_point_set: Take_Point1 | Take_Point2 | Take_Point3 | Take_Point4
  69     @ID: size(__deque) == 0 ? DEFAULT_CALL_ID : get_id(back(__deque))
  70     @Action:
  71         int _Old_Val = EMPTY;
  72                 if (size(__deque) > 0) {
  73                         _Old_Val = get_data(back(__deque));
  74                 pop_back(__deque);
  75                 }
  76     @Post_check:
  77         _Old_Val == __RET__
  78     @End
  79 */
  80 int take(Deque *q);
  81
  82 /**
  83     @Begin
  84     @Interface: Push
  85     @Commit_point_set: Push_Point
  86     @ID: get_and_inc(tag);
  87     @Action:
  88         tag_elem_t *elem = new_tag_elem(__ID__, x);
  89         push_back(__deque, elem);
  90     @End
  91 */
  92 void push(Deque *q, int x);
  93
  94 /**
  95     @Begin
  96     @Interface: Steal
  97     @Commit_point_set: Steal_Point1 | Steal_Point2 | Steal_Point3
  98     @ID: size(__deque) == 0 ? DEFAULT_CALL_ID : get_id(front(__deque))
  99     @Action:
 100         int _Old_Val = EMPTY;
 101                 if (size(__deque) > 0) {
 102                         _Old_Val = get_data(front(__deque));
 103                 pop_front(__deque);
 104                 }
 105     @Post_check:
 106         _Old_Val == __RET__
 107     @End
 108 */
 109 int steal(Deque *q);
 110
 111 #endif