{
memset(&stats,0,sizeof(struct execution_stats));
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
+#ifdef TLS
+ init_thread->setTLS((char *)get_tls_addr());
+#endif
execution->add_thread(init_thread);
scheduler->set_current_thread(init_thread);
execution->setParams(¶ms);
return execution->assert_bug(str);
}
-/**
- * @brief Assert a data race in the executing program.
- *
- * Different from assert_bug, the program will not be aborted immediately
- * upon calling this function, unless the number of data races exceeds
- * a threshold.
- *
- * @param msg Descriptive message for the bug (do not include newline char)
- * @return True if bug is immediately-feasible
- */
-bool ModelChecker::assert_race(const char *msg, ...)
-{
- char str[800];
-
- va_list ap;
- va_start(ap, msg);
- vsnprintf(str, sizeof(str), msg, ap);
- va_end(ap);
-
- return execution->assert_race(str);
-}
-
/**
* @brief Assert a bug in the executing program, asserted by a user thread
* @see ModelChecker::assert_bug
*/
uint64_t ModelChecker::switch_to_master(ModelAction *act)
{
- if (forklock) {
+ if (modellock) {
static bool fork_message_printed = false;
if (!fork_message_printed) {
- model_print("Fork handler trying to call into model checker...\n");
+ model_print("Fork handler or dead thread trying to call into model checker...\n");
fork_message_printed = true;
}
delete act;
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;
}
void ModelChecker::startMainThread() {
init_thread->set_state(THREAD_RUNNING);
scheduler->set_current_thread(init_thread);
- thread_startup();
+ main_thread_startup();
}
static bool is_nonsc_write(const ModelAction *act) {
* 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);