#ifndef DEQUE_H
#define DEQUE_H
+#include <spec_lib.h>
+#include <stdlib.h>
+#include <cdsannotate.h>
+#include <specannotation.h>
+#include <model_memory.h>
+#include "common.h"
+
typedef struct {
atomic_size_t size;
atomic_int buffer[];
atomic_uintptr_t array; /* Atomic(Array *) */
} Deque;
+#define EMPTY 0xffffffff
+#define ABORT 0xfffffffe
+
+/**
+ @Begin
+ @Options:
+ LANG = C;
+ @Global_define:
+ @DeclareStruct:
+ typedef struct tag_elem {
+ call_id_t id;
+ int data;
+ } tag_elem_t;
+
+ @DeclareVar:
+ spec_list *__deque;
+ id_tag_t *tag;
+ @InitVar:
+ __deque= new_spec_list();
+ tag = new_id_tag(); // Beginning of available id
+ @DefineFunc:
+ tag_elem_t* new_tag_elem(call_id_t id, int data) {
+ tag_elem_t *e = (tag_elem_t*) CMODEL_MALLOC(sizeof(tag_elem_t));
+ e->id = id;
+ e->data = data;
+ return e;
+ }
+ @DefineFunc:
+ call_id_t get_id(void *wrapper) {
+ tag_elem_t *res = (tag_elem_t*) wrapper;
+ if (res == NULL) {
+ //model_print("wrong id here\n");
+ return 0;
+ }
+ return res->id;
+ }
+ @DefineFunc:
+ int get_data(void *wrapper) {
+ tag_elem_t *res = (tag_elem_t*) wrapper;
+ return res->data;
+ }
+ @Happens_before:
+ Push -> Steal
+ Push -> Take
+ @End
+*/
+
+
Deque * create();
-int take(Deque *q);
void resize(Deque *q);
+
+/**
+ @Begin
+ @Interface: Take
+ //@Commit_point_set: Take_Read_Bottom | Take_CAS_Top | Take_Additional_Point
+ @Commit_point_set: Take_Read_Bottom | Take_Additional_Point
+ @ID: __RET__ == EMPTY ? DEFAULT_CALL_ID : get_id(back(__deque))
+ @Action:
+ int _Old_Val = EMPTY;
+ if (__RET__ != EMPTY) {
+ if (size(__deque) > 0) {
+ _Old_Val = get_data(back(__deque));
+ pop_back(__deque);
+ }
+ }
+ @Post_check:
+ _Old_Val == __RET__
+ @End
+*/
+int take(Deque *q);
+
+/**
+ @Begin
+ @Interface: Push
+ @Commit_point_set: Push_Update_Bottom
+ @ID: get_and_inc(tag);
+ @Action:
+ tag_elem_t *elem = new_tag_elem(__ID__, x);
+ push_back(__deque, elem);
+ @End
+*/
void push(Deque *q, int x);
-#define EMPTY 0xffffffff
-#define ABORT 0xfffffffe
+/**
+ @Begin
+ @Interface: Steal
+ //@Commit_point_set: Steal_Read_Bottom | Steal_CAS_Top | Steal_Additional_Point
+ @Commit_point_set: Steal_Read_Bottom | Steal_Additional_Point
+ @ID: (__RET__ == EMPTY || __RET__ == ABORT) ? DEFAULT_CALL_ID : get_id(front(__deque))
+ @Action:
+ int _Old_Val = EMPTY;
+ if (__RET__ != EMPTY && __RET__ != ABORT) {
+ if (size(__deque) > 0) {
+ _Old_Val = get_data(front(__deque));
+ pop_front(__deque);
+ }
+ }
+ @Post_check:
+ _Old_Val == __RET__ || __RET__ == EMPTY || __RET__ == ABORT
+ @End
+*/
+int steal(Deque *q);
#endif