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