typedef struct Data {
int data1;
int data2;
- int data3;
} Data;
atomic<Data*> data;
@Begin
@Global_define:
@DeclareVar:
- int data1;
- int data2;
- int data3;
+ IntegerList *set;
@InitVar:
- data1 = 0;
- data2 = 0;
- data3 = 0;
+ set = createIntegerList();
+ Data *d = (Data*) MODEL_MALLOC(sizeof(Data));
+ d->data1 = 0;
+ d->data2 = 0;
+ push_back(set, (int64_t) d);
+ @Finalize:
+ if (set)
+ destroyIntegerList(set);
+ return true;
+ @DefineFunc:
+ // This is a trick to get unique id
+ // The testcase should have a unique sum
+ call_id_t getID(int64_t d1, int64_t d2) {
+ return d1 + d2;
+ }
+ @DefineFunc:
+ bool print(int64_t p) {
+ Data *d = (Data*) p;
+ model_print("Elem-> d1 = %d, d2 = %d\n", d->data1, d->data2);
+ }
+ bool equal(int64_t p1, int64_t p2) {
+ if (!p1 || !p2)
+ return false;
+ Data *d1 = (Data*) p1;
+ Data *d2 = (Data*) p2;
+ if (d1->data1 == d2->data1 &&
+ d1->data2 == d2->data2) {
+ return true;
+ } else {
+ return false;
+ }
+ }
+ @DefineFunc:
+ void _write(int64_t d1, int64_t d2) {
+ Data *d = (Data*) MODEL_MALLOC(sizeof(Data));
+ d->data1 = d1;
+ d->data2 = d2;
+ push_back(set, (int64_t) d);
+ }
+ @DefineFunc:
+ bool _read(Data *res) {
+ bool hasElem = has_elem_by_value(set, (int64_t) res, &equal);
+ return hasElem;
+ }
@Happens_before:
Write -> Read
Write -> Write
+ @Commutativity: Write <-> Read: true
@End
*/
@Begin
@Interface: Read
@Commit_point_set: Read_Success_Point
- //@ID: isOriginalRead(__RET__) ? 1 : DEFAULT_CALL_ID
+ @ID: getID(__RET__->data1, __RET__->data2)
+ //@Action:
+ //model_print("Read_ID = %d, d1 = %d, d2 = %d\n", getID(__RET__->data1,
+ // __RET__->data2), __RET__->data1, __RET__->data2);
+ //do_by_value(set, &print);
@Post_check:
- data1 == __RET__->data1 &&
- data2 == __RET__->data2 &&
- data3 == __RET__->data3
+ _read(__RET__);
@End
*/
Data* read() {
+ /********** SPEC (sync) **********/
Data *res = data.load(memory_order_acquire);
- load_32(&res->data1);
+ //load_32(&res->data1);
/**
@Begin
@Commit_point_define_check: true
@Label: Read_Success_Point
@End
*/
- //model_print("Read: %d, %d, %d\n", res->data1, res->data2, res->data3);
return res;
}
@Begin
@Interface: Write
@Commit_point_set: Write_Success_Point
+ @ID: getID(d1, d2);
@Action:
- data1 += d1;
- data2 += d2;
- data3 += d3;
+ //model_print("Write_ID = %d\n", getID(d1, d2));
+ _write(d1, d2);
@End
*/
-Data* write(int d1, int d2, int d3) {
- Data *prev = data.load(memory_order_acquire);
+Data* write(int d1, int d2) {
bool succ = false;
Data *tmp = (Data*) malloc(sizeof(Data));
do {
- store_32(&tmp->data1, prev->data1 + d1);
- //tmp->data1 = prev->data1 + d1;
- tmp->data2 = prev->data2 + d2;
- tmp->data3 = prev->data3 + d3;
+ //store_32(&tmp->data1, prev->data1 + d1);
+ /********** Inadmissibility **********/
+ Data *prev = data.load(memory_order_acquire);
+ tmp->data1 = d1;
+ tmp->data2 = d2;
+ /********** Inadmissibility **********/
succ = data.compare_exchange_strong(prev, tmp,
- memory_order_acq_rel, memory_order_acquire);
+ memory_order_release, memory_order_relaxed);
/**
@Begin
@Commit_point_define_check: succ
void threadA(void *arg) {
- write(1, 0, 0);
+ write(1, 0);
}
void threadB(void *arg) {
- write(0, 1, 0);
+ write(0, 2);
}
void threadC(void *arg) {
- write(0, 0, 1);
+ write(2, 2);
}
void threadD(void *arg) {
- Data *dataC = read();
+ Data *d = read();
+ printf("ThreadD: d1=%d, d2=%d\n", d->data1, d->data2);
}
int user_main(int argc, char **argv) {
Data *dataInit = (Data*) malloc(sizeof(Data));
dataInit->data1 = 0;
dataInit->data2 = 0;
- dataInit->data3 = 0;
atomic_init(&data, dataInit);
- write(0, 0, 0);
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;