lots of change and add notes

[cdsspec-compiler.git] / benchmark / ms-queue / my_queue.h

diff --git a/benchmark/ms-queue/my_queue.h b/benchmark/ms-queue/my_queue.h
index c92e420657c1847ec3575156be8e6a7b133e2dae..3a344d698337279597aff78b144b81c31858b9db 100644 (file)
--- a/benchmark/ms-queue/my_queue.h
+++ b/benchmark/ms-queue/my_queue.h
@@ -26,6 +26,61 @@ typedef struct {
 } queue_t;
 
 void init_queue(queue_t *q, int num_threads);
+
+/**
+       @Begin
+       @Global_define:
+               @DeclareVar:
+               typedef struct tag_elem {
+                       Tag id;
+                       unsigned int data;
+                       
+                       tag_elem(Tag _id, unsigned int _data) {
+                               id = _id;
+                               data = _data;
+                       }
+               } tag_elem_t;
+
+               spec_queue<tag_elem_t> queue;
+               Tag tag;
+               @InitVar:
+                       queue = spec_queue<tag_elem_t>();
+                       tag = Tag();
+       @Happens_before:
+               # Only check the happens-before relationship according to the id of the
+               # commit_point_set. For commit_point_set that has same ID, A -> B means
+               # B happens after the previous A.
+               Enqueue -> Dequeue
+       @End
+*/
+
+
+
+/**
+       @Begin
+       @Interface: Enqueue
+       @Commit_point_set: Enqueue_Success_Point
+       @ID: __sequential.tag.getCurAndInc()
+       @Action:
+               # __ID__ is an internal macro that refers to the id of the current
+               # interface call
+               @Code:
+               __sequential.queue.enqueue(tag_elem_t(__ID__, val));
+       @End
+*/
 void enqueue(queue_t *q, unsigned int val);
+
+/**
+       @Begin
+       @Interface: Dequeue
+       @Commit_point_set: Dequeue_Success_Point
+       @ID: __sequential.queue.peak().tag
+       @Action:
+               @Code:
+               unsigned int _Old_Val = __sequential.queue.dequeue().data;
+       @Post_check:
+               _Old_Val == __RET__
+       @End
+*/
 unsigned int dequeue(queue_t *q);
 int get_thread_num();