thrd_last_fence_release(),
node_stack(node_stack),
priv(new struct model_snapshot_members ()),
- mo_graph(new CycleGraph()),
+ mo_graph(new CycleGraph()),
fuzzer(new Fuzzer())
{
/* Initialize a model-checker thread, for special ModelActions */
get_thread(curr)->set_return_value(curr->get_return_value());
delete priorset;
if (canprune && curr->get_type() == ATOMIC_READ) {
- int tid = id_to_int(curr->get_tid());
- (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
+ int tid = id_to_int(curr->get_tid());
+ (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
}
return;
}
int tid = curr->get_tid();
ModelAction *prev_same_thread = NULL;
/* Iterate over all threads */
- for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0: tid + 1) {
+ for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
/* Last SC fence in thread tid */
ModelAction *last_sc_fence_thread_local = NULL;
if (i != 0)
//Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
if (prev_same_thread != NULL &&
- (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
- (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
- continue;
+ (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
+ (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
+ continue;
}
-
+
/* Iterate over actions in thread, starting from most recent */
action_list_t *list = &(*thrd_lists)[tid];
action_list_t::reverse_iterator rit;
* before" curr
*/
if (act->happens_before(curr)) {
- if (i==0) {
- if (last_sc_fence_local == NULL ||
- (*last_sc_fence_local < *prev_same_thread)) {
- prev_same_thread = act;
- }
- }
+ if (i==0) {
+ if (last_sc_fence_local == NULL ||
+ (*last_sc_fence_local < *prev_same_thread)) {
+ prev_same_thread = act;
+ }
+ }
if (act->is_write()) {
if (mo_graph->checkReachable(rf, act))
return false;
bugs->size(),
bugs->size() > 1 ? "s" : "");
for (unsigned int i = 0;i < bugs->size();i++)
- (*bugs)[i] -> print();
+ (*bugs)[i]->print();
}
/**
*/
void ModelChecker::record_stats()
{
- stats.num_total ++;
+ stats.num_total++;
if (!execution->isfeasibleprefix())
- stats.num_infeasible ++;
+ stats.num_infeasible++;
else if (execution->have_bug_reports())
- stats.num_buggy_executions ++;
+ stats.num_buggy_executions++;
else if (execution->is_complete_execution())
- stats.num_complete ++;
+ stats.num_complete++;
else {
- stats.num_redundant ++;
+ stats.num_redundant++;
/**
* @todo We can violate this ASSERT() when fairness/sleep sets
return true;
}
// test code
- execution_number ++;
+ execution_number++;
reset_to_initial_state();
node_stack->full_reset();
return false;
/** @brief Run trace analyses on complete trace */
void ModelChecker::run_trace_analyses() {
- for (unsigned int i = 0;i < trace_analyses.size();i ++)
- trace_analyses[i] -> analyze(execution->get_action_trace());
+ for (unsigned int i = 0;i < trace_analyses.size();i++)
+ trace_analyses[i]->analyze(execution->get_action_trace());
}
/**
char random_state[256];
initstate(423121, random_state, sizeof(random_state));
- for(int exec = 0;exec < params.maxexecutions;exec ++) {
+ for(int exec = 0;exec < params.maxexecutions;exec++) {
thrd_t user_thread;
Thread *t = new Thread(execution->get_next_id(), &user_thread, &user_main_wrapper, NULL, NULL); // L: user_main_wrapper passes the user program
execution->add_thread(t);