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