model.cc

   1 #include <stdio.h>
   2
   3 #include "model.h"
   4 #include "action.h"
   5 #include "nodestack.h"
   6 #include "schedule.h"
   7 #include "snapshot-interface.h"
   8 #include "common.h"
   9 #include "clockvector.h"
  10
  11 #define INITIAL_THREAD_ID       0
  12
  13 ModelChecker *model;
  14
  15 /** @brief Constructor */
  16 ModelChecker::ModelChecker()
  17         :
  18         /* Initialize default scheduler */
  19         scheduler(new Scheduler()),
  20         /* First thread created will have id INITIAL_THREAD_ID */
  21         next_thread_id(INITIAL_THREAD_ID),
  22         used_sequence_numbers(0),
  23
  24         num_executions(0),
  25         current_action(NULL),
  26         diverge(NULL),
  27         nextThread(THREAD_ID_T_NONE),
  28         action_trace(new action_list_t()),
  29         thread_map(new std::map<int, Thread *>),
  30         obj_thrd_map(new std::map<void *, std::vector<action_list_t> >()),
  31         thrd_last_action(new std::vector<ModelAction *>(1)),
  32         node_stack(new NodeStack()),
  33         next_backtrack(NULL)
  34 {
  35 }
  36
  37 /** @brief Destructor */
  38 ModelChecker::~ModelChecker()
  39 {
  40         std::map<int, Thread *>::iterator it;
  41         for (it = thread_map->begin(); it != thread_map->end(); it++)
  42                 delete (*it).second;
  43         delete thread_map;
  44
  45         delete obj_thrd_map;
  46         delete action_trace;
  47         delete thrd_last_action;
  48         delete node_stack;
  49         delete scheduler;
  50 }
  51
  52 /**
  53  * Restores user program to initial state and resets all model-checker data
  54  * structures.
  55  */
  56 void ModelChecker::reset_to_initial_state()
  57 {
  58         DEBUG("+++ Resetting to initial state +++\n");
  59         node_stack->reset_execution();
  60         current_action = NULL;
  61         next_thread_id = INITIAL_THREAD_ID;
  62         used_sequence_numbers = 0;
  63         nextThread = 0;
  64         next_backtrack = NULL;
  65         snapshotObject->backTrackBeforeStep(0);
  66 }
  67
  68 /** @returns a thread ID for a new Thread */
  69 thread_id_t ModelChecker::get_next_id()
  70 {
  71         return next_thread_id++;
  72 }
  73
  74 /** @returns the number of user threads created during this execution */
  75 int ModelChecker::get_num_threads()
  76 {
  77         return next_thread_id;
  78 }
  79
  80 /** @returns a sequence number for a new ModelAction */
  81 modelclock_t ModelChecker::get_next_seq_num()
  82 {
  83         return ++used_sequence_numbers;
  84 }
  85
  86 /**
  87  * Performs the "scheduling" for the model-checker. That is, it checks if the
  88  * model-checker has selected a "next thread to run" and returns it, if
  89  * available. This function should be called from the Scheduler routine, where
  90  * the Scheduler falls back to a default scheduling routine if needed.
  91  *
  92  * @return The next thread chosen by the model-checker. If the model-checker
  93  * makes no selection, retuns NULL.
  94  */
  95 Thread * ModelChecker::schedule_next_thread()
  96 {
  97         Thread *t;
  98         if (nextThread == THREAD_ID_T_NONE)
  99                 return NULL;
 100         t = (*thread_map)[id_to_int(nextThread)];
 101
 102         ASSERT(t != NULL);
 103
 104         return t;
 105 }
 106
 107 /**
 108  * Choose the next thread in the replay sequence.
 109  *
 110  * If the replay sequence has reached the 'diverge' point, returns a thread
 111  * from the backtracking set. Otherwise, simply returns the next thread in the
 112  * sequence that is being replayed.
 113  */
 114 thread_id_t ModelChecker::get_next_replay_thread()
 115 {
 116         ModelAction *next;
 117         thread_id_t tid;
 118
 119         /* Have we completed exploring the preselected path? */
 120         if (diverge == NULL)
 121                 return THREAD_ID_T_NONE;
 122
 123         /* Else, we are trying to replay an execution */
 124         next = node_stack->get_next()->get_action();
 125
 126         if (next == diverge) {
 127                 Node *node = next->get_node()->get_parent();
 128
 129                 /* Reached divergence point */
 130                 DEBUG("*** Divergence point ***\n");
 131                 tid = node->get_next_backtrack();
 132                 diverge = NULL;
 133         } else {
 134                 tid = next->get_tid();
 135         }
 136         DEBUG("*** ModelChecker chose next thread = %d ***\n", tid);
 137         return tid;
 138 }
 139
 140 /**
 141  * Queries the model-checker for more executions to explore and, if one
 142  * exists, resets the model-checker state to execute a new execution.
 143  *
 144  * @return If there are more executions to explore, return true. Otherwise,
 145  * return false.
 146  */
 147 bool ModelChecker::next_execution()
 148 {
 149         DBG();
 150
 151         num_executions++;
 152         print_summary();
 153         if ((diverge = model->get_next_backtrack()) == NULL)
 154                 return false;
 155
 156         if (DBG_ENABLED()) {
 157                 printf("Next execution will diverge at:\n");
 158                 diverge->print();
 159         }
 160
 161         model->reset_to_initial_state();
 162         return true;
 163 }
 164
 165 ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 166 {
 167         action_type type = act->get_type();
 168
 169         switch (type) {
 170                 case ATOMIC_READ:
 171                 case ATOMIC_WRITE:
 172                 case ATOMIC_RMW:
 173                         break;
 174                 default:
 175                         return NULL;
 176         }
 177         /* linear search: from most recent to oldest */
 178         action_list_t::reverse_iterator rit;
 179         for (rit = action_trace->rbegin(); rit != action_trace->rend(); rit++) {
 180                 ModelAction *prev = *rit;
 181                 if (act->is_synchronizing(prev))
 182                         return prev;
 183         }
 184         return NULL;
 185 }
 186
 187 void ModelChecker::set_backtracking(ModelAction *act)
 188 {
 189         ModelAction *prev;
 190         Node *node;
 191         Thread *t = get_thread(act->get_tid());
 192
 193         prev = get_last_conflict(act);
 194         if (prev == NULL)
 195                 return;
 196
 197         node = prev->get_node()->get_parent();
 198
 199         while (!node->is_enabled(t))
 200                 t = t->get_parent();
 201
 202         /* Check if this has been explored already */
 203         if (node->has_been_explored(t->get_id()))
 204                 return;
 205
 206         /* Cache the latest backtracking point */
 207         if (!next_backtrack || *prev > *next_backtrack)
 208                 next_backtrack = prev;
 209
 210         /* If this is a new backtracking point, mark the tree */
 211         if (!node->set_backtrack(t->get_id()))
 212                 return;
 213         DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
 214                         prev->get_tid(), t->get_id());
 215         if (DBG_ENABLED()) {
 216                 prev->print();
 217                 act->print();
 218         }
 219 }
 220
 221 ModelAction * ModelChecker::get_next_backtrack()
 222 {
 223         ModelAction *next = next_backtrack;
 224         next_backtrack = NULL;
 225         return next;
 226 }
 227
 228 void ModelChecker::check_current_action(void)
 229 {
 230         Node *currnode;
 231
 232         ModelAction *curr = this->current_action;
 233         ModelAction *tmp;
 234         current_action = NULL;
 235         if (!curr) {
 236                 DEBUG("trying to push NULL action...\n");
 237                 return;
 238         }
 239
 240         tmp = node_stack->explore_action(curr);
 241         if (tmp) {
 242                 /* Discard duplicate ModelAction; use action from NodeStack */
 243                 delete curr;
 244                 curr = tmp;
 245         } else {
 246                 /*
 247                  * Perform one-time actions when pushing new ModelAction onto
 248                  * NodeStack
 249                  */
 250                 curr->create_cv(get_parent_action(curr->get_tid()));
 251                 /* Build may_read_from set */
 252                 if (curr->is_read())
 253                         build_reads_from_past(curr);
 254         }
 255
 256         /* Assign 'creation' parent */
 257         if (curr->get_type() == THREAD_CREATE) {
 258                 Thread *th = (Thread *)curr->get_location();
 259                 th->set_creation(curr);
 260         }
 261
 262         nextThread = get_next_replay_thread();
 263
 264         currnode = curr->get_node()->get_parent();
 265
 266         if (!currnode->backtrack_empty())
 267                 if (!next_backtrack || *curr > *next_backtrack)
 268                         next_backtrack = curr;
 269
 270         set_backtracking(curr);
 271
 272         add_action_to_lists(curr);
 273
 274         /* Assign reads_from values */
 275         /* TODO: perform release/acquire synchronization here; include
 276          * reads_from as ModelAction member? */
 277         Thread *th = get_thread(curr->get_tid());
 278         int value = VALUE_NONE;
 279         if (curr->is_read()) {
 280                 const ModelAction *reads_from = curr->get_node()->get_next_read_from();
 281                 value = reads_from->get_value();
 282                 /* Assign reads_from, perform release/acquire synchronization */
 283                 curr->read_from(reads_from);
 284         }
 285         th->set_return_value(value);
 286 }
 287
 288 /**
 289  * Performs various bookkeeping operations for the current ModelAction. For
 290  * instance, adds action to the per-object, per-thread action vector and to the
 291  * action trace list of all thread actions.
 292  *
 293  * @param act is the ModelAction to add.
 294  */
 295 void ModelChecker::add_action_to_lists(ModelAction *act)
 296 {
 297         int tid = id_to_int(act->get_tid());
 298         action_trace->push_back(act);
 299
 300         std::vector<action_list_t> *vec = &(*obj_thrd_map)[act->get_location()];
 301         if (tid >= (int)vec->size())
 302                 vec->resize(next_thread_id);
 303         (*vec)[tid].push_back(act);
 304
 305         if ((int)thrd_last_action->size() <= tid)
 306                 thrd_last_action->resize(get_num_threads());
 307         (*thrd_last_action)[tid] = act;
 308 }
 309
 310 ModelAction * ModelChecker::get_last_action(thread_id_t tid)
 311 {
 312         int nthreads = get_num_threads();
 313         if ((int)thrd_last_action->size() < nthreads)
 314                 thrd_last_action->resize(nthreads);
 315         return (*thrd_last_action)[id_to_int(tid)];
 316 }
 317
 318 ModelAction * ModelChecker::get_parent_action(thread_id_t tid)
 319 {
 320         ModelAction *parent = get_last_action(tid);
 321         if (!parent)
 322                 parent = get_thread(tid)->get_creation();
 323         return parent;
 324 }
 325
 326 ClockVector * ModelChecker::get_cv(thread_id_t tid) {
 327         return get_parent_action(tid)->get_cv();
 328 }
 329
 330 /**
 331  * Build up an initial set of all past writes that this 'read' action may read
 332  * from. This set is determined by the clock vector's "happens before"
 333  * relationship.
 334  * @param curr is the current ModelAction that we are exploring; it must be a
 335  * 'read' operation.
 336  */
 337 void ModelChecker::build_reads_from_past(ModelAction *curr)
 338 {
 339         std::vector<action_list_t> *thrd_lists = &(*obj_thrd_map)[curr->get_location()];
 340         unsigned int i;
 341
 342         ASSERT(curr->is_read());
 343
 344         /* Track whether this object has been initialized */
 345         bool initialized = false;
 346
 347         for (i = 0; i < thrd_lists->size(); i++) {
 348                 action_list_t *list = &(*thrd_lists)[i];
 349                 action_list_t::reverse_iterator rit;
 350                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
 351                         ModelAction *act = *rit;
 352
 353                         /* Only consider 'write' actions */
 354                         if (!act->is_write())
 355                                 continue;
 356
 357                         DEBUG("Adding action to may_read_from:\n");
 358                         if (DBG_ENABLED()) {
 359                                 act->print();
 360                                 curr->print();
 361                         }
 362                         curr->get_node()->add_read_from(act);
 363
 364                         /* Include at most one act per-thread that "happens before" curr */
 365                         if (act->happens_before(curr)) {
 366                                 initialized = true;
 367                                 break;
 368                         }
 369                 }
 370         }
 371
 372         if (!initialized) {
 373                 /* TODO: need a more informative way of reporting errors */
 374                 printf("ERROR: may read from uninitialized atomic\n");
 375         }
 376
 377         if (DBG_ENABLED() || !initialized) {
 378                 printf("Reached read action:\n");
 379                 curr->print();
 380                 printf("Printing may_read_from\n");
 381                 curr->get_node()->print_may_read_from();
 382                 printf("End printing may_read_from\n");
 383         }
 384
 385         ASSERT(initialized);
 386 }
 387
 388 static void print_list(action_list_t *list)
 389 {
 390         action_list_t::iterator it;
 391
 392         printf("---------------------------------------------------------------------\n");
 393         printf("Trace:\n");
 394
 395         for (it = list->begin(); it != list->end(); it++) {
 396                 (*it)->print();
 397         }
 398         printf("---------------------------------------------------------------------\n");
 399 }
 400
 401 void ModelChecker::print_summary(void)
 402 {
 403         printf("\n");
 404         printf("Number of executions: %d\n", num_executions);
 405         printf("Total nodes created: %d\n", node_stack->get_total_nodes());
 406
 407         scheduler->print();
 408
 409         print_list(action_trace);
 410         printf("\n");
 411 }
 412
 413 int ModelChecker::add_thread(Thread *t)
 414 {
 415         (*thread_map)[id_to_int(t->get_id())] = t;
 416         scheduler->add_thread(t);
 417         return 0;
 418 }
 419
 420 void ModelChecker::remove_thread(Thread *t)
 421 {
 422         scheduler->remove_thread(t);
 423 }
 424
 425 int ModelChecker::switch_to_master(ModelAction *act)
 426 {
 427         Thread *old;
 428
 429         DBG();
 430         old = thread_current();
 431         set_current_action(act);
 432         old->set_state(THREAD_READY);
 433         return Thread::swap(old, get_system_context());
 434 }