try to generate in-place code

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

diff --git a/benchmark/ms-queue/my_queue.c b/benchmark/ms-queue/my_queue.c
index fc8e02abb28e05ae79bdf09958ad7cca5635935e..6a2737f91825a9bdcee355027f6baad9135ea826 100644 (file)
--- a/benchmark/ms-queue/my_queue.c
+++ b/benchmark/ms-queue/my_queue.c
@@ -79,6 +79,7 @@ void init_queue(queue_t *q, int num_threads)
 /**
        @Begin
        @Global_define:
+               @DeclareVar:
                typedef struct tag_elem {
                        Tag id;
                        unsigned int data;
@@ -89,8 +90,11 @@ void init_queue(queue_t *q, int num_threads)
                        }
                } tag_elem_t;
 
-               spec_queue<tag_elem_t> __queue;
-               Tag __tag;
+               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
@@ -103,12 +107,12 @@ void init_queue(queue_t *q, int num_threads)
        @Begin
        @Interface: Enqueue
        @Commit_point_set: Enqueue_Success_Point
-       @ID: __tag.getCurAndInc()
+       @ID: __sequential.tag.getCurAndInc()
        @Action:
                # __ID__ is an internal macro that refers to the id of the current
                # interface call
                @Code:
-               __queue.enqueue(tag_elem_t(__ID__, val));
+               __sequential.queue.enqueue(tag_elem_t(__ID__, val));
        @End
 */
 void enqueue(queue_t *q, unsigned int val)
@@ -165,10 +169,10 @@ void enqueue(queue_t *q, unsigned int val)
        @Begin
        @Interface: Dequeue
        @Commit_point_set: Dequeue_Success_Point
-       @ID: __queue.peak().tag
+       @ID: __sequential.queue.peak().tag
        @Action:
                @Code:
-               unsigned int _Old_Val = __queue.dequeue().data;
+               unsigned int _Old_Val = __sequential.queue.dequeue().data;
        @Post_check:
                _Old_Val == __RET__
        @End