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 }