void ModelChecker::startChecker() {
startExecution(get_system_context(), runChecker);
+ snapshot_stack_init();
+ snapshot_record(0);
}
bool ModelChecker::should_terminate_execution()
else if (execution->isfeasibleprefix() && execution->have_fatal_bug_reports()) {
execution->set_assert();
return true;
+ } else if (execution->isFinished()) {
+ return true;
}
return false;
}
main_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()
{
* 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() && ((!(pending=thr->get_pending())) || is_nonsc_write(pending)) ) {
+ if (!thr->is_model_thread() && !thr->is_complete() && (!thr->get_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);
/* Have the trace analyses dump their output. */
for (unsigned int i = 0;i < trace_analyses.size();i++)
trace_analyses[i]->finish();
+
+ /* unlink tmp file created by last child process */
+ char filename[256];
+ snprintf_(filename, sizeof(filename), "C11FuzzerTmp%d", getpid());
+ unlink(filename);
}