HashTable<FuncInst *, ModelAction *, uintptr_t, 0> * inst_act_map,
SnapVector<Predicate *> * unset_predicates)
{
- /* check if a branch with func_inst and corresponding predicate exists */
+ /* Check if a branch with func_inst and corresponding predicate exists */
bool branch_found = false;
ModelVector<Predicate *> * branches = (*curr_pred)->get_children();
for (uint i = 0; i < branches->size(); i++) {
/* Check against predicate expressions */
bool predicate_correct = true;
PredExprSet * pred_expressions = branch->get_pred_expressions();
+ PredExprSetIter * pred_expr_it = pred_expressions->iterator();
/* Only read and rmw actions my have unset predicate expressions */
if (pred_expressions->getSize() == 0) {
unset_predicates->push_back(branch);
}
- ConcretePredicate * concrete_pred = branch->evaluate(inst_act_map, next_act->get_tid());
- SnapVector<struct concrete_pred_expr> * concrete_exprs = concrete_pred->getExpressions();
- for (uint i = 0; i < concrete_exprs->size(); i++) {
- struct concrete_pred_expr concrete = (*concrete_exprs)[i];
- uint64_t next_read;
+ while (pred_expr_it->hasNext()) {
+ pred_expr * pred_expression = pred_expr_it->next();
+ uint64_t last_read, next_read;
bool equality;
- switch (concrete.token) {
+ switch(pred_expression->token) {
case NOPREDICATE:
predicate_correct = true;
break;
case EQUALITY:
+ FuncInst * to_be_compared;
+ ModelAction * last_act;
+
+ to_be_compared = pred_expression->func_inst;
+ last_act = inst_act_map->get(to_be_compared);
+
+ last_read = last_act->get_reads_from_value();
next_read = next_act->get_reads_from_value();
- equality = (next_read == concrete.value);
- if (equality != concrete.equality)
+ equality = (last_read == next_read);
+ if (equality != pred_expression->value)
predicate_correct = false;
+
break;
case NULLITY:
next_read = next_act->get_reads_from_value();
equality = ((void*)next_read == NULL);
- if (equality != concrete.equality)
+ if (equality != pred_expression->value)
predicate_correct = false;
break;
default:
break;
}
}
- delete concrete_pred;
if (predicate_correct) {
*curr_pred = branch;
// No write satisfies the selected predicate, so pause this thread.
while ( rf_set->size() == 0 ) {
Thread * read_thread = execution->get_thread(tid);
- model_print("the %d read action of thread %d at %p is unsuccessful\n", read->get_seq_number(), read_thread->get_id(), read->get_location());
+ //model_print("the %d read action of thread %d at %p is unsuccessful\n", read->get_seq_number(), read_thread->get_id(), read->get_location());
if (find_threads(read)) {
// reset thread pending action and revert sequence numbers
bool pruned = false;
uint index = 0;
- ConcretePredicate * concrete_pred = pred->evaluate(inst_act_map, tid);
- SnapVector<struct concrete_pred_expr> * concrete_exprs = concrete_pred->getExpressions();
-
while ( index < rf_set->size() ) {
ModelAction * write_act = (*rf_set)[index];
uint64_t write_val = write_act->get_write_value();
bool satisfy_predicate = true;
- for (uint i = 0; i < concrete_exprs->size(); i++) {
- struct concrete_pred_expr concrete = (*concrete_exprs)[i];
+ PredExprSetIter * pred_expr_it = pred_expressions->iterator();
+ while (pred_expr_it->hasNext()) {
+ struct pred_expr * expression = pred_expr_it->next();
bool equality;
- switch (concrete.token) {
+ switch (expression->token) {
case NOPREDICATE:
return false;
case EQUALITY:
- equality = (write_val == concrete.value);
- if (equality != concrete.equality)
+ FuncInst * to_be_compared;
+ ModelAction * last_act;
+ uint64_t last_read;
+
+ to_be_compared = expression->func_inst;
+ last_act = inst_act_map->get(to_be_compared);
+ last_read = last_act->get_reads_from_value();
+
+ equality = (write_val == last_read);
+ if (equality != expression->value)
satisfy_predicate = false;
break;
case NULLITY:
equality = ((void*)write_val == NULL);
- if (equality != concrete.equality)
+ if (equality != expression->value)
satisfy_predicate = false;
break;
default:
index++;
}
- delete concrete_pred;
-
return pruned;
}
history->remove_waiting_write(tid);
history->remove_waiting_thread(tid);
- model_print("thread %d is woken up\n", tid);
+ //model_print("thread %d is woken up\n", tid);
threadlist[*numthreads] = tid;
(*numthreads)++;
}
if (distance != -1) {
history->add_waiting_thread(self_id, tid, target_node, distance);
finds_waiting_for = true;
- model_print("thread: %d; distance from node %d to node %d: %d\n", tid, node->get_func_id(), target_node->get_func_id(), distance);
+ //model_print("thread: %d; distance from node %d to node %d: %d\n", tid, node->get_func_id(), target_node->get_func_id(), distance);
}
}
}