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
  10 #define INITIAL_THREAD_ID       0
  11
  12 ModelChecker *model;
  13
  14 /** @brief Constructor */
  15 ModelChecker::ModelChecker()
  16         :
  17         /* Initialize default scheduler */
  18         scheduler(new Scheduler()),
  19         /* First thread created will have id INITIAL_THREAD_ID */
  20         next_thread_id(INITIAL_THREAD_ID),
  21         used_sequence_numbers(0),
  22
  23         num_executions(0),
  24         current_action(NULL),
  25         diverge(NULL),
  26         nextThread(THREAD_ID_T_NONE),
  27         action_trace(new action_list_t()),
  28         thread_map(new std::map<int, class Thread *>),
  29         obj_thrd_map(new std::map<void *, std::vector<action_list_t> >()),
  30         thrd_last_action(new std::vector<ModelAction *>(1)),
  31         node_stack(new NodeStack()),
  32         next_backtrack(NULL)
  33 {
  34 }
  35
  36 /** @brief Destructor */
  37 ModelChecker::~ModelChecker()
  38 {
  39         std::map<int, class Thread *>::iterator it;
  40         for (it = thread_map->begin(); it != thread_map->end(); it++)
  41                 delete (*it).second;
  42         delete thread_map;
  43
  44         delete obj_thrd_map;
  45         delete action_trace;
  46         delete thrd_last_action;
  47         delete node_stack;
  48         delete scheduler;
  49 }
  50
  51 /**
  52  * Restores user program to initial state and resets all model-checker data
  53  * structures.
  54  */
  55 void ModelChecker::reset_to_initial_state()
  56 {
  57         DEBUG("+++ Resetting to initial state +++\n");
  58         node_stack->reset_execution();
  59         current_action = NULL;
  60         next_thread_id = INITIAL_THREAD_ID;
  61         used_sequence_numbers = 0;
  62         nextThread = 0;
  63         next_backtrack = NULL;
  64         snapshotObject->backTrackBeforeStep(0);
  65 }
  66
  67 /** @returns a thread ID for a new Thread */
  68 thread_id_t ModelChecker::get_next_id()
  69 {
  70         return next_thread_id++;
  71 }
  72
  73 /** @returns the number of user threads created during this execution */
  74 int ModelChecker::get_num_threads()
  75 {
  76         return next_thread_id;
  77 }
  78
  79 /** @returns a sequence number for a new ModelAction */
  80 int ModelChecker::get_next_seq_num()
  81 {
  82         return ++used_sequence_numbers;
  83 }
  84
  85 /**
  86  * Performs the "scheduling" for the model-checker. That is, it checks if the
  87  * model-checker has selected a "next thread to run" and returns it, if
  88  * available. This function should be called from the Scheduler routine, where
  89  * the Scheduler falls back to a default scheduling routine if needed.
  90  *
  91  * @return The next thread chosen by the model-checker. If the model-checker
  92  * makes no selection, retuns NULL.
  93  */
  94 Thread * ModelChecker::schedule_next_thread()
  95 {
  96         Thread *t;
  97         if (nextThread == THREAD_ID_T_NONE)
  98                 return NULL;
  99         t = (*thread_map)[id_to_int(nextThread)];
 100
 101         ASSERT(t != NULL);
 102
 103         return t;
 104 }
 105
 106 /**
 107  * Choose the next thread in the replay sequence.
 108  *
 109  * If the replay sequence has reached the 'diverge' point, returns a thread
 110  * from the backtracking set. Otherwise, simply returns the next thread in the
 111  * sequence that is being replayed.
 112  */
 113 thread_id_t ModelChecker::get_next_replay_thread()
 114 {
 115         ModelAction *next;
 116         thread_id_t tid;
 117
 118         /* Have we completed exploring the preselected path? */
 119         if (diverge == NULL)
 120                 return THREAD_ID_T_NONE;
 121
 122         /* Else, we are trying to replay an execution */
 123         next = node_stack->get_next()->get_action();
 124
 125         if (next == diverge) {
 126                 Node *node = next->get_node();
 127
 128                 /* Reached divergence point */
 129                 DEBUG("*** Divergence point ***\n");
 130                 tid = node->get_next_backtrack();
 131                 diverge = NULL;
 132         } else {
 133                 tid = next->get_tid();
 134         }
 135         DEBUG("*** ModelChecker chose next thread = %d ***\n", tid);
 136         return tid;
 137 }
 138
 139 /**
 140  * Queries the model-checker for more executions to explore and, if one
 141  * exists, resets the model-checker state to execute a new execution.
 142  *
 143  * @return If there are more executions to explore, return true. Otherwise,
 144  * return false.
 145  */
 146 bool ModelChecker::next_execution()
 147 {
 148         DBG();
 149
 150         num_executions++;
 151         print_summary();
 152         if ((diverge = model->get_next_backtrack()) == NULL)
 153                 return false;
 154
 155         if (DBG_ENABLED()) {
 156                 printf("Next execution will diverge at:\n");
 157                 diverge->print();
 158         }
 159
 160         model->reset_to_initial_state();
 161         return true;
 162 }
 163
 164 ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 165 {
 166         action_type type = act->get_type();
 167
 168         switch (type) {
 169                 case THREAD_CREATE:
 170                 case THREAD_YIELD:
 171                 case THREAD_JOIN:
 172                         return NULL;
 173                 case ATOMIC_READ:
 174                 case ATOMIC_WRITE:
 175                 default:
 176                         break;
 177         }
 178         /* linear search: from most recent to oldest */
 179         action_list_t::reverse_iterator rit;
 180         for (rit = action_trace->rbegin(); rit != action_trace->rend(); rit++) {
 181                 ModelAction *prev = *rit;
 182                 if (act->is_synchronizing(prev))
 183                         return prev;
 184         }
 185         return NULL;
 186 }
 187
 188 void ModelChecker::set_backtracking(ModelAction *act)
 189 {
 190         ModelAction *prev;
 191         Node *node;
 192         Thread *t = get_thread(act->get_tid());
 193
 194         prev = get_last_conflict(act);
 195         if (prev == NULL)
 196                 return;
 197
 198         node = prev->get_node();
 199
 200         while (!node->is_enabled(t))
 201                 t = t->get_parent();
 202
 203         /* Check if this has been explored already */
 204         if (node->has_been_explored(t->get_id()))
 205                 return;
 206
 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 */
 243                 delete curr;
 244                 curr = tmp;
 245         } else {
 246                 curr->create_cv(get_parent_action(curr->get_tid()));
 247         }
 248
 249         /* Assign 'creation' parent */
 250         if (curr->get_type() == THREAD_CREATE) {
 251                 Thread *th = (Thread *)curr->get_location();
 252                 th->set_creation(curr);
 253         }
 254
 255         nextThread = get_next_replay_thread();
 256
 257         currnode = curr->get_node();
 258
 259         if (!currnode->backtrack_empty())
 260                 if (!next_backtrack || *curr > *next_backtrack)
 261                         next_backtrack = curr;
 262
 263         set_backtracking(curr);
 264
 265         add_action_to_lists(curr);
 266 }
 267
 268
 269 /**
 270  * Adds an action to the per-object, per-thread action vector.
 271  * @param act is the ModelAction to add.
 272  */
 273
 274 void ModelChecker::add_action_to_lists(ModelAction *act)
 275 {
 276         action_trace->push_back(act);
 277
 278         std::vector<action_list_t> *vec = &(*obj_thrd_map)[act->get_location()];
 279         if (id_to_int(act->get_tid()) >= (int)vec->size())
 280                 vec->resize(next_thread_id);
 281         (*vec)[id_to_int(act->get_tid())].push_back(act);
 282
 283         (*thrd_last_action)[id_to_int(act->get_tid())] = act;
 284 }
 285
 286 ModelAction * ModelChecker::get_last_action(thread_id_t tid)
 287 {
 288         int nthreads = get_num_threads();
 289         if ((int)thrd_last_action->size() < nthreads)
 290                 thrd_last_action->resize(nthreads);
 291         return (*thrd_last_action)[id_to_int(tid)];
 292 }
 293
 294 ModelAction * ModelChecker::get_parent_action(thread_id_t tid)
 295 {
 296         ModelAction *parent = get_last_action(tid);
 297         if (!parent)
 298                 parent = get_thread(tid)->get_creation();
 299         return parent;
 300 }
 301
 302 void ModelChecker::print_summary(void)
 303 {
 304         printf("\n");
 305         printf("Number of executions: %d\n", num_executions);
 306         printf("Total nodes created: %d\n", node_stack->get_total_nodes());
 307
 308         scheduler->print();
 309
 310         print_list(action_trace);
 311         printf("\n");
 312 }
 313
 314 void ModelChecker::print_list(action_list_t *list)
 315 {
 316         action_list_t::iterator it;
 317
 318         printf("---------------------------------------------------------------------\n");
 319         printf("Trace:\n");
 320
 321         for (it = list->begin(); it != list->end(); it++) {
 322                 (*it)->print();
 323         }
 324         printf("---------------------------------------------------------------------\n");
 325 }
 326
 327 int ModelChecker::add_thread(Thread *t)
 328 {
 329         (*thread_map)[id_to_int(t->get_id())] = t;
 330         scheduler->add_thread(t);
 331         return 0;
 332 }
 333
 334 void ModelChecker::remove_thread(Thread *t)
 335 {
 336         scheduler->remove_thread(t);
 337 }
 338
 339 int ModelChecker::switch_to_master(ModelAction *act)
 340 {
 341         Thread *old;
 342
 343         DBG();
 344         old = thread_current();
 345         set_current_action(act);
 346         old->set_state(THREAD_READY);
 347         return Thread::swap(old, get_system_context());
 348 }