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 ModelChecker::ModelChecker()
  15         :
  16         /* Initialize default scheduler */
  17         scheduler(new Scheduler()),
  18         /* First thread created will have id INITIAL_THREAD_ID */
  19         next_thread_id(INITIAL_THREAD_ID),
  20         used_sequence_numbers(0),
  21
  22         num_executions(0),
  23         current_action(NULL),
  24         diverge(NULL),
  25         nextThread(THREAD_ID_T_NONE),
  26         action_trace(new action_list_t()),
  27         thread_map(new std::map<int, class Thread *>),
  28         obj_thrd_map(new std::map<void *, std::vector<action_list_t> >()),
  29         node_stack(new NodeStack()),
  30         next_backtrack(NULL)
  31 {
  32 }
  33
  34 ModelChecker::~ModelChecker()
  35 {
  36         std::map<int, class Thread *>::iterator it;
  37         for (it = thread_map->begin(); it != thread_map->end(); it++)
  38                 delete (*it).second;
  39         delete thread_map;
  40
  41         delete obj_thrd_map;
  42         delete action_trace;
  43         delete node_stack;
  44         delete scheduler;
  45 }
  46
  47 void ModelChecker::reset_to_initial_state()
  48 {
  49         DEBUG("+++ Resetting to initial state +++\n");
  50         node_stack->reset_execution();
  51         current_action = NULL;
  52         next_thread_id = INITIAL_THREAD_ID;
  53         used_sequence_numbers = 0;
  54         nextThread = 0;
  55         next_backtrack = NULL;
  56         snapshotObject->backTrackBeforeStep(0);
  57 }
  58
  59 thread_id_t ModelChecker::get_next_id()
  60 {
  61         return next_thread_id++;
  62 }
  63
  64 int ModelChecker::get_num_threads()
  65 {
  66         return next_thread_id;
  67 }
  68
  69 int ModelChecker::get_next_seq_num()
  70 {
  71         return ++used_sequence_numbers;
  72 }
  73
  74 Thread * ModelChecker::schedule_next_thread()
  75 {
  76         Thread *t;
  77         if (nextThread == THREAD_ID_T_NONE)
  78                 return NULL;
  79         t = (*thread_map)[id_to_int(nextThread)];
  80
  81         ASSERT(t != NULL);
  82
  83         return t;
  84 }
  85
  86 /*
  87  * get_next_replay_thread() - Choose the next thread in the replay sequence
  88  *
  89  * If we've reached the 'diverge' point, then we pick a thread from the
  90  *   backtracking set.
  91  * Otherwise, we simply return the next thread in the sequence.
  92  */
  93 thread_id_t ModelChecker::get_next_replay_thread()
  94 {
  95         ModelAction *next;
  96         thread_id_t tid;
  97
  98         /* Have we completed exploring the preselected path? */
  99         if (diverge == NULL)
 100                 return THREAD_ID_T_NONE;
 101
 102         /* Else, we are trying to replay an execution */
 103         next = node_stack->get_next()->get_action();
 104
 105         if (next == diverge) {
 106                 Node *node = next->get_node();
 107
 108                 /* Reached divergence point */
 109                 DEBUG("*** Divergence point ***\n");
 110                 tid = node->get_next_backtrack();
 111                 diverge = NULL;
 112         } else {
 113                 tid = next->get_tid();
 114         }
 115         DEBUG("*** ModelChecker chose next thread = %d ***\n", tid);
 116         return tid;
 117 }
 118
 119 bool ModelChecker::next_execution()
 120 {
 121         DBG();
 122
 123         num_executions++;
 124         print_summary();
 125         if ((diverge = model->get_next_backtrack()) == NULL)
 126                 return false;
 127
 128         if (DBG_ENABLED()) {
 129                 printf("Next execution will diverge at:\n");
 130                 diverge->print();
 131         }
 132
 133         model->reset_to_initial_state();
 134         return true;
 135 }
 136
 137 ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 138 {
 139         action_type type = act->get_type();
 140
 141         switch (type) {
 142                 case THREAD_CREATE:
 143                 case THREAD_YIELD:
 144                 case THREAD_JOIN:
 145                         return NULL;
 146                 case ATOMIC_READ:
 147                 case ATOMIC_WRITE:
 148                 default:
 149                         break;
 150         }
 151         /* linear search: from most recent to oldest */
 152         action_list_t::reverse_iterator rit;
 153         for (rit = action_trace->rbegin(); rit != action_trace->rend(); rit++) {
 154                 ModelAction *prev = *rit;
 155                 if (act->is_dependent(prev))
 156                         return prev;
 157         }
 158         return NULL;
 159 }
 160
 161 void ModelChecker::set_backtracking(ModelAction *act)
 162 {
 163         ModelAction *prev;
 164         Node *node;
 165         Thread *t = get_thread(act->get_tid());
 166
 167         prev = get_last_conflict(act);
 168         if (prev == NULL)
 169                 return;
 170
 171         node = prev->get_node();
 172
 173         while (!node->is_enabled(t))
 174                 t = t->get_parent();
 175
 176         /* Check if this has been explored already */
 177         if (node->has_been_explored(t->get_id()))
 178                 return;
 179
 180         if (!next_backtrack || *prev > *next_backtrack)
 181                 next_backtrack = prev;
 182
 183         /* If this is a new backtracking point, mark the tree */
 184         if (!node->set_backtrack(t->get_id()))
 185                 return;
 186         DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
 187                         prev->get_tid(), t->get_id());
 188         if (DBG_ENABLED()) {
 189                 prev->print();
 190                 act->print();
 191         }
 192 }
 193
 194 ModelAction * ModelChecker::get_next_backtrack()
 195 {
 196         ModelAction *next = next_backtrack;
 197         next_backtrack = NULL;
 198         return next;
 199 }
 200
 201 void ModelChecker::check_current_action(void)
 202 {
 203         Node *currnode;
 204
 205         ModelAction *curr = this->current_action;
 206         current_action = NULL;
 207         if (!curr) {
 208                 DEBUG("trying to push NULL action...\n");
 209                 return;
 210         }
 211
 212         curr = node_stack->explore_action(curr, NULL);
 213         nextThread = get_next_replay_thread();
 214
 215         currnode = curr->get_node();
 216
 217         if (!currnode->backtrack_empty())
 218                 if (!next_backtrack || *curr > *next_backtrack)
 219                         next_backtrack = curr;
 220
 221         set_backtracking(curr);
 222         this->action_trace->push_back(curr);
 223
 224         std::vector<action_list_t> *vec = &(*obj_thrd_map)[curr->get_location()];
 225         if (id_to_int(curr->get_tid()) >= (int)vec->size())
 226                 vec->resize(next_thread_id);
 227         (*vec)[id_to_int(curr->get_tid())].push_back(curr);
 228 }
 229
 230 void ModelChecker::print_summary(void)
 231 {
 232         printf("\n");
 233         printf("Number of executions: %d\n", num_executions);
 234         printf("Total nodes created: %d\n", Node::get_total_nodes());
 235
 236         scheduler->print();
 237
 238         print_list(action_trace);
 239         printf("\n");
 240 }
 241
 242 void ModelChecker::print_list(action_list_t *list)
 243 {
 244         action_list_t::iterator it;
 245
 246         printf("---------------------------------------------------------------------\n");
 247         printf("Trace:\n");
 248
 249         for (it = list->begin(); it != list->end(); it++) {
 250                 (*it)->print();
 251         }
 252         printf("---------------------------------------------------------------------\n");
 253 }
 254
 255 int ModelChecker::add_thread(Thread *t)
 256 {
 257         (*thread_map)[id_to_int(t->get_id())] = t;
 258         scheduler->add_thread(t);
 259         return 0;
 260 }
 261
 262 void ModelChecker::remove_thread(Thread *t)
 263 {
 264         scheduler->remove_thread(t);
 265 }
 266
 267 int ModelChecker::switch_to_master(ModelAction *act)
 268 {
 269         Thread *old;
 270
 271         DBG();
 272         old = thread_current();
 273         set_current_action(act);
 274         old->set_state(THREAD_READY);
 275         return Thread::swap(old, get_system_context());
 276 }