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                         int data1;
  34                         int data2;
  35                         int data3;
  36                 @InitVar:
  37                         data1 = 0;
  38                         data2 = 0;
  39                         data3 = 0;
  40         @Happens_before:
  41                 Write -> Read
  42                 Write -> Write
  43         @End
  44 */
  45
  46 /**
  47         @Begin
  48         @Interface: Read
  49         @Commit_point_set: Read_Success_Point
  50         //@ID: isOriginalRead(__RET__) ? 1 : DEFAULT_CALL_ID
  51         @Post_check:
  52                 data1 == __RET__->data1 &&
  53                 data2 == __RET__->data2 &&
  54                 data3 == __RET__->data3
  55         @End
  56 */
  57 Data* read() {
  58         Data *res = data.load(memory_order_acquire);
  59         load_32(&res->data1);
  60         /**
  61                 @Begin
  62                 @Commit_point_define_check: true
  63                 @Label: Read_Success_Point
  64                 @End
  65         */
  66         //model_print("Read: %d, %d, %d\n", res->data1, res->data2, res->data3);
  67         return res;
  68 }
  69
  70 /**
  71         @Begin
  72         @Interface: Write
  73         @Commit_point_set: Write_Success_Point
  74         @Action:
  75                 data1 += d1;
  76                 data2 += d2;
  77                 data3 += d3;
  78         @End
  79 */
  80 Data* write(int d1, int d2, int d3) {
  81         Data *prev = data.load(memory_order_acquire);
  82         bool succ = false;
  83         Data *tmp = (Data*) malloc(sizeof(Data));
  84         do {
  85         store_32(&tmp->data1, prev->data1 + d1);
  86         //tmp->data1 = prev->data1 + d1;
  87             tmp->data2 = prev->data2 + d2;
  88             tmp->data3 = prev->data3 + d3;
  89         succ = data.compare_exchange_strong(prev, tmp,
  90             memory_order_acq_rel, memory_order_acquire);
  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, %d, %d\n", tmp->data1, tmp->data2, tmp->data3);
  99         return tmp;
 100 }
 101
 102
 103 void threadA(void *arg) {
 104         write(1, 0, 0);
 105 }
 106
 107 void threadB(void *arg) {
 108         write(0, 1, 0);
 109 }
 110
 111 void threadC(void *arg) {
 112         write(0, 0, 1);
 113 }
 114
 115 void threadD(void *arg) {
 116         Data *dataC = read();
 117 }
 118
 119 int user_main(int argc, char **argv) {
 120         /**
 121                 @Begin
 122                 @Entry_point
 123                 @End
 124         */
 125
 126         thrd_t t1, t2, t3, t4;
 127         Data *dataInit = (Data*) malloc(sizeof(Data));
 128         dataInit->data1 = 0;
 129         dataInit->data2 = 0;
 130         dataInit->data3 = 0;
 131         atomic_init(&data, dataInit);
 132         write(0, 0, 0);
 133
 134         thrd_create(&t1, threadA, NULL);
 135         thrd_create(&t2, threadB, NULL);
 136         thrd_create(&t3, threadC, NULL);
 137         thrd_create(&t4, threadD, NULL);
 138
 139         thrd_join(t1);
 140         thrd_join(t2);
 141         thrd_join(t3);
 142         thrd_join(t4);
 143
 144         return 0;
 145 }