projects
/
model-checker-benchmarks.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
add another testcase for dekker-fences
[model-checker-benchmarks.git]
/
mcs-lock
/
testcase1.cc
diff --git
a/mcs-lock/testcase1.cc
b/mcs-lock/testcase1.cc
index 971bf1d591f5314c0236b911bd6749fcf4af8426..461f5b1a6ee1aa9026e920608a81ff81d82225e2 100644
(file)
--- a/
mcs-lock/testcase1.cc
+++ b/
mcs-lock/testcase1.cc
@@
-7,25
+7,29
@@
#include "librace.h"
struct mcs_mutex *mutex;
#include "librace.h"
struct mcs_mutex *mutex;
-static
uint32_
t shared;
+static
atomic_in
t shared;
void threadA(void *arg)
{
mcs_mutex::guard g(mutex);
printf("store: %d\n", 17);
void threadA(void *arg)
{
mcs_mutex::guard g(mutex);
printf("store: %d\n", 17);
- store_32(&shared, 17);
+ //store_32(&shared, 17);
+ atomic_store_explicit(&shared, 17, relaxed);
mutex->unlock(&g);
mutex->lock(&g);
mutex->unlock(&g);
mutex->lock(&g);
- printf("load: %u\n", load_32(&shared));
+ //printf("load: %u\n", load_32(&shared));
+ atomic_load_explicit(&shared, relaxed);
}
void threadB(void *arg)
{
mcs_mutex::guard g(mutex);
}
void threadB(void *arg)
{
mcs_mutex::guard g(mutex);
- printf("load: %u\n", load_32(&shared));
+ //printf("load: %u\n", load_32(&shared));
+ atomic_load_explicit(&shared, relaxed);
mutex->unlock(&g);
mutex->lock(&g);
mutex->unlock(&g);
mutex->lock(&g);
- printf("store: %d\n", 17);
+ atomic_store_explicit(&shared, 17, relaxed);
+ //printf("store: %d\n", 17);
store_32(&shared, 17);
}
store_32(&shared, 17);
}