typedef SnapList<ModelAction *> action_list_t;
typedef SnapList<uint32_t> func_id_list_t;
typedef SnapList<FuncInst *> func_inst_list_t;
-typedef HSIterator<Predicate *, uintptr_t, 0, model_malloc, model_calloc, model_free> PredSetIter;
+
typedef HashSet<Predicate *, uintptr_t, 0, model_malloc, model_calloc, model_free> PredSet;
-typedef HSIterator<uint64_t, uint64_t, 0, model_malloc, model_calloc, model_free> write_set_iter;
-typedef HashSet<uint64_t, uint64_t, 0, model_malloc, model_calloc, model_free> write_set_t;
+typedef HSIterator<Predicate *, uintptr_t, 0, model_malloc, model_calloc, model_free> PredSetIter;
+
+typedef HashSet<uint64_t, uint64_t, 0, snapshot_malloc, snapshot_calloc, snapshot_free> value_set_t;
+typedef HSIterator<uint64_t, uint64_t, 0, snapshot_malloc, snapshot_calloc, snapshot_free> value_set_iter;
+typedef HashSet<void *, uintptr_t, 0, snapshot_malloc, snapshot_calloc, snapshot_free> loc_set_t;
+typedef HSIterator<void *, uintptr_t, 0, snapshot_malloc, snapshot_calloc, snapshot_free> loc_set_iter;
extern volatile int modellock;
#endif
FuncNode::FuncNode(ModelHistory * history) :
history(history),
predicate_tree_initialized(false),
- predicate_tree_entry(new Predicate(NULL, true)),
exit_count(0),
func_inst_map(),
inst_list(),
entry_insts(),
- thrd_read_map(),
+// thrd_read_map(),
action_list_buffer()
{
+ predicate_tree_entry = new Predicate(NULL, true);
predicate_tree_entry->add_predicate_expr(NOPREDICATE, NULL, true);
+
+ // memory will be reclaimed after each execution
+ read_locations = new loc_set_t();
+ val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0>();
}
void FuncNode::set_new_exec_flag()
{
- for (uint i = 0; i < thrd_read_map.size(); i++)
- thrd_read_map[i] = new read_map_t();
+// for (uint i = 0; i < thrd_read_map.size(); i++)
+// thrd_read_map[i] = new read_map_t();
for (mllnode<FuncInst *> * it = inst_list.begin(); it != NULL; it = it->getNext()) {
FuncInst * inst = it->getVal();
inst->reset_location();
}
+
+ read_locations = new loc_set_t();
+ val_loc_map = new HashTable<uint64_t, loc_set_t *, uint64_t, 0>();
}
/* Check whether FuncInst with the same type, position, and location
if (act_list == NULL || act_list->size() == 0)
return;
+ HashTable<void *, value_set_t *, uintptr_t, 4> * write_history = history->getWriteHistory();
+
/* build inst_list from act_list for later processing */
func_inst_list_t inst_list;
action_list_t read_act_list;
inst_list.push_back(func_inst);
- if (func_inst->is_read())
+ if (func_inst->is_read()) {
read_act_list.push_back(act);
+
+ /* the first time an action reads from some location, import all the values that have
+ * been written to this location from ModelHistory and notify ModelHistory that this
+ * FuncNode may read from this location.
+ */
+ void * loc = act->get_location();
+ if (!read_locations->contains(loc)) {
+ read_locations->add(loc);
+ value_set_t * write_values = write_history->get(loc);
+ add_to_val_loc_map(write_values, loc);
+ history->add_to_loc_func_nodes_map(loc, this);
+ }
+ }
}
// model_print("function %s\n", func_name);
* Store the values read by atomic read actions into thrd_read_map */
void FuncNode::store_read(ModelAction * act, uint32_t tid)
{
+/*
ASSERT(act);
void * location = act->get_location();
uint64_t read_from_val = act->get_reads_from_value();
- /* resize and initialize */
-
+ // resize and initialize
uint32_t old_size = thrd_read_map.size();
if (old_size <= tid) {
thrd_read_map.resize(tid + 1);
read_map_t * read_map = thrd_read_map[tid];
read_map->put(location, read_from_val);
-
- /* Store the memory locations where atomic reads happen */
- // read_locations.add(location);
+*/
}
uint64_t FuncNode::query_last_read(void * location, uint32_t tid)
{
+/*
if (thrd_read_map.size() <= tid)
return VALUE_NONE;
read_map_t * read_map = thrd_read_map[tid];
- /* last read value not found */
+ // last read value not found
if ( !read_map->contains(location) )
return VALUE_NONE;
uint64_t read_val = read_map->get(location);
return read_val;
+*/
}
/* @param tid thread id
*/
void FuncNode::clear_read_map(uint32_t tid)
{
+/*
if (thrd_read_map.size() <= tid)
return;
thrd_read_map[tid]->reset();
+*/
}
void FuncNode::update_predicate_tree(action_list_t * act_list)
return branch_found;
}
+void FuncNode::add_to_val_loc_map(uint64_t val, void * loc)
+{
+ loc_set_t * locations = val_loc_map->get(val);
+
+ if (locations == NULL) {
+ locations = new loc_set_t();
+ val_loc_map->put(val, locations);
+ }
+
+ locations->add(loc);
+
+/*
+ model_print("val %llx: ", val);
+ loc_set_iter * it = locations->iterator();
+ while (it->hasNext()) {
+ void * location = it->next();
+ model_print("%p ", location);
+ }
+ model_print("\n");
+*/
+}
+
+void FuncNode::add_to_val_loc_map(value_set_t * values, void * loc)
+{
+ value_set_iter * it = values->iterator();
+ while (it->hasNext()) {
+ uint64_t val = it->next();
+ add_to_val_loc_map(val, loc);
+ }
+}
+
+
void FuncNode::print_predicate_tree()
{
model_print("digraph function_%s {\n", func_name);
ModelList<action_list_t *> * get_action_list_buffer() { return &action_list_buffer; }
+ void add_to_val_loc_map(uint64_t val, void * loc);
+ void add_to_val_loc_map(value_set_t * values, void * loc);
+
void print_predicate_tree();
void print_last_read(uint32_t tid);
func_inst_list_mt entry_insts;
/* Store the values read by atomic read actions per memory location for each thread */
- ModelVector<read_map_t *> thrd_read_map;
+ //ModelVector<read_map_t *> thrd_read_map;
+ /* store action_lists when calls to update_tree are deferred */
ModelList<action_list_t *> action_list_buffer;
+
+ loc_set_t * read_locations;
+ HashTable<uint64_t, loc_set_t *, uint64_t, 0> * val_loc_map;
};
#endif /* __FUNCNODE_H__ */
func_map(),
func_map_rev(),
func_nodes(),
- write_history(),
- write_locations()
+ write_history(), // snapshot data structure
+ loc_func_nodes_map() // shapshot data structure
{}
void ModelHistory::enter_function(const uint32_t func_id, thread_id_t tid)
if (last_func_id == func_id) {
FuncNode * func_node = func_nodes[func_id];
- func_node->clear_read_map(tid);
+ //func_node->clear_read_map(tid);
action_list_t * curr_act_list = func_act_lists->back();
- func_node->incr_exit_count();
-
/* defer the processing of curr_act_list until the function has exits a few times
* (currently 2 times) so that more information can be gathered to infer nullity predicates.
*/
+ func_node->incr_exit_count();
if (func_node->get_exit_count() >= 2) {
ModelList<action_list_t *> * action_list_buffer = func_node->get_action_list_buffer();
while (action_list_buffer->size() > 0) {
uint32_t func_id = (*thrd_func_list)[id].back();
SnapList<action_list_t *> * func_act_lists = (*thrd_func_act_lists)[id];
- if (act->is_write())
+ if (act->is_write()) {
add_to_write_history(act->get_location(), act->get_write_value());
+
+ }
- if (func_id == 0)
+ /* the following does not care about actions without a position */
+ if (func_id == 0 || act->get_position() == NULL)
return;
- else if ( func_nodes.size() <= func_id )
+
+ if ( func_nodes.size() <= func_id )
resize_func_nodes( func_id + 1 );
FuncNode * func_node = func_nodes[func_id];
- /* do not care about actions without a position */
-
- if (act->get_position() == NULL)
- return;
-
- if (act->is_read())
- func_node->store_read(act, tid);
+// if (act->is_read())
+// func_node->store_read(act, tid);
/* add to curr_inst_list */
-
bool second_part_of_rmw = act->is_rmwc() || act->is_rmw();
if (!second_part_of_rmw) {
action_list_t * curr_act_list = func_act_lists->back();
ASSERT(curr_act_list != NULL);
- ModelAction * last_act;
+ ModelAction * last_act = NULL;
if (curr_act_list->size() != 0)
last_act = curr_act_list->back();
return func_nodes[func_id];
}
+/*
uint64_t ModelHistory::query_last_read(void * location, thread_id_t tid)
{
SnapVector<func_id_list_t> * thrd_func_list = model->get_execution()->get_thrd_func_list();
return last_read_val;
}
+*/
void ModelHistory::add_to_write_history(void * location, uint64_t write_val)
{
- write_set_t * write_set = write_history.get(location);
+ value_set_t * write_set = write_history.get(location);
if (write_set == NULL) {
- write_set = new write_set_t();
+ write_set = new value_set_t();
write_history.put(location, write_set);
}
write_set->add(write_val);
- write_locations.add(location);
+}
+
+void ModelHistory::add_to_loc_func_nodes_map(void * location, FuncNode * node)
+{
+ SnapList<FuncNode *> * func_node_list = loc_func_nodes_map.get(location);
+ if (func_node_list == NULL) {
+ func_node_list = new SnapList<FuncNode *>();
+ loc_func_nodes_map.put(location, func_node_list);
+ }
+
+ func_node_list->push_back(node);
}
void ModelHistory::set_new_exec_flag()
#include "hashset.h"
#include "threads-model.h"
-
class ModelHistory {
public:
ModelHistory();
ModelVector<FuncNode *> * getFuncNodes() { return &func_nodes; }
FuncNode * get_func_node(uint32_t func_id);
- uint64_t query_last_read(void * location, thread_id_t tid);
+// uint64_t query_last_read(void * location, thread_id_t tid);
void add_to_write_history(void * location, uint64_t write_val);
- HashTable<void *, write_set_t *, uintptr_t, 4> * getWriteHistory() { return &write_history; }
+ HashTable<void *, value_set_t *, uintptr_t, 4> * getWriteHistory() { return &write_history; }
+ void add_to_loc_func_nodes_map(void * location, FuncNode * node);
void set_new_exec_flag();
void print_write();
/* map function names to integer ids */
HashTable<const char *, uint32_t, uintptr_t, 4, model_malloc, model_calloc, model_free> func_map;
+
/* map integer ids to function names */
ModelVector<const char *> func_map_rev;
ModelVector<FuncNode *> func_nodes;
- HashTable<void *, write_set_t *, uintptr_t, 4> write_history;
- HashSet<void *, uintptr_t, 4> write_locations;
+ HashTable<void *, value_set_t *, uintptr_t, 4> write_history;
+ HashTable<void *, SnapList<FuncNode *> *, uintptr_t, 4> loc_func_nodes_map;
};
#endif /* __HISTORY_H__ */
inspect_plugin(NULL)
{
memset(&stats,0,sizeof(struct execution_stats));
- init_thread = new Thread(execution->get_next_id(), (thrd_t *) model_malloc(sizeof(thrd_t)), &user_main_wrapper, NULL, NULL); // L: user_main_wrapper passes the user program
+ init_thread = new Thread(execution->get_next_id(), (thrd_t *) model_malloc(sizeof(thrd_t)), &user_main_wrapper, NULL, NULL);
#ifdef TLS
init_thread->setTLS((char *)get_tls_addr());
#endif