scanalysis.cc

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