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                 bool isOriginalRead(Data *ptr) {
  50                         return ptr->data1 == 0 &&
  51                                 ptr->data2 == 0 && ptr->data3 == 0;
  52                 }
  53
  54         @Happens_before:
  55                 Write -> Read
  56                 Write -> Write
  57         @End
  58 */
  59
  60 /**
  61         @Begin
  62         @Interface: Read
  63         @Commit_point_set: Read_Success_Point
  64         //@ID: isOriginalRead(__RET__) ? 1 : DEFAULT_CALL_ID
  65         @Action:
  66                 Data *_Old_Data = _cur_data;
  67         @Post_check:
  68                 _Old_Data = __RET__
  69         @End
  70 */
  71 Data* read() {
  72         Data *res = data.load(memory_order_acquire);
  73         /**
  74                 @Begin
  75                 @Commit_point_define_check: true
  76                 @Label: Read_Success_Point
  77                 @End
  78         */
  79         //model_print("Read: %d, %d, %d\n", res->data1, res->data2, res->data3);
  80         return res;
  81 }
  82
  83 /**
  84         @Begin
  85         @Interface: Write
  86         @Commit_point_set: Write_Success_Point
  87         @Action:
  88                 Data *_Old_data = _cur_data;
  89                 _cur_data = __RET__;
  90         @Post_check:
  91                 _Old_data == NULL ?
  92                         (__RET__->data1 == d1   &&
  93                         __RET__->data2 == d2    &&
  94                         __RET__->data3 == d3)
  95                         :
  96                         (__RET__->data1 == _Old_data->data1 + d1 &&
  97                         __RET__->data2 == _Old_data->data2 + d2 &&
  98                         __RET__->data3 == _Old_data->data3 + d3)
  99         @End
 100 */
 101 Data* write(int d1, int d2, int d3) {
 102         Data *prev = data.load(memory_order_acquire);
 103         bool succ = false;
 104         Data *tmp = (Data*) malloc(sizeof(Data));
 105         do {
 106         tmp->data1 = prev->data1 + d1;
 107             tmp->data2 = prev->data2 + d2;
 108             tmp->data3 = prev->data3 + d3;
 109         succ = data.compare_exchange_strong(prev, tmp,
 110             memory_order_acq_rel, memory_order_acquire);
 111                 /**
 112                         @Begin
 113                         @Commit_point_define_check: succ
 114                         @Label: Write_Success_Point
 115                         @End
 116                 */
 117         } while (!succ);
 118         //model_print("Write: %d, %d, %d\n", tmp->data1, tmp->data2, tmp->data3);
 119         return tmp;
 120 }
 121
 122
 123 void threadA(void *arg) {
 124         write(1, 0, 0);
 125 }
 126
 127 void threadB(void *arg) {
 128         write(0, 1, 0);
 129 }
 130
 131 void threadC(void *arg) {
 132         write(0, 0, 1);
 133 }
 134
 135 void threadD(void *arg) {
 136         Data *dataC = read();
 137 }
 138
 139 int user_main(int argc, char **argv) {
 140         /**
 141                 @Begin
 142                 @Entry_point
 143                 @End
 144         */
 145
 146         thrd_t t1, t2, t3, t4;
 147         Data *dataInit = (Data*) malloc(sizeof(Data));
 148         dataInit->data1 = 0;
 149         dataInit->data2 = 0;
 150         dataInit->data3 = 0;
 151         atomic_init(&data, dataInit);
 152         write(0, 0, 0);
 153
 154         thrd_create(&t1, threadA, NULL);
 155         thrd_create(&t2, threadB, NULL);
 156         //thrd_create(&t3, threadC, NULL);
 157         thrd_create(&t4, threadD, NULL);
 158
 159         thrd_join(t1);
 160         thrd_join(t2);
 161         //thrd_join(t3);
 162         thrd_join(t4);
 163
 164         return 0;
 165 }