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