+ if (curr_pred) {
+ // Follow child
+ curr_pred = curr_pred->follow_write_child(curr_inst);
+ }
+ func_node->set_predicate_tree_position(tid, curr_pred);
+ }
+}
+
+/* Return the FuncNode given its func_id */
+FuncNode * ModelHistory::get_func_node(uint32_t func_id)
+{
+ if (func_id == 0)
+ return NULL;
+
+ // This node has not been added to func_nodes
+ if (func_nodes.size() <= func_id)
+ return NULL;
+
+ return func_nodes[func_id];
+}
+
+/* Return the current FuncNode when given a thread id */
+FuncNode * ModelHistory::get_curr_func_node(thread_id_t tid)
+{
+ int thread_id = id_to_int(tid);
+ uint32_t func_id = (*thrd_func_list)[thread_id].back();
+
+ if (func_id != 0) {
+ return func_nodes[func_id];
+ }
+
+ return NULL;
+}
+
+void ModelHistory::update_write_history(void * location, uint64_t write_val)
+{
+ value_set_t * write_set = write_history->get(location);
+
+ if (write_set == NULL) {
+ write_set = new value_set_t();
+ write_history->put(location, write_set);
+ }
+
+ write_set->add(write_val);
+}
+
+void ModelHistory::update_loc_rd_func_nodes_map(void * location, FuncNode * node)
+{
+ SnapVector<FuncNode *> * func_node_list = getRdFuncNodes(location);
+ func_node_list->push_back(node);
+}
+
+void ModelHistory::update_loc_wr_func_nodes_map(void * location, FuncNode * node)
+{
+ SnapVector<FuncNode *> * func_node_list = getWrFuncNodes(location);
+ func_node_list->push_back(node);
+}
+
+SnapVector<FuncNode *> * ModelHistory::getRdFuncNodes(void * location)
+{
+ SnapVector<FuncNode *> * func_node_list = loc_rd_func_nodes_map->get(location);
+ if (func_node_list == NULL) {
+ func_node_list = new SnapVector<FuncNode *>();
+ loc_rd_func_nodes_map->put(location, func_node_list);
+ }
+
+ return func_node_list;
+}
+
+SnapVector<FuncNode *> * ModelHistory::getWrFuncNodes(void * location)
+{
+ SnapVector<FuncNode *> * func_node_list = loc_wr_func_nodes_map->get(location);
+ if (func_node_list == NULL) {
+ func_node_list = new SnapVector<FuncNode *>();
+ loc_wr_func_nodes_map->put(location, func_node_list);
+ }
+
+ return func_node_list;
+}
+
+/* When a thread is paused by Fuzzer, keep track of the condition it is waiting for */
+void ModelHistory::add_waiting_write(ConcretePredicate * concrete)
+{
+ void * location = concrete->get_location();
+ SnapVector<ConcretePredicate *> * waiting_conditions = loc_waiting_writes_map->get(location);
+ if (waiting_conditions == NULL) {
+ waiting_conditions = new SnapVector<ConcretePredicate *>();
+ loc_waiting_writes_map->put(location, waiting_conditions);
+ }
+
+ /* waiting_conditions should not have duplications */
+ waiting_conditions->push_back(concrete);
+
+ int thread_id = id_to_int(concrete->get_tid());
+ if (thrd_waiting_write->size() <= (uint) thread_id) {
+ thrd_waiting_write->resize(thread_id + 1);
+ }
+
+ (*thrd_waiting_write)[thread_id] = concrete;
+}
+
+void ModelHistory::remove_waiting_write(thread_id_t tid)
+{
+ ConcretePredicate * concrete = (*thrd_waiting_write)[ id_to_int(tid) ];
+ void * location = concrete->get_location();
+ SnapVector<ConcretePredicate *> * concrete_preds = loc_waiting_writes_map->get(location);
+
+ /* Linear search should be fine because presumably not many ConcretePredicates
+ * are at the same memory location */
+ for (uint i = 0;i < concrete_preds->size();i++) {
+ ConcretePredicate * current = (*concrete_preds)[i];
+ if (concrete == current) {
+ (*concrete_preds)[i] = concrete_preds->back();
+ concrete_preds->pop_back();
+ break;
+ }
+ }
+
+ int thread_id = id_to_int( concrete->get_tid() );
+ (*thrd_waiting_write)[thread_id] = NULL;
+ delete concrete;
+}
+
+/* Check if any other thread is waiting for this write action. If so, "notify" them */
+void ModelHistory::check_waiting_write(ModelAction * write_act)
+{
+ void * location = write_act->get_location();
+ uint64_t value = write_act->get_write_value();
+ SnapVector<ConcretePredicate *> * concrete_preds = loc_waiting_writes_map->get(location);
+ if (concrete_preds == NULL)