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 } Data;
  25
  26 atomic<Data*> data;
  27
  28 /**
  29         @Begin
  30         @Global_define:
  31                 @DeclareVar:
  32                         IntegerList *set;
  33                 @InitVar:
  34                         set = createIntegerList();
  35                         Data *d = (Data*) MODEL_MALLOC(sizeof(Data));
  36                         d->data1 = 0;
  37                         d->data2 = 0;
  38                         push_back(set, (int64_t) d);
  39                 @Finalize:
  40                         if (set)
  41                                 destroyIntegerList(set);
  42                         return true;
  43         @DefineFunc:
  44                 // This is a trick to get unique id
  45                 // The testcase should have a unique sum
  46                 call_id_t getID(int64_t d1, int64_t d2) {
  47                         return d1 + d2;
  48                 }
  49         @DefineFunc:
  50                 bool print(int64_t p) {
  51                         Data *d = (Data*) p;
  52                         model_print("Elem-> d1 = %d, d2 = %d\n", d->data1, d->data2);
  53                 }
  54                 bool equal(int64_t p1, int64_t p2) {
  55                         if (!p1 || !p2)
  56                                 return false;
  57                         Data *d1 = (Data*) p1;
  58                         Data *d2 = (Data*) p2;
  59                         if (d1->data1 == d2->data1 &&
  60                                 d1->data2 == d2->data2) {
  61                                 return true;
  62                         } else {
  63                                 return false;
  64                         }
  65                 }
  66         @DefineFunc:
  67                 void _write(int64_t d1, int64_t d2) {
  68                         Data *d = (Data*) MODEL_MALLOC(sizeof(Data));
  69                         d->data1 = d1;
  70                         d->data2 = d2;
  71                         push_back(set, (int64_t) d);
  72                 }
  73         @DefineFunc:
  74                 bool _read(Data *res) {
  75                         bool hasElem = has_elem_by_value(set, (int64_t) res, &equal);
  76                         return hasElem;
  77                 }
  78         @Happens_before:
  79                 Write -> Read
  80                 Write -> Write
  81         @Commutativity: Write <-> Read: true
  82         @End
  83 */
  84
  85 /**
  86         @Begin
  87         @Interface: Read
  88         @Commit_point_set: Read_Success_Point
  89         @ID: getID(__RET__->data1, __RET__->data2)
  90         //@Action:
  91                 //model_print("Read_ID = %d, d1 = %d, d2 = %d\n", getID(__RET__->data1,
  92                 //      __RET__->data2), __RET__->data1, __RET__->data2);
  93                 //do_by_value(set, &print);
  94         @Post_check:
  95                 _read(__RET__);
  96         @End
  97 */
  98 Data* read() {
  99         /**********    SPEC (sync)    **********/
 100         Data *res = data.load(memory_order_acquire);
 101         //load_32(&res->data1);
 102         /**
 103                 @Begin
 104                 @Commit_point_define_check: true
 105                 @Label: Read_Success_Point
 106                 @End
 107         */
 108         return res;
 109 }
 110
 111 /**
 112         @Begin
 113         @Interface: Write
 114         @Commit_point_set: Write_Success_Point
 115         @ID: getID(d1, d2);
 116         @Action:
 117                 //model_print("Write_ID = %d\n", getID(d1, d2));
 118                 _write(d1, d2);
 119         @End
 120 */
 121 Data* write(int d1, int d2) {
 122         bool succ = false;
 123         Data *tmp = (Data*) malloc(sizeof(Data));
 124         do {
 125         //store_32(&tmp->data1, prev->data1 + d1);
 126                 /**********   Inadmissibility    **********/
 127                 Data *prev = data.load(memory_order_acquire);
 128         tmp->data1 = d1;
 129             tmp->data2 = d2;
 130                 /**********   Inadmissibility    **********/
 131         succ = data.compare_exchange_strong(prev, tmp,
 132             memory_order_release, memory_order_relaxed);
 133                 /**
 134                         @Begin
 135                         @Commit_point_define_check: succ
 136                         @Label: Write_Success_Point
 137                         @End
 138                 */
 139         } while (!succ);
 140         //model_print("Write: %d, %d, %d\n", tmp->data1, tmp->data2, tmp->data3);
 141         return tmp;
 142 }
 143
 144
 145 void threadA(void *arg) {
 146         write(1, 0);
 147 }
 148
 149 void threadB(void *arg) {
 150         write(0, 2);
 151 }
 152
 153 void threadC(void *arg) {
 154         write(2, 2);
 155 }
 156
 157 void threadD(void *arg) {
 158         Data *d = read();
 159         printf("ThreadD: d1=%d, d2=%d\n", d->data1, d->data2);
 160 }
 161
 162 int user_main(int argc, char **argv) {
 163         /**
 164                 @Begin
 165                 @Entry_point
 166                 @End
 167         */
 168
 169         thrd_t t1, t2, t3, t4;
 170         Data *dataInit = (Data*) malloc(sizeof(Data));
 171         dataInit->data1 = 0;
 172         dataInit->data2 = 0;
 173         atomic_init(&data, dataInit);
 174
 175         thrd_create(&t1, threadA, NULL);
 176         thrd_create(&t2, threadB, NULL);
 177         //thrd_create(&t3, threadC, NULL);
 178         thrd_create(&t4, threadD, NULL);
 179
 180         thrd_join(t1);
 181         thrd_join(t2);
 182         //thrd_join(t3);
 183         thrd_join(t4);
 184
 185         return 0;
 186 }