+ 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;
+ 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) {
+ to_remove.push_back(concrete_pred);
+ }
+
+ index++;
+ }
+
+ for (uint i = 0; i < to_remove.size(); i++) {
+ ConcretePredicate * concrete_pred = to_remove[i];
+
+ /* 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());
+ model->get_execution()->getFuzzer()->notify_paused_thread(thread);
+ }
+}
+
+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);
+
+ /* Update waited-by relation */
+ WaitObj * other_wait_obj = getWaitObj(waiting_for_id);
+ other_wait_obj->add_waited_by(self_id);
+}
+
+/* Thread tid is woken up (or notified), so it is not waiting for others anymore */
+void ModelHistory::remove_waiting_thread(thread_id_t tid)
+{
+ WaitObj * self_wait_obj = getWaitObj(tid);
+ thrd_id_set_t * waiting_for = self_wait_obj->getWaitingFor();
+
+ /* Remove tid from waited_by's */
+ thrd_id_set_iter * iter = waiting_for->iterator();
+ while (iter->hasNext()) {
+ thread_id_t other_id = iter->next();
+ WaitObj * other_wait_obj = getWaitObj(other_id);
+ other_wait_obj->remove_waited_by(tid);
+ }
+
+ self_wait_obj->clear_waiting_for();
+}
+
+void ModelHistory::stop_waiting_for_node(thread_id_t self_id,
+ thread_id_t waiting_for_id, FuncNode * target_node)
+{
+ WaitObj * self_wait_obj = getWaitObj(self_id);
+ bool thread_removed = self_wait_obj->remove_waiting_for_node(waiting_for_id, target_node);
+
+ // model_print("\t%d gives up %d on node %d\n", self_id, waiting_for_id, target_node->get_func_id());
+
+ /* If thread self_id is not waiting for waiting_for_id anymore */
+ if (thread_removed) {
+ WaitObj * other_wait_obj = getWaitObj(waiting_for_id);
+ other_wait_obj->remove_waited_by(self_id);
+
+ thrd_id_set_t * self_waiting_for = self_wait_obj->getWaitingFor();
+ if ( self_waiting_for->isEmpty() ) {
+ // model_print("\tthread %d waits for nobody, wake up\n", self_id);
+ ModelExecution * execution = model->get_execution();
+ Thread * thread = execution->get_thread(self_id);
+ execution->getFuzzer()->notify_paused_thread(thread);
+ }
+ }
+}
+
+SnapVector<inst_act_map_t *> * ModelHistory::getThrdInstActMap(uint32_t func_id)
+{
+ ASSERT(func_id != 0);
+
+ SnapVector<inst_act_map_t *> * maps = func_inst_act_maps->get(func_id);
+ if (maps == NULL) {
+ maps = new SnapVector<inst_act_map_t *>();
+ func_inst_act_maps->put(func_id, maps);
+ }
+
+ return maps;
+}
+
+bool ModelHistory::skip_action(ModelAction * act, SnapList<ModelAction *> * curr_act_list)
+{
+ ASSERT(curr_act_list != NULL);
+
+ bool second_part_of_rmw = act->is_rmwc() || act->is_rmw();
+ modelclock_t curr_seq_number = act->get_seq_number();
+
+ /* Skip actions that are second part of a read modify write */
+ if (second_part_of_rmw)
+ return true;