stats.num_buggy_executions++;
else if (is_complete_execution())
stats.num_complete++;
- else
+ else if (scheduler->all_threads_sleeping())
stats.num_redundant++;
+ else
+ ASSERT(false);
}
/** @brief Print execution stats */
write_thread = write_thread->get_parent();
struct future_value fv = {
- writer->get_value(),
+ writer->get_write_value(),
writer->get_seq_number() + params.maxfuturedelay,
write_thread->get_id(),
};
*/
bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
{
+ ASSERT(rf);
act->set_read_from(rf);
- if (rf != NULL && act->is_acquire()) {
+ if (act->is_acquire()) {
rel_heads_list_t release_heads;
get_release_seq_heads(act, act, &release_heads);
int num_heads = release_heads.size();
ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
- ModelAction *action = *it;
- if (action->is_read()) {
- fprintf(file, "N%u [label=\"N%u, T%u\"];\n", action->get_seq_number(), action->get_seq_number(), action->get_tid());
- if (action->get_reads_from() != NULL)
- fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
+ ModelAction *act = *it;
+ if (act->is_read()) {
+ mo_graph->dot_print_node(file, act);
+ if (act->get_reads_from())
+ mo_graph->dot_print_edge(file,
+ act->get_reads_from(),
+ act,
+ "label=\"rf\", color=red, weight=2");
+ else
+ mo_graph->dot_print_edge(file,
+ act->get_reads_from_promise(),
+ act,
+ "label=\"rf\", color=red");
}
- if (thread_array[action->get_tid()] != NULL) {
- fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
+ if (thread_array[act->get_tid()]) {
+ mo_graph->dot_print_edge(file,
+ thread_array[id_to_int(act->get_tid())],
+ act,
+ "label=\"sb\", color=blue, weight=400");
}
- thread_array[action->get_tid()] = action;
+ thread_array[act->get_tid()] = act;
}
fprintf(file, "}\n");
model_free(thread_array);
#endif
model_print("Execution %d:", stats.num_total);
- if (isfeasibleprefix())
+ if (isfeasibleprefix()) {
+ if (scheduler->all_threads_sleeping())
+ model_print(" SLEEP-SET REDUNDANT");
model_print("\n");
- else
+ } else
print_infeasibility(" INFEASIBLE");
print_list(action_trace);
model_print("\n");