12 This is an example about how to specify the correctness of the
13 read-copy-update synchronization mechanism.
33 bool equals(Data *ptr1, Data *ptr2) {
34 if (ptr1->data1 == ptr2->data2
35 && ptr1->data2 == ptr2->data2
36 && ptr1->data3 == ptr2->data3) {
52 @Commit_point_set: Read_Success_Point
54 Data *_Old_Data = _cur_data;
56 equals(__RET__, _Old_Data)
60 Data *res = data.load(memory_order_acquire);
63 @Commit_point_define_check: true
64 @Label: Read_Success_Point
73 @Commit_point_set: Write_Success_Point
78 void write(Data *new_data) {
80 Data *prev = data.load(memory_order_relaxed);
81 bool succ = data.compare_exchange_strong(prev, new_data,
82 memory_order_release, memory_order_relaxed);
85 @Commit_point_define_check: succ == true
86 @Label: Write_Success_Point
95 void threadA(void *arg) {
96 Data *dataA = (Data*) malloc(sizeof(Data));
103 void threadB(void *arg) {
104 Data *dataB = read();
105 printf("ThreadB data1: %d\n", dataB->data1);
106 printf("ThreadB data2: %d\n", dataB->data2);
107 printf("ThreadB data3: %d\n", dataB->data3);
110 int user_main(int argc, char **argv) {
118 Data *data_init = (Data*) malloc(sizeof(Data));
119 data_init->data1 = 1;
120 data_init->data2 = 2;
121 data_init->data3 = 3;
124 thrd_create(&t1, threadA, NULL);
125 thrd_create(&t2, threadB, NULL);