X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=funcnode.h;h=b167e4a1e17ec850d59e6da7ebe1d9c83e98b930;hp=ffc56119d4897179066b1b72e97d16bcce4e88b3;hb=7719c6dc7e1a6dade8dfa022f3c9e19853f3e89f;hpb=acc3332c059d0dd7113409a1e3e4664eada0cec0

diff --git a/funcnode.h b/funcnode.h
index ffc56119..b167e4a1 100644
--- a/funcnode.h
+++ b/funcnode.h
@@ -9,6 +9,8 @@
 #define MAX_DIST 10
 
 typedef ModelList<FuncInst *> func_inst_list_mt;
+typedef ModelList<Predicate *> predicate_trace_t;
+
 typedef HashTable<void *, FuncInst *, uintptr_t, 0, model_malloc, model_calloc, model_free> loc_inst_map_t;
 typedef HashTable<FuncInst *, uint32_t, uintptr_t, 0, model_malloc, model_calloc, model_free> inst_id_map_t;
 typedef HashTable<FuncInst *, Predicate *, uintptr_t, 0, model_malloc, model_calloc, model_free> inst_pred_map_t;
@@ -32,7 +34,6 @@ public:
 	FuncInst * create_new_inst(ModelAction *act);
 	FuncInst * get_inst(ModelAction *act);
 
-	HashTable<const char *, FuncInst *, uintptr_t, 4, model_malloc, model_calloc, model_free> * getFuncInstMap() { return &func_inst_map; }
 	func_inst_list_mt * get_inst_list() { return &inst_list; }
 	func_inst_list_mt * get_entry_insts() { return &entry_insts; }
 	void add_entry_inst(FuncInst * inst);
@@ -41,30 +42,23 @@ public:
 	void function_exit_handler(thread_id_t tid);
 
 	void update_tree(ModelAction * act);
-	void update_inst_tree(func_inst_list_t * inst_list);
-	void update_predicate_tree(ModelAction * act);
-	bool follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act, Predicate ** unset_predicate);
-
-	uint32_t get_exit_count() { return exit_count; }
 
 	void add_to_val_loc_map(uint64_t val, void * loc);
 	void add_to_val_loc_map(value_set_t * values, void * loc);
 	void update_loc_may_equal_map(void * new_loc, loc_set_t * old_locations);
 
-	void set_predicate_tree_position(thread_id_t tid, Predicate * pred);
 	Predicate * get_predicate_tree_position(thread_id_t tid);
 
-	void init_inst_act_map(thread_id_t tid);
-	void reset_inst_act_map(thread_id_t tid);
-	void update_inst_act_map(thread_id_t tid, ModelAction * read_act);
-	inst_act_map_t * get_inst_act_map(thread_id_t tid);
+	void add_predicate_to_trace(thread_id_t tid, Predicate *pred);
+
+	uint32_t get_marker(thread_id_t tid);
+	int get_recursion_depth(thread_id_t tid);
+	uint64_t get_associated_read(thread_id_t tid, FuncInst * inst);
 
 	void add_out_edge(FuncNode * other);
 	ModelList<FuncNode *> * get_out_edges() { return &out_edges; }
 	int compute_distance(FuncNode * target, int max_step = MAX_DIST);
 
-	void add_failed_predicate(Predicate * pred);
-
 	void print_predicate_tree();
 
 	MEMALLOC
@@ -75,12 +69,12 @@ private:
 	Predicate * predicate_tree_entry;	// A dummy node whose children are the real entries
 	Predicate * predicate_tree_exit;	// A dummy node
 
-	uint32_t exit_count;
 	uint32_t inst_counter;
 	uint32_t marker;
-	ModelVector<uint32_t> thrd_marker;
+	ModelVector< ModelVector<uint32_t> *> thrd_markers;
+	ModelVector<int> thrd_recursion_depth;	// Recursion depth starts from 0 to match with vector indexes.
 
-	void set_marker(thread_id_t tid);
+	void init_marker(thread_id_t tid);
 
 	/* Use source line number as the key of hashtable, to check if
 	 * atomic operation with this line number has been added or not
@@ -94,16 +88,20 @@ private:
 	func_inst_list_mt entry_insts;
 
 	/* Map a FuncInst to the its predicate when updating predicate trees */
-	ModelVector<inst_pred_map_t *> thrd_inst_pred_map;
+	ModelVector< ModelVector<inst_pred_map_t *> * > thrd_inst_pred_maps;
 
 	/* Number FuncInsts to detect loops when updating predicate trees */
-	ModelVector<inst_id_map_t *> thrd_inst_id_map;
+	ModelVector< ModelVector<inst_id_map_t *> *> thrd_inst_id_maps;
 
-	/* Delect read actions at the same locations when updating predicate trees */
-	ModelVector<loc_inst_map_t *> thrd_loc_inst_map;
+	/* Detect read actions at the same locations when updating predicate trees */
+	ModelVector< ModelVector<loc_inst_map_t *> *> thrd_loc_inst_maps;
 
-	void init_maps(thread_id_t tid);
-	void reset_maps(thread_id_t tid);
+	void init_local_maps(thread_id_t tid);
+	void reset_local_maps(thread_id_t tid);
+
+	void update_inst_tree(func_inst_list_t * inst_list);
+	void update_predicate_tree(ModelAction * act);
+	bool follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act, Predicate ** unset_predicate);
 
 	void infer_predicates(FuncInst * next_inst, ModelAction * next_act, SnapVector<struct half_pred_expr *> * half_pred_expressions);
 	void generate_predicates(Predicate * curr_pred, FuncInst * next_inst, SnapVector<struct half_pred_expr *> * half_pred_expressions);
@@ -123,13 +121,16 @@ private:
 
 	// value_set_t * values_may_read_from;
 
-	/* Run-time position in the predicate tree for each thread */
-	ModelVector<Predicate *> predicate_tree_position;
+	/* Run-time position in the predicate tree for each thread
+	 * The inner vector is used to deal with recursive functions. */
+	ModelVector< ModelVector<Predicate *> * > thrd_predicate_tree_position;
+
+	ModelVector< ModelVector<predicate_trace_t *> * > thrd_predicate_trace;
+
+	void set_predicate_tree_position(thread_id_t tid, Predicate * pred);
 
-	PredSet predicate_leaves;
-	ModelVector<Predicate *> leaves_tmp_storage;
-	ModelVector<Predicate *> weight_debug_vec;
-	PredSet failed_predicates;
+	void init_predicate_tree_data_structure(thread_id_t tid);
+	void reset_predicate_tree_data_structure(thread_id_t tid);
 
 	/* Store the relation between this FuncNode and other FuncNodes */
 	HashTable<FuncNode *, edge_type_t, uintptr_t, 0, model_malloc, model_calloc, model_free> edge_table;
@@ -137,8 +138,7 @@ private:
 	/* FuncNodes that follow this node */
 	ModelList<FuncNode *> out_edges;
 
-	void assign_initial_weight();
-	void update_predicate_tree_weight();
+	void update_predicate_tree_weight(thread_id_t tid);
 };
 
 #endif	/* __FUNCNODE_H__ */