9 #include <cdsannotate.h>
10 #include <specannotation.h>
11 #include <model_memory.h>
17 This is an example about how to specify the correctness of the
18 read-copy-update synchronization mechanism.
34 set = createIntegerList();
35 Data *d = (Data*) MODEL_MALLOC(sizeof(Data));
38 push_back(set, (int64_t) d);
41 destroyIntegerList(set);
44 // This is a trick to get unique id
45 // The testcase should have a unique sum
46 call_id_t getID(int64_t d1, int64_t d2) {
50 bool print(int64_t p) {
52 model_print("Elem-> d1 = %d, d2 = %d\n", d->data1, d->data2);
54 bool equal(int64_t p1, int64_t p2) {
57 Data *d1 = (Data*) p1;
58 Data *d2 = (Data*) p2;
59 if (d1->data1 == d2->data1 &&
60 d1->data2 == d2->data2) {
67 void _write(int64_t d1, int64_t d2) {
68 Data *d = (Data*) MODEL_MALLOC(sizeof(Data));
71 push_back(set, (int64_t) d);
74 bool _read(Data *res) {
75 bool hasElem = has_elem_by_value(set, (int64_t) res, &equal);
81 @Commutativity: Write <-> Read: true
88 @Commit_point_set: Read_Success_Point
89 @ID: getID(__RET__->data1, __RET__->data2)
91 //model_print("Read_ID = %d, d1 = %d, d2 = %d\n", getID(__RET__->data1,
92 // __RET__->data2), __RET__->data1, __RET__->data2);
93 //do_by_value(set, &print);
99 /********** SPEC (sync) **********/
100 Data *res = data.load(memory_order_acquire);
101 //load_32(&res->data1);
104 @Commit_point_define_check: true
105 @Label: Read_Success_Point
114 @Commit_point_set: Write_Success_Point
117 //model_print("Write_ID = %d\n", getID(d1, d2));
121 Data* write(int d1, int d2) {
123 Data *tmp = (Data*) malloc(sizeof(Data));
125 //store_32(&tmp->data1, prev->data1 + d1);
126 /********** Inadmissibility **********/
127 Data *prev = data.load(memory_order_acquire);
130 /********** Inadmissibility **********/
131 succ = data.compare_exchange_strong(prev, tmp,
132 memory_order_release, memory_order_relaxed);
135 @Commit_point_define_check: succ
136 @Label: Write_Success_Point
140 //model_print("Write: %d, %d, %d\n", tmp->data1, tmp->data2, tmp->data3);
145 void threadA(void *arg) {
149 void threadB(void *arg) {
153 void threadC(void *arg) {
157 void threadD(void *arg) {
159 printf("ThreadD: d1=%d, d2=%d\n", d->data1, d->data2);
162 int user_main(int argc, char **argv) {
169 thrd_t t1, t2, t3, t4;
170 Data *dataInit = (Data*) malloc(sizeof(Data));
173 atomic_init(&data, dataInit);
175 thrd_create(&t1, threadA, NULL);
176 thrd_create(&t2, threadB, NULL);
177 //thrd_create(&t3, threadC, NULL);
178 thrd_create(&t4, threadD, NULL);