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