4 #include "fence_common.h"
12 extern const char* get_mo_str(memory_order order);
13 extern bool isTheInference(Inference *infer);
20 /** It's initial inference, if not assigned, set it as itself */
21 Inference *initialInfer;
23 /** Whether this inference will lead to a buggy execution */
26 /** Whether this inference has been explored */
29 /** Whether this inference is the leaf node in the inference lattice, see
30 * inferset.h for more details */
33 /** When this inference will have buggy executions, this indicates whether
34 * it has any fixes. */
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. */
43 void resize(int newsize);
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);
55 Inference(Inference *infer);
59 * 1 -> mo1 stronger than mo2;
60 * -1 -> mo1 weaker than mo2;
61 * 2 -> mo1 & mo2 are uncomparable.
63 static int compareMemoryOrder(memory_order mo1, memory_order mo2);
66 /** Try to calculate the set of inferences that are weaker than this, but
67 * still stronger than infer */
68 InferenceList* getWeakerInferences(Inference *infer);
70 static memory_order nextWeakOrder(memory_order mo1, memory_order mo2);
72 void getWeakerInferences(InferenceList* list, Inference *tmpRes, Inference *infer1,
73 Inference *infer2, SnapVector<int> *strengthened, unsigned idx);
79 memory_order &operator[](int idx);
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,
91 INFERENCE_INCOMPARABLE(x) -> true means incomparable
93 int compareTo(const Inference *infer) const;
95 void setInitialInfer(Inference *val) {
99 Inference* getInitialInfer() {
103 void setShouldFix(bool val) {
107 bool getShouldFix() {
111 void setHasFixes(bool val) {
119 void setBuggy(bool val) {
127 void setExplored(bool val) {
135 void setLeaf(bool val) {
143 unsigned long getHash();
146 void print(bool hasHash);