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);
101 void threadA(void *arg) {
102 Data *dataA = (Data*) malloc(sizeof(Data));
109 void threadB(void *arg) {
110 Data *dataB = read();
111 printf("ThreadB data1: %d\n", dataB->data1);
112 printf("ThreadB data2: %d\n", dataB->data2);
113 printf("ThreadB data3: %d\n", dataB->data3);
116 void threadC(void *arg) {
117 Data *dataC = read();
118 printf("ThreadC data1: %d\n", dataC->data1);
119 printf("ThreadC data2: %d\n", dataC->data2);
120 printf("ThreadC data3: %d\n", dataC->data3);
123 void threadD(void *arg) {
124 Data *dataD = (Data*) malloc(sizeof(Data));
131 int user_main(int argc, char **argv) {
138 thrd_t t1, t2, t3, t4;
139 data.store(NULL, memory_order_relaxed);
140 Data *data_init = (Data*) malloc(sizeof(Data));
141 data_init->data1 = 0;
142 data_init->data2 = 0;
143 data_init->data3 = 0;
146 thrd_create(&t1, threadA, NULL);
147 thrd_create(&t2, threadB, NULL);
148 thrd_create(&t3, threadC, NULL);
149 thrd_create(&t4, threadD, NULL);