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         /* Initialize default scheduler */
  46         scheduler(new Scheduler()),
  47         /* First thread created will have id INITIAL_THREAD_ID */
  48         next_thread_id(INITIAL_THREAD_ID),
  49         used_sequence_numbers(0),
  50
  51         num_executions(0),
  52         current_action(NULL),
  53         exploring(NULL),
  54         nextThread(THREAD_ID_T_NONE),
  55         action_trace(new action_list_t()),
  56         rootNode(new TreeNode()),
  57         currentNode(rootNode)
  58 {
  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 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         nextThread = 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         /* Have we completed exploring the preselected path? */
 125         if (exploring == NULL)
 126                 return THREAD_ID_T_NONE;
 127
 128         /* Else, we are trying to replay an execution */
 129         exploring->advance_state();
 130
 131         ASSERT(exploring->get_state() != NULL);
 132
 133         next = exploring->get_state();
 134
 135         if (next == exploring->get_diverge()) {
 136                 TreeNode *node = next->get_treenode();
 137
 138                 /* Reached divergence point; discard our current 'exploring' */
 139                 DEBUG("*** Discard 'Backtrack' object ***\n");
 140                 tid = node->getNextBacktrack();
 141                 delete exploring;
 142                 exploring = NULL;
 143         } else {
 144                 tid = next->get_tid();
 145         }
 146         DEBUG("*** ModelChecker chose next thread = %d ***\n", tid);
 147         return tid;
 148 }
 149
 150 bool ModelChecker::next_execution()
 151 {
 152         DBG();
 153
 154         num_executions++;
 155         print_summary();
 156         if ((exploring = model->get_next_backtrack()) == NULL)
 157                 return false;
 158
 159         if (DBG_ENABLED()) {
 160                 printf("Next execution will diverge at:\n");
 161                 exploring->get_diverge()->print();
 162                 print_list(exploring->get_trace());
 163         }
 164
 165         model->reset_to_initial_state();
 166         return true;
 167 }
 168
 169 ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 170 {
 171         action_type type = act->get_type();
 172
 173         switch (type) {
 174                 case THREAD_CREATE:
 175                 case THREAD_YIELD:
 176                 case THREAD_JOIN:
 177                         return NULL;
 178                 case ATOMIC_READ:
 179                 case ATOMIC_WRITE:
 180                 default:
 181                         break;
 182         }
 183         /* linear search: from most recent to oldest */
 184         action_list_t::reverse_iterator rit;
 185         for (rit = action_trace->rbegin(); rit != action_trace->rend(); rit++) {
 186                 ModelAction *prev = *rit;
 187                 if (act->is_dependent(prev))
 188                         return prev;
 189         }
 190         return NULL;
 191 }
 192
 193 void ModelChecker::set_backtracking(ModelAction *act)
 194 {
 195         ModelAction *prev;
 196         TreeNode *node;
 197         Thread *t = get_thread(act->get_tid());
 198
 199         prev = get_last_conflict(act);
 200         if (prev == NULL)
 201                 return;
 202
 203         node = prev->get_treenode();
 204
 205         while (t && !node->is_enabled(t))
 206                 t = t->get_parent();
 207
 208         /* Check if this has been explored already */
 209         if (node->hasBeenExplored(t->get_id()))
 210                 return;
 211         /* If this is a new backtracking point, mark the tree */
 212         if (node->setBacktrack(t->get_id()) != 0)
 213                 return;
 214
 215         DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
 216                         prev->get_tid(), t->get_id());
 217         if (DBG_ENABLED()) {
 218                 prev->print();
 219                 act->print();
 220         }
 221
 222         Backtrack *back = new Backtrack(prev, action_trace);
 223         backtrack_list.push_back(back);
 224 }
 225
 226 Backtrack * ModelChecker::get_next_backtrack()
 227 {
 228         Backtrack *next;
 229         if (backtrack_list.empty())
 230                 return NULL;
 231         next = backtrack_list.back();
 232         backtrack_list.pop_back();
 233         return next;
 234 }
 235
 236 void ModelChecker::check_current_action(void)
 237 {
 238         ModelAction *curr = this->current_action;
 239         current_action = NULL;
 240         if (!curr) {
 241                 DEBUG("trying to push NULL action...\n");
 242                 return;
 243         }
 244
 245         nextThread = get_next_replay_thread();
 246         curr->set_node(currentNode);
 247         set_backtracking(curr);
 248         currentNode = currentNode->explore_child(curr);
 249         this->action_trace->push_back(curr);
 250 }
 251
 252 void ModelChecker::print_summary(void)
 253 {
 254         printf("\n");
 255         printf("Number of executions: %d\n", num_executions);
 256         printf("Total nodes created: %d\n", TreeNode::getTotalNodes());
 257
 258         scheduler->print();
 259
 260         print_list(action_trace);
 261         printf("\n");
 262
 263 }
 264
 265 void ModelChecker::print_list(action_list_t *list)
 266 {
 267         action_list_t::iterator it;
 268
 269         printf("---------------------------------------------------------------------\n");
 270         printf("Trace:\n");
 271
 272         for (it = list->begin(); it != list->end(); it++) {
 273                 (*it)->print();
 274         }
 275         printf("---------------------------------------------------------------------\n");
 276 }
 277
 278 int ModelChecker::add_thread(Thread *t)
 279 {
 280         thread_map[id_to_int(t->get_id())] = t;
 281         scheduler->add_thread(t);
 282         return 0;
 283 }
 284
 285 void ModelChecker::remove_thread(Thread *t)
 286 {
 287         scheduler->remove_thread(t);
 288 }
 289
 290 int ModelChecker::switch_to_master(ModelAction *act)
 291 {
 292         Thread *old;
 293
 294         DBG();
 295         old = thread_current();
 296         set_current_action(act);
 297         old->set_state(THREAD_READY);
 298         return Thread::swap(old, get_system_context());
 299 }