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

diff --git a/scfence/scgen.h b/scfence/scgen.h
new file mode 100644
index 0000000..a16e6b0
--- /dev/null
+++ b/scfence/scgen.h
@@ -0,0 +1,119 @@
+#ifndef _SCGEN_H
+#define _SCGEN_H
+
+#include "hashtable.h"
+#include "memoryorder.h"
+#include "action.h"
+#include "scanalysis.h"
+#include "model.h"
+#include "execution.h"
+#include "threads-model.h"
+#include "clockvector.h"
+#include "sc_annotation.h"
+
+#include <sys/time.h>
+
+typedef struct SCGeneratorOption {
+	bool print_always;
+	bool print_buggy;
+	bool print_nonsc;
+	bool annotationMode;
+} SCGeneratorOption;
+
+
+class SCGenerator {
+public:
+	SCGenerator();
+	~SCGenerator();
+
+	bool getCyclic();
+	SnapVector<action_list_t>* getDupThreadLists();
+
+	struct sc_statistics* getStats();
+
+	void setExecution(ModelExecution *execution);
+	void setActions(action_list_t *actions);
+	void setPrintAlways(bool val);
+	bool getPrintAlways();
+	bool getHasBadRF();
+
+	void setAnnotationMode(bool val);
+
+	void setPrintBuggy(bool val);
+	
+	void setPrintNonSC(bool val);
+
+	action_list_t * getSCList();
+	
+	HashTable<const ModelAction *, const ModelAction *, uintptr_t, 4> *getBadrfset();
+
+	HashTable<const ModelAction *, const ModelAction *, uintptr_t, 4 > *getAnnotatedReadSet();
+
+	void print_list(action_list_t *list);
+
+	SNAPSHOTALLOC
+private:
+	/********************** SC-related stuff (beginning) **********************/
+	ModelExecution *execution;
+
+	action_list_t *actions;
+
+	bool fastVersion;
+	bool allowNonSC;
+
+	action_list_t * generateSC(action_list_t *list);
+
+	void update_stats();
+
+	int buildVectors(SnapVector<action_list_t> *threadlist, int *maxthread,
+		action_list_t *list);
+
+	bool updateConstraints(ModelAction *act);
+
+	void computeCV(action_list_t *list);
+
+	bool processReadFast(ModelAction *read, ClockVector *cv);
+
+	bool processReadSlow(ModelAction *read, ClockVector *cv, bool *updateFuture);
+
+	bool processAnnotatedReadSlow(ModelAction *read, ClockVector *cv, bool *updateFuture);
+
+	int getNextActions(ModelAction **array);
+
+	bool merge(ClockVector *cv, const ModelAction *act, const ModelAction *act2);
+
+	void check_rf(action_list_t *list);
+	void check_rf1(action_list_t *list);
+	
+	void reset(action_list_t *list);
+	
+	ModelAction* pruneArray(ModelAction **array, int count);
+
+	/** This routine is operated based on the built threadlists */
+	void collectAnnotatedReads();
+
+	int maxthreads;
+	HashTable<const ModelAction *, ClockVector *, uintptr_t, 4 > cvmap;
+	bool cyclic;
+	HashTable<const ModelAction *, const ModelAction *, uintptr_t, 4 > badrfset;
+	HashTable<void *, const ModelAction *, uintptr_t, 4 > lastwrmap;
+	SnapVector<action_list_t> threadlists;
+	SnapVector<action_list_t> dup_threadlists;
+	bool print_always;
+	bool print_buggy;
+	bool print_nonsc;
+	bool hasBadRF;
+
+	struct sc_statistics *stats;
+
+	/** The set of read actions that are annotated to be special and will
+	 *  receive special treatment */
+	HashTable<const ModelAction *, const ModelAction *, uintptr_t, 4 > annotatedReadSet;
+	int annotatedReadSetSize;
+	bool annotationMode;
+	bool annotationError;
+
+	/** A set of actions that should be ignored in the partially SC analysis */
+	HashTable<const ModelAction*, const ModelAction*, uintptr_t, 4> ignoredActions;
+};
+#endif