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