projects
/
cdsspec-compiler.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
changes
[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 d4999299351daa98109cf96b938cce0cdfeb1fd7..0768428df5d9fadc1a1b29195b3de2c94068e87b 100644
(file)
--- a/
benchmark/ms-queue/my_queue.h
+++ b/
benchmark/ms-queue/my_queue.h
@@
-3,6
+3,13
@@
#include <stdatomic.h>
#include <stdatomic.h>
+#include <spec_lib.h>
+#include <stdlib.h>
+#include <cdsannotate.h>
+#include <specannotation.h>
+#include <model_memory.h>
+#include "common.h"
+
#define MAX_NODES 0xf
typedef unsigned long long pointer;
#define MAX_NODES 0xf
typedef unsigned long long pointer;
@@
-32,6
+39,8
@@
void init_queue(queue_t *q, int num_threads);
/**
@Begin
/**
@Begin
+ @Options:
+ LANG = C;
@Global_define:
@DeclareStruct:
typedef struct tag_elem {
@Global_define:
@DeclareStruct:
typedef struct tag_elem {
@@
-47,7
+56,7
@@
void init_queue(queue_t *q, int num_threads);
tag = new_id_tag(); // Beginning of available id
@DefineFunc:
tag_elem_t* new_tag_elem(call_id_t id, unsigned int data) {
tag = new_id_tag(); // Beginning of available id
@DefineFunc:
tag_elem_t* new_tag_elem(call_id_t id, unsigned int data) {
- tag_elem_t *e = (tag_elem_t*) MODEL_MALLOC(sizeof(tag_elem_t));
+ tag_elem_t *e = (tag_elem_t*)
C
MODEL_MALLOC(sizeof(tag_elem_t));
e->id = id;
e->data = data;
return e;
e->id = id;
e->data = data;
return e;
@@
-58,6
+67,8
@@
void init_queue(queue_t *q, int num_threads);
}
@DefineFunc:
call_id_t get_id(void *wrapper) {
}
@DefineFunc:
call_id_t get_id(void *wrapper) {
+ if (wrapper == NULL)
+ return 0;
return ((tag_elem_t*) wrapper)->id;
}
@DefineFunc:
return ((tag_elem_t*) wrapper)->id;
}
@DefineFunc:
@@
-77,13
+88,14
@@
void init_queue(queue_t *q, int num_threads);
/**
@Begin
@Interface: Enqueue
/**
@Begin
@Interface: Enqueue
- @Commit_point_set: Enqueue_
Success_Poin
t
- @ID: get_and_inc(tag)
;
+ @Commit_point_set: Enqueue_
Read_Tail | Enqueue_UpdateNex
t
+ @ID: get_and_inc(tag)
@Action:
# __ID__ is an internal macro that refers to the id of the current
# interface call
tag_elem_t *elem = new_tag_elem(__ID__, val);
push_back(__queue, elem);
@Action:
# __ID__ is an internal macro that refers to the id of the current
# interface call
tag_elem_t *elem = new_tag_elem(__ID__, val);
push_back(__queue, elem);
+ //model_print("Enqueue: input=%d\n", val);
@End
*/
void enqueue(queue_t *q, unsigned int val);
@End
*/
void enqueue(queue_t *q, unsigned int val);
@@
-91,16
+103,20
@@
void enqueue(queue_t *q, unsigned int val);
/**
@Begin
@Interface: Dequeue
/**
@Begin
@Interface: Dequeue
- @Commit_point_set: Dequeue_
Success_Point | Dequeue_Empty_Poin
t
- @ID: get_id(
back
(__queue))
+ @Commit_point_set: Dequeue_
Read_Head | Dequeue_Read_Tail | Dequeue_LoadNex
t
+ @ID: get_id(
front
(__queue))
@Action:
@Action:
- unsigned int _Old_Val = get_data(front(__queue));
- pop_front(__queue);
+ unsigned int _Old_Val = 0;
+ if (size(__queue) > 0) {
+ _Old_Val = get_data(front(__queue));
+ pop_front(__queue);
+ }
+ // model_print("Dequeue: __RET__=%d, retVal=%d, Old_Val=%d\n", __RET__, *retVal, _Old_Val);
@Post_check:
@Post_check:
- _Old_Val ==
__RET__
+ _Old_Val ==
0 ? !__RET__ : _Old_Val == *retVal
@End
*/
@End
*/
-
unsigned int dequeue(queue_t *q
);
+
bool dequeue(queue_t *q, int *retVal
);
int get_thread_num();
#endif
int get_thread_num();
#endif