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) {
58 @Commit_point_set: Read_Success_Point
60 Data *_Old_Data = _cur_data;
62 equals(__RET__, _Old_Data)
66 Data *res = data.load(memory_order_acquire);
69 @Commit_point_define_check: true
70 @Label: Read_Success_Point
73 //model_print("Read: %d\n", res);
80 @Commit_point_set: Write_Success_Point
85 void write(Data *new_data) {
86 Data *prev = data.load(memory_order_relaxed);
89 succ = data.compare_exchange_strong(prev, new_data,
90 memory_order_acq_rel, memory_order_relaxed);
93 @Commit_point_define_check: succ
94 @Label: Write_Success_Point
98 //model_print("Write: %d\n", new_data);
102 Data *prev = data.load(memory_order_acquire);
104 Data *tmp = malloc(sizeof(Data));
106 tmp->data1=prev->data1+new_data->data1;
107 tmp->data2=prev->data2+new_data->data2;
108 tmp->data3=prev->data3+new_data->data3;
109 succ = data.compare_exchange_strong(prev, tmp,
110 memory_order_release, memory_order_acquire);
112 //model_print("Write: %d\n", new_data);
116 void threadA(void *arg) {
117 Data *dataA = (Data*) malloc(sizeof(Data));
124 void threadB(void *arg) {
125 Data *dataB = read();
126 printf("ThreadB data1: %d\n", dataB->data1);
127 printf("ThreadB data2: %d\n", dataB->data2);
128 printf("ThreadB data3: %d\n", dataB->data3);
131 void threadC(void *arg) {
132 Data *dataC = read();
133 printf("ThreadC data1: %d\n", dataC->data1);
134 printf("ThreadC data2: %d\n", dataC->data2);
135 printf("ThreadC data3: %d\n", dataC->data3);
138 void threadD(void *arg) {
139 Data *dataD = (Data*) malloc(sizeof(Data));
146 int user_main(int argc, char **argv) {
153 thrd_t t1, t2, t3, t4;
154 data.store(NULL, memory_order_relaxed);
155 Data *data_init = (Data*) malloc(sizeof(Data));
156 data_init->data1 = 0;
157 data_init->data2 = 0;
158 data_init->data3 = 0;
161 thrd_create(&t1, threadA, NULL);
162 thrd_create(&t2, threadB, NULL);
163 thrd_create(&t3, threadC, NULL);
164 thrd_create(&t4, threadD, NULL);