11 #include "snapshot-interface.h"
14 #include "threads-model.h"
16 #include "traceanalysis.h"
17 #include "execution.h"
19 #include "bugmessage.h"
22 ModelChecker *model = NULL;
24 /** @brief Constructor */
25 ModelChecker::ModelChecker() :
26 /* Initialize default scheduler */
29 scheduler(new Scheduler()),
30 history(new ModelHistory()),
31 execution(new ModelExecution(this, scheduler)),
37 "Copyright (c) 2013 and 2019 Regents of the University of California. All rights reserved.\n"
38 "Distributed under the GPLv2\n"
39 "Written by Weiyu Luo, Brian Norris, and Brian Demsky\n\n");
40 memset(&stats,0,sizeof(struct execution_stats));
41 init_thread = new Thread(execution->get_next_id(), (thrd_t *) model_malloc(sizeof(thrd_t)), NULL, NULL, NULL);
43 init_thread->setTLS((char *)get_tls_addr());
45 execution->add_thread(init_thread);
46 scheduler->set_current_thread(init_thread);
48 execution->setParams(¶ms);
49 param_defaults(¶ms);
50 parse_options(¶ms);
52 /* Configure output redirection for the model-checker */
54 install_trace_analyses(model->get_execution());
57 /** @brief Destructor */
58 ModelChecker::~ModelChecker()
63 /** Method to set parameters */
64 model_params * ModelChecker::getParams() {
69 * Restores user program to initial state and resets all model-checker data
72 void ModelChecker::reset_to_initial_state()
76 * FIXME: if we utilize partial rollback, we will need to free only
77 * those pending actions which were NOT pending before the rollback
80 for (unsigned int i = 0;i < get_num_threads();i++)
81 delete get_thread(int_to_id(i))->get_pending();
83 snapshot_backtrack_before(0);
86 /** @return the number of user threads created during this execution */
87 unsigned int ModelChecker::get_num_threads() const
89 return execution->get_num_threads();
93 * Must be called from user-thread context (e.g., through the global
94 * thread_current() interface)
96 * @return The currently executing Thread.
98 Thread * ModelChecker::get_current_thread() const
100 return scheduler->get_current_thread();
104 * @brief Choose the next thread to execute.
106 * This function chooses the next thread that should execute. It can enforce
107 * execution replay/backtracking or, if the model-checker has no preference
108 * regarding the next thread (i.e., when exploring a new execution ordering),
109 * we defer to the scheduler.
111 * @return The next chosen thread to run, if any exist. Or else if the current
112 * execution should terminate, return NULL.
114 Thread * ModelChecker::get_next_thread()
118 * Have we completed exploring the preselected path? Then let the
121 return scheduler->select_next_thread();
125 * @brief Assert a bug in the executing program.
127 * Use this function to assert any sort of bug in the user program. If the
128 * current trace is feasible (actually, a prefix of some feasible execution),
129 * then this execution will be aborted, printing the appropriate message. If
130 * the current trace is not yet feasible, the error message will be stashed and
131 * printed if the execution ever becomes feasible.
133 * @param msg Descriptive message for the bug (do not include newline char)
134 * @return True if bug is immediately-feasible
136 void ModelChecker::assert_bug(const char *msg, ...)
142 vsnprintf(str, sizeof(str), msg, ap);
145 execution->assert_bug(str);
149 * @brief Assert a bug in the executing program, asserted by a user thread
150 * @see ModelChecker::assert_bug
151 * @param msg Descriptive message for the bug (do not include newline char)
153 void ModelChecker::assert_user_bug(const char *msg)
155 /* If feasible bug, bail out now */
157 switch_to_master(NULL);
160 /** @brief Print bug report listing for this execution (if any bugs exist) */
161 void ModelChecker::print_bugs() const
163 SnapVector<bug_message *> *bugs = execution->get_bugs();
165 model_print("Bug report: %zu bug%s detected\n",
167 bugs->size() > 1 ? "s" : "");
168 for (unsigned int i = 0;i < bugs->size();i++)
169 (*bugs)[i] -> print();
173 * @brief Record end-of-execution stats
175 * Must be run when exiting an execution. Records various stats.
176 * @see struct execution_stats
178 void ModelChecker::record_stats()
181 if (execution->have_bug_reports())
182 stats.num_buggy_executions ++;
183 else if (execution->is_complete_execution())
184 stats.num_complete ++;
186 //All threads are sleeping
188 * @todo We can violate this ASSERT() when fairness/sleep sets
189 * conflict to cause an execution to terminate, e.g. with:
190 * Scheduler: [0: disabled][1: disabled][2: sleep][3: current, enabled]
192 //ASSERT(scheduler->all_threads_sleeping());
196 /** @brief Print execution stats */
197 void ModelChecker::print_stats() const
199 model_print("Number of complete, bug-free executions: %d\n", stats.num_complete);
200 model_print("Number of buggy executions: %d\n", stats.num_buggy_executions);
201 model_print("Total executions: %d\n", stats.num_total);
205 * @brief End-of-exeuction print
206 * @param printbugs Should any existing bugs be printed?
208 void ModelChecker::print_execution(bool printbugs) const
210 model_print("Program output from execution %d:\n",
211 get_execution_number());
212 print_program_output();
214 if (params.verbose >= 3) {
218 /* Don't print invalid bugs */
219 if (printbugs && execution->have_bug_reports()) {
225 execution->print_summary();
229 * Queries the model-checker for more executions to explore and, if one
230 * exists, resets the model-checker state to execute a new execution.
232 * @return If there are more executions to explore, return true. Otherwise,
235 bool ModelChecker::next_execution()
238 /* Is this execution a feasible execution that's worth bug-checking? */
239 bool complete = (execution->is_complete_execution() ||
240 execution->have_bug_reports());
242 /* End-of-execution bug checks */
244 if (execution->is_deadlocked())
245 assert_bug("Deadlock detected");
247 run_trace_analyses();
252 if ( (complete && params.verbose) || params.verbose>1 || (complete && execution->have_bug_reports()))
253 print_execution(complete);
255 clear_program_output();
263 reset_to_initial_state();
264 history->set_new_exec_flag();
268 /** @brief Run trace analyses on complete trace */
269 void ModelChecker::run_trace_analyses() {
270 for (unsigned int i = 0;i < trace_analyses.size();i ++)
271 trace_analyses[i] -> analyze(execution->get_action_trace());
275 * @brief Get a Thread reference by its ID
276 * @param tid The Thread's ID
277 * @return A Thread reference
279 Thread * ModelChecker::get_thread(thread_id_t tid) const
281 return execution->get_thread(tid);
285 * @brief Get a reference to the Thread in which a ModelAction was executed
286 * @param act The ModelAction
287 * @return A Thread reference
289 Thread * ModelChecker::get_thread(const ModelAction *act) const
291 return execution->get_thread(act);
295 * Switch from a model-checker context to a user-thread context. This is the
296 * complement of ModelChecker::switch_to_master and must be called from the
297 * model-checker context
299 * @param thread The user-thread to switch to
301 void ModelChecker::switch_from_master(Thread *thread)
303 scheduler->set_current_thread(thread);
304 Thread::swap(&system_context, thread);
308 * Switch from a user-context to the "master thread" context (a.k.a. system
309 * context). This switch is made with the intention of exploring a particular
310 * model-checking action (described by a ModelAction object). Must be called
311 * from a user-thread context.
313 * @param act The current action that will be explored. May be NULL only if
314 * trace is exiting via an assertion (see ModelExecution::set_assert and
315 * ModelExecution::has_asserted).
316 * @return Return the value returned by the current action
318 uint64_t ModelChecker::switch_to_master(ModelAction *act)
321 static bool fork_message_printed = false;
323 if (!fork_message_printed) {
324 model_print("Fork handler or dead thread trying to call into model checker...\n");
325 fork_message_printed = true;
331 Thread *old = thread_current();
332 scheduler->set_current_thread(NULL);
333 ASSERT(!old->get_pending());
335 if (inspect_plugin != NULL) {
336 inspect_plugin->inspectModelAction(act);
339 old->set_pending(act);
340 if (Thread::swap(old, &system_context) < 0) {
341 perror("swap threads");
344 return old->get_return_value();
347 static void runChecker() {
352 void ModelChecker::startChecker() {
353 startExecution(get_system_context(), runChecker);
354 snapshot_stack_init();
358 bool ModelChecker::should_terminate_execution()
360 if (execution->have_bug_reports()) {
361 execution->set_assert();
363 } else if (execution->isFinished()) {
369 /** @brief Restart ModelChecker upon returning to the run loop of the
371 void ModelChecker::restart()
376 void ModelChecker::do_restart()
378 restart_flag = false;
379 reset_to_initial_state();
380 memset(&stats,0,sizeof(struct execution_stats));
381 execution_number = 1;
384 void ModelChecker::startMainThread() {
385 init_thread->set_state(THREAD_RUNNING);
386 scheduler->set_current_thread(init_thread);
387 main_thread_startup();
390 /** @brief Run ModelChecker for the user program */
391 void ModelChecker::run()
393 //Need to initial random number generator state to avoid resets on rollback
394 char random_state[256];
395 initstate(423121, random_state, sizeof(random_state));
397 for(int exec = 0;exec < params.maxexecutions;exec++) {
398 Thread * t = init_thread;
402 * Stash next pending action(s) for thread(s). There
403 * should only need to stash one thread's action--the
404 * thread which just took a step--plus the first step
405 * for any newly-created thread
407 for (unsigned int i = 0;i < get_num_threads();i++) {
408 thread_id_t tid = int_to_id(i);
409 Thread *thr = get_thread(tid);
410 if (!thr->is_model_thread() && !thr->is_complete() && !thr->get_pending()) {
411 switch_from_master(thr);
412 if (thr->is_waiting_on(thr))
413 assert_bug("Deadlock detected (thread %u)", i);
417 /* Don't schedule threads which should be disabled */
418 for (unsigned int i = 0;i < get_num_threads();i++) {
419 Thread *th = get_thread(int_to_id(i));
420 ModelAction *act = th->get_pending();
421 if (act && execution->is_enabled(th) && !execution->check_action_enabled(act)) {
422 scheduler->sleep(th);
426 for (unsigned int i = 1;i < get_num_threads();i++) {
427 Thread *th = get_thread(int_to_id(i));
428 ModelAction *act = th->get_pending();
429 if (act && execution->is_enabled(th) && (th->get_state() != THREAD_BLOCKED) ) {
430 if (act->is_write()) {
431 std::memory_order order = act->get_mo();
432 if (order == std::memory_order_relaxed || \
433 order == std::memory_order_release) {
437 } else if (act->get_type() == THREAD_CREATE || \
438 act->get_type() == PTHREAD_CREATE || \
439 act->get_type() == THREAD_START || \
440 act->get_type() == THREAD_FINISH) {
447 /* Catch assertions from prior take_step or from
448 * between-ModelAction bugs (e.g., data races) */
450 if (execution->has_asserted())
453 t = get_next_thread();
454 if (!t || t->is_model_thread())
456 if (t->just_woken_up()) {
457 t->set_wakeup_state(false);
458 t->set_pending(NULL);
460 continue; // Allow this thread to stash the next pending action
463 /* Consume the next action for a Thread */
464 ModelAction *curr = t->get_pending();
465 t->set_pending(NULL);
466 t = execution->take_step(curr);
467 } while (!should_terminate_execution());
469 //restore random number generator state after rollback
470 setstate(random_state);
473 model_print("******* Model-checking complete: *******\n");
476 /* Have the trace analyses dump their output. */
477 for (unsigned int i = 0;i < trace_analyses.size();i++)
478 trace_analyses[i]->finish();
480 /* unlink tmp file created by last child process */
482 snprintf_(filename, sizeof(filename), "C11FuzzerTmp%d", getpid());