*id2 = (id_tag_t*) ptr2;
if (id1 == NULL || id2 == NULL)
return false;
- return *id1 == *id2;
+ return (*id1).tag == (*id2).tag;
}
@DefineFunc:
// Should initialize the CHM for the construction of the table
// For other CHM in kvs_data, they should be initialzed in resize()
// because the size is determined dynamically
+ /**
+ @Begin
+ @Entry_point
+ @End
+ */
+
kvs_data *kvs = new kvs_data(init_size);
void *chm = (void*) new CHM(0);
kvs->_data[0].store(chm, memory_order_relaxed);
#include <cdsannotate.h>
#include <specannotation.h>
#include <model_memory.h>
+#include "common.h"
#include "librace.h"
@DefineFunc:
bool equals(Data *ptr1, Data *ptr2) {
- if (ptr1->data1 == ptr2->data1
- && ptr1->data2 == ptr2->data2
- && ptr1->data3 == ptr2->data3) {
- return true;
- } else {
- return false;
- }
+ //if (ptr1->data1 == ptr2->data1
+ // && ptr1->data2 == ptr2->data2
+ // && ptr1->data3 == ptr2->data3) {
+ // return true;
+ //} else {
+ // return false;
+ //}
+ return ptr1 == ptr2;
}
@Happens_before:
@Label: Read_Success_Point
@End
*/
+ //model_print("Read: %d\n", res);
return res;
}
@End
*/
void write(Data *new_data) {
- while (true) {
- Data *prev = data.load(memory_order_relaxed);
- bool succ = data.compare_exchange_strong(prev, new_data,
+ Data *prev = data.load(memory_order_relaxed);
+ bool succ = false;
+ do {
+ succ = data.compare_exchange_strong(prev, new_data,
memory_order_release, memory_order_relaxed);
/**
@Begin
- @Commit_point_define_check: succ == true
+ @Commit_point_define_check: succ
@Label: Write_Success_Point
@End
*/
- if (succ) {
- break;
- }
- }
+ } while (!succ);
+ //model_print("Write: %d\n", new_data);
}
void threadA(void *arg) {
thrd_t t1, t2, t3, t4;
data.store(NULL, memory_order_relaxed);
Data *data_init = (Data*) malloc(sizeof(Data));
- data_init->data1 = 1;
- data_init->data2 = 2;
- data_init->data3 = 3;
+ data_init->data1 = 0;
+ data_init->data2 = 0;
+ data_init->data3 = 0;
write(data_init);
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_join(t3);
+ thrd_join(t3);
thrd_join(t4);
return 0;