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