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