10 This is an example about how to specify the correctness of the
11 read-copy-update synchronization mechanism.
31 bool equals(Data *ptr1, Data *ptr2) {
32 if (ptr1->data1 == ptr2->data1
33 && ptr1->data2 == ptr2->data2
34 && ptr1->data3 == ptr2->data3) {
50 @Commit_point_set: Read_Success_Point
52 Data *_Old_Data = _cur_data;
54 equals(__RET__, _Old_Data)
58 Data *res = data.load(memory_order_acquire);
61 @Commit_point_define_check: true
62 @Label: Read_Success_Point
71 @Commit_point_set: Write_Success_Point
76 void write(Data *new_data) {
78 Data *prev = data.load(memory_order_relaxed);
79 bool succ = data.compare_exchange_strong(prev, new_data,
80 memory_order_release, memory_order_relaxed);
83 @Commit_point_define_check: succ == true
84 @Label: Write_Success_Point
93 void threadA(void *arg) {
94 Data *dataA = (Data*) malloc(sizeof(Data));
101 void threadB(void *arg) {
102 Data *dataB = read();
103 printf("ThreadB data1: %d\n", dataB->data1);
104 printf("ThreadB data2: %d\n", dataB->data2);
105 printf("ThreadB data3: %d\n", dataB->data3);
108 void threadC(void *arg) {
109 Data *dataC = read();
110 printf("ThreadC data1: %d\n", dataC->data1);
111 printf("ThreadC data2: %d\n", dataC->data2);
112 printf("ThreadC data3: %d\n", dataC->data3);
115 void threadD(void *arg) {
116 Data *dataD = (Data*) malloc(sizeof(Data));
123 int user_main(int argc, char **argv) {
130 thrd_t t1, t2, t3, t4;
131 data.store(NULL, memory_order_relaxed);
132 Data *data_init = (Data*) malloc(sizeof(Data));
133 data_init->data1 = 1;
134 data_init->data2 = 2;
135 data_init->data3 = 3;
138 thrd_create(&t1, threadA, NULL);
139 thrd_create(&t2, threadB, NULL);
140 //thrd_create(&t3, threadC, NULL);
141 //thrd_create(&t4, threadD, NULL);