X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=funcnode.h;h=ffc56119d4897179066b1b72e97d16bcce4e88b3;hb=acc3332c059d0dd7113409a1e3e4664eada0cec0;hp=be0fdd86ceabd5311a376f2c7f590125082d68ce;hpb=9ecf77b2763e447363738b6453042982f787a184;p=c11tester.git

diff --git a/funcnode.h b/funcnode.h
index be0fdd86..ffc56119 100644
--- a/funcnode.h
+++ b/funcnode.h
@@ -9,7 +9,7 @@
 #define MAX_DIST 10
 
 typedef ModelList<FuncInst *> func_inst_list_mt;
-typedef HashTable<void *, ModelAction *, uintptr_t, 0, model_malloc, model_calloc, model_free> loc_act_map_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;
 
@@ -51,7 +51,6 @@ public:
 	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 init_predicate_tree_position(thread_id_t tid);
 	void set_predicate_tree_position(thread_id_t tid, Predicate * pred);
 	Predicate * get_predicate_tree_position(thread_id_t tid);
 
@@ -77,8 +76,11 @@ private:
 	Predicate * predicate_tree_exit;	// A dummy node
 
 	uint32_t exit_count;
-	uint32_t marker;
 	uint32_t inst_counter;
+	uint32_t marker;
+	ModelVector<uint32_t> thrd_marker;
+
+	void set_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
@@ -92,13 +94,13 @@ private:
 	func_inst_list_mt entry_insts;
 
 	/* Map a FuncInst to the its predicate when updating predicate trees */
-	SnapVector<inst_pred_map_t *> thrd_inst_pred_map;
+	ModelVector<inst_pred_map_t *> thrd_inst_pred_map;
 
 	/* Number FuncInsts to detect loops when updating predicate trees */
-	SnapVector<inst_id_map_t *> thrd_inst_id_map;
+	ModelVector<inst_id_map_t *> thrd_inst_id_map;
 
 	/* Delect read actions at the same locations when updating predicate trees */
-	SnapVector<loc_act_map_t *> thrd_loc_act_map;
+	ModelVector<loc_inst_map_t *> thrd_loc_inst_map;
 
 	void init_maps(thread_id_t tid);
 	void reset_maps(thread_id_t tid);