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 // XXX-injection-#1: Weaken the parameter "memory_order_acquire" to
16 // "memory_order_relaxed", run "make" to recompile, and then run:
17 // "./run.sh ./read-copy-update/testcase -m2 -y -u3 -tSPEC"
18 /********** Detected Correctness **********/
19 Data *res = dataPtr.load(memory_order_acquire);
20 /** @OPDefine: true */
23 //load_32(&res->data1);
26 static void inc(Data *newPtr, Data *prev, int d1, int d2) {
27 newPtr->data1 = prev->data1 + d1;
28 newPtr->data2 = prev->data2 + d2;
31 /** @Transition: STATE(data1) += data1;
32 STATE(data2) += data2; */
33 void write(int data1, int data2) {
37 // XXX-injection-#2: Weaken the parameter "memory_order_acquire" to
38 // "memory_order_relaxed", run "make" to recompile, and then run:
39 // "./run.sh ./read-copy-update/testcase -m2 -y -u3 -tSPEC"
40 /********** Detected Correctness **********/
41 Data *prev = dataPtr.load(memory_order_acquire);
42 inc(tmp, prev, data1, data2);
44 // XXX-injection-#3: Weaken the parameter "memory_order_release" to
45 // "memory_order_relaxed", run "make" to recompile, and then run:
46 // "./run.sh ./read-copy-update/testcase -m2 -y -u3 -tSPEC"
47 /********** Detected Correctness **********/
48 succ = dataPtr.compare_exchange_strong(prev, tmp,
49 memory_order_release, memory_order_relaxed);
50 /** @OPClearDefine: succ */