#include <algorithm>
#include <mutex>
#include <new>
+#include <stdarg.h>
#include "model.h"
#include "action.h"
#include "datarace.h"
#include "threads-model.h"
#include "output.h"
+#include "traceanalysis.h"
#define INITIAL_THREAD_ID 0
thrd_last_action(new SnapVector<ModelAction *>(1)),
thrd_last_fence_release(new SnapVector<ModelAction *>()),
node_stack(new NodeStack()),
+ trace_analyses(new ModelVector<Trace_Analysis *>()),
priv(new struct model_snapshot_members()),
mo_graph(new CycleGraph())
{
delete thrd_last_action;
delete thrd_last_fence_release;
delete node_stack;
+ for (unsigned int i = 0; i < trace_analyses->size(); i++)
+ delete (*trace_analyses)[i];
+ delete trace_analyses;
delete scheduler;
delete mo_graph;
delete priv;
return tmp;
}
+action_list_t * ModelChecker::get_actions_on_obj(void * obj, thread_id_t tid) {
+ SnapVector<action_list_t> *wrv=obj_thrd_map->get(obj);
+ if (wrv==NULL)
+ return NULL;
+ unsigned int thread=id_to_int(tid);
+ if (thread < wrv->size())
+ return &(*wrv)[thread];
+ else
+ return NULL;
+}
+
+
/**
* Restores user program to initial state and resets all model-checker data
* structures.
* @param msg Descriptive message for the bug (do not include newline char)
* @return True if bug is immediately-feasible
*/
-bool ModelChecker::assert_bug(const char *msg)
+bool ModelChecker::assert_bug(const char *msg, ...)
{
- priv->bugs.push_back(new bug_message(msg));
+ char str[800];
+
+ va_list ap;
+ va_start(ap, msg);
+ vsnprintf(str, sizeof(str), msg, ap);
+ va_end(ap);
+
+ priv->bugs.push_back(new bug_message(str));
if (isfeasibleprefix()) {
set_assert();
assert_bug("Deadlock detected");
checkDataRaces();
+ run_trace_analyses();
}
record_stats();
return true;
}
+/** @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(action_trace);
+}
+
/**
* @brief Find the last fence-related backtracking conflict for a ModelAction
*
bool newly_explored = initialize_curr_action(&curr);
DBG();
- if (DBG_ENABLED())
- curr->print();
wake_up_sleeping_actions(curr);
}
/**
- * Updates the mo_graph with the constraints imposed from the current
+ * @brief Updates the mo_graph with the constraints imposed from the current
* read.
*
* Basic idea is the following: Go through each other thread and find
* the last action that happened before our read. Two cases:
*
- * (1) The action is a write => that write must either occur before
+ * -# The action is a write: that write must either occur before
* the write we read from or be the write we read from.
- *
- * (2) The action is a read => the write that that action read from
+ * -# The action is a read: the write that that action read from
* must occur before the write we read from or be the same write.
*
* @param curr The current action. Must be a read.
Thread *curr_thrd = get_thread(curr);
ASSERT(curr_thrd->get_state() == THREAD_READY);
- if (!check_action_enabled(curr)) {
- /* Make the execution look like we chose to run this action
- * much later, when a lock/join can succeed */
- get_thread(curr)->set_pending(curr);
- scheduler->sleep(curr_thrd);
- curr = NULL;
- } else {
- curr = check_current_action(curr);
- ASSERT(curr);
- }
+ ASSERT(check_action_enabled(curr)); /* May have side effects? */
+ curr = check_current_action(curr);
+ ASSERT(curr);
if (curr_thrd->is_blocked() || curr_thrd->is_complete())
scheduler->remove_thread(curr_thrd);
- if (curr)
- return action_select_next_thread(curr);
- return NULL;
+ return action_select_next_thread(curr);
}
/** Wrapper to run the user's main function, with appropriate arguments */
user_main(model->params.argc, model->params.argv);
}
+/** @return True if the execution has taken too many steps */
+bool ModelChecker::too_many_steps() const
+{
+ return params.bound != 0 && priv->used_sequence_numbers > params.bound;
+}
+
bool ModelChecker::should_terminate_execution()
{
/* Infeasible -> don't take any more steps */
return true;
}
- if (params.bound != 0 && priv->used_sequence_numbers > params.bound)
+ if (too_many_steps())
return true;
return false;
}
if (!thr->is_model_thread() && !thr->is_complete() && !thr->get_pending()) {
switch_from_master(thr);
if (thr->is_waiting_on(thr))
- assert_bug("Deadlock detected");
+ assert_bug("Deadlock detected (thread %u)", i);
+ }
+ }
+
+ /* Don't schedule threads which should be disabled */
+ for (unsigned int i = 0; i < get_num_threads(); i++) {
+ Thread *th = get_thread(int_to_id(i));
+ ModelAction *act = th->get_pending();
+ if (act && is_enabled(th) && !check_action_enabled(act)) {
+ scheduler->sleep(th);
}
}