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     // 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 UL **********/
  19         Data *res = dataPtr.load(memory_order_acquire);
  20         /** @OPDefine: true */
  21         *data1 = res->data1.load(memory_order_relaxed);
  22         *data2 = res->data2.load(memory_order_relaxed);
  23         //load_32(&res->data1);
  24 }
  25
  26 static void inc(Data *newPtr, Data *prev, int d1, int d2) {
  27         newPtr->data1.store(prev->data1.load(memory_order_relaxed) + d1, memory_order_relaxed);
  28         newPtr->data2.store(prev->data2.load(memory_order_relaxed) + d2, memory_order_relaxed);
  29 }
  30
  31 /** @Transition: STATE(data1) += data1;
  32                 STATE(data2) += data2; */
  33 void write(int data1, int data2) {
  34         bool succ = false;
  35         Data *tmp = new Data;
  36         do {
  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 UL **********/
  41                 Data *prev = dataPtr.load(memory_order_acquire);
  42                 inc(tmp, prev, data1, data2);
  43
  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 UL **********/
  48                 succ = dataPtr.compare_exchange_strong(prev, tmp,
  49             memory_order_release, memory_order_relaxed);
  50                 /** @OPClearDefine: succ */
  51         } while (!succ);
  52 }