size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed) - 1;
Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
atomic_store_explicit(&q->bottom, b, memory_order_relaxed);
+ /**** detected correctness ****/
atomic_thread_fence(memory_order_seq_cst);
size_t t = atomic_load_explicit(&q->top, memory_order_relaxed);
/**
for(i=top; i < bottom; i++) {
atomic_store_explicit(&new_a->buffer[i % new_size], atomic_load_explicit(&a->buffer[i % size], memory_order_relaxed), memory_order_relaxed);
}
- /**** FIXME: detected failure ****/
+ /**** detected UL ****/
atomic_store_explicit(&q->array, new_a, memory_order_release);
printf("resize\n");
}
*/
void push(Deque *q, int x) {
size_t b = atomic_load_explicit(&q->bottom, memory_order_relaxed);
- /**** FIXME: detected correctness ****/
+ /**** detected correctness ****/
size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_relaxed);
if (b - t > atomic_load_explicit(&a->size, memory_order_relaxed) - 1) /* Full queue. */ {
@Label: Push_Point
@End
*/
+ /**** correctness error ****/
atomic_thread_fence(memory_order_release);
atomic_store_explicit(&q->bottom, b + 1, memory_order_relaxed);
int steal(Deque *q) {
//FIXME: weaken the following acquire causes no spec problem
size_t t = atomic_load_explicit(&q->top, memory_order_acquire);
+ //FIXME: remove the fence causes no error and fewer executions..
atomic_thread_fence(memory_order_seq_cst);
+ /**** detected UL ****/
size_t b = atomic_load_explicit(&q->bottom, memory_order_acquire);
/**
@Begin
int x = EMPTY;
if (t < b) {
/* Non-empty queue. */
+ /**** detected UL ****/
Array *a = (Array *) atomic_load_explicit(&q->array, memory_order_acquire);
int size = atomic_load_explicit(&a->size, memory_order_relaxed);
x = atomic_load_explicit(&a->buffer[t % size], memory_order_relaxed);
@Label: Potential_Steal
@End
*/
-
+ /**** detected correctness failure ****/
bool succ = atomic_compare_exchange_strong_explicit(&q->top, &t, t + 1,
memory_order_seq_cst, memory_order_relaxed);
/**
}
@DefineFunc:
call_id_t get_id(void *wrapper) {
- return ((tag_elem_t*) wrapper)->id;
+ tag_elem_t *res = (tag_elem_t*) wrapper;
+ if (res == NULL) {
+ //model_print("wrong id here\n");
+ return 0;
+ }
+ return res->id;
}
@DefineFunc:
int get_data(void *wrapper) {
- return ((tag_elem_t*) wrapper)->data;
+ tag_elem_t *res = (tag_elem_t*) wrapper;
+ return res->data;
}
@Happens_before:
Push -> Steal
static void task(void * param) {
a=steal(q);
+ a=steal(q);
}
int user_main(int argc, char **argv)
kvs_data *desired = (kvs_data*) NULL;
kvs_data *expected = (kvs_data*) newkvs;
if (!_newkvs.compare_exchange_strong(desired, expected, memory_order_release,
- memory_order_release)) {
+ memory_order_relaxed)) {
// Should clean the allocated area
delete newkvs;
newkvs = _newkvs.load(memory_order_acquire);
copyidx = _copy_idx.load(memory_order_acquire);
while (copyidx < (oldlen << 1) &&
!_copy_idx.compare_exchange_strong(copyidx, copyidx +
- min_copy_work, memory_order_release, memory_order_release))
+ min_copy_work, memory_order_release, memory_order_relaxed))
copyidx = _copy_idx.load(memory_order_relaxed);
if (!(copyidx < (oldlen << 1)))
panic_start = copyidx;
topmap->_kvs.load(memory_order_acquire) == oldkvs) {
kvs_data *newkvs = _newkvs.load(memory_order_acquire);
topmap->_kvs.compare_exchange_strong(oldkvs, newkvs, memory_order_release,
- memory_order_release);
+ memory_order_relaxed);
}
}
// inserted keys
static inline bool CAS_key(kvs_data *kvs, int idx, void *expected, void *desired) {
return kvs->_data[2 * idx + 2].compare_exchange_strong(expected,
- desired, memory_order_release, memory_order_release);
+ desired, memory_order_release, memory_order_relaxed);
}
/**
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_release);
+ desired, memory_order_release, memory_order_relaxed);
/**
# If it is a successful put instead of a copy or any other internal
# operantions, expected != NULL
// publish me to previous lock-holder :
// FIXME: detection miss, don't think it's necessary
pred->next.store(me, std::mo_release );
+ printf("lock_miss1\n");
// (*2) pred not touched any more
// FIXME: detection miss, don't think it's necessary
mcs_node * next = me->next.load(std::mo_acquire);
+ printf("unlock_miss2\n");
if ( next == NULL )
{
mcs_node * tail_was_me = me;
for(;;) {
// FIXME: detection miss, don't think it's necessary
next = me->next.load(std::mo_acquire);
+ printf("unlock_miss3\n");
if ( next != NULL )
break;
thrd_yield();
*/
t_element * read_fetch() {
// Try this new weaker semantics
- //unsigned int rdwr = m_rdwr.load(mo_acquire);
- unsigned int rdwr = m_rdwr.load(mo_relaxed);
+ unsigned int rdwr = m_rdwr.load(mo_acquire);
+ //unsigned int rdwr = m_rdwr.load(mo_relaxed);
/**
@Begin
@Potential_commit_point_define: true
@End
*/
void read_consume(t_element *bin) {
+ /**** FIXME: miss ****/
m_read.fetch_add(1,mo_release);
/**
@Begin
*/
t_element * write_prepare() {
// Try weaker semantics
- //unsigned int rdwr = m_rdwr.load(mo_acquire);
- unsigned int rdwr = m_rdwr.load(mo_relaxed);
+ unsigned int rdwr = m_rdwr.load(mo_acquire);
+ //unsigned int rdwr = m_rdwr.load(mo_relaxed);
/**
@Begin
@Potential_commit_point_define: true
*/
void write_publish(t_element *bin)
{
+ /**** hb violation ****/
m_written.fetch_add(1,mo_release);
/**
@Begin
} else {
input[1] = 37;
enqueue(queue, input[1]);
- output[1] = dequeue(queue);
+ //output[1] = dequeue(queue);
+ output[0] = dequeue(queue);
+ output[0] = dequeue(queue);
}
}
atomic_store_explicit(&q->nodes[node].next, tmp, relaxed);
while (!success) {
- /****FIXME: detected UL ****/
+ /**** detected UL ****/
tail = atomic_load_explicit(&q->tail, acquire);
/****FIXME: miss ****/
next = atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire);
if (get_ptr(next) == 0) { // == NULL
pointer value = MAKE_POINTER(node, get_count(next) + 1);
- /****FIXME: first release UL ****/
+ /**** detected UL ****/
// Second release can be just relaxed
success = atomic_compare_exchange_strong_explicit(&q->nodes[get_ptr(tail)].next,
&next, value, release, relaxed);
}
if (!success) {
// This routine helps the other enqueue to update the tail
- /****FIXME: detected UL ****/
+ /**** detected UL ****/
unsigned int ptr = get_ptr(atomic_load_explicit(&q->nodes[get_ptr(tail)].next, acquire));
pointer value = MAKE_POINTER(ptr,
get_count(tail) + 1);
/****FIXME: miss ****/
- // Seconde release can be just relaxed
+ // Second release can be just relaxed
bool succ = false;
succ = atomic_compare_exchange_strong_explicit(&q->tail,
&tail, value, release, relaxed);
}
}
}
- /****FIXME: first UL ****/
+ /**** dectected UL ****/
// Second release can be just relaxed
atomic_compare_exchange_strong_explicit(&q->tail,
&tail,
pointer next;
while (!success) {
- /****FIXME: detected correctness error ****/
+ /**** detected correctness error ****/
head = atomic_load_explicit(&q->head, acquire);
tail = atomic_load_explicit(&q->tail, relaxed);
/****FIXME: miss ****/
return 0; // NULL
}
/****FIXME: miss (not reached) ****/
- // Seconde release can be just relaxed
+ // Second release can be just relaxed
bool succ = false;
succ = atomic_compare_exchange_strong_explicit(&q->tail,
&tail,