+#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
{
- /**
- @Begin
- @Global_define:
- typedef struct tag_elem {
- Tag id;
- T data;
- } tag_elem_t;
-
- Tag tag;
- spec_queue<tag_elem> __queue;
-
- static bool _is_elem_equals(void *ptr1, void *ptr2) {
- // ...
- // return if the elements pointed to are equal
- }
-
- @Happens-before:
- Enqueue -> Dequeue
- @End
- **/
+
public:
+
+
spsc_queue()
{
+
+ /**
+ @Begin
+ @Entry_point
+ @End
+ */
+
node* n = new node ();
head = n;
tail = n;
~spsc_queue()
{
- RL_ASSERT(head == tail);
+ //RL_ASSERT(head == tail);
delete ((node*)head($));
}
+
+ /**
+ @Begin
+ @Options:
+ 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;
+ @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
+ @End
+ */
+
/**
@Begin
- @Commit_point_set:
- Enqueue = Enqueue_Success_Point
- @ID: tag.current()
- @Action:
- __queue.enqueue(tag_elem_t(tag.current(), node(data));
- tag.next();
+ @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);
@End
*/
void enqueue(T data)
head($)->next.store(n, std::memory_order_release);
/**
@Begin
- @Commit_point_define: true
- @Label: Enqueue_Success_Point
+ @Commit_point_define_check: true
+ @Label: Enqueue_Point
@End
*/
head = n;
// #Mark delete this
ec.signal();
}
-
/**
@Begin
- @Commit_point_set:
- Dequeue = Try_Dequeue_Success_Point
- @ID: __queue.peak().tag
- @Check: __queue.size() > 0 && _is_elem_equals(&RET, &__queue.peek().data)
- @Action: __queue.dequeue();
+ @Interface: Dequeue
+ @Commit_point_set: Dequeue_Point
+ @ID: get_id(front(__queue))
+ @Action:
+ T _Old_Val = get_data(front(__queue));
+ pop_front(__queue);
+ @Post_check: _Old_Val == __RET__
@End
*/
T dequeue()
node* n = t->next.load(std::memory_order_acquire);
/**
@Begin
- @Commit_point_define: ATOMIC_RET != NULL
- @Label: Try_Dequeue_Success_Point
+ @Commit_point_define_check: n != 0
+ @Label: Dequeue_Point
@End
*/
if (0 == n)
return data;
}
};
+/**
+ @Begin
+ @Class_end
+ @End
+*/
+
+#endif