projects
/
cdsspec-compiler.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
minor fix
[cdsspec-compiler.git]
/
benchmark
/
read-copy-update
/
rcu.cc
diff --git
a/benchmark/read-copy-update/rcu.cc
b/benchmark/read-copy-update/rcu.cc
index ebe36a9f1a3fc924f0895f3b08c158cb6cc602ce..6f791263c677abb002629a5c68c68afd9ccf3ba7 100644
(file)
--- a/
benchmark/read-copy-update/rcu.cc
+++ b/
benchmark/read-copy-update/rcu.cc
@@
-4,6
+4,13
@@
#include <stdlib.h>
#include <stdio.h>
#include <stdlib.h>
#include <stdio.h>
+#include <spec_lib.h>
+#include <stdlib.h>
+#include <cdsannotate.h>
+#include <specannotation.h>
+#include <model_memory.h>
+#include "common.h"
+
#include "librace.h"
/**
#include "librace.h"
/**
@@
-29,13
+36,14
@@
atomic<Data*> data;
@DefineFunc:
bool equals(Data *ptr1, Data *ptr2) {
@DefineFunc:
bool equals(Data *ptr1, Data *ptr2) {
- if (ptr1->data1 == ptr2->data1
- && ptr1->data2 == ptr2->data2
- && ptr1->data3 == ptr2->data3) {
- return true;
- } else {
- return false;
- }
+ //if (ptr1->data1 == ptr2->data1
+ // && ptr1->data2 == ptr2->data2
+ // && ptr1->data3 == ptr2->data3) {
+ // return true;
+ //} else {
+ // return false;
+ //}
+ return ptr1 == ptr2;
}
@Happens_before:
}
@Happens_before:
@@
-62,6
+70,7
@@
Data* read() {
@Label: Read_Success_Point
@End
*/
@Label: Read_Success_Point
@End
*/
+ //model_print("Read: %d\n", res);
return res;
}
return res;
}
@@
-74,20
+83,19
@@
Data* read() {
@End
*/
void write(Data *new_data) {
@End
*/
void write(Data *new_data) {
- while (true) {
- Data *prev = data.load(memory_order_relaxed);
- bool succ = data.compare_exchange_strong(prev, new_data,
+ Data *prev = data.load(memory_order_relaxed);
+ bool succ = false;
+ do {
+ succ = data.compare_exchange_strong(prev, new_data,
memory_order_release, memory_order_relaxed);
/**
@Begin
memory_order_release, memory_order_relaxed);
/**
@Begin
- @Commit_point_define_check: succ
== true
+ @Commit_point_define_check: succ
@Label: Write_Success_Point
@End
*/
@Label: Write_Success_Point
@End
*/
- if (succ) {
- break;
- }
- }
+ } while (!succ);
+ //model_print("Write: %d\n", new_data);
}
void threadA(void *arg) {
}
void threadA(void *arg) {
@@
-130,19
+138,19
@@
int user_main(int argc, char **argv) {
thrd_t t1, t2, t3, t4;
data.store(NULL, memory_order_relaxed);
Data *data_init = (Data*) malloc(sizeof(Data));
thrd_t t1, t2, t3, t4;
data.store(NULL, memory_order_relaxed);
Data *data_init = (Data*) malloc(sizeof(Data));
- data_init->data1 =
1
;
- data_init->data2 =
2
;
- data_init->data3 =
3
;
+ data_init->data1 =
0
;
+ data_init->data2 =
0
;
+ data_init->data3 =
0
;
write(data_init);
thrd_create(&t1, threadA, NULL);
thrd_create(&t2, threadB, NULL);
write(data_init);
thrd_create(&t1, threadA, NULL);
thrd_create(&t2, threadB, NULL);
-
//
thrd_create(&t3, threadC, NULL);
+ thrd_create(&t3, threadC, NULL);
thrd_create(&t4, threadD, NULL);
thrd_join(t1);
thrd_join(t2);
thrd_create(&t4, threadD, NULL);
thrd_join(t1);
thrd_join(t2);
-
//
thrd_join(t3);
+ thrd_join(t3);
thrd_join(t4);
return 0;
thrd_join(t4);
return 0;