#include "params.h"
ModelChecker *model = NULL;
-bool modelchecker_started = false;
/** Wrapper to run the user's main function, with appropriate arguments */
void user_main_wrapper(void *)
inspect_plugin(NULL)
{
memset(&stats,0,sizeof(struct execution_stats));
- init_thread = new Thread(execution->get_next_id(), (thrd_t *) malloc(sizeof(thrd_t)), &user_main_wrapper, NULL, NULL); // L: user_main_wrapper passes the user program
+ init_thread = new Thread(execution->get_next_id(), (thrd_t *) model_malloc(sizeof(thrd_t)), &user_main_wrapper, NULL, NULL); // L: user_main_wrapper passes the user program
execution->add_thread(init_thread);
scheduler->set_current_thread(init_thread);
execution->setParams(¶ms);
return old->get_return_value();
}
+static void runChecker() {
+ model->run();
+ delete model;
+}
+
+void ModelChecker::startChecker() {
+ startExecution(get_system_context(), runChecker);
+}
+
bool ModelChecker::should_terminate_execution()
{
/* Infeasible -> don't take any more steps */
execution_number = 1;
}
+void ModelChecker::startMainThread() {
+ init_thread->set_state(THREAD_RUNNING);
+ scheduler->set_current_thread(init_thread);
+ thread_startup();
+}
+
+static bool is_nonsc_write(const ModelAction *act) {
+ if (act->get_type() == ATOMIC_WRITE) {
+ std::memory_order order = act->get_mo();
+ switch(order) {
+ case std::memory_order_relaxed:
+ case std::memory_order_release:
+ return true;
+ default:
+ return false;
+ }
+ }
+ return false;
+}
+
/** @brief Run ModelChecker for the user program */
void ModelChecker::run()
{
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++) {
Thread * t = init_thread;
do {
* thread which just took a step--plus the first step
* for any newly-created thread
*/
-
+ ModelAction * pending;
for (unsigned int i = 0;i < get_num_threads();i++) {
thread_id_t tid = int_to_id(i);
Thread *thr = get_thread(tid);
- if (!thr->is_model_thread() && !thr->is_complete() && !thr->get_pending()) {
+ if (!thr->is_model_thread() && !thr->is_complete() && ((!(pending=thr->get_pending())) || is_nonsc_write(pending)) ) {
switch_from_master(thr); // L: context swapped, and action type of thr changed.
if (thr->is_waiting_on(thr))
assert_bug("Deadlock detected (thread %u)", i);