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_release, 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 void threadA(void *arg) {
 102         Data *dataA = (Data*) malloc(sizeof(Data));
 103         dataA->data1 = 3;
 104         dataA->data2 = 2;
 105         dataA->data3 = 1;
 106         write(dataA);
 107 }
 108
 109 void threadB(void *arg) {
 110         Data *dataB = read();
 111         printf("ThreadB data1: %d\n", dataB->data1);
 112         printf("ThreadB data2: %d\n", dataB->data2);
 113         printf("ThreadB data3: %d\n", dataB->data3);
 114 }
 115
 116 void threadC(void *arg) {
 117         Data *dataC = read();
 118         printf("ThreadC data1: %d\n", dataC->data1);
 119         printf("ThreadC data2: %d\n", dataC->data2);
 120         printf("ThreadC data3: %d\n", dataC->data3);
 121 }
 122
 123 void threadD(void *arg) {
 124         Data *dataD = (Data*) malloc(sizeof(Data));
 125         dataD->data1 = -3;
 126         dataD->data2 = -2;
 127         dataD->data3 = -1;
 128         write(dataD);
 129 }
 130
 131 int user_main(int argc, char **argv) {
 132         /**
 133                 @Begin
 134                 @Entry_point
 135                 @End
 136         */
 137
 138         thrd_t t1, t2, t3, t4;
 139         data.store(NULL, memory_order_relaxed);
 140         Data *data_init = (Data*) malloc(sizeof(Data));
 141         data_init->data1 = 0;
 142         data_init->data2 = 0;
 143         data_init->data3 = 0;
 144         write(data_init);
 145
 146         thrd_create(&t1, threadA, NULL);
 147         thrd_create(&t2, threadB, NULL);
 148         thrd_create(&t3, threadC, NULL);
 149         thrd_create(&t4, threadD, NULL);
 150
 151         thrd_join(t1);
 152         thrd_join(t2);
 153         thrd_join(t3);
 154         thrd_join(t4);
 155
 156         return 0;
 157 }