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