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.
49 @Commit_point_set: Read_Success_Point
50 //@ID: isOriginalRead(__RET__) ? 1 : DEFAULT_CALL_ID
52 data1 == __RET__->data1 &&
53 data2 == __RET__->data2 &&
54 data3 == __RET__->data3
58 Data *res = data.load(memory_order_acquire);
59 //load_32(&res->data1);
62 @Commit_point_define_check: true
63 @Label: Read_Success_Point
66 //model_print("Read: %d, %d, %d\n", res->data1, res->data2, res->data3);
73 @Commit_point_set: Write_Success_Point
80 Data* write(int d1, int d2, int d3) {
82 Data *tmp = (Data*) malloc(sizeof(Data));
83 Data *prev = data.load(memory_order_acquire);
85 //store_32(&tmp->data1, prev->data1 + d1);
86 tmp->data1 = prev->data1 + d1;
87 tmp->data2 = prev->data2 + d2;
88 tmp->data3 = prev->data3 + d3;
89 succ = data.compare_exchange_strong(prev, tmp,
90 memory_order_release, memory_order_acquire);
93 @Commit_point_define_check: succ
94 @Label: Write_Success_Point
98 //model_print("Write: %d, %d, %d\n", tmp->data1, tmp->data2, tmp->data3);
103 void threadA(void *arg) {
107 void threadB(void *arg) {
111 void threadC(void *arg) {
115 void threadD(void *arg) {
116 Data *dataC = read();
119 int user_main(int argc, char **argv) {
126 thrd_t t1, t2, t3, t4;
127 Data *dataInit = (Data*) malloc(sizeof(Data));
131 atomic_init(&data, dataInit);
134 thrd_create(&t1, threadA, NULL);
135 thrd_create(&t2, threadB, NULL);
136 //thrd_create(&t3, threadC, NULL);
137 //thrd_create(&t4, threadD, NULL);