loadrf.cc

   1 /*      Copyright (c) 2015 Regents of the University of California
   2  *
   3  *      Author: Brian Demsky <bdemsky@uci.edu>
   4  *
   5  *      This program is free software; you can redistribute it and/or
   6  *      modify it under the terms of the GNU General Public License
   7  *      version 2 as published by the Free Software Foundation.
   8  */
   9
  10 #include "loadrf.h"
  11 #include "constgen.h"
  12 #include "mcutil.h"
  13 #include "constraint.h"
  14 #include "storeloadset.h"
  15 #include "eprecord.h"
  16 #include "execpoint.h"
  17
  18 LoadRF::LoadRF(EPRecord *_load, ConstGen *cg) : load(_load) {
  19         RecordSet *mrfSet=cg->getMayReadFromSet(load);
  20         uint numstores=mrfSet->getSize();
  21         numvars=NUMBITS(numstores-1);
  22         vars=(Constraint **)model_malloc(numvars*sizeof(Constraint *));
  23         cg->getArrayNewVars(numvars, vars);
  24 }
  25
  26 LoadRF::~LoadRF() {
  27         model_free(vars);
  28 }
  29
  30 void LoadRF::genConstraints(ConstGen *cg) {
  31         uint storeindex=0;
  32         RecordSet *mrfSet=cg->getMayReadFromSet(load);
  33         StoreLoadSet * sls=cg->getStoreLoadSet(load);
  34         uint numvalvars=sls->getNumValVars();
  35         uint numaddrvars=sls->getNumAddrVars();
  36         Constraint ** loadvalvars=(load->getType()==RMW)?sls->getRMWRValVars(cg, load):sls->getValVars(cg, load);
  37         Constraint ** loadaddrvars=sls->getAddrVars(cg, load);
  38
  39         RecordIterator *sri=mrfSet->iterator();
  40         while(sri->hasNext()) {
  41                 EPRecord *store=sri->next();
  42                 Constraint ** storevalvars=sls->getValVars(cg, store);
  43
  44
  45                 Constraint *rfconst=(numvars==0)?&ctrue:generateConstraint(numvars, vars, storeindex);
  46                 //if we read from a store, it should happen before us
  47 #ifdef TSO
  48                 Constraint *storebeforeload;
  49                 if (store->getEP()->get_tid()==load->getEP()->get_tid()) {
  50                         if (store->getEP()->compare(load->getEP())==CR_AFTER) {
  51                                 storebeforeload=&ctrue;
  52                         } else
  53                                 storebeforeload=&cfalse;
  54                 } else
  55                         storebeforeload=cg->getOrderConstraint(store, load);
  56 #else
  57                 Constraint * storebeforeload=cg->getOrderConstraint(store, load);
  58 #endif
  59                 //if we read from a store, we should have the same value
  60                 Constraint *storevalmatch=generateEquivConstraint(numvalvars, loadvalvars, storevalvars);
  61                 //if we read from a store, it must have been executed
  62                 Constraint *storeexecuted=cg->getExecutionConstraint(store);
  63
  64
  65
  66                 //if we read from a store, we should have the same address
  67                 Constraint ** storeaddrvars=sls->getAddrVars(cg, store);
  68                 Constraint * storeaddressmatch=generateEquivConstraint(numaddrvars, loadaddrvars, storeaddrvars);
  69                 Constraint *array[] = {storebeforeload, storevalmatch, storeexecuted, storeaddressmatch};
  70
  71
  72                 ADDCONSTRAINT2(cg, new Constraint(IMPLIES, rfconst, new Constraint(AND, 4, array)), "storeaddressmatch");
  73
  74
  75                 //Also need to make sure that we don't have conflicting stores
  76                 //ordered between the load and store
  77
  78                 RecordSet *conflictSet=cg->computeConflictSet(store, load, mrfSet);
  79                 RecordIterator *sit=conflictSet!=NULL?conflictSet->iterator():mrfSet->iterator();
  80
  81                 while(sit->hasNext()) {
  82                         EPRecord *conflictstore=sit->next();
  83                         Constraint ** confstoreaddrvars=sls->getAddrVars(cg, conflictstore);
  84                         Constraint * storebeforeconflict=cg->getOrderConstraint(store, conflictstore);
  85                         if (storebeforeconflict->isFalse())
  86                                 continue;
  87 #ifdef TSO
  88                         //Have to cover the same thread case
  89                         Constraint *conflictbeforeload;
  90                         if (conflictstore->getEP()->get_tid()==load->getEP()->get_tid()) {
  91                                 if (conflictstore->getEP()->compare(load->getEP())==CR_AFTER)
  92                                         conflictbeforeload=&ctrue;
  93                                 else
  94                                         conflictbeforeload=&cfalse;
  95                         } else {
  96                                 conflictbeforeload=cg->getOrderConstraint(conflictstore, load);
  97                         }
  98                         if (conflictbeforeload->isFalse()) {
  99                                 storebeforeconflict->freerec();
 100                                 continue;
 101                         }
 102 #else
 103                         Constraint * conflictbeforeload=cg->getOrderConstraint(conflictstore, load);
 104                         if (conflictbeforeload->isFalse()) {
 105                                 storebeforeconflict->freerec();
 106                                 continue;
 107                         }
 108 #endif
 109                         rfconst=generateConstraint(numvars, vars, storeindex);
 110                         Constraint *array[]={storebeforeconflict,
 111                                                                                                          conflictbeforeload,
 112                                                                                                          rfconst,
 113                                                                                                          cg->getExecutionConstraint(conflictstore)};
 114                         Constraint *confstore=new Constraint(IMPLIES,
 115                                                                                                                                                                          new Constraint(AND, 4, array),
 116                                                                                                                                                                          generateEquivConstraint(numaddrvars, loadaddrvars, confstoreaddrvars)->negate());
 117
 118                         ADDCONSTRAINT2(cg, confstore, "confstore");
 119                 }
 120                 delete sit;
 121                 if (conflictSet != NULL)
 122                         delete conflictSet;
 123
 124                 storeindex++;
 125         }
 126         delete sri;
 127
 128         Constraint *mustrf=generateLTConstraint(cg, numvars, vars, storeindex);
 129         Constraint *validrf=new Constraint(IMPLIES, cg->getExecutionConstraint(load), mustrf);
 130         ADDCONSTRAINT2(cg, validrf, "validrf");
 131 }