scfence/inference.h

   1 #ifndef _INFERENCE_H
   2 #define _INFERENCE_H
   3
   4 #include "fence_common.h"
   5 #include "wildcard.h"
   6 #include "patch.h"
   7 #include "inferlist.h"
   8
   9 class InferenceList;
  10 class Inference;
  11
  12 extern const char* get_mo_str(memory_order order);
  13 extern bool isTheInference(Inference *infer);
  14
  15 class Inference {
  16         private:
  17         memory_order *orders;
  18         int size;
  19
  20         /** It's initial inference, if not assigned, set it as itself */
  21         Inference *initialInfer;
  22
  23         /** Whether this inference will lead to a buggy execution */
  24         bool buggy;
  25
  26         /** Whether this inference has been explored */
  27         bool explored;
  28
  29         /** Whether this inference is the leaf node in the inference lattice, see
  30          * inferset.h for more details */
  31         bool leaf;
  32
  33         /** When this inference will have buggy executions, this indicates whether
  34          * it has any fixes. */
  35         bool hasFixes;
  36
  37         /** When we have a strong enough inference, we also want to weaken specific
  38          *  parameters to see if it is possible to be weakened. So we will this
  39          *  field to mark if we should fix the inference or not if we get non-SC
  40          *  behaviros. By default true. */
  41         bool shouldFix;
  42
  43         void resize(int newsize);
  44
  45         /** Return the state of how we update a specific mo; If we have to make an
  46          * uncompatible inference or that inference cannot be imposed because it's
  47          * not a wildcard, it returns -1; if it is a compatible memory order but the
  48          * current memory order is no weaker than mo, it returns 0; otherwise, it
  49          * does strengthen the order, and returns 1 */
  50         int strengthen(const ModelAction *act, memory_order mo);
  51
  52         public:
  53         Inference();
  54
  55         Inference(Inference *infer);
  56
  57         /** return value:
  58           * 0 -> mo1 == mo2;
  59           * 1 -> mo1 stronger than mo2;
  60           * -1 -> mo1 weaker than mo2;
  61           * 2 -> mo1 & mo2 are uncomparable.
  62          */
  63         static int compareMemoryOrder(memory_order mo1, memory_order mo2);
  64
  65
  66         /** Try to calculate the set of inferences that are weaker than this, but
  67          *  still stronger than infer */
  68         InferenceList* getWeakerInferences(Inference *infer);
  69
  70         static memory_order nextWeakOrder(memory_order mo1, memory_order mo2);
  71
  72         void getWeakerInferences(InferenceList* list, Inference *tmpRes, Inference *infer1,
  73                 Inference *infer2, SnapVector<int> *strengthened, unsigned idx);
  74
  75         int getSize() {
  76                 return size;
  77         }
  78
  79         memory_order &operator[](int idx);
  80
  81         /** A simple overload, which allows caller to pass two boolean refrence, and
  82          * we will set those two variables indicating whether we can update the
  83          * order (copatible or not) and have updated the order */
  84         int strengthen(const ModelAction *act, memory_order mo, bool &canUpdate,
  85                 bool &hasUpdated);
  86
  87         /** @Return:
  88                 1 -> 'this> infer';
  89                 -1 -> 'this < infer'
  90                 0 -> 'this == infer'
  91                 INFERENCE_INCOMPARABLE(x) -> true means incomparable
  92          */
  93         int compareTo(const Inference *infer) const;
  94
  95         void setInitialInfer(Inference *val) {
  96                 initialInfer = val;
  97         }
  98
  99         Inference* getInitialInfer() {
 100                 return initialInfer;
 101         }
 102
 103         void setShouldFix(bool val) {
 104                 shouldFix = val;
 105         }
 106
 107         bool getShouldFix() {
 108                 return shouldFix;
 109         }
 110
 111         void setHasFixes(bool val) {
 112                 hasFixes = val;
 113         }
 114
 115         bool getHasFixes() {
 116                 return hasFixes;
 117         }
 118
 119         void setBuggy(bool val) {
 120                 buggy = val;
 121         }
 122
 123         bool getBuggy() {
 124                 return buggy;
 125         }
 126
 127         void setExplored(bool val) {
 128                 explored = val;
 129         }
 130
 131         bool isExplored() {
 132                 return explored;
 133         }
 134
 135         void setLeaf(bool val) {
 136                 leaf = val;
 137         }
 138
 139         bool isLeaf() {
 140                 return leaf;
 141         }
 142
 143         unsigned long getHash();
 144
 145         void print();
 146         void print(bool hasHash);
 147
 148         ~Inference() {
 149                 model_free(orders);
 150         }
 151
 152         MEMALLOC
 153 };
 154 #endif