+ 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)
+ return;
+
+ uint index = 0;
+ while (index < concrete_preds->size()) {
+ ConcretePredicate * concrete_pred = (*concrete_preds)[index];
+ SnapVector<struct concrete_pred_expr> * concrete_exprs = concrete_pred->getExpressions();
+ bool satisfy_predicate = true;
+ /* Check if the written value satisfies every predicate expression */
+ for (uint i = 0;i < concrete_exprs->size();i++) {
+ struct concrete_pred_expr concrete = (*concrete_exprs)[i];
+ bool equality = false;
+ switch (concrete.token) {
+ case EQUALITY:
+ equality = (value == concrete.value);
+ break;
+ case NULLITY:
+ equality = ((void*)value == NULL);
+ break;
+ default:
+ model_print("unknown predicate token");
+ break;
+ }
+
+ if (equality != concrete.equality) {
+ satisfy_predicate = false;
+ break;
+ }
+ }
+
+ if (satisfy_predicate) {
+ /* Wake up threads */
+ thread_id_t tid = concrete_pred->get_tid();
+ Thread * thread = model->get_thread(tid);
+
+ //model_print("** thread %d is woken up\n", thread->get_id());
+ ((NewFuzzer *)model->get_execution()->getFuzzer())->notify_paused_thread(thread);
+ }
+
+ index++;
+ }
+}
+
+WaitObj * ModelHistory::getWaitObj(thread_id_t tid)
+{
+ int thread_id = id_to_int(tid);
+ int old_size = thrd_wait_obj->size();
+ if (old_size <= thread_id) {
+ thrd_wait_obj->resize(thread_id + 1);
+ for (int i = old_size;i < thread_id + 1;i++) {
+ (*thrd_wait_obj)[i] = new WaitObj( int_to_id(i) );
+ }
+ }
+
+ return (*thrd_wait_obj)[thread_id];
+}
+
+void ModelHistory::add_waiting_thread(thread_id_t self_id,
+ thread_id_t waiting_for_id, FuncNode * target_node, int dist)
+{
+ WaitObj * self_wait_obj = getWaitObj(self_id);
+ self_wait_obj->add_waiting_for(waiting_for_id, target_node, dist);