benchmark/read-copy-update/rcu.cc

   1 #include <atomic>
   2
   3 using namespace std;
   4
   5 /**
   6         This is an example about how to specify the correctness of the
   7         read-copy-update synchronization mechanism.
   8 */
   9
  10 // Properties to check:
  11
  12
  13 typedef void* (*read_func_ptr_t)(void*);
  14
  15 template <typename Type>
  16 class rcu {
  17         /**
  18                 @Begin
  19                 @Global_define:
  20                         Type *__cur_data;
  21
  22                         static bool equals(void *ptr1, void *ptr2) {
  23                                 // ...
  24                                 // Return if the two data instances pointed to equals to each
  25                                 // other
  26                         }
  27
  28                 @Happens-before:
  29                         Write -> Read
  30                         Write -> Write
  31                 @End
  32         */
  33 private:
  34         atomic<Type*> _data;
  35
  36         public:
  37         /**
  38                 @Begin
  39                 @Interface: Read
  40                 @Commit_point_set: Read_Success_Point
  41                 @Action:
  42                         @Code:
  43                         void *_Old_Data = __cur_data;
  44                 @Post_check:
  45                         equals(__RET__, _Old_Data->read())
  46                 @End
  47         */
  48         void* read() {
  49                 void *res = NULL;
  50                 Type *cur_data_ptr = _data.load(memory_order_acquire);
  51                 /**
  52                         @Begin
  53                         @Commit_point_check_define: true
  54                         @Label: Read_Success_Point
  55                         @End
  56                 */
  57                 res = cur_data_ptr->read();
  58                 return res;
  59         }
  60
  61         /**
  62                 @Begin
  63                 @Interface: Write
  64                 @Commit_point_set: Write_Success_Point
  65                 @Action:
  66                         @Code:
  67                         __cur_data = new_data;
  68                 @End
  69         */
  70         void write(Type *new_data) {
  71                 while (true) {
  72                         Type *prev = _data.load(memory_order_acquire);
  73                         if (_data.compare_exchange_weak(prev, new_data,
  74                                 memory_order_release, memory_order_release)) {
  75                                 /**
  76                                         @Begin
  77                                         @Commit_point_check_define: __ATOMIC_RET__ == true
  78                                         @Label: Write_Success_Point
  79                                         @End
  80                                 */
  81                                 break;
  82                         }
  83                 }
  84         }
  85 };