void resetstoreloadtable(StoreLoadSetHashTable * storeloadtable) {
for(uint i=0;i<storeloadtable->capacity;i++) {
void resetstoreloadtable(StoreLoadSetHashTable * storeloadtable) {
for(uint i=0;i<storeloadtable->capacity;i++) {
#endif
model_print("start %lu, finish %lu\n", start,finish);
model_print("Incremental time = %12.6f\n", ((double)(finish-start))/1000000);
#endif
model_print("start %lu, finish %lu\n", start,finish);
model_print("Incremental time = %12.6f\n", ((double)(finish-start))/1000000);
//Zero out the achieved goals
for(uint i=0;i<goalset->size();i++) {
Constraint *var=goalvararray[i];
//Zero out the achieved goals
for(uint i=0;i<goalset->size();i++) {
Constraint *var=goalvararray[i];
model_print("start %lu, finish %lu\n", start,finish);
model_print("Initial time = %12.6f\n", ((double)(finish-start))/1000000);
model_print("start %lu, finish %lu\n", start,finish);
model_print("Initial time = %12.6f\n", ((double)(finish-start))/1000000);
//Zero out the achieved goals
for(uint i=0;i<goalset->size();i++) {
Constraint *var=goalvararray[i];
//Zero out the achieved goals
for(uint i=0;i<goalset->size();i++) {
Constraint *var=goalvararray[i];
schedule_graph++;
int file=open(buffer,O_WRONLY|O_CREAT|O_TRUNC, S_IRWXU);
model_dprintf(file, "digraph eventgraph {\n");
schedule_graph++;
int file=open(buffer,O_WRONLY|O_CREAT|O_TRUNC, S_IRWXU);
model_dprintf(file, "digraph eventgraph {\n");
EPRecord *first=execution->getEPRecord(MCID_FIRST);
printRecord(first, file);
while(!workstack->empty()) {
EPRecord *first=execution->getEPRecord(MCID_FIRST);
printRecord(first, file);
while(!workstack->empty()) {
model_dprintf(file, "\"];\n");
if (record->getNextRecord()!=NULL)
model_dprintf(file, "%lu->%lu;\n", (uintptr_t) record, (uintptr_t) record->getNextRecord());
model_dprintf(file, "\"];\n");
if (record->getNextRecord()!=NULL)
model_dprintf(file, "%lu->%lu;\n", (uintptr_t) record, (uintptr_t) record->getNextRecord());
if (record->getChildRecord()!=NULL)
model_dprintf(file, "%lu->%lu[color=red];\n", (uintptr_t) record, (uintptr_t) record->getChildRecord());
}
if (record->getChildRecord()!=NULL)
model_dprintf(file, "%lu->%lu[color=red];\n", (uintptr_t) record, (uintptr_t) record->getChildRecord());
}
workstack->push_back(next);
for(uint i=0;i<record->numValues();i++) {
EPValue *branchdir=record->getValue(i);
workstack->push_back(next);
for(uint i=0;i<record->numValues();i++) {
EPValue *branchdir=record->getValue(i);
//Could have an empty branch, so make sure the branch actually
//runs code
if (branchdir->getFirstRecord()!=NULL) {
//Could have an empty branch, so make sure the branch actually
//runs code
if (branchdir->getFirstRecord()!=NULL) {
- potentially share a location, and build partitions of memory
- locations such that all memory locations that can share the same
- address are in the same group.
-
- These memory operations should share an encoding of addresses and
- values.
-*/
+ potentially share a location, and build partitions of memory
+ locations such that all memory locations that can share the same
+ address are in the same group.
+
+ These memory operations should share an encoding of addresses and
+ values.
+ */
RecordSet *srscopy=baseset->copy();
RecordIterator *sri=srscopy->iterator();
while(sri->hasNext()) {
bool pruneconflictstore=false;
EPRecord *conflictstore=sri->next();
bool conflictafterstore=getOrderConstraint(store,conflictstore)->isTrue();
RecordSet *srscopy=baseset->copy();
RecordIterator *sri=srscopy->iterator();
while(sri->hasNext()) {
bool pruneconflictstore=false;
EPRecord *conflictstore=sri->next();
bool conflictafterstore=getOrderConstraint(store,conflictstore)->isTrue();
bool checkbeforeconflict=getOrderConstraint(checkstore,conflictstore)->isTrue();
if (!checkbeforeconflict)
continue;
bool checkbeforeconflict=getOrderConstraint(checkstore,conflictstore)->isTrue();
if (!checkbeforeconflict)
continue;
//See if the checkstore must store to the relevant address
IntHashSet * storeaddr=checkstore->getSet(VC_ADDRINDEX);
//See if the checkstore must store to the relevant address
IntHashSet * storeaddr=checkstore->getSet(VC_ADDRINDEX);
//See if the checkstore must store to the relevant address
IntHashSet * storeaddr=checkstore->getSet(VC_ADDRINDEX);
if (storeaddr->getSize()!=1 || !storeaddr->contains((uint64_t)commonaddr))
//See if the checkstore must store to the relevant address
IntHashSet * storeaddr=checkstore->getSet(VC_ADDRINDEX);
if (storeaddr->getSize()!=1 || !storeaddr->contains((uint64_t)commonaddr))
RecordSet * ConstGen::getMayReadFromSet(EPRecord *load) {
if (load->getSet(VC_ADDRINDEX)->getSize()==1)
return getMayReadFromSetOpt(load);
RecordSet * ConstGen::getMayReadFromSet(EPRecord *load) {
if (load->getSet(VC_ADDRINDEX)->getSize()==1)
return getMayReadFromSetOpt(load);
RecordSet *srs=loadtable->get(load);
ExecPoint *epload=load->getEP();
thread_id_t loadtid=epload->get_tid();
RecordSet *srs=loadtable->get(load);
ExecPoint *epload=load->getEP();
thread_id_t loadtid=epload->get_tid();
void ConstGen::mergeSets(StoreLoadSet *to, StoreLoadSet *from) {
RecordIterator * sri=from->iterator();
void ConstGen::mergeSets(StoreLoadSet *to, StoreLoadSet *from) {
RecordIterator * sri=from->iterator();
- in the first loop and the last constraint in the last loop.
- I tried this and performance suffered on linuxrwlocks and
- linuxlocks at the current time. BD - August 2014*/
+ in the first loop and the last constraint in the last loop.
+ I tried this and performance suffered on linuxrwlocks and
+ linuxlocks at the current time. BD - August 2014*/
Constraint *c21=getOrderConstraint(t2rec, t1rec);
/* short circuit for the trivial case */
if (c21->isTrue())
continue;
Constraint *c21=getOrderConstraint(t2rec, t1rec);
/* short circuit for the trivial case */
if (c21->isTrue())
continue;
for(uint t3i=t2i+1;t3i<t2vec->size();t3i++) {
EPRecord *t3rec=(*t2vec)[t3i];
Constraint *c13=getOrderConstraint(t1rec, t3rec);
for(uint t3i=t2i+1;t3i<t2vec->size();t3i++) {
EPRecord *t3rec=(*t2vec)[t3i];
Constraint *c13=getOrderConstraint(t1rec, t3rec);
Constraint *intratransorder=new Constraint(OR, c21, c13);
#endif
ADDCONSTRAINT(intratransorder,"intratransorder");
Constraint *intratransorder=new Constraint(OR, c21, c13);
#endif
ADDCONSTRAINT(intratransorder,"intratransorder");
Constraint *intratransorder=new Constraint(OR, c21, c02);
#endif
ADDCONSTRAINT(intratransorder,"intratransorder");
Constraint *intratransorder=new Constraint(OR, c21, c02);
#endif
ADDCONSTRAINT(intratransorder,"intratransorder");
bool * ConstGen::runSolver() {
int solution=solver->solve();
if (solution == IS_UNSAT) {
bool * ConstGen::runSolver() {
int solution=solver->solve();
if (solution == IS_UNSAT) {
Constraint * ConstGen::getRetValueEncoding(EPRecord *record, uint64_t value) {
switch(record->getType()) {
Constraint * ConstGen::getRetValueEncoding(EPRecord *record, uint64_t value) {
switch(record->getType()) {
Constraint * ConstGen::getExecutionConstraint(EPRecord *record) {
EPValue *branch=record->getBranch();
RecordSet *srs=execcondtable->get(record);
Constraint * ConstGen::getExecutionConstraint(EPRecord *record) {
EPValue *branch=record->getBranch();
RecordSet *srs=execcondtable->get(record);
bool ConstGen::isAlwaysExecuted(EPRecord *record) {
EPValue *branch=record->getBranch();
RecordSet *srs=execcondtable->get(record);
bool ConstGen::isAlwaysExecuted(EPRecord *record) {
EPValue *branch=record->getBranch();
RecordSet *srs=execcondtable->get(record);
Constraint *parentbranch=new Constraint(IMPLIES, br->getAnyBranch(), baseconstraint);
ADDCONSTRAINT(parentbranch, "parentbranch");
}
Constraint *parentbranch=new Constraint(IMPLIES, br->getAnyBranch(), baseconstraint);
ADDCONSTRAINT(parentbranch, "parentbranch");
}
/** Insert criteria for directions */
ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
ASSERT(depvec->size()==1);
/** Insert criteria for directions */
ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
ASSERT(depvec->size()==1);
for(unsigned int i=0;i<record->numValues();i++) {
EPValue * branchval=record->getValue(i);
uint64_t val=branchval->getValue();
for(unsigned int i=0;i<record->numValues();i++) {
EPValue * branchval=record->getValue(i);
uint64_t val=branchval->getValue();
if (val==0) {
Constraint *execconstraint=getExecutionConstraint(record);
Constraint *br_false=new Constraint(IMPLIES,
if (val==0) {
Constraint *execconstraint=getExecutionConstraint(record);
Constraint *br_false=new Constraint(IMPLIES,
Constraint *execconstraint=getExecutionConstraint(record);
Constraint *br_true1=new Constraint(IMPLIES, new Constraint(AND, getRetValueEncoding(val_record, 0)->negate(),
execconstraint),
Constraint *execconstraint=getExecutionConstraint(record);
Constraint *br_true1=new Constraint(IMPLIES, new Constraint(AND, getRetValueEncoding(val_record, 0)->negate(),
execconstraint),
ADDCONSTRAINT(br_true1, "br_true1");
} else {
for(unsigned int j=0;j<val_record->numValues();j++) {
ADDCONSTRAINT(br_true1, "br_true1");
} else {
for(unsigned int j=0;j<val_record->numValues();j++) {
while(it->hasNext()) {
uint64_t addr=it->next();
Constraint *srcenc=getRetValueEncoding(src, addr-offset);
while(it->hasNext()) {
uint64_t addr=it->next();
Constraint *srcenc=getRetValueEncoding(src, addr-offset);
ASSERT(depveccas->size()==1);
EPRecord *src=(*depveccas)[0];
IntIterator *it=getStoreLoadSet(record)->getValues()->iterator();
ASSERT(depveccas->size()==1);
EPRecord *src=(*depveccas)[0];
IntIterator *it=getStoreLoadSet(record)->getValues()->iterator();
while(it->hasNext()) {
uint64_t valcas=it->next();
Constraint *srcenc=getRetValueEncoding(src, valcas);
while(it->hasNext()) {
uint64_t valcas=it->next();
Constraint *srcenc=getRetValueEncoding(src, valcas);
ASSERT(depvec->size()==1);
EPRecord *src=(*depvec)[0];
IntIterator *it=record->getStoreSet()->iterator();
ASSERT(depvec->size()==1);
EPRecord *src=(*depvec)[0];
IntIterator *it=record->getStoreSet()->iterator();
Constraint *repeatval=generateEquivConstraint(sls->getNumValVars(), sls->getValVars(this, record), sls->getRMWRValVars(this, record));
Constraint *failcas=new Constraint(IMPLIES, eq->negate(), repeatval);
ADDCONSTRAINT(failcas,"casmemfail");
Constraint *repeatval=generateEquivConstraint(sls->getNumValVars(), sls->getValVars(this, record), sls->getRMWRValVars(this, record));
Constraint *failcas=new Constraint(IMPLIES, eq->negate(), repeatval);
ADDCONSTRAINT(failcas,"casmemfail");
ASSERT(depvec->size()==1);
EPRecord *src=(*depvec)[0];
IntIterator *it=record->getStoreSet()->iterator();
ASSERT(depvec->size()==1);
EPRecord *src=(*depvec)[0];
IntIterator *it=record->getStoreSet()->iterator();
Constraint *var=getNewVar();
Constraint *newadd=new Constraint(AND, var, getExecutionConstraint(record));
ADDGOAL(record, newadd, "newadd");
Constraint *var=getNewVar();
Constraint *newadd=new Constraint(AND, var, getExecutionConstraint(record));
ADDGOAL(record, newadd, "newadd");
ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
if (depvec==NULL) {
IntIterator *valit=record->getSet(VC_BASEINDEX)->iterator();
ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
if (depvec==NULL) {
IntIterator *valit=record->getSet(VC_BASEINDEX)->iterator();
Constraint *storeenc=getMemValueEncoding(record, sum);
Constraint *notvar=var->negate();
Constraint *addop=new Constraint(IMPLIES, new Constraint(AND, srcenc, loadenc),
Constraint *storeenc=getMemValueEncoding(record, sum);
Constraint *notvar=var->negate();
Constraint *addop=new Constraint(IMPLIES, new Constraint(AND, srcenc, loadenc),
void ConstGen::processStore(EPRecord *record) {
ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
void ConstGen::processStore(EPRecord *record) {
ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
ASSERT(depvec->size()==1);
EPRecord *src=(*depvec)[0];
IntIterator *it=record->getStoreSet()->iterator();
ASSERT(depvec->size()==1);
EPRecord *src=(*depvec)[0];
IntIterator *it=record->getStoreSet()->iterator();
ModelVector<EPRecord *> * inputs=execution->getRevDependences(record, VC_BASEINDEX);
for(uint i=0;i<inputs->size();i++) {
EPRecord * input=(*inputs)[i];
ModelVector<EPRecord *> * inputs=execution->getRevDependences(record, VC_BASEINDEX);
for(uint i=0;i<inputs->size();i++) {
EPRecord * input=(*inputs)[i];
for(uint i=0;i<2;i++) {
ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, i+VC_BASEINDEX);
if (depvec==NULL) {
inputs[i]=NULL;
} else if (depvec->size()==1) {
inputs[i]=(*depvec)[0];
for(uint i=0;i<2;i++) {
ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, i+VC_BASEINDEX);
if (depvec==NULL) {
inputs[i]=NULL;
} else if (depvec->size()==1) {
inputs[i]=(*depvec)[0];
}
//rely on this being a variable
Constraint * outputtrue=getRetValueEncoding(record, 1);
ASSERT(outputtrue->getType()==VAR);
}
//rely on this being a variable
Constraint * outputtrue=getRetValueEncoding(record, 1);
ASSERT(outputtrue->getType()==VAR);
if (inputs[0]!=NULL && inputs[1]!=NULL &&
(inputs[0]->getType()==LOAD || inputs[0]->getType()==RMW) &&
(inputs[1]->getType()==LOAD || inputs[1]->getType()==RMW) &&
(getStoreLoadSet(inputs[0])==getStoreLoadSet(inputs[1]))) {
StoreLoadSet * sls=getStoreLoadSet(inputs[0]);
int numvalvars=sls->getNumValVars();
if (inputs[0]!=NULL && inputs[1]!=NULL &&
(inputs[0]->getType()==LOAD || inputs[0]->getType()==RMW) &&
(inputs[1]->getType()==LOAD || inputs[1]->getType()==RMW) &&
(getStoreLoadSet(inputs[0])==getStoreLoadSet(inputs[1]))) {
StoreLoadSet * sls=getStoreLoadSet(inputs[0]);
int numvalvars=sls->getNumValVars();
- Constraint **valvar1=(inputs[0]->getType()==RMW)?sls->getRMWRValVars(this, inputs[0]):sls->getValVars(this, inputs[0]);
- Constraint **valvar2=(inputs[1]->getType()==RMW)?sls->getRMWRValVars(this, inputs[1]):sls->getValVars(this, inputs[1]);
+ Constraint **valvar1=(inputs[0]->getType()==RMW) ? sls->getRMWRValVars(this, inputs[0]) : sls->getValVars(this, inputs[0]);
+ Constraint **valvar2=(inputs[1]->getType()==RMW) ? sls->getRMWRValVars(this, inputs[1]) : sls->getValVars(this, inputs[1]);
ADDCONSTRAINT(new Constraint(IMPLIES, outputtrue, new Constraint(AND, numvalvars, vars)), "impequal2");
/*
ADDCONSTRAINT(new Constraint(IMPLIES, outputtrue, new Constraint(AND, numvalvars, vars)), "impequal2");
/*
-
- Constraint * functionimplication=new Constraint(IMPLIES,generateEquivConstraint(numvalvars, valvar1, valvar2), outputtrue);
- ADDCONSTRAINT(functionimplication,"equalsimplspecial");
- Constraint * functionimplicationneg=new Constraint(IMPLIES,outputtrue, generateEquivConstraint(numvalvars, valvar1, valvar2));
- ADDCONSTRAINT(functionimplicationneg,"equalsimplspecialneg");
- */
+
+ Constraint * functionimplication=new Constraint(IMPLIES,generateEquivConstraint(numvalvars, valvar1, valvar2), outputtrue);
+ ADDCONSTRAINT(functionimplication,"equalsimplspecial");
+ Constraint * functionimplicationneg=new Constraint(IMPLIES,outputtrue, generateEquivConstraint(numvalvars, valvar1, valvar2));
+ ADDCONSTRAINT(functionimplicationneg,"equalsimplspecialneg");
+ */
- int nullindex=inputs[0]==NULL?0:1;
- IntIterator *iit=record->getSet(VC_BASEINDEX+nullindex)->iterator();
+ int nullindex=inputs[0]==NULL ? 0 : 1;
+ IntIterator *iit=record->getSet(VC_BASEINDEX+nullindex)->iterator();
Constraint *functionimplication2=new Constraint(IMPLIES, outputtrue, l2);
ADDCONSTRAINT(functionimplication2,"equalsimpl");
}
Constraint *functionimplication2=new Constraint(IMPLIES, outputtrue, l2);
ADDCONSTRAINT(functionimplication2,"equalsimpl");
}
while(iit2->hasNext()) {
uint64_t val2=iit2->next();
Constraint *l=getRetValueEncoding(inputs[0], val1);
Constraint *r=getRetValueEncoding(inputs[1], val2);
while(iit2->hasNext()) {
uint64_t val2=iit2->next();
Constraint *l=getRetValueEncoding(inputs[0], val1);
Constraint *r=getRetValueEncoding(inputs[1], val2);
Constraint * functionimplication=new Constraint(IMPLIES, new Constraint(AND, l, r), imp);
ADDCONSTRAINT(functionimplication,"equalsimpl");
}
Constraint * functionimplication=new Constraint(IMPLIES, new Constraint(AND, l, r), imp);
ADDCONSTRAINT(functionimplication,"equalsimpl");
}
void ConstGen::recordExecCond(EPRecord *record) {
ExecPoint *eprecord=record->getEP();
EPValue * branchval=record->getBranch();
void ConstGen::recordExecCond(EPRecord *record) {
ExecPoint *eprecord=record->getEP();
EPValue * branchval=record->getBranch();
ExecPoint *epbranch= (branch==NULL) ? NULL : branch->getEP();
RecordSet *srs=NULL;
RecordIterator *sri=nonlocaltrans->iterator();
ExecPoint *epbranch= (branch==NULL) ? NULL : branch->getEP();
RecordSet *srs=NULL;
RecordIterator *sri=nonlocaltrans->iterator();
workstack->push_back(next);
for(uint i=0;i<record->numValues();i++) {
EPValue *branchdir=record->getValue(i);
workstack->push_back(next);
for(uint i=0;i<record->numValues();i++) {
EPValue *branchdir=record->getValue(i);
//Could have an empty branch, so make sure the branch actually
//runs code
if (branchdir->getFirstRecord()!=NULL)
//Could have an empty branch, so make sure the branch actually
//runs code
if (branchdir->getFirstRecord()!=NULL)
bool RecPairEquals(RecPair *r1, RecPair *r2) {
return ((r1->epr1==r2->epr1)&&(r1->epr2==r2->epr2)) ||
bool RecPairEquals(RecPair *r1, RecPair *r2) {
return ((r1->epr1==r2->epr1)&&(r1->epr2==r2->epr2)) ||