+++ /dev/null
-#ifndef _QUEUE_H
-#define _QUEUE_H
-
-#include <unrelacy.h>
-#include <atomic>
-
-#include <spec_lib.h>
-#include <stdlib.h>
-#include <cdsannotate.h>
-#include <specannotation.h>
-#include <model_memory.h>
-#include "common.h"
-
-#include "eventcount.h"
-
-/**
- @Begin
- @Class_begin
- @End
-*/
-template<typename T>
-class spsc_queue
-{
-
-public:
-
-
- spsc_queue()
- {
-
- /**
- @Begin
- @Entry_point
- @End
- */
-
- node* n = new node ();
- head = n;
- tail = n;
- }
-
- ~spsc_queue()
- {
- //RL_ASSERT(head == tail);
- //delete ((node*)head($));
- delete ((node*)head);
- }
-
- /**
- @Begin
- @Options:
- LANG = CPP;
- CLASS = spsc_queue;
- @Global_define:
- @DeclareVar:
- IntegerList *__queue;
- @InitVar:
- __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: data
- @Action:
- push_back(__queue, data);
- //model_print("Enqueue: val=%d\n", val);
- @End
- */
- void enqueue(T data)
- {
- node* n = new node (data);
- /********** 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
- @Label: Enqueue_Point
- @End
- */
- head = n;
- // #Mark delete this
- ec.signal();
- }
- /**
- @Begin
- @Interface: Dequeue
- @Commit_point_set: Dequeue_Point
- @ID: __RET__ ? __RET__ : 0
- @Action:
- 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()
- {
- T data = try_dequeue();
- while (0 == data)
- {
- int cmp = ec.get();
- data = try_dequeue();
- if (data)
- break;
- ec.wait(cmp);
- data = try_dequeue();
- if (data)
- break;
- }
- return data;
- }
-
-private:
- struct node
- {
- std::atomic<node*> next;
- //rl::var<T> data;
- T data;
-
- node(T data = T())
- : data(data)
- {
- next = 0;
- }
- };
-
- //rl::var<node*> head;
- //rl::var<node*> tail;
- node *head;
- node *tail;
-
-
-
- eventcount ec;
-
- T try_dequeue()
- {
- //node* t = tail($);
- node *t = tail;
- /********** DR & SPEC (sequential) **********/
- node* n = t->next.load(std::memory_order_acquire);
- /**
- @Begin
- @Commit_point_define_check: n != 0
- @Label: Dequeue_Point
- @End
- */
- if (0 == n)
- return 0;
- //T data = n->data($);
- T data = n->data;
- delete (t);
- tail = n;
- return data;
- }
-};
-/**
- @Begin
- @Class_end
- @End
-*/
-
-#endif