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