projects
/
model-checker-benchmarks.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
deque: fix bugs in assertion code and move up 3 variables...
[model-checker-benchmarks.git]
/
mcs-lock
/
mcs-lock.h
diff --git
a/mcs-lock/mcs-lock.h
b/mcs-lock/mcs-lock.h
index df64d8b999c050688f08cea52c7a8a1dd540406b..2d39f2f6cab8d2aa5b10f5cd6e1b9092a818955e 100644
(file)
--- a/
mcs-lock/mcs-lock.h
+++ b/
mcs-lock/mcs-lock.h
@@
-1,12
+1,15
@@
// mcs on stack
// mcs on stack
+#include <stdatomic.h>
+#include <unrelacy.h>
+
struct mcs_node {
std::atomic<mcs_node *> next;
std::atomic<int> gate;
mcs_node() {
struct mcs_node {
std::atomic<mcs_node *> next;
std::atomic<int> gate;
mcs_node() {
- next
($)
.store(0);
- gate
($)
.store(0);
+ next.store(0);
+ gate.store(0);
}
};
}
};
@@
-16,10
+19,10
@@
public:
std::atomic<mcs_node *> m_tail;
mcs_mutex() {
std::atomic<mcs_node *> m_tail;
mcs_mutex() {
- m_tail
($)
.store( NULL );
+ m_tail.store( NULL );
}
~mcs_mutex() {
}
~mcs_mutex() {
- ASSERT( m_tail
($)
.load() == NULL );
+ ASSERT( m_tail.load() == NULL );
}
class guard {
}
class guard {
@@
-36,25
+39,25
@@
public:
// set up my node :
// not published yet so relaxed :
// set up my node :
// not published yet so relaxed :
- me->next
($)
.store(NULL, std::mo_relaxed );
- me->gate
($)
.store(1, std::mo_relaxed );
+ me->next.store(NULL, std::mo_relaxed );
+ me->gate.store(1, std::mo_relaxed );
// publish my node as the new tail :
// publish my node as the new tail :
- mcs_node * pred = m_tail
($)
.exchange(me, std::mo_acq_rel);
+ mcs_node * pred = m_tail.exchange(me, std::mo_acq_rel);
if ( pred != NULL ) {
// (*1) race here
// unlock of pred can see me in the tail before I fill next
// publish me to previous lock-holder :
if ( pred != NULL ) {
// (*1) race here
// unlock of pred can see me in the tail before I fill next
// publish me to previous lock-holder :
- pred->next
($)
.store(me, std::mo_release );
+ pred->next.store(me, std::mo_release );
// (*2) pred not touched any more
// now this is the spin -
// wait on predecessor setting my flag -
rl::linear_backoff bo;
// (*2) pred not touched any more
// now this is the spin -
// wait on predecessor setting my flag -
rl::linear_backoff bo;
- while ( me->gate
($)
.load(std::mo_acquire) ) {
- bo.yield(
$
);
+ while ( me->gate.load(std::mo_acquire) ) {
+ bo.yield();
}
}
}
}
}
}
@@
-62,11
+65,11
@@
public:
void unlock(guard * I) {
mcs_node * me = &(I->m_node);
void unlock(guard * I) {
mcs_node * me = &(I->m_node);
- mcs_node * next = me->next
($)
.load(std::mo_acquire);
+ mcs_node * next = me->next.load(std::mo_acquire);
if ( next == NULL )
{
mcs_node * tail_was_me = me;
if ( next == NULL )
{
mcs_node * tail_was_me = me;
- if ( m_tail
($)
.compare_exchange_strong( tail_was_me,NULL,std::mo_acq_rel) ) {
+ if ( m_tail.compare_exchange_strong( tail_was_me,NULL,std::mo_acq_rel) ) {
// got null in tail, mutex is unlocked
return;
}
// got null in tail, mutex is unlocked
return;
}
@@
-74,10
+77,10
@@
public:
// (*1) catch the race :
rl::linear_backoff bo;
for(;;) {
// (*1) catch the race :
rl::linear_backoff bo;
for(;;) {
- next = me->next
($)
.load(std::mo_acquire);
+ next = me->next.load(std::mo_acquire);
if ( next != NULL )
break;
if ( next != NULL )
break;
- bo.yield(
$
);
+ bo.yield();
}
}
}
}
@@
-85,6
+88,6
@@
public:
// so no locker can be viewing my node any more
// let next guy in :
// so no locker can be viewing my node any more
// let next guy in :
- next->gate
($)
.store( 0, std::mo_release );
+ next->gate.store( 0, std::mo_release );
}
};
}
};