52a82db028651ace056766b5aa4205564e6f3774
[model-checker-benchmarks.git] / read-copy-update / rcu.cc
1 #include "rcu.h"
2
3 /**
4         This is an example about how to specify the correctness of the
5         read-copy-update synchronization mechanism.
6 */
7
8 atomic<Data*> dataPtr;
9         
10 /** @DeclareState: int data1;
11                 int data2; */
12
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 */
18         *data1 = res->data1;
19         *data2 = res->data2;
20         //load_32(&res->data1);
21 }
22
23 static void inc(Data *newPtr, Data *prev, int d1, int d2) {
24         newPtr->data1 = prev->data1 + d1;
25         newPtr->data2 = prev->data2 + d2;
26 }
27
28 /** @Transition: STATE(data1) += data1;
29                 STATE(data2) += data2; */
30 void write(int data1, int data2) {
31         bool succ = false;
32         Data *tmp = new Data;
33         do {
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 */
41         } while (!succ);
42 }