4 This is an example about how to specify the correctness of the
5 read-copy-update synchronization mechanism.
10 /** @DeclareState: int data1;
13 /** @JustifyingPrecondition: return STATE(data1) == *data1 && STATE(data2) == *data2; */
14 void read(int *data1, int *data2) {
15 /********** Detected Correctness **********/
16 Data *res = dataPtr.load(memory_order_acquire);
17 /** @OPDefine: true */
20 //load_32(&res->data1);
23 static void inc(Data *newPtr, Data *prev, int d1, int d2) {
24 newPtr->data1 = prev->data1 + d1;
25 newPtr->data2 = prev->data2 + d2;
28 /** @Transition: STATE(data1) += data1;
29 STATE(data2) += data2; */
30 void write(int data1, int data2) {
34 /********** Detected Correctness **********/
35 Data *prev = dataPtr.load(memory_order_acquire);
36 inc(tmp, prev, data1, data2);
37 /********** Detected Correctness **********/
38 succ = dataPtr.compare_exchange_strong(prev, tmp,
39 memory_order_release, memory_order_relaxed);
40 /** @OPClearDefine: succ */