1 /* Copyright (c) 2015 Regents of the University of California
3 * Author: Brian Demsky <bdemsky@uci.edu>
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.
13 #include "constraint.h"
14 #include "storeloadset.h"
16 #include "execpoint.h"
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);
30 void LoadRF::genConstraints(ConstGen *cg) {
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);
39 RecordIterator *sri=mrfSet->iterator();
40 while(sri->hasNext()) {
41 EPRecord *store=sri->next();
42 Constraint ** storevalvars=sls->getValVars(cg, store);
45 Constraint *rfconst=(numvars==0) ? &ctrue : generateConstraint(numvars, vars, storeindex);
46 //if we read from a store, it should happen before us
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;
53 storebeforeload=&cfalse;
55 storebeforeload=cg->getOrderConstraint(store, load);
57 Constraint * storebeforeload=cg->getOrderConstraint(store, load);
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);
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};
72 ADDCONSTRAINT2(cg, new Constraint(IMPLIES, rfconst, new Constraint(AND, 4, array)), "storeaddressmatch");
75 //Also need to make sure that we don't have conflicting stores
76 //ordered between the load and store
78 RecordSet *conflictSet=cg->computeConflictSet(store, load, mrfSet);
79 RecordIterator *sit=conflictSet!=NULL ? conflictSet->iterator() : mrfSet->iterator();
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())
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;
94 conflictbeforeload=&cfalse;
96 conflictbeforeload=cg->getOrderConstraint(conflictstore, load);
98 if (conflictbeforeload->isFalse()) {
99 storebeforeconflict->freerec();
103 Constraint * conflictbeforeload=cg->getOrderConstraint(conflictstore, load);
104 if (conflictbeforeload->isFalse()) {
105 storebeforeconflict->freerec();
109 rfconst=generateConstraint(numvars, vars, storeindex);
110 Constraint *array[]={storebeforeconflict,
113 cg->getExecutionConstraint(conflictstore)};
114 Constraint *confstore=new Constraint(IMPLIES,
115 new Constraint(AND, 4, array),
116 generateEquivConstraint(numaddrvars, loadaddrvars, confstoreaddrvars)->negate());
118 ADDCONSTRAINT2(cg, confstore, "confstore");
121 if (conflictSet != NULL)
128 Constraint *mustrf=generateLTConstraint(cg, numvars, vars, storeindex);
129 Constraint *validrf=new Constraint(IMPLIES, cg->getExecutionConstraint(load), mustrf);
130 ADDCONSTRAINT2(cg, validrf, "validrf");