projects
/
cdsspec-compiler.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
edits
[cdsspec-compiler.git]
/
benchmark
/
spsc-bugfix
/
queue.h
diff --git
a/benchmark/spsc-bugfix/queue.h
b/benchmark/spsc-bugfix/queue.h
index 8ff765e66cf0d95ab34227f22ab06053eed36f04..67be1b7723489a3950f6c8585b44c2a59d8f66da 100644
(file)
--- a/
benchmark/spsc-bugfix/queue.h
+++ b/
benchmark/spsc-bugfix/queue.h
@@
-4,6
+4,13
@@
#include <unrelacy.h>
#include <atomic>
#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"
/**
#include "eventcount.h"
/**
@@
-34,7
+41,7
@@
public:
~spsc_queue()
{
~spsc_queue()
{
- RL_ASSERT(head == tail);
+
//
RL_ASSERT(head == tail);
delete ((node*)head($));
}
delete ((node*)head($));
}
@@
-71,8
+78,7
@@
public:
unsigned int get_data(void *wrapper) {
return ((tag_elem_t*) wrapper)->data;
}
unsigned int get_data(void *wrapper) {
return ((tag_elem_t*) wrapper)->data;
}
- @Happens_before:
- Enqueue -> Dequeue
+ @Happens_before: Enqueue -> Dequeue
@End
*/
@End
*/
@@
-82,9
+88,9
@@
public:
@Interface: Enqueue
@Commit_point_set: Enqueue_Point
@ID: get_and_inc(tag)
@Interface: Enqueue
@Commit_point_set: Enqueue_Point
@ID: get_and_inc(tag)
- @Action:
- tag_elem_t *elem = new_tag_elem(__ID__, data);
- push_back(__queue, elem);
+ @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)
@End
*/
void enqueue(T data)
@@
-109,8
+115,7
@@
public:
@Action:
T _Old_Val = get_data(front(__queue));
pop_front(__queue);
@Action:
T _Old_Val = get_data(front(__queue));
pop_front(__queue);
- @Post_check:
- _Old_Val == __RET__
+ @Post_check: _Old_Val == __RET__
@End
*/
T dequeue()
@End
*/
T dequeue()