Fix snapshot code
[model-checker.git] / scfence / inferset.h
1 #ifndef _INFERSET_H
2 #define _INFERSET_H
3
4 #include "fence_common.h"
5 #include "patch.h"
6 #include "inference.h"
7 #include "inferlist.h"
8
9 typedef struct inference_stat {
10         int notAddedAtFirstPlace;
11
12         inference_stat() :
13                 notAddedAtFirstPlace(0) {}
14
15         void print() {
16                 model_print("Inference process statistics output:...\n");
17                 model_print("The number of inference not added at the first place: %d\n",
18                         notAddedAtFirstPlace);
19         }
20 } inference_stat_t;
21
22
23 /** Essentially, we have to explore a big lattice of inferences, the bottom of
24  *  which is the inference that has all relaxed orderings, and the top of which
25  *  is the one that has all SC orderings. We define the partial ordering between
26  *  inferences as in compareTo() function in the Infereence class. In another
27  *  word, we compare ordering parameters one by one as a vector. Theoretically,
28  *  we need to explore up to the number of 5^N inferences, where N denotes the
29  *  number of wildcards (since we have 5 possible options for each memory order).
30
31  *  We try to reduce the searching space by recording whether an inference has
32  *  been discovered or not, and if so, we only need to explore from that
33  *  inference for just once. We can use a set to record the inferences to be be
34  *  explored, and insert new undiscovered fixes to that set iteratively until it
35  *  gets empty.
36
37  *  In detail, we use the InferenceList to represent that set, and use a
38  *  LIFO-like actions in pushing and popping inferences. When we add an
39  *  inference to the stack, we will set it to leaf or non-leaf node. For the
40  *  current inference to be added, it is non-leaf node because it generates
41  *  stronger inferences. On the other hands, for those generated inferences, we
42  *  set them to be leaf node. So when we pop a leaf node, we know that it is
43  *  not just discovered but thoroughly explored. Therefore, when we dicide
44  *  whether an inference is discovered, we can first try to look up the
45  *  discovered set and also derive those inferences that are stronger the
46  *  explored ones to be discovered.
47
48  ********** The main algorithm **********
49  Initial:
50         InferenceSet set; // Store the candiates to explore in a set
51         Set discoveredSet; // Store the discovered candidates. For each discovered
52                 // candidate, if it's explored (feasible or infeasible, meaning that
53                 // they are already known to work or not work), we set it to be
54                 // explored. With that, we can reduce the searching space by ignoring
55                 // those candidates that are stronger than the explored ones.
56         Inference curInfer = RELAX; // Initialize the current inference to be all relaxed (RELAX)
57
58  API Methods:
59         bool addInference(infer, bool isLeaf) {
60                 // Push back infer to the discovered when it's not discvoerd, and return
61                 // whether it's added or not
62         }
63         
64         void commitInference(infer, isFeasible) {
65                 // Set the infer to be explored and add it to the result set if feasible 
66         }
67
68         Inference* getNextInference() {
69                 // Get the next unexplored inference so that we can contine searching
70         }
71 */
72
73 class InferenceSet {
74         private:
75
76         /** The set of already discovered nodes in the tree */
77         InferenceList *discoveredSet;
78
79         /** The list of feasible inferences */
80         InferenceList *results;
81
82         /** The set of candidates */
83         InferenceList *candidates;
84
85         /** The staticstics of inference process */
86         inference_stat_t stat;
87         
88         public:
89         InferenceSet();
90
91         /** Print the result of inferences  */
92         void printResults();
93
94         /** Print candidates of inferences */
95         void printCandidates();
96
97         /** When we finish model checking or cannot further strenghen with the
98          * inference, we commit the inference to be explored; if it is feasible, we
99          * put it in the result list */
100         void commitInference(Inference *infer, bool feasible);
101
102         int getCandidatesSize();
103
104         int getResultsSize();
105
106         /** Be careful that if the candidate is not added, it will be deleted in this
107          *  function. Therefore, caller of this function should just delete the list when
108          *  finishing calling this function. */
109         bool addCandidates(Inference *curInfer, InferenceList *inferList);
110
111
112         /** Check if we have stronger or equal inferences in the current result
113          * list; if we do, we remove them and add the passed-in parameter infer */
114          void addResult(Inference *infer);
115
116         /** Get the next available unexplored node; @Return NULL 
117          * if we don't have next, meaning that we are done with exploring */
118         Inference* getNextInference();
119
120         /** Add the current inference to the set before adding fixes to it; in
121          * this case, fixes will be added afterwards, and infer should've been
122          * discovered */
123         void addCurInference(Inference *infer);
124         
125         /** Add one weaker node (the stronger one has been explored and known to be SC,
126          *  we just want to know if a weaker one might also be SC).
127          *  @Return true if the node to add has not been explored yet
128          */
129         void addWeakerInference(Inference *curInfer);
130
131         /** Add one possible node that represents a fix for the current inference;
132          * @Return true if the node to add has not been explored yet
133          */
134         bool addInference(Inference *infer);
135
136         /** Return false if we haven't discovered that inference yet. Basically we
137          * search the candidates list */
138         bool hasBeenDiscovered(Inference *infer);
139
140         /** Return true if we have explored this inference yet. Basically we
141          * search the candidates list */
142         bool hasBeenExplored(Inference *infer);
143
144         MEMALLOC
145 };
146
147 #endif