benchmark/read-copy-update/rcu.cc

   1 #include <atomic>
   2 #include <threads.h>
   3 #include <stdatomic.h>
   4 #include <stdlib.h>
   5 #include <stdio.h>
   6
   7 #include "librace.h"
   8
   9 using namespace std;
  10
  11 /**
  12         This is an example about how to specify the correctness of the
  13         read-copy-update synchronization mechanism.
  14 */
  15
  16 typedef struct Data {
  17         int data1;
  18         int data2;
  19         int data3;
  20 } Data;
  21
  22 atomic<Data*> data;
  23
  24 /**
  25         @Begin
  26         @Global_define:
  27                 @DeclareVar:
  28                         Data *_cur_data;
  29                 @InitVar:
  30                         _cur_data = NULL;
  31
  32                 @DefineFunc:
  33                 bool equals(Data *ptr1, Data *ptr2) {
  34                         if (ptr1->data1 == ptr2->data2
  35                                 && ptr1->data2 == ptr2->data2
  36                                 && ptr1->data3 == ptr2->data3) {
  37                                 return true;
  38                         } else {
  39                                 return false;
  40                         }
  41                 }
  42
  43         @Happens_before:
  44                 Write -> Read
  45                 Write -> Write
  46         @End
  47 */
  48
  49 /**
  50         @Begin
  51         @Interface: Read
  52         @Commit_point_set: Read_Success_Point
  53         @Action:
  54                 Data *_Old_Data = _cur_data;
  55         @Post_check:
  56                 equals(__RET__, _Old_Data)
  57         @End
  58 */
  59 Data* read() {
  60         Data *res = data.load(memory_order_acquire);
  61         /**
  62                 @Begin
  63                 @Commit_point_define_check: true
  64                 @Label: Read_Success_Point
  65                 @End
  66         */
  67         return res;
  68 }
  69
  70 /**
  71         @Begin
  72         @Interface: Write
  73         @Commit_point_set: Write_Success_Point
  74         @Action:
  75                 _cur_data = new_data;
  76         @End
  77 */
  78 void write(Data *new_data) {
  79         while (true) {
  80                 Data *prev = data.load(memory_order_relaxed);
  81                 bool succ = data.compare_exchange_strong(prev, new_data,
  82                         memory_order_release, memory_order_relaxed);
  83                 /**
  84                         @Begin
  85                         @Commit_point_define_check: succ == true
  86                         @Label: Write_Success_Point
  87                         @End
  88                 */
  89                 if (succ) {
  90                         break;
  91                 }
  92         }
  93 }
  94
  95 void threadA(void *arg) {
  96         Data *dataA = (Data*) malloc(sizeof(Data));
  97         dataA->data1 = 3;
  98         dataA->data2 = 2;
  99         dataA->data3 = 1;
 100         write(dataA);
 101 }
 102
 103 void threadB(void *arg) {
 104         Data *dataB = read();
 105         printf("ThreadB data1: %d\n", dataB->data1);
 106         printf("ThreadB data2: %d\n", dataB->data2);
 107         printf("ThreadB data3: %d\n", dataB->data3);
 108 }
 109
 110 int user_main(int argc, char **argv) {
 111         /**
 112                 @Begin
 113                 @Entry_point
 114                 @End
 115         */
 116
 117         thrd_t t1, t2;
 118         Data *data_init = (Data*) malloc(sizeof(Data));
 119         data_init->data1 = 1;
 120         data_init->data2 = 2;
 121         data_init->data3 = 3;
 122         write(data_init);
 123
 124         thrd_create(&t1, threadA, NULL);
 125         thrd_create(&t2, threadB, NULL);
 126
 127         thrd_join(t1);
 128         thrd_join(t2);
 129
 130         return 0;
 131 }