11 #include "snapshot-interface.h"
14 #include "threads-model.h"
16 #include "traceanalysis.h"
17 #include "execution.h"
19 #include "bugmessage.h"
23 ModelChecker *model = NULL;
25 void placeholder(void *) {
29 /** @brief Constructor */
30 ModelChecker::ModelChecker() :
31 /* Initialize default scheduler */
34 scheduler(new Scheduler()),
35 history(new ModelHistory()),
36 execution(new ModelExecution(this, scheduler)),
42 "Copyright (c) 2013 and 2019 Regents of the University of California. All rights reserved.\n"
43 "Distributed under the GPLv2\n"
44 "Written by Weiyu Luo, Brian Norris, and Brian Demsky\n\n");
45 memset(&stats,0,sizeof(struct execution_stats));
46 init_thread = new Thread(execution->get_next_id(), (thrd_t *) model_malloc(sizeof(thrd_t)), &placeholder, NULL, NULL);
48 init_thread->setTLS((char *)get_tls_addr());
50 execution->add_thread(init_thread);
51 scheduler->set_current_thread(init_thread);
53 execution->setParams(¶ms);
54 param_defaults(¶ms);
55 parse_options(¶ms);
57 /* Configure output redirection for the model-checker */
59 install_trace_analyses(model->get_execution());
62 /** @brief Destructor */
63 ModelChecker::~ModelChecker()
68 /** Method to set parameters */
69 model_params * ModelChecker::getParams() {
74 * Restores user program to initial state and resets all model-checker data
77 void ModelChecker::reset_to_initial_state()
81 * FIXME: if we utilize partial rollback, we will need to free only
82 * those pending actions which were NOT pending before the rollback
85 for (unsigned int i = 0;i < get_num_threads();i++)
86 delete get_thread(int_to_id(i))->get_pending();
88 snapshot_backtrack_before(0);
91 /** @return the number of user threads created during this execution */
92 unsigned int ModelChecker::get_num_threads() const
94 return execution->get_num_threads();
98 * Must be called from user-thread context (e.g., through the global
99 * thread_current() interface)
101 * @return The currently executing Thread.
103 Thread * ModelChecker::get_current_thread() const
105 return scheduler->get_current_thread();
109 * @brief Choose the next thread to execute.
111 * This function chooses the next thread that should execute. It can enforce
112 * execution replay/backtracking or, if the model-checker has no preference
113 * regarding the next thread (i.e., when exploring a new execution ordering),
114 * we defer to the scheduler.
116 * @return The next chosen thread to run, if any exist. Or else if the current
117 * execution should terminate, return NULL.
119 Thread * ModelChecker::get_next_thread()
123 * Have we completed exploring the preselected path? Then let the
126 return scheduler->select_next_thread();
130 * @brief Assert a bug in the executing program.
132 * Use this function to assert any sort of bug in the user program. If the
133 * current trace is feasible (actually, a prefix of some feasible execution),
134 * then this execution will be aborted, printing the appropriate message. If
135 * the current trace is not yet feasible, the error message will be stashed and
136 * printed if the execution ever becomes feasible.
138 * @param msg Descriptive message for the bug (do not include newline char)
139 * @return True if bug is immediately-feasible
141 void ModelChecker::assert_bug(const char *msg, ...)
147 vsnprintf(str, sizeof(str), msg, ap);
150 execution->assert_bug(str);
154 * @brief Assert a bug in the executing program, asserted by a user thread
155 * @see ModelChecker::assert_bug
156 * @param msg Descriptive message for the bug (do not include newline char)
158 void ModelChecker::assert_user_bug(const char *msg)
160 /* If feasible bug, bail out now */
162 switch_to_master(NULL);
165 /** @brief Print bug report listing for this execution (if any bugs exist) */
166 void ModelChecker::print_bugs() const
168 SnapVector<bug_message *> *bugs = execution->get_bugs();
170 model_print("Bug report: %zu bug%s detected\n",
172 bugs->size() > 1 ? "s" : "");
173 for (unsigned int i = 0;i < bugs->size();i++)
174 (*bugs)[i] -> print();
178 * @brief Record end-of-execution stats
180 * Must be run when exiting an execution. Records various stats.
181 * @see struct execution_stats
183 void ModelChecker::record_stats()
186 if (execution->have_bug_reports())
187 stats.num_buggy_executions ++;
188 else if (execution->is_complete_execution())
189 stats.num_complete ++;
191 //All threads are sleeping
193 * @todo We can violate this ASSERT() when fairness/sleep sets
194 * conflict to cause an execution to terminate, e.g. with:
195 * Scheduler: [0: disabled][1: disabled][2: sleep][3: current, enabled]
197 //ASSERT(scheduler->all_threads_sleeping());
201 /** @brief Print execution stats */
202 void ModelChecker::print_stats() const
204 model_print("Number of complete, bug-free executions: %d\n", stats.num_complete);
205 model_print("Number of buggy executions: %d\n", stats.num_buggy_executions);
206 model_print("Total executions: %d\n", stats.num_total);
210 * @brief End-of-exeuction print
211 * @param printbugs Should any existing bugs be printed?
213 void ModelChecker::print_execution(bool printbugs) const
215 model_print("Program output from execution %d:\n",
216 get_execution_number());
217 print_program_output();
219 if (params.verbose >= 3) {
223 /* Don't print invalid bugs */
224 if (printbugs && execution->have_bug_reports()) {
230 execution->print_summary();
234 * Queries the model-checker for more executions to explore and, if one
235 * exists, resets the model-checker state to execute a new execution.
237 * @return If there are more executions to explore, return true. Otherwise,
240 bool ModelChecker::next_execution()
243 /* Is this execution a feasible execution that's worth bug-checking? */
244 bool complete = (execution->is_complete_execution() ||
245 execution->have_bug_reports());
247 /* End-of-execution bug checks */
249 if (execution->is_deadlocked())
250 assert_bug("Deadlock detected");
252 run_trace_analyses();
257 if ( (complete && params.verbose) || params.verbose>1 || (complete && execution->have_bug_reports()))
258 print_execution(complete);
260 clear_program_output();
268 reset_to_initial_state();
269 history->set_new_exec_flag();
273 /** @brief Run trace analyses on complete trace */
274 void ModelChecker::run_trace_analyses() {
275 for (unsigned int i = 0;i < trace_analyses.size();i ++)
276 trace_analyses[i] -> analyze(execution->get_action_trace());
280 * @brief Get a Thread reference by its ID
281 * @param tid The Thread's ID
282 * @return A Thread reference
284 Thread * ModelChecker::get_thread(thread_id_t tid) const
286 return execution->get_thread(tid);
290 * @brief Get a reference to the Thread in which a ModelAction was executed
291 * @param act The ModelAction
292 * @return A Thread reference
294 Thread * ModelChecker::get_thread(const ModelAction *act) const
296 return execution->get_thread(act);
300 * Switch from a model-checker context to a user-thread context. This is the
301 * complement of ModelChecker::switch_to_master and must be called from the
302 * model-checker context
304 * @param thread The user-thread to switch to
306 void ModelChecker::switch_from_master(Thread *thread)
308 scheduler->set_current_thread(thread);
309 Thread::swap(&system_context, thread);
313 * Switch from a user-context to the "master thread" context (a.k.a. system
314 * context). This switch is made with the intention of exploring a particular
315 * model-checking action (described by a ModelAction object). Must be called
316 * from a user-thread context.
318 * @param act The current action that will be explored. May be NULL only if
319 * trace is exiting via an assertion (see ModelExecution::set_assert and
320 * ModelExecution::has_asserted).
321 * @return Return the value returned by the current action
323 uint64_t ModelChecker::switch_to_master(ModelAction *act)
326 static bool fork_message_printed = false;
328 if (!fork_message_printed) {
329 model_print("Fork handler or dead thread trying to call into model checker...\n");
330 fork_message_printed = true;
336 Thread *old = thread_current();
337 scheduler->set_current_thread(NULL);
338 ASSERT(!old->get_pending());
340 if (inspect_plugin != NULL) {
341 inspect_plugin->inspectModelAction(act);
344 old->set_pending(act);
345 if (Thread::swap(old, &system_context) < 0) {
346 perror("swap threads");
349 return old->get_return_value();
352 static void runChecker() {
357 void ModelChecker::startChecker() {
358 startExecution(get_system_context(), runChecker);
359 snapshot_stack_init();
363 bool ModelChecker::should_terminate_execution()
365 if (execution->have_bug_reports()) {
366 execution->set_assert();
368 } else if (execution->isFinished()) {
374 /** @brief Restart ModelChecker upon returning to the run loop of the
376 void ModelChecker::restart()
381 void ModelChecker::do_restart()
383 restart_flag = false;
384 reset_to_initial_state();
385 memset(&stats,0,sizeof(struct execution_stats));
386 execution_number = 1;
389 void ModelChecker::startMainThread() {
390 init_thread->set_state(THREAD_RUNNING);
391 scheduler->set_current_thread(init_thread);
392 main_thread_startup();
395 /** @brief Run ModelChecker for the user program */
396 void ModelChecker::run()
398 //Need to initial random number generator state to avoid resets on rollback
399 char random_state[256];
400 initstate(423121, random_state, sizeof(random_state));
402 for(int exec = 0;exec < params.maxexecutions;exec++) {
403 Thread * t = init_thread;
407 * Stash next pending action(s) for thread(s). There
408 * should only need to stash one thread's action--the
409 * thread which just took a step--plus the first step
410 * for any newly-created thread
412 for (unsigned int i = 0;i < get_num_threads();i++) {
413 thread_id_t tid = int_to_id(i);
414 Thread *thr = get_thread(tid);
415 if (!thr->is_model_thread() && !thr->is_complete() && !thr->get_pending()) {
416 switch_from_master(thr);
417 if (thr->is_waiting_on(thr))
418 assert_bug("Deadlock detected (thread %u)", i);
422 /* Don't schedule threads which should be disabled */
423 for (unsigned int i = 0;i < get_num_threads();i++) {
424 Thread *th = get_thread(int_to_id(i));
425 ModelAction *act = th->get_pending();
426 if (act && execution->is_enabled(th) && !execution->check_action_enabled(act)) {
427 scheduler->sleep(th);
431 for (unsigned int i = 1;i < get_num_threads();i++) {
432 Thread *th = get_thread(int_to_id(i));
433 ModelAction *act = th->get_pending();
434 if (act && execution->is_enabled(th) && (th->get_state() != THREAD_BLOCKED) ) {
435 if (act->is_write()) {
436 std::memory_order order = act->get_mo();
437 if (order == std::memory_order_relaxed || \
438 order == std::memory_order_release) {
442 } else if (act->get_type() == THREAD_CREATE || \
443 act->get_type() == PTHREAD_CREATE || \
444 act->get_type() == THREAD_START || \
445 act->get_type() == THREAD_FINISH) {
452 /* Catch assertions from prior take_step or from
453 * between-ModelAction bugs (e.g., data races) */
455 if (execution->has_asserted())
458 t = get_next_thread();
459 if (!t || t->is_model_thread())
461 if (t->just_woken_up()) {
462 t->set_wakeup_state(false);
463 t->set_pending(NULL);
465 continue; // Allow this thread to stash the next pending action
468 /* Consume the next action for a Thread */
469 ModelAction *curr = t->get_pending();
470 t->set_pending(NULL);
471 t = execution->take_step(curr);
472 } while (!should_terminate_execution());
474 //restore random number generator state after rollback
475 setstate(random_state);
478 model_print("******* Model-checking complete: *******\n");
481 /* Have the trace analyses dump their output. */
482 for (unsigned int i = 0;i < trace_analyses.size();i++)
483 trace_analyses[i]->finish();
485 /* unlink tmp file created by last child process */
487 snprintf_(filename, sizeof(filename), "C11FuzzerTmp%d", getpid());