}
/**** detected UL ****/
atomic_store_explicit(&q->array, new_a, memory_order_release);
- printf("resize\n");
+ //printf("resize\n");
}
/**
int c;
static void task(void * param) {
- a=steal(q);
+ //a=steal(q);
a=steal(q);
}
b=take(q);
c=take(q);
thrd_join(t);
-
+/*
bool correct=true;
if (a!=1 && a!=2 && a!=4 && a!= EMPTY)
correct=false;
correct=false;
if (!correct)
printf("a=%d b=%d c=%d\n",a,b,c);
+ */
//MODEL_ASSERT(correct);
return 0;
}
kvs_data* resize(cliffc_hashtable *topmap, kvs_data *kvs) {
- model_print("resizing...\n");
+ //model_print("resizing...\n");
kvs_data *newkvs = _newkvs.load(memory_order_acquire);
if (newkvs != NULL)
return newkvs;
// Last check cause the 'new' below is expensive
newkvs = _newkvs.load(memory_order_acquire);
- model_print("hey1\n");
+ //model_print("hey1\n");
if (newkvs != NULL) return newkvs;
newkvs = new kvs_data(newsz);
void *chm = (void*) new CHM(sz);
- model_print("hey2\n");
+ //model_print("hey2\n");
newkvs->_data[0].store(chm, memory_order_relaxed);
kvs_data *cur_newkvs;
if (!passed) {
int old = _Old_Val == NULL ? 0 : _Old_Val->_val;
int ret = __RET__ == NULL ? 0 : __RET__->_val;
- model_print("Get: key: %d, _Old_Val: %d, RET: %d\n",
- key->_val, old, ret);
+ //model_print("Get: key: %d, _Old_Val: %d, RET: %d\n",
+ //key->_val, old, ret);
}
@Post_check:
//__RET__ == NULL ? true : equals_val(_Old_Val, __RET__)
if (!passed) {
int old = _Old_Val == NULL ? 0 : _Old_Val->_val;
int ret = __RET__ == NULL ? 0 : __RET__->_val;
- model_print("Put: key: %d, val: %d, _Old_Val: %d, RET: %d\n",
- key->_val, val->_val, old, ret);
+ //model_print("Put: key: %d, val: %d, _Old_Val: %d, RET: %d\n",
+ // key->_val, val->_val, old, ret);
}
@Post_check:
equals_val(__RET__, _Old_Val)
static inline bool CAS_val(kvs_data *kvs, int idx, void *expected, void
*desired) {
bool res = kvs->_data[2 * idx + 3].compare_exchange_strong(expected,
- desired, memory_order_release, memory_order_relaxed);
+ desired, memory_order_acq_rel, memory_order_relaxed);
/**
# If it is a successful put instead of a copy or any other internal
# operantions, expected != NULL
if (K == NULL) {
- model_print("Key is null\n");
+ //model_print("Key is null\n");
return NULL; // A miss
}
IntWrapper *v0, *v1, *v2, *v3, *v4, *v5;
void threadA(void *arg) {
- table->put(k1, v1);
+ table->put(k3, v3);
+ table->put(k1, v4);
//table->put(k2, v2);
//table->put(k3, v3);
/*
}
void threadB(void *arg) {
- table->put(k1, v1);
- table->put(k2, v4);
- table->put(k3, v3);
+ //table->put(k1, v1);
+ //table->put(k2, v4);
+ //table->put(k3, v3);
}
void threadMain(void *arg) {
val1 = table->get(k1);
- val2 = table->get(k2);
+ //val2 = table->get(k2);
+ /*
if (val1 != NULL)
model_print("val1: %d\n", val1->_val);
else
if (val2 != NULL)
model_print("val2: %d\n", val2->_val);
else
- model_print("val2: NULL\n");
+ model_print("val2: NULL\n");*/
}
int user_main(int argc, char *argv[]) {
v0 = new IntWrapper(2048);
table->put(k1, v0);
table->put(k2, v0);
- model_print("hey\n");
+ //model_print("hey\n");
thrd_create(&t1, threadA, NULL);
thrd_create(&t2, threadB, NULL);
threadMain(NULL);
//shared = 17;
mutex->unlock(&g);
mutex->lock(&g);
- printf("load: %u\n", load_32(&shared));
+ //printf("load: %u\n", load_32(&shared));
//printf("load: %u\n", shared);
}
void threadB(void *arg)
{
mcs_mutex::guard g(mutex);
- printf("load: %u\n", load_32(&shared));
+ //printf("load: %u\n", load_32(&shared));
//printf("load: %u\n", shared);
mutex->unlock(&g);
mutex->lock(&g);
- printf("store: %d\n", 17);
+ //printf("store: %d\n", 17);
//shared = 17;
store_32(&shared, 17);
}
// unlock of pred can see me in the tail before I fill next
// publish me to previous lock-holder :
- // FIXME: detection miss, don't think it's necessary
+ // FIXME: detection miss, execution never ends
+ // If this is relaxed, the store 0 to gate will be read before and
+ // that lock will never ends.
pred->next.store(me, std::mo_release );
- printf("lock_miss1\n");
+ //printf("lock_miss1\n");
// (*2) pred not touched any more
int my_gate = 1;
while (my_gate ) {
my_gate = me->gate.load(std::mo_acquire);
- if (my_gate == 0)
- printf("lock at gate!\n");
+ //if (my_gate == 0)
+ //printf("lock at gate!\n");
/**
@Begin
@Commit_point_define_check: my_gate == 0
void unlock(guard * I) {
mcs_node * me = &(I->m_node);
- // FIXME: detection miss, don't think it's necessary
+ // FIXME: detection miss, execution never ends
mcs_node * next = me->next.load(std::mo_acquire);
- printf("unlock_miss2\n");
+ //printf("unlock_miss2\n");
if ( next == NULL )
{
mcs_node * tail_was_me = me;
// (*1) catch the race :
rl::linear_backoff bo;
for(;;) {
- // FIXME: detection miss, don't think it's necessary
+ // FIXME: detection miss, execution never ends
next = me->next.load(std::mo_acquire);
- printf("unlock_miss3\n");
+ //printf("unlock_miss3\n");
if ( next != NULL )
break;
thrd_yield();
~spsc_queue()
{
- RL_ASSERT(head == tail);
+ //RL_ASSERT(head == tail);
delete ((node*)head($));
}
else
{
int d = q.dequeue();
- RL_ASSERT(11 == d);
+ //RL_ASSERT(11 == d);
}
}
};