+ 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);
+
+ /* 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();
+ delete iter;
+}
+
+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);
+ ((NewFuzzer *)execution->getFuzzer())->notify_paused_thread(thread);
+ }
+ }
+}
+
+bool ModelHistory::skip_action(ModelAction * act)
+{
+ 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;
+
+ /* Skip actions with the same sequence number */
+ if (last_action != NULL) {
+ if (last_action->get_seq_number() == curr_seq_number)
+ return true;
+ }