projects
/
cdsspec-compiler.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
da4f565
)
new rcu
author
Peizhao Ou
<peizhaoo@uci.edu>
Thu, 20 Mar 2014 22:07:24 +0000
(15:07 -0700)
committer
Peizhao Ou
<peizhaoo@uci.edu>
Thu, 20 Mar 2014 22:07:24 +0000
(15:07 -0700)
benchmark/read-copy-update/rcu.cc
patch
|
blob
|
history
diff --git
a/benchmark/read-copy-update/rcu.cc
b/benchmark/read-copy-update/rcu.cc
index 34deba7e857aca5c85c8705a80d49e98e2d0791e..44ce9862bd7cc713fd0fdbc60f9b57be7f26e416 100644
(file)
--- a/
benchmark/read-copy-update/rcu.cc
+++ b/
benchmark/read-copy-update/rcu.cc
@@
-46,9
+46,14
@@
atomic<Data*> data;
return ptr1 == ptr2;
}
return ptr1 == ptr2;
}
+ bool isOriginalRead(Data *ptr) {
+ return ptr->data1 == 0 &&
+ ptr->data2 == 0 && ptr->data3 == 0;
+ }
+
@Happens_before:
Write -> Read
@Happens_before:
Write -> Read
- Write -> Write
+
//
Write -> Write
@End
*/
@End
*/
@@
-56,10
+61,11
@@
atomic<Data*> data;
@Begin
@Interface: Read
@Commit_point_set: Read_Success_Point
@Begin
@Interface: Read
@Commit_point_set: Read_Success_Point
+ //@ID: isOriginalRead(__RET__) ? 1 : DEFAULT_CALL_ID
@Action:
Data *_Old_Data = _cur_data;
@Post_check:
@Action:
Data *_Old_Data = _cur_data;
@Post_check:
- equals(__RET__, _Old_Data)
+ _Old_Data = __RET__
@End
*/
Data* read() {
@End
*/
Data* read() {
@@
-70,7
+76,7
@@
Data* read() {
@Label: Read_Success_Point
@End
*/
@Label: Read_Success_Point
@End
*/
- //model_print("Read: %d
\n", res
);
+ //model_print("Read: %d
, %d, %d\n", res->data1, res->data2, res->data3
);
return res;
}
return res;
}
@@
-79,15
+85,29
@@
Data* read() {
@Interface: Write
@Commit_point_set: Write_Success_Point
@Action:
@Interface: Write
@Commit_point_set: Write_Success_Point
@Action:
- _cur_data = new_data;
+ Data *_Old_data = _cur_data;
+ _cur_data = __RET__;
+ @Post_check:
+ _Old_data == NULL ?
+ (__RET__->data1 == d1 &&
+ __RET__->data2 == d2 &&
+ __RET__->data3 == d3)
+ :
+ (__RET__->data1 == _Old_data->data1 + d1 &&
+ __RET__->data2 == _Old_data->data2 + d2 &&
+ __RET__->data3 == _Old_data->data3 + d3)
@End
*/
@End
*/
-
void write(Data *new_data
) {
- Data *prev = data.load(memory_order_
relaxed
);
+
Data* write(int d1, int d2, int d3
) {
+ Data *prev = data.load(memory_order_
acquire
);
bool succ = false;
bool succ = false;
+ Data *tmp = (Data*) malloc(sizeof(Data));
do {
do {
- succ = data.compare_exchange_strong(prev, new_data,
- memory_order_acq_rel, memory_order_relaxed);
+ tmp->data1 = prev->data1 + d1;
+ tmp->data2 = prev->data2 + d2;
+ tmp->data3 = prev->data3 + d3;
+ succ = data.compare_exchange_strong(prev, tmp,
+ memory_order_release, memory_order_acquire);
/**
@Begin
@Commit_point_define_check: succ
/**
@Begin
@Commit_point_define_check: succ
@@
-95,52
+115,25
@@
void write(Data *new_data) {
@End
*/
} while (!succ);
@End
*/
} while (!succ);
- //model_print("Write: %d\n", new_data);
+ //model_print("Write: %d, %d, %d\n", tmp->data1, tmp->data2, tmp->data3);
+ return tmp;
}
}
-/*
-Data *prev = data.load(memory_order_acquire);
-bool succ = false;
-Data *tmp = malloc(sizeof(Data));
-do {
- tmp->data1=prev->data1+new_data->data1;
- tmp->data2=prev->data2+new_data->data2;
- tmp->data3=prev->data3+new_data->data3;
- succ = data.compare_exchange_strong(prev, tmp,
- memory_order_release, memory_order_acquire);
- } while (!succ);
- //model_print("Write: %d\n", new_data);
-}
-*/
void threadA(void *arg) {
void threadA(void *arg) {
- Data *dataA = (Data*) malloc(sizeof(Data));
- dataA->data1 = 3;
- dataA->data2 = 2;
- dataA->data3 = 1;
- write(dataA);
+ write(1, 0, 0);
}
void threadB(void *arg) {
}
void threadB(void *arg) {
- Data *dataB = read();
- printf("ThreadB data1: %d\n", dataB->data1);
- printf("ThreadB data2: %d\n", dataB->data2);
- printf("ThreadB data3: %d\n", dataB->data3);
+ write(0, 1, 0);
}
void threadC(void *arg) {
}
void threadC(void *arg) {
- Data *dataC = read();
- printf("ThreadC data1: %d\n", dataC->data1);
- printf("ThreadC data2: %d\n", dataC->data2);
- printf("ThreadC data3: %d\n", dataC->data3);
+ write(0, 0, 1);
}
void threadD(void *arg) {
}
void threadD(void *arg) {
- Data *dataD = (Data*) malloc(sizeof(Data));
- dataD->data1 = -3;
- dataD->data2 = -2;
- dataD->data3 = -1;
- write(dataD);
+ Data *dataC = read();
}
int user_main(int argc, char **argv) {
}
int user_main(int argc, char **argv) {
@@
-151,21
+144,21
@@
int user_main(int argc, char **argv) {
*/
thrd_t t1, t2, t3, t4;
*/
thrd_t t1, t2, t3, t4;
-
data.store(NULL, memory_order_relaxed
);
-
Data *data_init = (Data*) malloc(sizeof(Data))
;
- data
_init->data1
= 0;
- data
_init->data2
= 0;
-
data_init->data3 = 0
;
-
write(data_init
);
+
Data *dataInit = (Data*) malloc(sizeof(Data)
);
+
dataInit->data1 = 0
;
+ data
Init->data2
= 0;
+ data
Init->data3
= 0;
+
atomic_init(&data, dataInit)
;
+
//write(0, 0, 0
);
thrd_create(&t1, threadA, NULL);
thrd_create(&t2, threadB, NULL);
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;