X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=scfence%2Finferset.h;fp=scfence%2Finferset.h;h=965d2f9cff1cb4f5bc5b1acf1b152e0c63c646ba;hp=0000000000000000000000000000000000000000;hb=a65e234b607444355eb6e34097ee55ba93d4c01b;hpb=7c510878f9679da10de79c289df402356b092396

diff --git a/scfence/inferset.h b/scfence/inferset.h
new file mode 100644
index 0000000..965d2f9
--- /dev/null
+++ b/scfence/inferset.h
@@ -0,0 +1,147 @@
+#ifndef _INFERSET_H
+#define _INFERSET_H
+
+#include "fence_common.h"
+#include "patch.h"
+#include "inference.h"
+#include "inferlist.h"
+
+typedef struct inference_stat {
+	int notAddedAtFirstPlace;
+
+	inference_stat() :
+		notAddedAtFirstPlace(0) {}
+
+	void print() {
+		model_print("Inference process statistics output:...\n");
+		model_print("The number of inference not added at the first place: %d\n",
+			notAddedAtFirstPlace);
+	}
+} inference_stat_t;
+
+
+/** Essentially, we have to explore a big lattice of inferences, the bottom of
+ *  which is the inference that has all relaxed orderings, and the top of which
+ *  is the one that has all SC orderings. We define the partial ordering between
+ *  inferences as in compareTo() function in the Infereence class. In another
+ *  word, we compare ordering parameters one by one as a vector. Theoretically,
+ *  we need to explore up to the number of 5^N inferences, where N denotes the
+ *  number of wildcards (since we have 5 possible options for each memory order).
+
+ *  We try to reduce the searching space by recording whether an inference has
+ *  been discovered or not, and if so, we only need to explore from that
+ *  inference for just once. We can use a set to record the inferences to be be
+ *  explored, and insert new undiscovered fixes to that set iteratively until it
+ *  gets empty.
+
+ *  In detail, we use the InferenceList to represent that set, and use a
+ *  LIFO-like actions in pushing and popping inferences. When we add an
+ *  inference to the stack, we will set it to leaf or non-leaf node. For the
+ *  current inference to be added, it is non-leaf node because it generates
+ *  stronger inferences. On the other hands, for those generated inferences, we
+ *  set them to be leaf node. So when we pop a leaf node, we know that it is
+ *  not just discovered but thoroughly explored. Therefore, when we dicide
+ *  whether an inference is discovered, we can first try to look up the
+ *  discovered set and also derive those inferences that are stronger the
+ *  explored ones to be discovered.
+
+ ********** The main algorithm **********
+ Initial:
+ 	InferenceSet set; // Store the candiates to explore in a set
+	Set discoveredSet; // Store the discovered candidates. For each discovered
+		// candidate, if it's explored (feasible or infeasible, meaning that
+		// they are already known to work or not work), we set it to be
+		// explored. With that, we can reduce the searching space by ignoring
+		// those candidates that are stronger than the explored ones.
+	Inference curInfer = RELAX; // Initialize the current inference to be all relaxed (RELAX)
+
+ API Methods:
+ 	bool addInference(infer, bool isLeaf) {
+		// Push back infer to the discovered when it's not discvoerd, and return
+		// whether it's added or not
+	}
+	
+	void commitInference(infer, isFeasible) {
+		// Set the infer to be explored and add it to the result set if feasible 
+	}
+
+	Inference* getNextInference() {
+		// Get the next unexplored inference so that we can contine searching
+	}
+*/
+
+class InferenceSet {
+	private:
+
+	/** The set of already discovered nodes in the tree */
+	InferenceList *discoveredSet;
+
+	/** The list of feasible inferences */
+	InferenceList *results;
+
+	/** The set of candidates */
+	InferenceList *candidates;
+
+	/** The staticstics of inference process */
+	inference_stat_t stat;
+	
+	public:
+	InferenceSet();
+
+	/** Print the result of inferences  */
+	void printResults();
+
+	/** Print candidates of inferences */
+	void printCandidates();
+
+	/** When we finish model checking or cannot further strenghen with the
+	 * inference, we commit the inference to be explored; if it is feasible, we
+	 * put it in the result list */
+	void commitInference(Inference *infer, bool feasible);
+
+	int getCandidatesSize();
+
+	int getResultsSize();
+
+	/** Be careful that if the candidate is not added, it will be deleted in this
+	 *  function. Therefore, caller of this function should just delete the list when
+	 *  finishing calling this function. */
+	bool addCandidates(Inference *curInfer, InferenceList *inferList);
+
+
+	/** Check if we have stronger or equal inferences in the current result
+	 * list; if we do, we remove them and add the passed-in parameter infer */
+	 void addResult(Inference *infer);
+
+	/** Get the next available unexplored node; @Return NULL 
+	 * if we don't have next, meaning that we are done with exploring */
+	Inference* getNextInference();
+
+	/** Add the current inference to the set before adding fixes to it; in
+	 * this case, fixes will be added afterwards, and infer should've been
+	 * discovered */
+	void addCurInference(Inference *infer);
+	
+	/** Add one weaker node (the stronger one has been explored and known to be SC,
+	 *  we just want to know if a weaker one might also be SC).
+	 *  @Return true if the node to add has not been explored yet
+	 */
+	void addWeakerInference(Inference *curInfer);
+
+	/** Add one possible node that represents a fix for the current inference;
+	 * @Return true if the node to add has not been explored yet
+	 */
+	bool addInference(Inference *infer);
+
+	/** Return false if we haven't discovered that inference yet. Basically we
+	 * search the candidates list */
+	bool hasBeenDiscovered(Inference *infer);
+
+	/** Return true if we have explored this inference yet. Basically we
+	 * search the candidates list */
+	bool hasBeenExplored(Inference *infer);
+
+	MEMALLOC
+};
+
+#endif