scanalysis.cc

   1 #include "scanalysis.h"
   2 #include "action.h"
   3 #include "threads-model.h"
   4 #include "clockvector.h"
   5 #include "execution.h"
   6
   7 SCAnalysis::SCAnalysis() :
   8         cvmap(),
   9         cyclic(false),
  10         badrfset(),
  11         lastwrmap(),
  12         threadlists(1),
  13         execution(NULL),
  14         print_always(false),
  15         print_buggy(true)
  16 {
  17 }
  18
  19 SCAnalysis::~SCAnalysis() {
  20 }
  21
  22 void SCAnalysis::setExecution(ModelExecution * execution) {
  23         this->execution=execution;
  24 }
  25
  26 const char * SCAnalysis::name() {
  27         const char * name = "SC";
  28         return name;
  29 }
  30
  31 bool SCAnalysis::option(char * opt) {
  32         if (strcmp(opt, "verbose")==0) {
  33                 print_always=true;
  34                 return false;
  35         } else if (strcmp(opt, "buggy")==0) {
  36                 return false;
  37         } else if (strcmp(opt, "quiet")==0) {
  38                 print_buggy=false;
  39                 return false;
  40         } if (strcmp(opt, "help") != 0) {
  41                 model_print("Unrecognized option: %s\n", opt);
  42         }
  43
  44         model_print("SC Analysis options\n");
  45         model_print("verbose -- print all feasible executions\n");
  46         model_print("buggy -- print only buggy executions (default)\n");
  47         model_print("quiet -- print nothing\n");
  48         model_print("\n");
  49
  50         return true;
  51 }
  52
  53 void SCAnalysis::print_list(action_list_t *list) {
  54         model_print("---------------------------------------------------------------------\n");
  55         if (cyclic)
  56                 model_print("Not SC\n");
  57         unsigned int hash = 0;
  58
  59         for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
  60                 const ModelAction *act = *it;
  61                 if (act->get_seq_number() > 0) {
  62                         if (badrfset.contains(act))
  63                                 model_print("BRF ");
  64                         act->print();
  65                         if (badrfset.contains(act)) {
  66                                 model_print("Desired Rf: %u \n", badrfset.get(act)->get_seq_number());
  67                         }
  68                 }
  69                 hash = hash ^ (hash << 3) ^ ((*it)->hash());
  70         }
  71         model_print("HASH %u\n", hash);
  72         model_print("---------------------------------------------------------------------\n");
  73 }
  74
  75 void SCAnalysis::analyze(action_list_t *actions) {
  76         action_list_t *list = generateSC(actions);
  77         check_rf(list);
  78         if (print_always || (print_buggy && execution->have_bug_reports()))
  79                 print_list(list);
  80 }
  81
  82 void SCAnalysis::check_rf(action_list_t *list) {
  83         for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
  84                 const ModelAction *act = *it;
  85                 if (act->is_read()) {
  86                         if (act->get_reads_from() != lastwrmap.get(act->get_location()))
  87                                 badrfset.put(act, lastwrmap.get(act->get_location()));
  88                 }
  89                 if (act->is_write())
  90                         lastwrmap.put(act->get_location(), act);
  91         }
  92 }
  93
  94 bool SCAnalysis::merge(ClockVector *cv, const ModelAction *act, const ModelAction *act2) {
  95         ClockVector *cv2 = cvmap.get(act2);
  96         if (cv2 == NULL)
  97                 return true;
  98         if (cv2->getClock(act->get_tid()) >= act->get_seq_number() && act->get_seq_number() != 0) {
  99                 cyclic = true;
 100                 //refuse to introduce cycles into clock vectors
 101                 return false;
 102         }
 103
 104         return cv->merge(cv2);
 105 }
 106
 107 int SCAnalysis::getNextActions(ModelAction ** array) {
 108         int count=0;
 109
 110         for (int t = 0; t <= maxthreads; t++) {
 111                 action_list_t *tlt = &threadlists[t];
 112                 if (tlt->empty())
 113                         continue;
 114                 ModelAction *act = tlt->front();
 115                 ClockVector *cv = cvmap.get(act);
 116
 117                 /* Find the earliest in SC ordering */
 118                 for (int i = 0; i <= maxthreads; i++) {
 119                         if ( i == t )
 120                                 continue;
 121                         action_list_t *threadlist = &threadlists[i];
 122                         if (threadlist->empty())
 123                                 continue;
 124                         ModelAction *first = threadlist->front();
 125                         if (cv->synchronized_since(first)) {
 126                                 act = NULL;
 127                                 break;
 128                         }
 129                 }
 130                 if (act != NULL) {
 131                         array[count++]=act;
 132                 }
 133         }
 134         if (count != 0)
 135                 return count;
 136         for (int t = 0; t <= maxthreads; t++) {
 137                 action_list_t *tlt = &threadlists[t];
 138                 if (tlt->empty())
 139                         continue;
 140                 ModelAction *act = tlt->front();
 141                 ClockVector *cv = act->get_cv();
 142
 143                 /* Find the earliest in SC ordering */
 144                 for (int i = 0; i <= maxthreads; i++) {
 145                         if ( i == t )
 146                                 continue;
 147                         action_list_t *threadlist = &threadlists[i];
 148                         if (threadlist->empty())
 149                                 continue;
 150                         ModelAction *first = threadlist->front();
 151                         if (cv->synchronized_since(first)) {
 152                                 act = NULL;
 153                                 break;
 154                         }
 155                 }
 156                 if (act != NULL) {
 157                         array[count++]=act;
 158                 }
 159         }
 160
 161         ASSERT(count==0 || cyclic);
 162
 163         return count;
 164 }
 165
 166 ModelAction * SCAnalysis::pruneArray(ModelAction **array,int count) {
 167         /* No choice */
 168         if (count == 1)
 169                 return array[0];
 170
 171         /* Choose first non-write action */
 172         ModelAction *nonwrite=NULL;
 173         for(int i=0;i<count;i++) {
 174                 if (!array[i]->is_write())
 175                         if (nonwrite==NULL || nonwrite->get_seq_number() > array[i]->get_seq_number())
 176                                 nonwrite = array[i];
 177         }
 178         if (nonwrite != NULL)
 179                 return nonwrite;
 180
 181         /* Look for non-conflicting action */
 182         ModelAction *nonconflict=NULL;
 183         for(int a=0;a<count;a++) {
 184                 ModelAction *act=array[a];
 185                 for (int i = 0; i <= maxthreads && act != NULL; i++) {
 186                         thread_id_t tid = int_to_id(i);
 187                         if (tid == act->get_tid())
 188                                 continue;
 189
 190                         action_list_t *list = &threadlists[id_to_int(tid)];
 191                         for (action_list_t::iterator rit = list->begin(); rit != list->end(); rit++) {
 192                                 ModelAction *write = *rit;
 193                                 if (!write->is_write())
 194                                         continue;
 195                                 ClockVector *writecv = cvmap.get(write);
 196                                 if (writecv->synchronized_since(act))
 197                                         break;
 198                                 if (write->get_location() == act->get_location()) {
 199                                         //write is sc after act
 200                                         act = NULL;
 201                                         break;
 202                                 }
 203                         }
 204                 }
 205                 if (act != NULL) {
 206                         if (nonconflict == NULL || nonconflict->get_seq_number() > act->get_seq_number())
 207                                 nonconflict=act;
 208                 }
 209         }
 210         return nonconflict;
 211 }
 212
 213 action_list_t * SCAnalysis::generateSC(action_list_t *list) {
 214         int numactions=buildVectors(list);
 215         computeCV(list);
 216
 217         action_list_t *sclist = new action_list_t();
 218         ModelAction **array = (ModelAction **)model_calloc(1, (maxthreads + 1) * sizeof(ModelAction *));
 219         int * choices = (int *) model_calloc(1, sizeof(int)*numactions);
 220         int endchoice = 0;
 221         int currchoice = 0;
 222         int lastchoice = -1;
 223         while (true) {
 224                 int numActions = getNextActions(array);
 225                 if (numActions == 0)
 226                         break;
 227                 ModelAction * act=pruneArray(array, numActions);
 228                 if (act == NULL) {
 229                         if (currchoice < endchoice) {
 230                                 act = array[choices[currchoice]];
 231                                 //check whether there is still another option
 232                                 if ((choices[currchoice]+1)<numActions)
 233                                         lastchoice=currchoice;
 234                                 currchoice++;
 235                         } else {
 236                                 act = array[0];
 237                                 choices[currchoice]=0;
 238                                 if (numActions>1)
 239                                         lastchoice=currchoice;
 240                                 currchoice++;
 241                         }
 242                 }
 243                 thread_id_t tid = act->get_tid();
 244                 //remove action
 245                 threadlists[id_to_int(tid)].pop_front();
 246                 //add ordering constraints from this choice
 247                 if (updateConstraints(act)) {
 248                         //propagate changes if we have them
 249                         bool prevc=cyclic;
 250                         computeCV(list);
 251                         if (!prevc && cyclic) {
 252                                 model_print("ROLLBACK in SC\n");
 253                                 //check whether we have another choice
 254                                 if (lastchoice != -1) {
 255                                         //have to reset everything
 256                                         choices[lastchoice]++;
 257                                         endchoice=lastchoice+1;
 258                                         currchoice=0;
 259                                         lastchoice=-1;
 260                                         reset(list);
 261                                         buildVectors(list);
 262                                         computeCV(list);
 263                                         sclist->clear();
 264                                         continue;
 265                                 }
 266                         }
 267                 }
 268                 //add action to end
 269                 sclist->push_back(act);
 270         }
 271         model_free(array);
 272         return sclist;
 273 }
 274
 275 int SCAnalysis::buildVectors(action_list_t *list) {
 276         maxthreads = 0;
 277         int numactions = 0;
 278         for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
 279                 ModelAction *act = *it;
 280                 numactions++;
 281                 int threadid = id_to_int(act->get_tid());
 282                 if (threadid > maxthreads) {
 283                         threadlists.resize(threadid + 1);
 284                         maxthreads = threadid;
 285                 }
 286                 threadlists[threadid].push_back(act);
 287         }
 288         return numactions;
 289 }
 290
 291 void SCAnalysis::reset(action_list_t *list) {
 292         for (int t = 0; t <= maxthreads; t++) {
 293                 action_list_t *tlt = &threadlists[t];
 294                 tlt->clear();
 295         }
 296         for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
 297                 ModelAction *act = *it;
 298                 delete cvmap.get(act);
 299                 cvmap.put(act, NULL);
 300         }
 301
 302         cyclic=false;
 303 }
 304
 305 bool SCAnalysis::updateConstraints(ModelAction *act) {
 306         bool changed = false;
 307         for (int i = 0; i <= maxthreads; i++) {
 308                 thread_id_t tid = int_to_id(i);
 309                 if (tid == act->get_tid())
 310                         continue;
 311
 312                 action_list_t *list = &threadlists[id_to_int(tid)];
 313                 for (action_list_t::iterator rit = list->begin(); rit != list->end(); rit++) {
 314                         ModelAction *write = *rit;
 315                         if (!write->is_write())
 316                                 continue;
 317                         ClockVector *writecv = cvmap.get(write);
 318                         if (writecv->synchronized_since(act))
 319                                 break;
 320                         if (write->get_location() == act->get_location()) {
 321                                 //write is sc after act
 322                                 merge(writecv, write, act);
 323                                 changed = true;
 324                                 break;
 325                         }
 326                 }
 327         }
 328         return changed;
 329 }
 330
 331 bool SCAnalysis::processRead(ModelAction *read, ClockVector *cv) {
 332         bool changed = false;
 333
 334         /* Merge in the clock vector from the write */
 335         const ModelAction *write = read->get_reads_from();
 336         ClockVector *writecv = cvmap.get(write);
 337         changed |= merge(cv, read, write) && (*read < *write);
 338
 339         for (int i = 0; i <= maxthreads; i++) {
 340                 thread_id_t tid = int_to_id(i);
 341                 if (tid == read->get_tid())
 342                         continue;
 343                 if (tid == write->get_tid())
 344                         continue;
 345                 action_list_t *list = execution->get_actions_on_obj(read->get_location(), tid);
 346                 if (list == NULL)
 347                         continue;
 348                 for (action_list_t::reverse_iterator rit = list->rbegin(); rit != list->rend(); rit++) {
 349                         ModelAction *write2 = *rit;
 350                         if (!write2->is_write())
 351                                 continue;
 352
 353                         ClockVector *write2cv = cvmap.get(write2);
 354                         if (write2cv == NULL)
 355                                 continue;
 356
 357                         /* write -sc-> write2 &&
 358                                  write -rf-> R =>
 359                                  R -sc-> write2 */
 360                         if (write2cv->synchronized_since(write)) {
 361                                 changed |= merge(write2cv, write2, read);
 362                         }
 363
 364                         //looking for earliest write2 in iteration to satisfy this
 365                         /* write2 -sc-> R &&
 366                                  write -rf-> R =>
 367                                  write2 -sc-> write */
 368                         if (cv->synchronized_since(write2)) {
 369                                 changed |= writecv == NULL || merge(writecv, write, write2);
 370                                 break;
 371                         }
 372                 }
 373         }
 374         return changed;
 375 }
 376
 377 void SCAnalysis::computeCV(action_list_t *list) {
 378         bool changed = true;
 379         bool firsttime = true;
 380         ModelAction **last_act = (ModelAction **)model_calloc(1, (maxthreads + 1) * sizeof(ModelAction *));
 381         while (changed) {
 382                 changed = changed&firsttime;
 383                 firsttime = false;
 384
 385                 for (action_list_t::iterator it = list->begin(); it != list->end(); it++) {
 386                         ModelAction *act = *it;
 387                         ModelAction *lastact = last_act[id_to_int(act->get_tid())];
 388                         if (act->is_thread_start())
 389                                 lastact = execution->get_thread(act)->get_creation();
 390                         last_act[id_to_int(act->get_tid())] = act;
 391                         ClockVector *cv = cvmap.get(act);
 392                         if (cv == NULL) {
 393                                 cv = new ClockVector(NULL, act);
 394                                 cvmap.put(act, cv);
 395                         }
 396                         if (lastact != NULL) {
 397                                 merge(cv, act, lastact);
 398                         }
 399                         if (act->is_thread_join()) {
 400                                 Thread *joinedthr = act->get_thread_operand();
 401                                 ModelAction *finish = execution->get_last_action(joinedthr->get_id());
 402                                 changed |= merge(cv, act, finish);
 403                         }
 404                         if (act->is_read()) {
 405                                 changed |= processRead(act, cv);
 406                         }
 407                 }
 408                 /* Reset the last action array */
 409                 if (changed) {
 410                         bzero(last_act, (maxthreads + 1) * sizeof(ModelAction *));
 411                 }
 412         }
 413         model_free(last_act);
 414 }