model.cc

   1 #include <stdio.h>
   2 #include <algorithm>
   3 #include <new>
   4 #include <stdarg.h>
   5 #include <string.h>
   6 #include <cstdlib>
   7
   8 #include "model.h"
   9 #include "action.h"
  10 #include "schedule.h"
  11 #include "snapshot-interface.h"
  12 #include "common.h"
  13 #include "datarace.h"
  14 #include "threads-model.h"
  15 #include "output.h"
  16 #include "traceanalysis.h"
  17 #include "execution.h"
  18 #include "bugmessage.h"
  19 #include "params.h"
  20 #include "plugins.h"
  21
  22 ModelChecker *model = NULL;
  23 int inside_model = 0;
  24
  25 uint64_t get_nanotime()
  26 {
  27         struct timespec currtime;
  28         clock_gettime(CLOCK_MONOTONIC, &currtime);
  29
  30         return currtime.tv_nsec;
  31 }
  32
  33 void placeholder(void *) {
  34         ASSERT(0);
  35 }
  36
  37 #include <signal.h>
  38
  39 #define SIGSTACKSIZE 65536
  40 static void mprot_handle_pf(int sig, siginfo_t *si, void *unused)
  41 {
  42         model_print("Segmentation fault at %p\n", si->si_addr);
  43         model_print("For debugging, place breakpoint at: %s:%d\n",
  44                                                         __FILE__, __LINE__);
  45         print_trace();  // Trace printing may cause dynamic memory allocation
  46         while(1)
  47                 ;
  48 }
  49
  50 void install_handler() {
  51         stack_t ss;
  52         ss.ss_sp = model_malloc(SIGSTACKSIZE);
  53         ss.ss_size = SIGSTACKSIZE;
  54         ss.ss_flags = 0;
  55         sigaltstack(&ss, NULL);
  56         struct sigaction sa;
  57         sa.sa_flags = SA_SIGINFO | SA_NODEFER | SA_RESTART | SA_ONSTACK;
  58         sigemptyset(&sa.sa_mask);
  59         sa.sa_sigaction = mprot_handle_pf;
  60
  61         if (sigaction(SIGSEGV, &sa, NULL) == -1) {
  62                 perror("sigaction(SIGSEGV)");
  63                 exit(EXIT_FAILURE);
  64         }
  65 }
  66
  67 void createModelIfNotExist() {
  68         if (!model) {
  69                 ENTER_MODEL_FLAG;
  70                 snapshot_system_init(100000);
  71                 model = new ModelChecker();
  72                 model->startChecker();
  73                 EXIT_MODEL_FLAG;
  74         }
  75 }
  76
  77 /** @brief Constructor */
  78 ModelChecker::ModelChecker() :
  79         /* Initialize default scheduler */
  80         params(),
  81         scheduler(new Scheduler()),
  82         execution(new ModelExecution(this, scheduler)),
  83         execution_number(1),
  84         curr_thread_num(MAIN_THREAD_ID),
  85         trace_analyses(),
  86         inspect_plugin(NULL)
  87 {
  88         model_print("C11Tester\n"
  89                                                         "Copyright (c) 2013 and 2019 Regents of the University of California. All rights reserved.\n"
  90                                                         "Distributed under the GPLv2\n"
  91                                                         "Written by Weiyu Luo, Brian Norris, and Brian Demsky\n\n");
  92         init_memory_ops();
  93         real_memset(&stats,0,sizeof(struct execution_stats));
  94         init_thread = new Thread(execution->get_next_id(), (thrd_t *) model_malloc(sizeof(thrd_t)), &placeholder, NULL, NULL);
  95 #ifdef TLS
  96         init_thread->setTLS((char *)get_tls_addr());
  97 #endif
  98         execution->add_thread(init_thread);
  99         scheduler->set_current_thread(init_thread);
 100         register_plugins();
 101         execution->setParams(&params);
 102         param_defaults(&params);
 103         parse_options(&params);
 104         initRaceDetector();
 105         /* Configure output redirection for the model-checker */
 106         install_handler();
 107 }
 108
 109 /** @brief Destructor */
 110 ModelChecker::~ModelChecker()
 111 {
 112         delete scheduler;
 113 }
 114
 115 /** Method to set parameters */
 116 model_params * ModelChecker::getParams() {
 117         return &params;
 118 }
 119
 120 /**
 121  * Restores user program to initial state and resets all model-checker data
 122  * structures.
 123  */
 124 void ModelChecker::reset_to_initial_state()
 125 {
 126
 127         /**
 128          * FIXME: if we utilize partial rollback, we will need to free only
 129          * those pending actions which were NOT pending before the rollback
 130          * point
 131          */
 132         for (unsigned int i = 0;i < get_num_threads();i++)
 133                 delete get_thread(int_to_id(i))->get_pending();
 134
 135         snapshot_roll_back(snapshot);
 136 }
 137
 138 /** @return the number of user threads created during this execution */
 139 unsigned int ModelChecker::get_num_threads() const
 140 {
 141         return execution->get_num_threads();
 142 }
 143
 144 /**
 145  * Must be called from user-thread context (e.g., through the global
 146  * thread_current() interface)
 147  *
 148  * @return The currently executing Thread.
 149  */
 150 Thread * ModelChecker::get_current_thread() const
 151 {
 152         return scheduler->get_current_thread();
 153 }
 154
 155 /**
 156  * Must be called from user-thread context (e.g., through the global
 157  * thread_current_id() interface)
 158  *
 159  * @return The id of the currently executing Thread.
 160  */
 161 thread_id_t ModelChecker::get_current_thread_id() const
 162 {
 163         ASSERT(int_to_id(curr_thread_num) == get_current_thread()->get_id());
 164         return int_to_id(curr_thread_num);
 165 }
 166
 167 /**
 168  * @brief Choose the next thread to execute.
 169  *
 170  * This function chooses the next thread that should execute. It can enforce
 171  * execution replay/backtracking or, if the model-checker has no preference
 172  * regarding the next thread (i.e., when exploring a new execution ordering),
 173  * we defer to the scheduler.
 174  *
 175  * @return The next chosen thread to run, if any exist. Or else if the current
 176  * execution should terminate, return NULL.
 177  */
 178 Thread * ModelChecker::get_next_thread()
 179 {
 180
 181         /*
 182          * Have we completed exploring the preselected path? Then let the
 183          * scheduler decide
 184          */
 185         return scheduler->select_next_thread();
 186 }
 187
 188 /**
 189  * @brief Assert a bug in the executing program.
 190  *
 191  * Use this function to assert any sort of bug in the user program. If the
 192  * current trace is feasible (actually, a prefix of some feasible execution),
 193  * then this execution will be aborted, printing the appropriate message. If
 194  * the current trace is not yet feasible, the error message will be stashed and
 195  * printed if the execution ever becomes feasible.
 196  *
 197  * @param msg Descriptive message for the bug (do not include newline char)
 198  * @return True if bug is immediately-feasible
 199  */
 200 void ModelChecker::assert_bug(const char *msg, ...)
 201 {
 202         char str[800];
 203
 204         va_list ap;
 205         va_start(ap, msg);
 206         vsnprintf(str, sizeof(str), msg, ap);
 207         va_end(ap);
 208
 209         execution->assert_bug(str);
 210 }
 211
 212 /**
 213  * @brief Assert a bug in the executing program, asserted by a user thread
 214  * @see ModelChecker::assert_bug
 215  * @param msg Descriptive message for the bug (do not include newline char)
 216  */
 217 void ModelChecker::assert_user_bug(const char *msg)
 218 {
 219         /* If feasible bug, bail out now */
 220         assert_bug(msg);
 221         switch_thread(NULL);
 222 }
 223
 224 /** @brief Print bug report listing for this execution (if any bugs exist) */
 225 void ModelChecker::print_bugs() const
 226 {
 227         SnapVector<bug_message *> *bugs = execution->get_bugs();
 228
 229         model_print("Bug report: %zu bug%s detected\n",
 230                                                         bugs->size(),
 231                                                         bugs->size() > 1 ? "s" : "");
 232         for (unsigned int i = 0;i < bugs->size();i++)
 233                 (*bugs)[i] -> print();
 234 }
 235
 236 /**
 237  * @brief Record end-of-execution stats
 238  *
 239  * Must be run when exiting an execution. Records various stats.
 240  * @see struct execution_stats
 241  */
 242 void ModelChecker::record_stats()
 243 {
 244         stats.num_total ++;
 245         if (execution->have_bug_reports())
 246                 stats.num_buggy_executions ++;
 247         else if (execution->is_complete_execution())
 248                 stats.num_complete ++;
 249         else {
 250                 //All threads are sleeping
 251                 /**
 252                  * @todo We can violate this ASSERT() when fairness/sleep sets
 253                  * conflict to cause an execution to terminate, e.g. with:
 254                  * Scheduler: [0: disabled][1: disabled][2: sleep][3: current, enabled]
 255                  */
 256                 //ASSERT(scheduler->all_threads_sleeping());
 257         }
 258 }
 259
 260 /** @brief Print execution stats */
 261 void ModelChecker::print_stats() const
 262 {
 263         model_print("Number of complete, bug-free executions: %d\n", stats.num_complete);
 264         model_print("Number of buggy executions: %d\n", stats.num_buggy_executions);
 265         model_print("Total executions: %d\n", stats.num_total);
 266 }
 267
 268 /**
 269  * @brief End-of-exeuction print
 270  * @param printbugs Should any existing bugs be printed?
 271  */
 272 void ModelChecker::print_execution(bool printbugs) const
 273 {
 274         model_print("Program output from execution %d:\n",
 275                                                         get_execution_number());
 276         print_program_output();
 277
 278         if (params.verbose >= 3) {
 279                 print_stats();
 280         }
 281
 282         /* Don't print invalid bugs */
 283         if (printbugs && execution->have_bug_reports()) {
 284                 model_print("\n");
 285                 print_bugs();
 286         }
 287
 288         model_print("\n");
 289 #ifdef PRINT_TRACE
 290         execution->print_summary();
 291 #endif
 292 }
 293
 294 /**
 295  * Queries the model-checker for more executions to explore and, if one
 296  * exists, resets the model-checker state to execute a new execution.
 297  *
 298  * @return If there are more executions to explore, return true. Otherwise,
 299  * return false.
 300  */
 301 void ModelChecker::finish_execution(bool more_executions)
 302 {
 303         DBG();
 304         /* Is this execution a feasible execution that's worth bug-checking? */
 305         bool complete = (execution->is_complete_execution() ||
 306                                                                          execution->have_bug_reports());
 307
 308         /* End-of-execution bug checks */
 309         if (complete) {
 310                 if (execution->is_deadlocked())
 311                         assert_bug("Deadlock detected");
 312
 313                 run_trace_analyses();
 314         }
 315
 316         record_stats();
 317         /* Output */
 318         if ( (complete && params.verbose) || params.verbose>1 || (complete && execution->have_bug_reports()))
 319                 print_execution(complete);
 320         else
 321                 clear_program_output();
 322
 323         execution_number ++;
 324
 325         if (more_executions)
 326                 reset_to_initial_state();
 327 }
 328
 329 /** @brief Run trace analyses on complete trace */
 330 void ModelChecker::run_trace_analyses() {
 331         for (unsigned int i = 0;i < trace_analyses.size();i ++)
 332                 trace_analyses[i] -> analyze(execution->get_action_trace());
 333 }
 334
 335 /**
 336  * @brief Get a Thread reference by its ID
 337  * @param tid The Thread's ID
 338  * @return A Thread reference
 339  */
 340 Thread * ModelChecker::get_thread(thread_id_t tid) const
 341 {
 342         return execution->get_thread(tid);
 343 }
 344
 345 /**
 346  * @brief Get a reference to the Thread in which a ModelAction was executed
 347  * @param act The ModelAction
 348  * @return A Thread reference
 349  */
 350 Thread * ModelChecker::get_thread(const ModelAction *act) const
 351 {
 352         return execution->get_thread(act);
 353 }
 354
 355 void ModelChecker::startRunExecution(Thread *old) {
 356         while (true) {
 357                 if (params.traceminsize != 0 &&
 358                                 execution->get_curr_seq_num() > checkfree) {
 359                         checkfree += params.checkthreshold;
 360                         execution->collectActions();
 361                 }
 362
 363                 curr_thread_num = MAIN_THREAD_ID;
 364                 Thread *thr = getNextThread(old);
 365                 if (thr != nullptr) {
 366                         scheduler->set_current_thread(thr);
 367                         EXIT_MODEL_FLAG;
 368                         if (Thread::swap(old, thr) < 0) {
 369                                 perror("swap threads");
 370                                 exit(EXIT_FAILURE);
 371                         }
 372                         return;
 373                 }
 374
 375                 if (!handleChosenThread(old)) {
 376                         return;
 377                 }
 378         }
 379 }
 380
 381 Thread* ModelChecker::getNextThread(Thread *old)
 382 {
 383         Thread *nextThread = nullptr;
 384         for (unsigned int i = curr_thread_num;i < get_num_threads();i++) {
 385                 thread_id_t tid = int_to_id(i);
 386                 Thread *thr = get_thread(tid);
 387
 388                 if (!thr->is_complete()) {
 389                         if (!thr->get_pending()) {
 390                                 curr_thread_num = i;
 391                                 nextThread = thr;
 392                                 break;
 393                         }
 394                 } else if (thr != old && !thr->is_freed()) {
 395                         thr->freeResources();
 396                 }
 397
 398                 ModelAction *act = thr->get_pending();
 399                 if (act && scheduler->is_enabled(tid)){
 400                         /* Don't schedule threads which should be disabled */
 401                         if (!execution->check_action_enabled(act)) {
 402                                 scheduler->sleep(thr);
 403                         }
 404
 405                         /* Allow pending relaxed/release stores or thread actions to perform first */
 406                         else if (!chosen_thread) {
 407                                 if (act->is_write()) {
 408                                         std::memory_order order = act->get_mo();
 409                                         if (order == std::memory_order_relaxed || \
 410                                                         order == std::memory_order_release) {
 411                                                 chosen_thread = thr;
 412                                         }
 413                                 } else if (act->get_type() == THREAD_CREATE || \
 414                                                                          act->get_type() == PTHREAD_CREATE || \
 415                                                                          act->get_type() == THREAD_START || \
 416                                                                          act->get_type() == THREAD_FINISH) {
 417                                         chosen_thread = thr;
 418                                 }
 419                         }
 420                 }
 421         }
 422         return nextThread;
 423 }
 424
 425 /* Swap back to system_context and terminate this execution */
 426 void ModelChecker::finishRunExecution(Thread *old)
 427 {
 428         scheduler->set_current_thread(NULL);
 429
 430         /** Reset curr_thread_num to initial value for next execution. */
 431         curr_thread_num = MAIN_THREAD_ID;
 432
 433         /** If we have more executions, we won't make it past this call. */
 434         finish_execution(execution_number < params.maxexecutions);
 435
 436
 437         /** We finished the final execution.  Print stuff and exit. */
 438         model_print("******* Model-checking complete: *******\n");
 439         print_stats();
 440
 441         /* Have the trace analyses dump their output. */
 442         for (unsigned int i = 0;i < trace_analyses.size();i++)
 443                 trace_analyses[i]->finish();
 444
 445         /* unlink tmp file created by last child process */
 446         char filename[256];
 447         snprintf_(filename, sizeof(filename), "C11FuzzerTmp%d", getpid());
 448         unlink(filename);
 449
 450         /* Exit. */
 451         _Exit(0);
 452 }
 453
 454 uint64_t ModelChecker::switch_thread(ModelAction *act)
 455 {
 456         if (modellock) {
 457                 static bool fork_message_printed = false;
 458
 459                 if (!fork_message_printed) {
 460                         model_print("Fork handler or dead thread trying to call into model checker...\n");
 461                         fork_message_printed = true;
 462                 }
 463                 delete act;
 464                 return 0;
 465         }
 466         ENTER_MODEL_FLAG;
 467
 468         DBG();
 469         Thread *old = thread_current();
 470         old->set_state(THREAD_READY);
 471
 472         ASSERT(!old->get_pending());
 473
 474         if (inspect_plugin != NULL) {
 475                 inspect_plugin->inspectModelAction(act);
 476         }
 477
 478         old->set_pending(act);
 479
 480         if (old->is_waiting_on(old))
 481                 assert_bug("Deadlock detected (thread %u)", curr_thread_num);
 482
 483         Thread* next = getNextThread(old);
 484         if (next != nullptr) {
 485                 scheduler->set_current_thread(next);
 486                 if (Thread::swap(old, next) < 0) {
 487                         perror("swap threads");
 488                         exit(EXIT_FAILURE);
 489                 }
 490         } else {
 491                 if (handleChosenThread(old)) {
 492                         startRunExecution(old);
 493                 }
 494         }
 495         return old->get_return_value();
 496 }
 497
 498 bool ModelChecker::handleChosenThread(Thread *old)
 499 {
 500         if (execution->has_asserted()) {
 501                 finishRunExecution(old);
 502                 return false;
 503         }
 504         if (!chosen_thread) {
 505                 chosen_thread = get_next_thread();
 506         }
 507         if (!chosen_thread) {
 508                 finishRunExecution(old);
 509                 return false;
 510         }
 511         if (chosen_thread->just_woken_up()) {
 512                 chosen_thread->set_wakeup_state(false);
 513                 chosen_thread->set_pending(NULL);
 514                 chosen_thread = NULL;
 515                 // Allow this thread to stash the next pending action
 516                 return true;
 517         }
 518
 519         // Consume the next action for a Thread
 520         ModelAction *curr = chosen_thread->get_pending();
 521         chosen_thread->set_pending(NULL);
 522         chosen_thread = execution->take_step(curr);
 523
 524         if (should_terminate_execution()) {
 525                 finishRunExecution(old);
 526                 return false;
 527         } else {
 528                 return true;
 529         }
 530 }
 531
 532 void ModelChecker::startChecker() {
 533         startExecution();
 534         //Need to initial random number generator state to avoid resets on rollback
 535         //initstate(423121, random_state, sizeof(random_state));
 536         uint64_t seed = get_nanotime();
 537         srandom(seed);
 538
 539         snapshot = take_snapshot();
 540
 541         //reset random number generator state
 542         //setstate(random_state);
 543         seed = get_nanotime();
 544         srandom(seed);
 545
 546         install_trace_analyses(get_execution());
 547         redirect_output();
 548         initMainThread();
 549 }
 550
 551 bool ModelChecker::should_terminate_execution()
 552 {
 553         if (execution->have_bug_reports()) {
 554                 execution->set_assert();
 555                 return true;
 556         } else if (execution->isFinished()) {
 557                 return true;
 558         }
 559         return false;
 560 }