model.cc

   1 #include <stdio.h>
   2
   3 #include "model.h"
   4 #include "action.h"
   5 #include "tree.h"
   6 #include "schedule.h"
   7 #include "snapshot-interface.h"
   8 #undef DEBUG
   9 #include "common.h"
  10
  11 #define INITIAL_THREAD_ID       0
  12
  13 class Backtrack {
  14 public:
  15         Backtrack(ModelAction *d, action_list_t *t) {
  16                 diverge = d;
  17                 actionTrace = t;
  18                 iter = actionTrace->begin();
  19         }
  20         ModelAction * get_diverge() { return diverge; }
  21         action_list_t * get_trace() { return actionTrace; }
  22         void advance_state() { iter++; }
  23         ModelAction * get_state() {
  24                 return iter == actionTrace->end() ? NULL : *iter;
  25         }
  26 private:
  27         ModelAction *diverge;
  28         action_list_t *actionTrace;
  29         /* points to position in actionTrace as we replay */
  30         action_list_t::iterator iter;
  31 };
  32
  33 ModelChecker *model;
  34
  35 void free_action_list(action_list_t *list)
  36 {
  37         action_list_t::iterator it;
  38         for (it = list->begin(); it != list->end(); it++)
  39                 delete (*it);
  40         delete list;
  41 }
  42
  43 ModelChecker::ModelChecker()
  44 {
  45         /* First thread created will have id INITIAL_THREAD_ID */
  46         this->next_thread_id = INITIAL_THREAD_ID;
  47         used_sequence_numbers = 0;
  48         /* Initialize default scheduler */
  49         this->scheduler = new Scheduler();
  50
  51         num_executions = 0;
  52         this->current_action = NULL;
  53         this->exploring = NULL;
  54         this->nextThread = THREAD_ID_T_NONE;
  55
  56         rootNode = new TreeNode();
  57         currentNode = rootNode;
  58         action_trace = new action_list_t();
  59 }
  60
  61 ModelChecker::~ModelChecker()
  62 {
  63         std::map<int, class Thread *, std::less< int >, MyAlloc< std::pair< int, class Thread * > > >::iterator it;
  64         for (it = thread_map.begin(); it != thread_map.end(); it++)
  65                 delete (*it).second;
  66         thread_map.clear();
  67
  68         free_action_list(action_trace);
  69
  70         delete this->scheduler;
  71         delete rootNode;
  72 }
  73
  74 void ModelChecker::reset_to_initial_state()
  75 {
  76         DEBUG("+++ Resetting to initial state +++\n");
  77         std::map<int, class Thread *, std::less< int >, MyAlloc< std::pair< int, class Thread * > > >::iterator it;
  78         for (it = thread_map.begin(); it != thread_map.end(); it++)
  79                 delete (*it).second;
  80         thread_map.clear();
  81         action_trace = new action_list_t();
  82         currentNode = rootNode;
  83         current_action = NULL;
  84         next_thread_id = INITIAL_THREAD_ID;
  85         used_sequence_numbers = 0;
  86         /* scheduler reset ? */
  87 }
  88
  89 thread_id_t ModelChecker::get_next_id()
  90 {
  91         return next_thread_id++;
  92 }
  93
  94 int ModelChecker::get_next_seq_num()
  95 {
  96         return ++used_sequence_numbers;
  97 }
  98
  99 Thread * ModelChecker::schedule_next_thread()
 100 {
 101         Thread *t;
 102         if (nextThread == THREAD_ID_T_NONE)
 103                 return NULL;
 104         t = thread_map[id_to_int(nextThread)];
 105
 106         ASSERT(t != NULL);
 107
 108         return t;
 109 }
 110
 111 /*
 112  * get_next_replay_thread() - Choose the next thread in the replay sequence
 113  *
 114  * If we've reached the 'diverge' point, then we pick a thread from the
 115  *   backtracking set.
 116  * Otherwise, we simply return the next thread in the sequence.
 117  */
 118 thread_id_t ModelChecker::get_next_replay_thread()
 119 {
 120         ModelAction *next;
 121         thread_id_t tid;
 122
 123         next = exploring->get_state();
 124
 125         if (next == exploring->get_diverge()) {
 126                 TreeNode *node = next->get_node();
 127
 128                 /* Reached divergence point; discard our current 'exploring' */
 129                 DEBUG("*** Discard 'Backtrack' object ***\n");
 130                 tid = node->getNextBacktrack();
 131                 delete exploring;
 132                 exploring = NULL;
 133         } else {
 134                 tid = next->get_tid();
 135         }
 136         DEBUG("*** ModelChecker chose next thread = %d ***\n", tid);
 137         return tid;
 138 }
 139
 140 thread_id_t ModelChecker::advance_backtracking_state()
 141 {
 142         /* Have we completed exploring the preselected path? */
 143         if (exploring == NULL)
 144                 return THREAD_ID_T_NONE;
 145
 146         /* Else, we are trying to replay an execution */
 147         exploring->advance_state();
 148
 149         ASSERT(exploring->get_state() != NULL);
 150
 151         return get_next_replay_thread();
 152 }
 153
 154 bool ModelChecker::next_execution()
 155 {
 156         DBG();
 157
 158         num_executions++;
 159         print_summary();
 160         if ((exploring = model->get_next_backtrack()) == NULL)
 161                 return false;
 162
 163         if (DBG_ENABLED()) {
 164                 printf("Next execution will diverge at:\n");
 165                 exploring->get_diverge()->print();
 166                 print_list(exploring->get_trace());
 167         }
 168
 169         model->reset_to_initial_state();
 170         nextThread = get_next_replay_thread();
 171         return true;
 172 }
 173
 174 ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 175 {
 176         action_type type = act->get_type();
 177
 178         switch (type) {
 179                 case THREAD_CREATE:
 180                 case THREAD_YIELD:
 181                 case THREAD_JOIN:
 182                         return NULL;
 183                 case ATOMIC_READ:
 184                 case ATOMIC_WRITE:
 185                 default:
 186                         break;
 187         }
 188         /* linear search: from most recent to oldest */
 189         action_list_t::reverse_iterator rit;
 190         for (rit = action_trace->rbegin(); rit != action_trace->rend(); rit++) {
 191                 ModelAction *prev = *rit;
 192                 if (act->is_dependent(prev))
 193                         return prev;
 194         }
 195         return NULL;
 196 }
 197
 198 void ModelChecker::set_backtracking(ModelAction *act)
 199 {
 200         ModelAction *prev;
 201         TreeNode *node;
 202         Thread *t = get_thread(act->get_tid());
 203
 204         prev = get_last_conflict(act);
 205         if (prev == NULL)
 206                 return;
 207
 208         node = prev->get_node();
 209
 210         while (t && !node->is_enabled(t))
 211                 t = t->get_parent();
 212
 213         /* Check if this has been explored already */
 214         if (node->hasBeenExplored(t->get_id()))
 215                 return;
 216         /* If this is a new backtracking point, mark the tree */
 217         if (node->setBacktrack(t->get_id()) != 0)
 218                 return;
 219
 220         DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
 221                         prev->get_tid(), t->get_id());
 222         if (DBG_ENABLED()) {
 223                 prev->print();
 224                 act->print();
 225         }
 226
 227         Backtrack *back = new Backtrack(prev, action_trace);
 228         backtrack_list.push_back(back);
 229 }
 230
 231 Backtrack * ModelChecker::get_next_backtrack()
 232 {
 233         Backtrack *next;
 234         if (backtrack_list.empty())
 235                 return NULL;
 236         next = backtrack_list.back();
 237         backtrack_list.pop_back();
 238         return next;
 239 }
 240
 241 void ModelChecker::check_current_action(void)
 242 {
 243         ModelAction *next = this->current_action;
 244
 245         if (!next) {
 246                 DEBUG("trying to push NULL action...\n");
 247                 return;
 248         }
 249         current_action = NULL;
 250         nextThread = advance_backtracking_state();
 251         next->set_node(currentNode);
 252         set_backtracking(next);
 253         currentNode = currentNode->explore_child(next);
 254         this->action_trace->push_back(next);
 255 }
 256
 257 void ModelChecker::print_summary(void)
 258 {
 259         printf("\n");
 260         printf("Number of executions: %d\n", num_executions);
 261         printf("Total nodes created: %d\n", TreeNode::getTotalNodes());
 262
 263         scheduler->print();
 264
 265         print_list(action_trace);
 266         printf("\n");
 267
 268 }
 269
 270 void ModelChecker::print_list(action_list_t *list)
 271 {
 272         action_list_t::iterator it;
 273
 274         printf("---------------------------------------------------------------------\n");
 275         printf("Trace:\n");
 276
 277         for (it = list->begin(); it != list->end(); it++) {
 278                 (*it)->print();
 279         }
 280         printf("---------------------------------------------------------------------\n");
 281 }
 282
 283 int ModelChecker::add_thread(Thread *t)
 284 {
 285         thread_map[id_to_int(t->get_id())] = t;
 286         scheduler->add_thread(t);
 287         return 0;
 288 }
 289
 290 void ModelChecker::remove_thread(Thread *t)
 291 {
 292         scheduler->remove_thread(t);
 293 }
 294
 295 int ModelChecker::switch_to_master(ModelAction *act)
 296 {
 297         Thread *old;
 298
 299         DBG();
 300         old = thread_current();
 301         set_current_action(act);
 302         old->set_state(THREAD_READY);
 303         return Thread::swap(old, get_system_context());
 304 }