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.
38 bool equals(Data *ptr1, Data *ptr2) {
39 //if (ptr1->data1 == ptr2->data1
40 // && ptr1->data2 == ptr2->data2
41 // && ptr1->data3 == ptr2->data3) {
49 bool isOriginalRead(Data *ptr) {
50 return ptr->data1 == 0 &&
51 ptr->data2 == 0 && ptr->data3 == 0;
63 @Commit_point_set: Read_Success_Point
64 //@ID: isOriginalRead(__RET__) ? 1 : DEFAULT_CALL_ID
66 Data *_Old_Data = _cur_data;
72 Data *res = data.load(memory_order_acquire);
75 @Commit_point_define_check: true
76 @Label: Read_Success_Point
79 //model_print("Read: %d, %d, %d\n", res->data1, res->data2, res->data3);
86 @Commit_point_set: Write_Success_Point
88 Data *_Old_data = _cur_data;
92 (__RET__->data1 == d1 &&
93 __RET__->data2 == d2 &&
96 (__RET__->data1 == _Old_data->data1 + d1 &&
97 __RET__->data2 == _Old_data->data2 + d2 &&
98 __RET__->data3 == _Old_data->data3 + d3)
101 Data* write(int d1, int d2, int d3) {
102 Data *prev = data.load(memory_order_acquire);
104 Data *tmp = (Data*) malloc(sizeof(Data));
106 tmp->data1 = prev->data1 + d1;
107 tmp->data2 = prev->data2 + d2;
108 tmp->data3 = prev->data3 + d3;
109 succ = data.compare_exchange_strong(prev, tmp,
110 memory_order_acq_rel, memory_order_acquire);
113 @Commit_point_define_check: succ
114 @Label: Write_Success_Point
118 //model_print("Write: %d, %d, %d\n", tmp->data1, tmp->data2, tmp->data3);
123 void threadA(void *arg) {
127 void threadB(void *arg) {
131 void threadC(void *arg) {
135 void threadD(void *arg) {
136 Data *dataC = read();
139 int user_main(int argc, char **argv) {
146 thrd_t t1, t2, t3, t4;
147 Data *dataInit = (Data*) malloc(sizeof(Data));
151 atomic_init(&data, dataInit);
154 thrd_create(&t1, threadA, NULL);
155 thrd_create(&t2, threadB, NULL);
156 //thrd_create(&t3, threadC, NULL);
157 thrd_create(&t4, threadD, NULL);