~spsc_queue()
{
//RL_ASSERT(head == tail);
- delete ((node*)head($));
+ //delete ((node*)head($));
+ delete ((node*)head);
}
/**
LANG = CPP;
CLASS = spsc_queue;
@Global_define:
- @DeclareStruct:
- typedef struct tag_elem {
- call_id_t id;
- T data;
- } tag_elem_t;
-
@DeclareVar:
- spec_list *__queue;
- id_tag_t *tag;
+ IntegerList *__queue;
@InitVar:
- __queue = new_spec_list();
- tag = new_id_tag();
- @DefineFunc:
- tag_elem_t* new_tag_elem(call_id_t id, T data) {
- tag_elem_t *e = (tag_elem_t*) MODEL_MALLOC(sizeof(tag_elem_t));
- e->id = id;
- e->data = data;
- return e;
- }
- @DefineFunc:
- call_id_t get_id(void *wrapper) {
- return ((tag_elem_t*) wrapper)->id;
- }
- @DefineFunc:
- unsigned int get_data(void *wrapper) {
- return ((tag_elem_t*) wrapper)->data;
- }
- @Happens_before: Enqueue -> Dequeue
+ __queue = createIntegerList();
+ @Finalize:
+ if (__queue)
+ destroyIntegerList(__queue);
+ return true;
+ @Happens_before: Enqueue -> Dequeue
+ @Commutativity: Enqueue <-> Dequeue: true
+ @Commutativity: Dequeue <-> Dequeue: !_Method1.__RET__ || !_Method2.__RET__
+
@End
*/
@Begin
@Interface: Enqueue
@Commit_point_set: Enqueue_Point
- @ID: get_and_inc(tag)
- @Action: push_back(__queue, new_tag_elem(__ID__, data));
- //tag_elem_t *elem = new_tag_elem(__ID__, data);
- //push_back(__queue, elem);
+ @ID: data
+ @Action:
+ push_back(__queue, data);
+ //model_print("Enqueue: val=%d\n", val);
@End
*/
void enqueue(T data)
{
node* n = new node (data);
- head($)->next.store(n, std::memory_order_release);
+ /********** DR & SPEC (sequential) **********/
+ //head($)->next.store(n, std::memory_order_release);
+ head->next.store(n, std::memory_order_release);
/**
@Begin
@Commit_point_define_check: true
@Begin
@Interface: Dequeue
@Commit_point_set: Dequeue_Point
- @ID: get_id(front(__queue))
+ @ID: __RET__ ? __RET__ : 0
@Action:
- T _Old_Val = get_data(front(__queue));
- pop_front(__queue);
- @Post_check: _Old_Val == __RET__
+ int elem = 0;
+ if (__RET__) {
+ elem = front(__queue);
+ pop_front(__queue);
+ }
+ //model_print("Dequeue: __RET__=%d, retVal=%d, elem=%d, \n", __RET__, *retVal, elem);
+ //model_print("Result: %d\n", __RET__ ? *retVal == elem : true);
+ @Post_check: __RET__ ? __RET__ == elem : true
@End
*/
T dequeue()
struct node
{
std::atomic<node*> next;
- rl::var<T> data;
+ //rl::var<T> data;
+ T data;
node(T data = T())
: data(data)
}
};
- rl::var<node*> head;
- rl::var<node*> tail;
+ //rl::var<node*> head;
+ //rl::var<node*> tail;
+ node *head;
+ node *tail;
+
+
eventcount ec;
T try_dequeue()
{
- node* t = tail($);
+ //node* t = tail($);
+ node *t = tail;
+ /********** DR & SPEC (sequential) **********/
node* n = t->next.load(std::memory_order_acquire);
/**
@Begin
*/
if (0 == n)
return 0;
- T data = n->data($);
+ //T data = n->data($);
+ T data = n->data;
delete (t);
tail = n;
return data;