scfence/inference.cc

   1 #include "fence_common.h"
   2 #include "wildcard.h"
   3 #include "patch.h"
   4 #include "inferlist.h"
   5 #include "inference.h"
   6
   7 /** Forward declaration */
   8 class PatchUnit;
   9 class Patch;
  10 class Inference;
  11 class InferenceList;
  12
  13 bool isTheInference(Inference *infer) {
  14         for (int i = 0; i < infer->getSize(); i++) {
  15                 memory_order mo1 = (*infer)[i], mo2;
  16                 if (mo1 == WILDCARD_NONEXIST)
  17                         mo1 = relaxed;
  18                 switch (i) {
  19                         case 3:
  20                                 mo2 = acquire;
  21                         break;
  22                         case 11:
  23                                 mo2 = release;
  24                         break;
  25                         default:
  26                                 mo2 = relaxed;
  27                         break;
  28                 }
  29                 if (mo1 != mo2)
  30                         return false;
  31         }
  32         return true;
  33 }
  34
  35 const char* get_mo_str(memory_order order) {
  36         switch (order) {
  37                 case std::memory_order_relaxed: return "relaxed";
  38                 case std::memory_order_acquire: return "acquire";
  39                 case std::memory_order_release: return "release";
  40                 case std::memory_order_acq_rel: return "acq_rel";
  41                 case std::memory_order_seq_cst: return "seq_cst";
  42                 default:
  43                         //model_print("Weird memory order, a bug or something!\n");
  44                         //model_print("memory_order: %d\n", order);
  45                         return "unknown";
  46         }
  47 }
  48
  49
  50 void Inference::resize(int newsize) {
  51         ASSERT (newsize > size && newsize <= MAX_WILDCARD_NUM);
  52         memory_order *newOrders = (memory_order *) model_malloc((newsize + 1) * sizeof(memory_order*));
  53         int i;
  54         for (i = 0; i <= size; i++)
  55                 newOrders[i] = orders[i];
  56         for (; i <= newsize; i++)
  57                 newOrders[i] = WILDCARD_NONEXIST;
  58         model_free(orders);
  59         size = newsize;
  60         orders = newOrders;
  61 }
  62
  63 /** Return the state of how we update a specific mo; If we have to make an
  64  * uncompatible inference or that inference cannot be imposed because it's
  65  * not a wildcard, it returns -1; if it is a compatible memory order but the
  66  * current memory order is no weaker than mo, it returns 0; otherwise, it
  67  * does strengthen the order, and returns 1 */
  68 int Inference::strengthen(const ModelAction *act, memory_order mo) {
  69         memory_order wildcard = act->get_original_mo();
  70         int wildcardID = get_wildcard_id_zero(wildcard);
  71         if (!is_wildcard(wildcard)) {
  72                 FENCE_PRINT("We cannot make this update to %s!\n", get_mo_str(mo));
  73                 ACT_PRINT(act);
  74                 return -1;
  75         }
  76         if (wildcardID > size)
  77                 resize(wildcardID);
  78         ASSERT (is_normal_mo(mo));
  79         //model_print("wildcardID -> order: %d -> %d\n", wildcardID, orders[wildcardID]);
  80         ASSERT (is_normal_mo_infer(orders[wildcardID]));
  81         switch (orders[wildcardID]) {
  82                 case memory_order_seq_cst:
  83                         return 0;
  84                 case memory_order_relaxed:
  85                         if (mo == memory_order_relaxed)
  86                                 return 0;
  87                         orders[wildcardID] = mo;
  88                         break;
  89                 case memory_order_acquire:
  90                         if (mo == memory_order_acquire || mo == memory_order_relaxed)
  91                                 return 0;
  92                         if (mo == memory_order_release)
  93                                 orders[wildcardID] = memory_order_acq_rel;
  94                         else if (mo >= memory_order_acq_rel && mo <=
  95                                 memory_order_seq_cst)
  96                                 orders[wildcardID] = mo;
  97                         break;
  98                 case memory_order_release:
  99                         if (mo == memory_order_release || mo == memory_order_relaxed)
 100                                 return 0;
 101                         if (mo == memory_order_acquire)
 102                                 orders[wildcardID] = memory_order_acq_rel;
 103                         else if (mo >= memory_order_acq_rel)
 104                                 orders[wildcardID] = mo;
 105                         break;
 106                 case memory_order_acq_rel:
 107                         if (mo == memory_order_seq_cst)
 108                                 orders[wildcardID] = mo;
 109                         else
 110                                 return 0;
 111                         break;
 112                 default:
 113                         orders[wildcardID] = mo;
 114                         break;
 115         }
 116         return 1;
 117 }
 118
 119 Inference::Inference() {
 120         orders = (memory_order *) model_malloc((4 + 1) * sizeof(memory_order*));
 121         size = 4;
 122         for (int i = 0; i <= size; i++)
 123                 orders[i] = WILDCARD_NONEXIST;
 124         initialInfer = this;
 125         buggy = false;
 126         hasFixes = false;
 127         leaf = false;
 128         explored = false;
 129         shouldFix = true;
 130 }
 131
 132 Inference::Inference(Inference *infer) {
 133         ASSERT (infer->size > 0 && infer->size <= MAX_WILDCARD_NUM);
 134         orders = (memory_order *) model_malloc((infer->size + 1) * sizeof(memory_order*));
 135         this->size = infer->size;
 136         for (int i = 0; i <= size; i++)
 137                 orders[i] = infer->orders[i];
 138
 139         initialInfer = infer->initialInfer;
 140         buggy = false;
 141         hasFixes = false;
 142         leaf = false;
 143         explored = false;
 144         shouldFix = true;
 145 }
 146
 147 /** return value:
 148   * 0 -> mo1 == mo2;
 149   * 1 -> mo1 stronger than mo2;
 150   * -1 -> mo1 weaker than mo2;
 151   * 2 -> mo1 & mo2 are uncomparable.
 152  */
 153 int Inference::compareMemoryOrder(memory_order mo1, memory_order mo2) {
 154         if (mo1 == WILDCARD_NONEXIST)
 155                 mo1 = memory_order_relaxed;
 156         if (mo2 == WILDCARD_NONEXIST)
 157                 mo2 = memory_order_relaxed;
 158         if (mo1 == mo2)
 159                 return 0;
 160         if (mo1 == memory_order_relaxed)
 161                 return -1;
 162         if (mo1 == memory_order_acquire) {
 163                 if (mo2 == memory_order_relaxed)
 164                         return 1;
 165                 if (mo2 == memory_order_release)
 166                         return 2;
 167                 return -1;
 168         }
 169         if (mo1 == memory_order_release) {
 170                 if (mo2 == memory_order_relaxed)
 171                         return 1;
 172                 if (mo2 == memory_order_acquire)
 173                         return 2;
 174                 return -1;
 175         }
 176         if (mo1 == memory_order_acq_rel) {
 177                 if (mo2 == memory_order_seq_cst)
 178                         return -1;
 179                 else
 180                         return 1;
 181         }
 182         // mo1 now must be SC and mo2 can't be SC
 183         return 1;
 184 }
 185
 186
 187 /** Try to calculate the set of inferences that are weaker than this, but
 188  *  still stronger than infer */
 189 InferenceList* Inference::getWeakerInferences(Inference *infer) {
 190         // An array of strengthened wildcards
 191         SnapVector<int> *strengthened = new SnapVector<int>;
 192         model_print("Strengthened wildcards\n");
 193         for (int i = 1; i <= size; i++) {
 194                 memory_order mo1 = orders[i],
 195                         mo2 = (*infer)[i];
 196                 int compVal = compareMemoryOrder(mo1, mo2);
 197                 if (!(compVal == 0 || compVal == 1)) {
 198                         model_print("assert failure\n");
 199                         model_print("compVal=%d\n", compVal);
 200                         ASSERT (false);
 201                 }
 202                 if (compVal == 0) // Same
 203                         continue;
 204                 model_print("wildcard %d -> %s (%s)\n", i, get_mo_str(mo1),
 205                         get_mo_str(mo2));
 206                 strengthened->push_back(i);
 207         }
 208
 209         // Got the strengthened wildcards, find out weaker inferences
 210         // First get a volatile copy of this inference
 211         Inference *tmpRes = new Inference(this);
 212         InferenceList *res = new InferenceList;
 213         if (strengthened->size() == 0)
 214                 return res;
 215         getWeakerInferences(res, tmpRes, this, infer, strengthened, 0);
 216         res->pop_front();
 217         res->pop_back();
 218         InferenceList::print(res, "Weakened");
 219         return res;
 220 }
 221
 222
 223 // seq_cst -> acq_rel -> acquire -> release -> relaxed
 224 memory_order Inference::nextWeakOrder(memory_order mo1, memory_order mo2) {
 225         memory_order res;
 226         switch (mo1) {
 227                 case memory_order_seq_cst:
 228                         res = memory_order_acq_rel;
 229                         break;
 230                 case memory_order_acq_rel:
 231                         res = memory_order_acquire;
 232                         break;
 233                 case memory_order_acquire:
 234                         res = memory_order_relaxed;
 235                         break;
 236                 case memory_order_release:
 237                         res = memory_order_relaxed;
 238                         break;
 239                 case memory_order_relaxed:
 240                         res = memory_order_relaxed;
 241                         break;
 242                 default:
 243                         res = memory_order_relaxed;
 244                         break;
 245         }
 246         int compVal = compareMemoryOrder(res, mo2);
 247         if (compVal == 2 || compVal == -1) // Incomparable
 248                 res = mo2;
 249         return res;
 250 }
 251
 252 void Inference::getWeakerInferences(InferenceList* list, Inference *tmpRes,
 253         Inference *infer1, Inference *infer2, SnapVector<int> *strengthened, unsigned idx) {
 254         if (idx == strengthened->size()) { // Ready to produce one weakened result
 255                 Inference *res = new Inference(tmpRes);
 256                 //model_print("Weakened inference:\n");
 257                 //res->print();
 258                 res->setShouldFix(false);
 259                 list->push_back(res);
 260                 return;
 261         }
 262
 263         int w = (*strengthened)[idx]; // The wildcard
 264         memory_order mo1 = (*infer1)[w];
 265         memory_order mo2 = (*infer2)[w];
 266         if (mo2 == WILDCARD_NONEXIST)
 267                 mo2 = memory_order_relaxed;
 268         memory_order weakenedMO = mo1;
 269         do {
 270                 (*tmpRes)[w] = weakenedMO;
 271                 getWeakerInferences(list, tmpRes, infer1, infer2,
 272                         strengthened, idx + 1);
 273                 if (weakenedMO == memory_order_acq_rel) {
 274                         (*tmpRes)[w] = memory_order_release;
 275                         getWeakerInferences(list, tmpRes, infer1, infer2,
 276                                 strengthened, idx + 1);
 277                 }
 278                 weakenedMO = nextWeakOrder(weakenedMO, mo2);
 279                 model_print("weakendedMO=%d\n", weakenedMO);
 280                 model_print("mo2=%d\n", mo2);
 281         } while (weakenedMO != mo2);
 282         (*tmpRes)[w] = weakenedMO;
 283         getWeakerInferences(list, tmpRes, infer1, infer2,
 284                 strengthened, idx + 1);
 285 }
 286
 287 memory_order& Inference::operator[](int idx) {
 288         if (idx > 0 && idx <= size)
 289                 return orders[idx];
 290         else {
 291                 resize(idx);
 292                 orders[idx] = WILDCARD_NONEXIST;
 293                 return orders[idx];
 294         }
 295 }
 296
 297 /** A simple overload, which allows caller to pass two boolean refrence, and
 298  * we will set those two variables indicating whether we can update the
 299  * order (copatible or not) and have updated the order */
 300 int Inference::strengthen(const ModelAction *act, memory_order mo, bool &canUpdate, bool &hasUpdated) {
 301         int res = strengthen(act, mo);
 302         if (res == -1)
 303                 canUpdate = false;
 304         if (res == 1)
 305                 hasUpdated = true;
 306
 307         return res;
 308 }
 309
 310 /** @Return:
 311         1 -> 'this> infer';
 312         -1 -> 'this < infer'
 313         0 -> 'this == infer'
 314         INFERENCE_INCOMPARABLE(x) -> true means incomparable
 315  */
 316 int Inference::compareTo(const Inference *infer) const {
 317         int result = size == infer->size ? 0 : (size > infer->size) ? 1 : -1;
 318         int smallerSize = size > infer->size ? infer->size : size;
 319         int subResult;
 320
 321         for (int i = 0; i <= smallerSize; i++) {
 322                 memory_order mo1 = orders[i],
 323                         mo2 = infer->orders[i];
 324                 if ((mo1 == memory_order_acquire && mo2 == memory_order_release) ||
 325                         (mo1 == memory_order_release && mo2 == memory_order_acquire)) {
 326                         // Incomparable
 327                         return -2;
 328                 } else {
 329                         if ((mo1 == WILDCARD_NONEXIST && mo2 != WILDCARD_NONEXIST)
 330                                 || (mo1 == WILDCARD_NONEXIST && mo2 == memory_order_relaxed)
 331                                 || (mo1 == memory_order_relaxed && mo2 == WILDCARD_NONEXIST)
 332                                 )
 333                                 subResult = 1;
 334                         else if (mo1 != WILDCARD_NONEXIST && mo2 == WILDCARD_NONEXIST)
 335                                 subResult = -1;
 336                         else
 337                                 subResult = mo1 > mo2 ? 1 : (mo1 == mo2) ? 0 : -1;
 338
 339                         if ((subResult > 0 && result < 0) || (subResult < 0 && result > 0)) {
 340                                 return -2;
 341                         }
 342                         if (subResult != 0)
 343                                 result = subResult;
 344                 }
 345         }
 346         return result;
 347 }
 348
 349 unsigned long Inference::getHash() {
 350         unsigned long hash = 0;
 351         for (int i = 1; i <= size; i++) {
 352                 memory_order mo = orders[i];
 353                 if (mo == WILDCARD_NONEXIST) {
 354                         mo = memory_order_relaxed;
 355                 }
 356                 hash *= 37;
 357                 hash += (mo + 4096);
 358         }
 359         return hash;
 360 }
 361
 362
 363 void Inference::print(bool hasHash) {
 364         ASSERT(size > 0 && size <= MAX_WILDCARD_NUM);
 365         for (int i = 1; i <= size; i++) {
 366                 memory_order mo = orders[i];
 367                 if (mo != WILDCARD_NONEXIST) {
 368                         // Print the wildcard inference result
 369                         FENCE_PRINT("wildcard %d -> memory_order_%s\n", i, get_mo_str(mo));
 370                 }
 371         }
 372         if (hasHash)
 373                 FENCE_PRINT("Hash: %lu\n", getHash());
 374 }
 375
 376 void Inference::print() {
 377         print(false);
 378 }