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)),
41 model_print("C11Tester\n"
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(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_roll_back(snapshot);
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 = take_snapshot();
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 /** @brief Run ModelChecker for the user program */
390 void ModelChecker::run()
392 //Need to initial random number generator state to avoid resets on rollback
393 char random_state[256];
394 initstate(423121, random_state, sizeof(random_state));
396 for(int exec = 0;exec < params.maxexecutions;exec++) {
397 Thread * t = init_thread;
401 * Stash next pending action(s) for thread(s). There
402 * should only need to stash one thread's action--the
403 * thread which just took a step--plus the first step
404 * for any newly-created thread
406 for (unsigned int i = 0;i < get_num_threads();i++) {
407 thread_id_t tid = int_to_id(i);
408 Thread *thr = get_thread(tid);
409 if (!thr->is_model_thread() && !thr->is_complete() && !thr->get_pending()) {
410 switch_from_master(thr);
411 if (thr->is_waiting_on(thr))
412 assert_bug("Deadlock detected (thread %u)", i);
416 /* Don't schedule threads which should be disabled */
417 for (unsigned int i = 0;i < get_num_threads();i++) {
418 Thread *th = get_thread(int_to_id(i));
419 ModelAction *act = th->get_pending();
420 if (act && execution->is_enabled(th) && !execution->check_action_enabled(act)) {
421 scheduler->sleep(th);
425 for (unsigned int i = 1;i < get_num_threads();i++) {
426 Thread *th = get_thread(int_to_id(i));
427 ModelAction *act = th->get_pending();
428 if (act && execution->is_enabled(th) && (th->get_state() != THREAD_BLOCKED) ) {
429 if (act->is_write()) {
430 std::memory_order order = act->get_mo();
431 if (order == std::memory_order_relaxed || \
432 order == std::memory_order_release) {
436 } else if (act->get_type() == THREAD_CREATE || \
437 act->get_type() == PTHREAD_CREATE || \
438 act->get_type() == THREAD_START || \
439 act->get_type() == THREAD_FINISH) {
446 /* Catch assertions from prior take_step or from
447 * between-ModelAction bugs (e.g., data races) */
449 if (execution->has_asserted())
452 t = get_next_thread();
453 if (!t || t->is_model_thread())
455 if (t->just_woken_up()) {
456 t->set_wakeup_state(false);
457 t->set_pending(NULL);
459 continue; // Allow this thread to stash the next pending action
462 /* Consume the next action for a Thread */
463 ModelAction *curr = t->get_pending();
464 t->set_pending(NULL);
465 t = execution->take_step(curr);
466 } while (!should_terminate_execution());
468 //restore random number generator state after rollback
469 setstate(random_state);
472 model_print("******* Model-checking complete: *******\n");
475 /* Have the trace analyses dump their output. */
476 for (unsigned int i = 0;i < trace_analyses.size();i++)
477 trace_analyses[i]->finish();
479 /* unlink tmp file created by last child process */
481 snprintf_(filename, sizeof(filename), "C11FuzzerTmp%d", getpid());