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 ff3d42d4697354fa96985e9f457425a1957d3fdc..90f57755d74dfe261330c73ef77139a10533ced6 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;
@@
-60,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:
@@
-79,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);
@@
-93,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