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 "common.h"
   8
   9 #define INITIAL_THREAD_ID       0
  10
  11 ModelChecker *model;
  12
  13 ModelChecker::ModelChecker()
  14 {
  15         /* First thread created will have id (INITIAL_THREAD_ID + 1) */
  16         this->used_thread_id = INITIAL_THREAD_ID;
  17         /* Initialize default scheduler */
  18         this->scheduler = new Scheduler();
  19
  20         num_executions = 0;
  21         this->current_action = NULL;
  22         this->exploring = NULL;
  23         this->nextThread = THREAD_ID_T_NONE;
  24
  25         rootNode = new TreeNode(NULL);
  26         currentNode = rootNode;
  27         action_trace = new action_list_t();
  28 }
  29
  30 ModelChecker::~ModelChecker()
  31 {
  32         delete action_trace;
  33         delete this->scheduler;
  34         delete rootNode;
  35 }
  36
  37 void ModelChecker::reset_to_initial_state()
  38 {
  39         DEBUG("+++ Resetting to initial state +++\n");
  40         std::map<thread_id_t, class Thread *>::iterator it;
  41         for (it = thread_map.begin(); it != thread_map.end(); it++) {
  42                 delete (*it).second;
  43         }
  44         thread_map.clear();
  45         action_trace = new action_list_t();
  46         currentNode = rootNode;
  47         current_action = NULL;
  48         used_thread_id = INITIAL_THREAD_ID;
  49         /* scheduler reset ? */
  50 }
  51
  52 int ModelChecker::get_next_id()
  53 {
  54         return ++used_thread_id;
  55 }
  56
  57 Thread * ModelChecker::schedule_next_thread()
  58 {
  59         Thread *t;
  60         if (nextThread == THREAD_ID_T_NONE)
  61                 return NULL;
  62         t = thread_map[nextThread];
  63         if (t == NULL)
  64                 DEBUG("*** error: thread not in thread_map: id = %d\n", nextThread);
  65         return t;
  66 }
  67
  68 /*
  69  * get_next_replay_thread() - Choose the next thread in the replay sequence
  70  *
  71  * If we've reached the 'diverge' point, then we pick a thread from the
  72  *   backtracking set.
  73  * Otherwise, we simply return the next thread in the sequence.
  74  */
  75 thread_id_t ModelChecker::get_next_replay_thread()
  76 {
  77         ModelAction *next;
  78         thread_id_t tid;
  79
  80         next = exploring->get_state();
  81
  82         if (next == exploring->get_diverge()) {
  83                 TreeNode *node = next->get_node();
  84
  85                 /* Reached divergence point; discard our current 'exploring' */
  86                 DEBUG("*** Discard 'Backtrack' object ***\n");
  87                 tid = node->getNextBacktrack();
  88                 delete exploring;
  89                 exploring = NULL;
  90         } else {
  91                 tid = next->get_tid();
  92         }
  93         DEBUG("*** ModelChecker chose next thread = %d ***\n", tid);
  94         return tid;
  95 }
  96
  97 thread_id_t ModelChecker::advance_backtracking_state()
  98 {
  99         /* Have we completed exploring the preselected path? */
 100         if (exploring == NULL)
 101                 return THREAD_ID_T_NONE;
 102
 103         /* Else, we are trying to replay an execution */
 104         exploring->advance_state();
 105         if (exploring->get_state() == NULL)
 106                 DEBUG("*** error: reached end of backtrack trace\n");
 107
 108         return get_next_replay_thread();
 109 }
 110
 111 bool ModelChecker::next_execution()
 112 {
 113         num_executions++;
 114         print_summary();
 115         if ((exploring = model->get_next_backtrack()) == NULL)
 116                 return false;
 117         model->reset_to_initial_state();
 118         nextThread = get_next_replay_thread();
 119         return true;
 120 }
 121
 122 ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 123 {
 124         action_type type = act->get_type();
 125
 126         switch (type) {
 127                 case THREAD_CREATE:
 128                 case THREAD_YIELD:
 129                 case THREAD_JOIN:
 130                         return NULL;
 131                 case ATOMIC_READ:
 132                 case ATOMIC_WRITE:
 133                 default:
 134                         break;
 135         }
 136         /* linear search: from most recent to oldest */
 137         action_list_t::reverse_iterator rit;
 138         for (rit = action_trace->rbegin(); rit != action_trace->rend(); rit++) {
 139                 ModelAction *prev = *rit;
 140                 if (act->is_dependent(prev))
 141                         return prev;
 142         }
 143         return NULL;
 144 }
 145
 146 void ModelChecker::set_backtracking(ModelAction *act)
 147 {
 148         ModelAction *prev;
 149         TreeNode *node;
 150
 151         prev = get_last_conflict(act);
 152         if (prev == NULL)
 153                 return;
 154
 155         node = prev->get_node();
 156
 157         /* Check if this has been explored already */
 158         if (node->hasBeenExplored(act->get_tid()))
 159                 return;
 160         /* If this is a new backtracking point, mark the tree */
 161         if (node->setBacktrack(act->get_tid()) != 0)
 162                 return;
 163
 164         DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
 165                         prev->get_tid(), act->get_tid());
 166         if (DBG_ENABLED()) {
 167                 prev->print();
 168                 act->print();
 169         }
 170
 171         Backtrack *back = new Backtrack(prev, action_trace);
 172         backtrack_list.push_back(back);
 173 }
 174
 175 Backtrack * ModelChecker::get_next_backtrack()
 176 {
 177         Backtrack *next;
 178         if (backtrack_list.empty())
 179                 return NULL;
 180         next = backtrack_list.back();
 181         backtrack_list.pop_back();
 182         return next;
 183 }
 184
 185 void ModelChecker::check_current_action(void)
 186 {
 187         ModelAction *next = this->current_action;
 188
 189         if (!next) {
 190                 DEBUG("trying to push NULL action...\n");
 191                 return;
 192         }
 193         current_action = NULL;
 194         nextThread = advance_backtracking_state();
 195         next->set_node(currentNode);
 196         set_backtracking(next);
 197         currentNode = currentNode->exploreChild(next->get_tid());
 198         this->action_trace->push_back(next);
 199 }
 200
 201 void ModelChecker::print_summary(void)
 202 {
 203         action_list_t::iterator it;
 204
 205         printf("\n");
 206         printf("---------------------------------------------------------------------\n");
 207         printf("Number of executions: %d\n", num_executions);
 208         printf("Total nodes created: %d\n\n", TreeNode::getTotalNodes());
 209
 210         scheduler->print();
 211
 212         printf("Trace:\n\n");
 213
 214         for (it = action_trace->begin(); it != action_trace->end(); it++) {
 215                 DBG();
 216                 (*it)->print();
 217         }
 218         printf("---------------------------------------------------------------------\n");
 219 }
 220
 221 int ModelChecker::add_thread(Thread *t)
 222 {
 223         thread_map[t->get_id()] = t;
 224         scheduler->add_thread(t);
 225         return 0;
 226 }
 227
 228 void ModelChecker::remove_thread(Thread *t)
 229 {
 230         scheduler->remove_thread(t);
 231 }
 232
 233 int ModelChecker::switch_to_master(ModelAction *act)
 234 {
 235         Thread *old;
 236
 237         DBG();
 238         old = thread_current();
 239         set_current_action(act);
 240         old->set_state(THREAD_READY);
 241         return Thread::swap(old, get_system_context());
 242 }
 243
 244 ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int value)
 245 {
 246         Thread *t = thread_current();
 247         ModelAction *act = this;
 248
 249         act->type = type;
 250         act->order = order;
 251         act->location = loc;
 252         act->tid = t->get_id();
 253         act->value = value;
 254 }
 255
 256 bool ModelAction::is_read()
 257 {
 258         return type == ATOMIC_READ;
 259 }
 260
 261 bool ModelAction::is_write()
 262 {
 263         return type == ATOMIC_WRITE;
 264 }
 265
 266 bool ModelAction::is_acquire()
 267 {
 268         switch (order) {
 269         case memory_order_acquire:
 270         case memory_order_acq_rel:
 271         case memory_order_seq_cst:
 272                 return true;
 273         default:
 274                 return false;
 275         }
 276 }
 277
 278 bool ModelAction::is_release()
 279 {
 280         switch (order) {
 281         case memory_order_release:
 282         case memory_order_acq_rel:
 283         case memory_order_seq_cst:
 284                 return true;
 285         default:
 286                 return false;
 287         }
 288 }
 289
 290 bool ModelAction::same_var(ModelAction *act)
 291 {
 292         return location == act->location;
 293 }
 294
 295 bool ModelAction::same_thread(ModelAction *act)
 296 {
 297         return tid == act->tid;
 298 }
 299
 300 bool ModelAction::is_dependent(ModelAction *act)
 301 {
 302         if (!is_read() && !is_write())
 303                 return false;
 304         if (!act->is_read() && !act->is_write())
 305                 return false;
 306         if (same_var(act) && !same_thread(act) &&
 307                         (is_write() || act->is_write()))
 308                 return true;
 309         return false;
 310 }
 311
 312 void ModelAction::print(void)
 313 {
 314         const char *type_str;
 315         switch (this->type) {
 316         case THREAD_CREATE:
 317                 type_str = "thread create";
 318                 break;
 319         case THREAD_YIELD:
 320                 type_str = "thread yield";
 321                 break;
 322         case THREAD_JOIN:
 323                 type_str = "thread join";
 324                 break;
 325         case ATOMIC_READ:
 326                 type_str = "atomic read";
 327                 break;
 328         case ATOMIC_WRITE:
 329                 type_str = "atomic write";
 330                 break;
 331         default:
 332                 type_str = "unknown type";
 333         }
 334
 335         printf("Thread: %d\tAction: %s\tMO: %d\tLoc: %#014zx\tValue: %d\n", tid, type_str, order, (size_t)location, value);
 336 }