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