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.
11 #include "mcexecution.h"
12 #include "constraint.h"
13 #include "branchrecord.h"
14 #include "functionrecord.h"
15 #include "equalsrecord.h"
16 #include "storeloadset.h"
18 #include "schedulebuilder.h"
23 #include "inc_solver.h"
28 gettimeofday(&tv, NULL);
29 return tv.tv_sec*1000000+tv.tv_usec;
32 ConstGen::ConstGen(MCExecution *e) :
33 storeloadtable(new StoreLoadSetHashTable()),
34 loadtable(new LoadHashTable()),
36 workstack(new ModelVector<EPRecord *>()),
37 threadactions(new ModelVector<ModelVector<EPRecord *> *>()),
38 rpt(new RecPairTable()),
40 goalset(new ModelVector<Constraint *>()),
42 vars(new ModelVector<Constraint *>()),
43 branchtable(new BranchTable()),
44 functiontable(new FunctionTable()),
45 equalstable(new EqualsTable()),
46 schedulebuilder(new ScheduleBuilder(e, this)),
47 nonlocaltrans(new RecordSet()),
48 execcondtable(new LoadHashTable()),
50 rectoint(new RecToIntTable()),
53 has_untaken_branches(false)
56 curr_stat=new MC_Stat();
58 curr_stat->was_incremental=false;
59 curr_stat->was_sat=true;
62 stats=new ModelVector<struct MC_Stat *>();
66 ConstGen::~ConstGen() {
70 for(uint i=0;i<vars->size();i++) {
71 Constraint *var=(*vars)[i];
72 Constraint *notvar=var->neg;
77 delete storeloadtable;
87 delete schedulebuilder;
93 void resetstoreloadtable(StoreLoadSetHashTable * storeloadtable) {
94 for(uint i=0;i<storeloadtable->capacity;i++) {
95 struct hashlistnode<const void *, StoreLoadSet *> * ptr=& storeloadtable->table[i];
96 if (ptr->val != NULL) {
97 if (ptr->val->removeAddress(ptr->key))
104 if (storeloadtable->zero != NULL) {
105 if (storeloadtable->zero->val->removeAddress(storeloadtable->zero->key)) {
106 delete storeloadtable->zero->val;
109 model_free(storeloadtable -> zero);
110 storeloadtable->zero = NULL;
112 storeloadtable->size = 0;
115 void ConstGen::reset() {
116 for(uint i=0;i<threadactions->size();i++) {
117 delete (*threadactions)[i];
119 if (goalvararray != NULL) {
120 model_free(goalvararray);
123 functiontable->resetanddelete();
124 equalstable->resetanddelete();
125 branchtable->resetanddelete();
126 loadtable->resetanddelete();
127 execcondtable->resetanddelete();
128 rpt->resetanddelete();
129 resetstoreloadtable(storeloadtable);
130 nonlocaltrans->reset();
131 threadactions->clear();
136 has_untaken_branches=false;
139 void ConstGen::translateGoals() {
140 int size=goalset->size();
141 goalvararray=(Constraint **) model_malloc(size*sizeof(Constraint *));
143 for(int i=0;i<size;i++) {
144 Constraint *goal=(*goalset)[i];
145 goalvararray[i]=getNewVar();
146 addConstraint(new Constraint(OR, goalvararray[i]->negate(), goal));
148 Constraint *atleastonegoal=new Constraint(OR, size, goalvararray);
149 ADDCONSTRAINT(atleastonegoal, "atleastonegoal");
152 bool ConstGen::canReuseEncoding() {
155 Constraint *array[goalset->size()];
156 int remaininggoals=0;
158 //Zero out the achieved goals
159 for(uint i=0;i<goalset->size();i++) {
160 Constraint *var=goalvararray[i];
162 array[remaininggoals++]=var;
165 if (remaininggoals == 0)
167 Constraint *atleastonegoal=new Constraint(OR, remaininggoals, array);
168 ADDCONSTRAINT(atleastonegoal, "atleastonegoal");
169 solver->finishedClauses();
170 clock_t start=myclock();
171 bool *solution=runSolver();
172 clock_t finish=myclock();
174 if (curr_stat != NULL)
175 stats->push_back(curr_stat);
176 curr_stat=new MC_Stat();
177 curr_stat->time=finish-start;
178 curr_stat->was_incremental=true;
179 curr_stat->was_sat=(solution!=NULL);
183 model_print("start %lu, finish %lu\n", start,finish);
184 model_print("Incremental time = %12.6f\n", ((double)(finish-start))/1000000);
186 if (solution==NULL) {
190 //Zero out the achieved goals
191 for(uint i=0;i<goalset->size();i++) {
192 Constraint *var=goalvararray[i];
194 if (solution[var->getVar()]) {
195 // if (goalvararray[i] != NULL)
196 //model_print("SAT clearing goal %d.\n", i);
198 goalvararray[i]=NULL;
203 schedulebuilder->buildSchedule(solution);
204 model_free(solution);
209 bool ConstGen::process() {
210 #ifdef DUMP_EVENT_GRAPHS
214 if (solver != NULL) {
219 solver=new IncrementalSolver();
222 genTransOrderConstraints();
224 genTSOTransOrderConstraints();
228 if (goalset->size()==0) {
230 stats->push_back(curr_stat);
231 for(uint i=0;i<stats->size();i++) {
232 struct MC_Stat *s=(*stats)[i];
233 model_print("time=%lld fgoals=%d bgoals=%d incremental=%d sat=%d\n", s->time, s->fgoals, s->bgoals, s->was_incremental, s->was_sat);
236 model_print("No goals, done\n");
242 if (model->params.branches && !has_untaken_branches) {
248 solver->finishedClauses();
250 //Freeze the goal variables
251 for(uint i=0;i<goalset->size();i++) {
252 Constraint *var=goalvararray[i];
253 solver->freeze(var->getVar());
256 clock_t start=myclock();
257 bool *solution=runSolver();
258 clock_t finish=myclock();
260 if (curr_stat != NULL)
261 stats->push_back(curr_stat);
262 curr_stat=new MC_Stat();
263 curr_stat->time=finish-start;
264 curr_stat->was_incremental=false;
265 curr_stat->was_sat=(solution!=NULL);
269 if (solution == NULL) {
270 stats->push_back(curr_stat);
271 for(uint i=0;i<stats->size();i++) {
272 struct MC_Stat *s=(*stats)[i];
273 model_print("time=%lld fgoals=%d bgoals=%d incremental=%d sat=%d\n", s->time, s->fgoals, s->bgoals, s->was_incremental, s->was_sat);
279 model_print("start %lu, finish %lu\n", start,finish);
280 model_print("Initial time = %12.6f\n", ((double)(finish-start))/1000000);
283 if (solution==NULL) {
289 //Zero out the achieved goals
290 for(uint i=0;i<goalset->size();i++) {
291 Constraint *var=goalvararray[i];
293 if (solution[var->getVar()]) {
294 //if (goalvararray[i] != NULL)
295 // model_print("SAT clearing goal %d.\n", i);
296 goalvararray[i]=NULL;
301 schedulebuilder->buildSchedule(solution);
302 model_free(solution);
306 void ConstGen::printEventGraph() {
308 sprintf(buffer, "eventgraph%u.dot",schedule_graph);
310 int file=open(buffer,O_WRONLY|O_CREAT|O_TRUNC, S_IRWXU);
311 dprintf(file, "digraph eventgraph {\n");
313 EPRecord *first=execution->getEPRecord(MCID_FIRST);
314 printRecord(first, file);
315 while(!workstack->empty()) {
316 EPRecord *record=workstack->back();
317 workstack->pop_back();
318 printRecord(record, file);
321 dprintf(file, "}\n");
325 void ConstGen::doPrint(EPRecord *record, int file) {
326 dprintf(file, "%lu[label=\"",(uintptr_t)record);
328 dprintf(file, "\"];\n");
329 if (record->getNextRecord()!=NULL)
330 dprintf(file, "%lu->%lu;\n", (uintptr_t) record, (uintptr_t) record->getNextRecord());
332 if (record->getChildRecord()!=NULL)
333 dprintf(file, "%lu->%lu[color=red];\n", (uintptr_t) record, (uintptr_t) record->getChildRecord());
336 void ConstGen::printRecord(EPRecord *record, int file) {
338 doPrint(record,file);
340 if (record->getType()==LOOPENTER) {
341 workstack->push_back(record->getNextRecord());
342 workstack->push_back(record->getChildRecord());
345 if (record->getChildRecord()!=NULL) {
346 workstack->push_back(record->getChildRecord());
348 if (record->getType()==NONLOCALTRANS) {
351 if (record->getType()==LOOPEXIT) {
354 if (record->getType()==BRANCHDIR) {
355 EPRecord *next=record->getNextRecord();
357 workstack->push_back(next);
358 for(uint i=0;i<record->numValues();i++) {
359 EPValue *branchdir=record->getValue(i);
361 //Could have an empty branch, so make sure the branch actually
363 if (branchdir->getFirstRecord()!=NULL) {
364 workstack->push_back(branchdir->getFirstRecord());
365 dprintf(file, "%lu->%lu[color=blue];\n", (uintptr_t) record, (uintptr_t) branchdir->getFirstRecord());
370 record=record->getNextRecord();
371 } while(record!=NULL);
375 /* This function traverses a thread's graph in execution order. */
377 void ConstGen::traverse(bool initial) {
378 EPRecord *first=execution->getEPRecord(MCID_FIRST);
379 traverseRecord(first, initial);
380 while(!workstack->empty()) {
381 EPRecord *record=workstack->back();
382 workstack->pop_back();
383 traverseRecord(record, initial);
387 /** This method looks for all other memory operations that could
388 potentially share a location, and build partitions of memory
389 locations such that all memory locations that can share the same
390 address are in the same group.
392 These memory operations should share an encoding of addresses and
396 void ConstGen::groupMemoryOperations(EPRecord *op) {
397 /** Handle our first address */
398 IntHashSet *addrset=op->getSet(VC_ADDRINDEX);
399 IntIterator *ait=addrset->iterator();
401 void *iaddr=(void *) ait->next();
402 StoreLoadSet *isls=storeloadtable->get(iaddr);
404 isls=new StoreLoadSet();
405 storeloadtable->put(iaddr, isls);
409 while(ait->hasNext()) {
410 void *addr=(void *)ait->next();
411 StoreLoadSet *sls=storeloadtable->get(addr);
413 storeloadtable->put(addr, isls);
414 } else if (sls!=isls) {
416 mergeSets(isls, sls);
423 RecordSet * ConstGen::computeConflictSet(EPRecord *store, EPRecord *load, RecordSet * baseset) {
424 //See if we can determine addresses that store/load may use
425 IntIterator * storeaddr=store->getSet(VC_ADDRINDEX)->iterator();
426 int numaddr=0;void *commonaddr=NULL;
427 while(storeaddr->hasNext()) {
428 void *addr=(void *) storeaddr->next();
429 if (load->getSet(VC_ADDRINDEX)->contains((uint64_t)addr)) {
440 RecordSet *srscopy=baseset->copy();
441 RecordIterator *sri=srscopy->iterator();
442 while(sri->hasNext()) {
443 bool pruneconflictstore=false;
444 EPRecord *conflictstore=sri->next();
445 bool conflictafterstore=getOrderConstraint(store,conflictstore)->isTrue();
446 bool conflictbeforeload=getOrderConstraint(conflictstore,load)->isTrue();
448 if (conflictafterstore) {
449 RecordIterator *sricheck=srscopy->iterator();
450 while(sricheck->hasNext()) {
451 EPRecord *checkstore=sricheck->next();
452 bool checkafterstore=getOrderConstraint(store, checkstore)->isTrue();
453 if (!checkafterstore)
455 bool checkbeforeconflict=getOrderConstraint(checkstore,conflictstore)->isTrue();
456 if (!checkbeforeconflict)
459 //See if the checkstore must store to the relevant address
460 IntHashSet * storeaddr=checkstore->getSet(VC_ADDRINDEX);
462 if (storeaddr->getSize()!=1 || !storeaddr->contains((uint64_t)commonaddr))
466 if (subsumesExecutionConstraint(checkstore, conflictstore)) {
467 pruneconflictstore=true;
474 if (conflictbeforeload && !pruneconflictstore) {
475 RecordIterator *sricheck=srscopy->iterator();
476 while(sricheck->hasNext()) {
477 EPRecord *checkstore=sricheck->next();
479 bool checkafterconflict=getOrderConstraint(conflictstore, checkstore)->isTrue();
480 if (!checkafterconflict)
483 bool checkbeforeload=getOrderConstraint(checkstore, load)->isTrue();
484 if (!checkbeforeload)
487 //See if the checkstore must store to the relevant address
488 IntHashSet * storeaddr=checkstore->getSet(VC_ADDRINDEX);
489 if (storeaddr->getSize()!=1 || !storeaddr->contains((uint64_t)commonaddr))
493 if (subsumesExecutionConstraint(checkstore, conflictstore)) {
494 pruneconflictstore=true;
500 if (pruneconflictstore) {
501 //This store is redundant
511 /** This method returns all stores that a load may read from. */
513 RecordSet * ConstGen::getMayReadFromSet(EPRecord *load) {
514 if (load->getSet(VC_ADDRINDEX)->getSize()==1)
515 return getMayReadFromSetOpt(load);
517 RecordSet *srs=loadtable->get(load);
518 ExecPoint *epload=load->getEP();
519 thread_id_t loadtid=epload->get_tid();
522 loadtable->put(load, srs);
524 IntHashSet *addrset=load->getSet(VC_ADDRINDEX);
525 IntIterator *ait=addrset->iterator();
527 while(ait->hasNext()) {
528 void *addr=(void *)ait->next();
529 RecordSet *rs=execution->getStoreTable(addr);
533 RecordIterator * rit=rs->iterator();
534 while(rit->hasNext()) {
535 EPRecord *rec=rit->next();
536 ExecPoint *epstore=rec->getEP();
537 thread_id_t storetid=epstore->get_tid();
538 if (storetid != loadtid ||
539 epstore->compare(epload) == CR_AFTER)
550 RecordSet * ConstGen::getMayReadFromSetOpt(EPRecord *load) {
551 RecordSet *srs=loadtable->get(load);
552 ExecPoint *epload=load->getEP();
553 thread_id_t loadtid=epload->get_tid();
556 loadtable->put(load, srs);
558 IntHashSet *addrset=load->getSet(VC_ADDRINDEX);
559 IntIterator *ait=addrset->iterator();
560 void *addr=(void *)ait->next();
563 RecordSet *rs=execution->getStoreTable(addr);
564 RecordIterator * rit=rs->iterator();
565 ExecPoint *latest=NULL;
566 while(rit->hasNext()) {
567 EPRecord *store=rit->next();
568 ExecPoint *epstore=store->getEP();
569 thread_id_t storetid=epstore->get_tid();
570 if (storetid == loadtid && isAlwaysExecuted(store) &&
571 store->getSet(VC_ADDRINDEX)->getSize()==1 &&
572 epstore->compare(epload) == CR_AFTER &&
573 (latest==NULL || latest->compare(epstore) == CR_AFTER)) {
579 while(rit->hasNext()) {
580 EPRecord *store=rit->next();
581 ExecPoint *epstore=store->getEP();
582 thread_id_t storetid=epstore->get_tid();
583 if (storetid == loadtid) {
584 if (epstore->compare(epload) == CR_AFTER &&
585 (latest==NULL || epstore->compare(latest) != CR_AFTER))
596 /** This function merges two recordsets and updates the storeloadtable
599 void ConstGen::mergeSets(StoreLoadSet *to, StoreLoadSet *from) {
600 RecordIterator * sri=from->iterator();
601 while(sri->hasNext()) {
602 EPRecord *rec=sri->next();
604 IntHashSet *addrset=rec->getSet(VC_ADDRINDEX);
605 IntIterator *ait=addrset->iterator();
606 while(ait->hasNext()) {
607 void *addr=(void *)ait->next();
608 storeloadtable->put(addr, to);
617 /** This function creates ordering variables between stores and loads
618 * in same thread for TSO. */
620 void ConstGen::insertTSOAction(EPRecord *load) {
621 if (load->getType() != LOAD)
623 ExecPoint *load_ep=load->getEP();
624 thread_id_t tid=load_ep->get_tid();
625 uint thread=id_to_int(tid);
626 ModelVector<EPRecord *> * vector=(*threadactions)[thread];
627 uint j=vector->size()-1;
629 EPRecord *oldrec=(*vector)[--j];
630 EventType oldrec_t=oldrec->getType();
632 if (((oldrec_t == RMW) || (oldrec_t==FENCE)) &&
633 isAlwaysExecuted(oldrec)) {
635 } else if (oldrec_t == STORE) {
636 /* Only generate variables for things that can actually both run */
638 createOrderConstraint(oldrec, load);
643 void ConstGen::genTSOTransOrderConstraints() {
644 for(uint t1=0;t1<threadactions->size();t1++) {
645 ModelVector<EPRecord *> *tvec=(*threadactions)[t1];
646 uint size=tvec->size();
647 EPRecord *laststore=NULL;
648 for(uint store_i=0;store_i<size;store_i++) {
649 EPRecord *store=(*tvec)[store_i];
650 EventType store_t=store->getType();
651 if (store_t != STORE)
653 EPRecord *lastload=NULL;
654 for(uint load_i=store_i+1;load_i<size;load_i++) {
655 EPRecord *rec=(*tvec)[store_i];
656 //Hit fence, don't need more stuff
657 EventType rec_t=rec->getType();
658 if (((rec_t == RMW) || (rec_t == FENCE)) &&
659 isAlwaysExecuted(rec))
663 if (laststore != NULL) {
664 Constraint * storeload=getOrderConstraint(store, rec);
665 Constraint * earlystoreload=getOrderConstraint(laststore, rec);
666 Constraint * c=new Constraint(IMPLIES, storeload, earlystoreload);
667 ADDCONSTRAINT(c, "earlystore");
669 if (lastload != NULL) {
670 Constraint * storeearlyload=getOrderConstraint(store, lastload);
671 Constraint * storeload=getOrderConstraint(store, rec);
672 Constraint * c=new Constraint(IMPLIES, storeearlyload, storeload);
673 ADDCONSTRAINT(c, "earlyload");
683 /** This function creates ordering constraints to implement SC for
684 memory operations. */
686 void ConstGen::insertAction(EPRecord *record) {
687 thread_id_t tid=record->getEP()->get_tid();
688 uint thread=id_to_int(tid);
689 if (threadactions->size()<=thread) {
690 uint oldsize=threadactions->size();
691 threadactions->resize(thread+1);
692 for(;oldsize<=thread;oldsize++) {
693 (*threadactions)[oldsize]=new ModelVector<EPRecord *>();
697 (*threadactions)[thread]->push_back(record);
699 for(uint i=0;i<threadactions->size();i++) {
702 ModelVector<EPRecord *> * vector=(*threadactions)[i];
703 for(uint j=0;j<vector->size();j++) {
704 EPRecord *oldrec=(*vector)[j];
705 createOrderConstraint(oldrec, record);
709 insertTSOAction(record);
713 void ConstGen::genTransOrderConstraints() {
714 for(uint t1=0;t1<threadactions->size();t1++) {
715 ModelVector<EPRecord *> *t1vec=(*threadactions)[t1];
716 for(uint t2=0;t2<t1;t2++) {
717 ModelVector<EPRecord *> *t2vec=(*threadactions)[t2];
718 genTransOrderConstraints(t1vec, t2vec);
719 genTransOrderConstraints(t2vec, t1vec);
720 for(uint t3=0;t3<t2;t3++) {
721 ModelVector<EPRecord *> *t3vec=(*threadactions)[t3];
722 genTransOrderConstraints(t1vec, t2vec, t3vec);
728 void ConstGen::genTransOrderConstraints(ModelVector<EPRecord *> * t1vec, ModelVector<EPRecord *> *t2vec) {
729 for(uint t1i=0;t1i<t1vec->size();t1i++) {
730 EPRecord *t1rec=(*t1vec)[t1i];
731 for(uint t2i=0;t2i<t2vec->size();t2i++) {
732 EPRecord *t2rec=(*t2vec)[t2i];
734 /* Note: One only really needs to generate the first constraint
735 in the first loop and the last constraint in the last loop.
736 I tried this and performance suffered on linuxrwlocks and
737 linuxlocks at the current time. BD - August 2014*/
738 Constraint *c21=getOrderConstraint(t2rec, t1rec);
740 /* short circuit for the trivial case */
744 for(uint t3i=t2i+1;t3i<t2vec->size();t3i++) {
745 EPRecord *t3rec=(*t2vec)[t3i];
746 Constraint *c13=getOrderConstraint(t1rec, t3rec);
748 Constraint *c32=getOrderConstraint(t3rec, t2rec);
749 Constraint * array[]={c21, c32, c13};
750 Constraint *intratransorder=new Constraint(OR, 3, array);
752 Constraint *intratransorder=new Constraint(OR, c21, c13);
754 ADDCONSTRAINT(intratransorder,"intratransorder");
757 for(uint t0i=0;t0i<t1i;t0i++) {
758 EPRecord *t0rec=(*t1vec)[t0i];
759 Constraint *c02=getOrderConstraint(t0rec, t2rec);
761 Constraint *c10=getOrderConstraint(t1rec, t0rec);
762 Constraint * array[]={c10, c21, c02};
763 Constraint *intratransorder=new Constraint(OR, 3, array);
765 Constraint *intratransorder=new Constraint(OR, c21, c02);
767 ADDCONSTRAINT(intratransorder,"intratransorder");
774 void ConstGen::genTransOrderConstraints(ModelVector<EPRecord *> * t1vec, ModelVector<EPRecord *> *t2vec, ModelVector<EPRecord *> * t3vec) {
775 for(uint t1i=0;t1i<t1vec->size();t1i++) {
776 EPRecord *t1rec=(*t1vec)[t1i];
777 for(uint t2i=0;t2i<t2vec->size();t2i++) {
778 EPRecord *t2rec=(*t2vec)[t2i];
779 for(uint t3i=0;t3i<t3vec->size();t3i++) {
780 EPRecord *t3rec=(*t3vec)[t3i];
781 genTransOrderConstraint(t1rec, t2rec, t3rec);
787 void ConstGen::genTransOrderConstraint(EPRecord *t1rec, EPRecord *t2rec, EPRecord *t3rec) {
788 Constraint *c21=getOrderConstraint(t2rec, t1rec);
789 Constraint *c32=getOrderConstraint(t3rec, t2rec);
790 Constraint *c13=getOrderConstraint(t1rec, t3rec);
791 Constraint * cimpl1[]={c21, c32, c13};
792 Constraint * c1=new Constraint(OR, 3, cimpl1);
793 ADDCONSTRAINT(c1, "intertransorder");
795 Constraint *c12=getOrderConstraint(t1rec, t2rec);
796 Constraint *c23=getOrderConstraint(t2rec, t3rec);
797 Constraint *c31=getOrderConstraint(t3rec, t1rec);
798 Constraint * cimpl2[]={c12, c23, c31};
799 Constraint *c2=new Constraint(OR, 3, cimpl2);
800 ADDCONSTRAINT(c2, "intertransorder");
803 void ConstGen::addGoal(EPRecord *r, Constraint *c) {
804 rectoint->put(r, goalset->size());
805 goalset->push_back(c);
808 void ConstGen::addBranchGoal(EPRecord *r, Constraint *c) {
809 has_untaken_branches=true;
810 rectoint->put(r, goalset->size());
811 goalset->push_back(c);
814 void ConstGen::achievedGoal(EPRecord *r) {
815 if (rectoint->contains(r)) {
816 uint index=rectoint->get(r);
817 //if (goalvararray[index] != NULL)
818 //model_print("Run Clearing goal index %d\n",index);
819 goalvararray[index]=NULL;
823 void ConstGen::addConstraint(Constraint *c) {
824 ModelVector<Constraint *> *vec=c->simplify();
825 for(uint i=0;i<vec->size();i++) {
826 Constraint *simp=(*vec)[i];
827 if (simp->type==TRUE)
829 ASSERT(simp->type!=FALSE);
830 simp->printDIMACS(this);
831 #ifdef VERBOSE_CONSTRAINTS
841 void ConstGen::printNegConstraint(uint value) {
843 solver->addClauseLiteral(val);
846 void ConstGen::printConstraint(uint value) {
847 solver->addClauseLiteral(value);
850 bool * ConstGen::runSolver() {
851 int solution=solver->solve();
852 if (solution == IS_UNSAT) {
854 } else if (solution == IS_SAT) {
855 bool * assignments=(bool *)model_malloc(sizeof(bool)*(varindex+1));
856 for(uint i=0;i<=varindex;i++)
857 assignments[i]=solver->getValue(i);
862 dprintf(2, "INDETER\n");
863 model_print("INDETER\n");
869 Constraint * ConstGen::getOrderConstraint(EPRecord *first, EPRecord *second) {
871 if (first->getEP()->get_tid()==second->getEP()->get_tid()) {
872 if (first->getEP()->compare(second->getEP())==CR_AFTER)
879 RecPair rp(first, second);
880 RecPair *rpc=rpt->get(&rp);
883 first->getEP()->get_tid()==second->getEP()->get_tid()) {
884 if (first->getEP()->compare(second->getEP())==CR_AFTER)
893 Constraint *c=rpc->constraint;
894 if (rpc->epr1!=first) {
895 //have to flip arguments
902 bool ConstGen::getOrder(EPRecord *first, EPRecord *second, bool * satsolution) {
903 RecPair rp(first, second);
904 RecPair *rpc=rpt->get(&rp);
907 first->getEP()->get_tid()==second->getEP()->get_tid()) {
908 if (first->getEP()->compare(second->getEP())==CR_AFTER)
918 Constraint *c=rpc->constraint;
919 CType type=c->getType();
924 else if (type==FALSE)
927 uint index=c->getVar();
928 order=satsolution[index];
930 if (rpc->epr1==first)
936 /** This function determines whether events first and second are
937 * ordered by start and join operations. */
939 bool ConstGen::orderThread(EPRecord *first, EPRecord *second) {
940 ExecPoint * ep1=first->getEP();
941 ExecPoint * ep2=second->getEP();
942 thread_id_t thr1=ep1->get_tid();
943 thread_id_t thr2=ep2->get_tid();
944 Thread *tr2=execution->get_thread(thr2);
945 EPRecord *thr2start=tr2->getParentRecord();
946 if (thr2start!=NULL) {
947 ExecPoint *epthr2start=thr2start->getEP();
948 if (epthr2start->get_tid()==thr1 &&
949 ep1->compare(epthr2start)==CR_AFTER)
952 ModelVector<EPRecord *> * joinvec=execution->getJoins();
953 for(uint i=0;i<joinvec->size();i++) {
954 EPRecord *join=(*joinvec)[i];
955 ExecPoint *jp=join->getEP();
956 if (jp->get_tid()==thr2 &&
957 jp->compare(ep2)==CR_AFTER)
963 /** This function generates an ordering constraint for two events. */
965 void ConstGen::createOrderConstraint(EPRecord *first, EPRecord *second) {
966 RecPair * rp=new RecPair(first, second);
967 if (!rpt->contains(rp)) {
968 if (orderThread(first, second))
969 rp->constraint=&ctrue;
970 else if (orderThread(second, first))
971 rp->constraint=&cfalse;
973 rp->constraint=getNewVar();
981 Constraint * ConstGen::getNewVar() {
983 if (varindex>vars->size()) {
984 var=new Constraint(VAR, varindex);
985 Constraint *varneg=new Constraint(NOTVAR, varindex);
988 vars->push_back(var);
990 var=(*vars)[varindex-1];
996 /** Gets an array of new variables. */
998 void ConstGen::getArrayNewVars(uint num, Constraint **carray) {
999 for(uint i=0;i<num;i++)
1000 carray[i]=getNewVar();
1003 StoreLoadSet * ConstGen::getStoreLoadSet(EPRecord *record) {
1004 IntIterator *it=record->getSet(VC_ADDRINDEX)->iterator();
1005 void *addr=(void *)it->next();
1007 return storeloadtable->get(addr);
1010 /** Returns a constraint that is true if the output of record has the
1013 Constraint * ConstGen::getRetValueEncoding(EPRecord *record, uint64_t value) {
1014 switch(record->getType()) {
1016 return equalstable->get(record)->getValueEncoding(value);
1018 return functiontable->get(record)->getValueEncoding(value);
1020 return getStoreLoadSet(record)->getValueEncoding(this, record, value);
1023 return getStoreLoadSet(record)->getRMWRValueEncoding(this, record, value);
1031 Constraint * ConstGen::getMemValueEncoding(EPRecord *record, uint64_t value) {
1032 switch(record->getType()) {
1034 return getStoreLoadSet(record)->getValueEncoding(this, record, value);
1036 return getStoreLoadSet(record)->getValueEncoding(this, record, value);
1043 /** Return true if the execution of record implies the execution of
1046 bool ConstGen::subsumesExecutionConstraint(EPRecord *recordsubsumes, EPRecord *record) {
1047 EPValue *branch=record->getBranch();
1048 EPValue *branchsubsumes=recordsubsumes->getBranch();
1049 if (branchsubsumes != NULL) {
1050 bool branchsubsumed=false;
1051 while(branch!=NULL) {
1052 if (branchsubsumes==branch) {
1053 branchsubsumed=true;
1056 branch=branch->getRecord()->getBranch();
1058 if (!branchsubsumed)
1061 RecordSet *srs=execcondtable->get(recordsubsumes);
1064 RecordIterator *sri=srs->iterator();
1065 while(sri->hasNext()) {
1066 EPRecord *rec=sri->next();
1068 if (!getOrderConstraint(rec, record)->isTrue()) {
1078 Constraint * ConstGen::getExecutionConstraint(EPRecord *record) {
1079 EPValue *branch=record->getBranch();
1080 RecordSet *srs=execcondtable->get(record);
1081 int size=srs==NULL?0:srs->getSize();
1085 Constraint *array[size];
1088 RecordIterator *sri=srs->iterator();
1089 while(sri->hasNext()) {
1090 EPRecord *rec=sri->next();
1091 EPValue *recbranch=rec->getBranch();
1092 BranchRecord *guardbr=branchtable->get(recbranch->getRecord());
1093 array[index++]=guardbr->getBranch(recbranch)->negate();
1098 BranchRecord *guardbr=branchtable->get(branch->getRecord());
1099 array[index++]=guardbr->getBranch(branch);
1106 return new Constraint(AND, index, array);
1109 bool ConstGen::isAlwaysExecuted(EPRecord *record) {
1110 EPValue *branch=record->getBranch();
1111 RecordSet *srs=execcondtable->get(record);
1112 int size=srs==NULL?0:srs->getSize();
1119 void ConstGen::insertBranch(EPRecord *record) {
1120 uint numvalue=record->numValues();
1121 /** need one value for new directions */
1122 if (numvalue<record->getLen())
1124 /** need extra value to represent that branch wasn't executed. **/
1125 bool alwaysexecuted=isAlwaysExecuted(record);
1126 if (!alwaysexecuted)
1128 uint numbits=NUMBITS(numvalue-1);
1129 Constraint *bits[numbits];
1130 getArrayNewVars(numbits, bits);
1131 BranchRecord *br=new BranchRecord(record, numbits, bits, alwaysexecuted);
1132 branchtable->put(record, br);
1135 void ConstGen::processBranch(EPRecord *record) {
1136 BranchRecord *br=branchtable->get(record);
1137 if (record->numValues()<record->getLen()) {
1138 Constraint *goal=br->getNewBranch();
1139 ADDBRANCHGOAL(record, goal,"newbranch");
1142 /** Insert criteria of parent branch going the right way. **/
1143 Constraint *baseconstraint=getExecutionConstraint(record);
1145 if (!isAlwaysExecuted(record)) {
1146 Constraint *parentbranch=new Constraint(IMPLIES, br->getAnyBranch(), baseconstraint);
1147 ADDCONSTRAINT(parentbranch, "parentbranch");
1150 /** Insert criteria for directions */
1151 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1152 ASSERT(depvec->size()==1);
1153 EPRecord * val_record=(*depvec)[0];
1154 for(unsigned int i=0;i<record->numValues();i++) {
1155 EPValue * branchval=record->getValue(i);
1156 uint64_t val=branchval->getValue();
1159 Constraint *execconstraint=getExecutionConstraint(record);
1160 Constraint *br_false=new Constraint(IMPLIES,
1161 new Constraint(AND, execconstraint,
1162 getRetValueEncoding(val_record, val)), br->getBranch(branchval));
1163 ADDCONSTRAINT(br_false, "br_false");
1165 if (record->getBranchAnyValue()) {
1166 if (getRetValueEncoding(val_record, 0)!=NULL) {
1167 Constraint *execconstraint=getExecutionConstraint(record);
1168 Constraint *br_true1=new Constraint(IMPLIES, new Constraint(AND, getRetValueEncoding(val_record, 0)->negate(),
1170 br->getBranch(branchval));
1171 ADDCONSTRAINT(br_true1, "br_true1");
1173 for(unsigned int j=0;j<val_record->numValues();j++) {
1174 EPValue * epval=val_record->getValue(j);
1175 Constraint *execconstraint=getExecutionConstraint(record);
1176 Constraint *valuematches=getRetValueEncoding(val_record, epval->getValue());
1177 Constraint *br_true2=new Constraint(IMPLIES, new Constraint(AND, execconstraint, valuematches), br->getBranch(branchval));
1178 ADDCONSTRAINT(br_true2, "br_true2");
1182 Constraint *execconstraint=getExecutionConstraint(record);
1183 Constraint *br_val=new Constraint(IMPLIES, new Constraint(AND, execconstraint, getRetValueEncoding(val_record, val)), br->getBranch(branchval));
1184 ADDCONSTRAINT(br_val, "br_val");
1190 void ConstGen::insertFunction(EPRecord *record) {
1191 FunctionRecord * fr=new FunctionRecord(this, record);
1192 functiontable->put(record, fr);
1195 void ConstGen::insertEquals(EPRecord *record) {
1196 EqualsRecord * fr=new EqualsRecord(this, record);
1197 equalstable->put(record, fr);
1200 void ConstGen::processLoad(EPRecord *record) {
1201 LoadRF * lrf=new LoadRF(record, this);
1202 lrf->genConstraints(this);
1204 processAddresses(record);
1207 /** This procedure generates the constraints that set the address
1208 variables for load/store/rmw operations. */
1210 void ConstGen::processAddresses(EPRecord *record) {
1211 StoreLoadSet *sls=getStoreLoadSet(record);
1212 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_ADDRINDEX);
1214 //we have a hard coded address
1215 const void *addr=record->getValue(0)->getAddr();
1216 Constraint *addrenc=sls->getAddressEncoding(this, record, addr);
1217 ADDCONSTRAINT(addrenc,"fixedaddress");
1219 //we take as input an address and have to generate implications
1220 //for each possible input address
1221 ASSERT(depvec->size()==1);
1222 EPRecord *src=(*depvec)[0];
1223 IntIterator *it=record->getSet(VC_ADDRINDEX)->iterator();
1225 uintptr_t offset=record->getOffset();
1227 while(it->hasNext()) {
1228 uint64_t addr=it->next();
1229 Constraint *srcenc=getRetValueEncoding(src, addr-offset);
1230 Constraint *addrenc=sls->getAddressEncoding(this, record, (void *) addr);
1231 Constraint *addrmatch=new Constraint(IMPLIES, srcenc, addrenc);
1232 ADDCONSTRAINT(addrmatch,"setaddress");
1238 void ConstGen::processCAS(EPRecord *record) {
1240 LoadRF * lrf=new LoadRF(record, this);
1241 lrf->genConstraints(this);
1243 //Next see if we are successful
1244 Constraint *eq=getNewVar();
1245 ModelVector<EPRecord *> * depveccas=execution->getRevDependences(record, VC_OLDVALCASINDEX);
1246 if (depveccas==NULL) {
1247 //Hard coded old value
1248 IntIterator *iit=record->getSet(VC_OLDVALCASINDEX)->iterator();
1249 uint64_t valcas=iit->next();
1251 Constraint *rmwr=getStoreLoadSet(record)->getRMWRValueEncoding(this, record, valcas);
1253 Constraint *cascond=eq->negate();
1254 ADDCONSTRAINT(cascond, "cascond");
1256 Constraint *cascond=generateEquivConstraint(eq, rmwr);
1257 ADDCONSTRAINT(cascond, "cascond");
1260 ASSERT(depveccas->size()==1);
1261 EPRecord *src=(*depveccas)[0];
1262 IntIterator *it=getStoreLoadSet(record)->getValues()->iterator();
1264 while(it->hasNext()) {
1265 uint64_t valcas=it->next();
1266 Constraint *srcenc=getRetValueEncoding(src, valcas);
1267 Constraint *storeenc=getStoreLoadSet(record)->getRMWRValueEncoding(this, record, valcas);
1269 if (srcenc!=NULL && storeenc!=NULL) {
1270 Constraint *cond=new Constraint(AND,
1271 new Constraint(IMPLIES, srcenc->clone(), eq),
1272 new Constraint(IMPLIES, eq, srcenc));
1273 Constraint *cas=new Constraint(IMPLIES, storeenc, cond);
1274 ADDCONSTRAINT(cas, "cas");
1275 } else if (srcenc==NULL) {
1276 Constraint *casfail=new Constraint(IMPLIES, storeenc, eq->negate());
1277 ADDCONSTRAINT(casfail,"casfail_eq");
1279 //srcenc must be non-null and store-encoding must be null
1284 IntIterator *iit=record->getSet(VC_OLDVALCASINDEX)->iterator();
1285 while(iit->hasNext()) {
1286 uint64_t val=iit->next();
1287 if (!getStoreLoadSet(record)->getValues()->contains(val)) {
1288 Constraint *srcenc=getRetValueEncoding(src, val);
1289 Constraint *casfail=new Constraint(IMPLIES, srcenc, eq->negate());
1290 ADDCONSTRAINT(casfail,"casfailretval");
1296 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1298 IntIterator *iit=record->getSet(VC_BASEINDEX)->iterator();
1299 uint64_t val=iit->next();
1301 Constraint *storeenc=getMemValueEncoding(record, val);
1302 Constraint *casmemsuc=new Constraint(IMPLIES, eq, storeenc);
1303 ADDCONSTRAINT(casmemsuc, "casmemsuc");
1305 ASSERT(depvec->size()==1);
1306 EPRecord *src=(*depvec)[0];
1307 IntIterator *it=record->getStoreSet()->iterator();
1309 while(it->hasNext()) {
1310 uint64_t val=it->next();
1311 Constraint *srcenc=getRetValueEncoding(src, val);
1313 //this can happen for values that are in the store set because
1314 //we re-stored them on a failed CAS
1317 Constraint *storeenc=getMemValueEncoding(record, val);
1318 Constraint *storevalue=new Constraint(IMPLIES, new Constraint(AND, eq, srcenc), storeenc);
1319 ADDCONSTRAINT(storevalue,"casmemsuc");
1323 StoreLoadSet *sls=getStoreLoadSet(record);
1325 Constraint *repeatval=generateEquivConstraint(sls->getNumValVars(), sls->getValVars(this, record), sls->getRMWRValVars(this, record));
1326 Constraint *failcas=new Constraint(IMPLIES, eq->negate(), repeatval);
1327 ADDCONSTRAINT(failcas,"casmemfail");
1329 processAddresses(record);
1332 void ConstGen::processEXC(EPRecord *record) {
1334 LoadRF * lrf=new LoadRF(record, this);
1335 lrf->genConstraints(this);
1338 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1340 IntIterator *iit=record->getSet(VC_BASEINDEX)->iterator();
1341 uint64_t val=iit->next();
1343 Constraint *storeenc=getMemValueEncoding(record, val);
1344 ADDCONSTRAINT(storeenc, "excmemsuc");
1346 ASSERT(depvec->size()==1);
1347 EPRecord *src=(*depvec)[0];
1348 IntIterator *it=record->getStoreSet()->iterator();
1350 while(it->hasNext()) {
1351 uint64_t val=it->next();
1352 Constraint *srcenc=getRetValueEncoding(src, val);
1353 Constraint *storeenc=getMemValueEncoding(record, val);
1354 Constraint *storevalue=new Constraint(IMPLIES, srcenc, storeenc);
1355 ADDCONSTRAINT(storevalue,"excmemsuc");
1360 processAddresses(record);
1363 void ConstGen::processAdd(EPRecord *record) {
1365 LoadRF * lrf=new LoadRF(record, this);
1366 lrf->genConstraints(this);
1368 Constraint *var=getNewVar();
1369 Constraint *newadd=new Constraint(AND, var, getExecutionConstraint(record));
1370 ADDGOAL(record, newadd, "newadd");
1372 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1374 IntIterator *valit=record->getSet(VC_BASEINDEX)->iterator();
1375 uint64_t val=valit->next();
1377 IntHashSet *valset=getStoreLoadSet(record)->getValues();
1378 IntIterator *sis=valset->iterator();
1379 while(sis->hasNext()) {
1380 uint64_t memval=sis->next();
1381 uint64_t sumval=(memval+val)&getmask(record->getLen());
1383 if (valset->contains(sumval)) {
1385 Constraint *loadenc=getStoreLoadSet(record)->getRMWRValueEncoding(this, record, memval);
1386 Constraint *storeenc=getMemValueEncoding(record, sumval);
1387 Constraint *notvar=var->negate();
1388 Constraint *addinputfix=new Constraint(IMPLIES, loadenc, new Constraint(AND, storeenc, notvar));
1389 ADDCONSTRAINT(addinputfix, "addinputfix");
1395 ASSERT(depvec->size()==1);
1396 EPRecord *src=(*depvec)[0];
1397 IntIterator *it=record->getStoreSet()->iterator();
1398 IntHashSet *valset=getStoreLoadSet(record)->getValues();
1400 while(it->hasNext()) {
1401 uint64_t val=it->next();
1402 IntIterator *sis=valset->iterator();
1403 while(sis->hasNext()) {
1404 uint64_t memval=sis->next();
1405 uint64_t sum=(memval+val)&getmask(record->getLen());
1406 if (valset->contains(sum)) {
1407 Constraint *srcenc=getRetValueEncoding(src, val);
1408 Constraint *loadenc=getStoreLoadSet(record)->getRMWRValueEncoding(this, record, memval);
1409 Constraint *storeenc=getMemValueEncoding(record, sum);
1410 Constraint *notvar=var->negate();
1411 Constraint *addop=new Constraint(IMPLIES, new Constraint(AND, srcenc, loadenc),
1412 new Constraint(AND, notvar, storeenc));
1413 ADDCONSTRAINT(addop,"addinputvar");
1421 processAddresses(record);
1424 /** This function ensures that the value of a store's SAT variables
1425 matches the store's input value.
1427 TODO: Could optimize the case where the encodings are the same...
1430 void ConstGen::processStore(EPRecord *record) {
1431 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1433 //We have a hard coded value
1434 uint64_t val=record->getValue(0)->getValue();
1435 Constraint *storeenc=getMemValueEncoding(record, val);
1436 ADDCONSTRAINT(storeenc,"storefix");
1438 //We have a value from an input
1439 ASSERT(depvec->size()==1);
1440 EPRecord *src=(*depvec)[0];
1441 IntIterator *it=record->getStoreSet()->iterator();
1443 while(it->hasNext()) {
1444 uint64_t val=it->next();
1445 Constraint *srcenc=getRetValueEncoding(src, val);
1446 Constraint *storeenc=getMemValueEncoding(record, val);
1447 Constraint *storevalue=new Constraint(IMPLIES, srcenc, storeenc);
1448 ADDCONSTRAINT(storevalue,"storevar");
1452 processAddresses(record);
1455 /** Handle yields by just forbidding them via the SAT formula. */
1457 void ConstGen::processYield(EPRecord *record) {
1458 if (model->params.noyields &&
1459 record->getBranch()!=NULL) {
1460 Constraint * noyield=getExecutionConstraint(record)->negate();
1461 ADDCONSTRAINT(noyield, "noyield");
1465 void ConstGen::processLoopPhi(EPRecord *record) {
1466 EPRecordIDSet *phiset=record->getPhiLoopTable();
1467 EPRecordIDIterator *rit=phiset->iterator();
1469 while(rit->hasNext()) {
1470 struct RecordIDPair *rip=rit->next();
1471 EPRecord *input=rip->idrecord;
1473 IntIterator * it=record->getSet(VC_BASEINDEX)->iterator();
1474 while(it->hasNext()) {
1475 uint64_t value=it->next();
1476 Constraint * inputencoding=getRetValueEncoding(input, value);
1477 if (inputencoding==NULL)
1479 Constraint * branchconstraint=getExecutionConstraint(rip->record);
1480 Constraint * outputencoding=getRetValueEncoding(record, value);
1481 Constraint * phiimplication=new Constraint(IMPLIES, new Constraint(AND, inputencoding, branchconstraint), outputencoding);
1482 ADDCONSTRAINT(phiimplication,"philoop");
1489 void ConstGen::processPhi(EPRecord *record) {
1490 ModelVector<EPRecord *> * inputs=execution->getRevDependences(record, VC_BASEINDEX);
1491 for(uint i=0;i<inputs->size();i++) {
1492 EPRecord * input=(*inputs)[i];
1494 IntIterator * it=record->getSet(VC_BASEINDEX)->iterator();
1495 while(it->hasNext()) {
1496 uint64_t value=it->next();
1497 Constraint * inputencoding=getRetValueEncoding(input, value);
1498 if (inputencoding==NULL)
1500 Constraint * branchconstraint=getExecutionConstraint(input);
1501 Constraint * outputencoding=getRetValueEncoding(record, value);
1502 Constraint * phiimplication=new Constraint(IMPLIES, new Constraint(AND, inputencoding, branchconstraint), outputencoding);
1503 ADDCONSTRAINT(phiimplication,"phi");
1509 void ConstGen::processFunction(EPRecord *record) {
1510 if (record->getLoopPhi()) {
1511 processLoopPhi(record);
1513 } else if (record->getPhi()) {
1518 CGoalSet *knownbehaviors=record->completedGoalSet();
1519 CGoalIterator *cit=knownbehaviors->iterator();
1520 uint numinputs=record->getNumFuncInputs();
1521 EPRecord * inputs[numinputs];
1522 for(uint i=0;i<numinputs;i++) {
1523 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, i+VC_BASEINDEX);
1524 ASSERT(depvec->size()==1);
1525 inputs[i]=(*depvec)[0];
1527 while(cit->hasNext()) {
1528 CGoal *goal=cit->next();
1529 Constraint *carray[numinputs];
1530 if (record->isSharedGoals()) {
1531 bool badvalue=false;
1532 for(uint i=0;i<numinputs;i++) {
1533 uint64_t inputval=goal->getValue(i+VC_BASEINDEX);
1534 if (!record->getSet(i+VC_BASEINDEX)->contains(inputval)) {
1543 /* Build up constraints for each input */
1544 for(uint i=0;i<numinputs;i++) {
1545 uint64_t inputval=goal->getValue(i+VC_BASEINDEX);
1546 Constraint * inputc=getRetValueEncoding(inputs[i], inputval);
1547 ASSERT(inputc!=NULL);
1550 Constraint * outputconstraint=getRetValueEncoding(record, goal->getOutput());
1552 ADDCONSTRAINT(outputconstraint,"functionimpl");
1554 Constraint * functionimplication=new Constraint(IMPLIES, new Constraint(AND, numinputs, carray), outputconstraint);
1555 ADDCONSTRAINT(functionimplication,"functionimpl");
1560 FunctionRecord *fr=functiontable->get(record);
1561 Constraint *goal=fr->getNoValueEncoding();
1562 Constraint *newfunc=new Constraint(AND, goal, getExecutionConstraint(record));
1563 ADDGOAL(record, newfunc, "newfunc");
1566 void ConstGen::processEquals(EPRecord *record) {
1567 ASSERT (record->getNumFuncInputs() == 2);
1568 EPRecord * inputs[2];
1570 for(uint i=0;i<2;i++) {
1571 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, i+VC_BASEINDEX);
1574 } else if (depvec->size()==1) {
1575 inputs[i]=(*depvec)[0];
1576 } else ASSERT(false);
1579 //rely on this being a variable
1580 Constraint * outputtrue=getRetValueEncoding(record, 1);
1581 ASSERT(outputtrue->getType()==VAR);
1583 if (inputs[0]!=NULL && inputs[1]!=NULL &&
1584 (inputs[0]->getType()==LOAD || inputs[0]->getType()==RMW) &&
1585 (inputs[1]->getType()==LOAD || inputs[1]->getType()==RMW) &&
1586 (getStoreLoadSet(inputs[0])==getStoreLoadSet(inputs[1]))) {
1587 StoreLoadSet * sls=getStoreLoadSet(inputs[0]);
1588 int numvalvars=sls->getNumValVars();
1589 Constraint **valvar1=(inputs[0]->getType()==RMW)?sls->getRMWRValVars(this, inputs[0]):sls->getValVars(this, inputs[0]);
1590 Constraint **valvar2=(inputs[1]->getType()==RMW)?sls->getRMWRValVars(this, inputs[1]):sls->getValVars(this, inputs[1]);
1593 Constraint *vars[numvalvars];
1594 for(int i=0;i<numvalvars;i++) {
1595 vars[i]=getNewVar();
1596 Constraint *var1=valvar1[i];
1597 Constraint *var2=valvar2[i];
1598 Constraint * array[]={var1, var2->negate(), vars[i]->negate()};
1599 Constraint * array2[]={var2, var1->negate(), vars[i]->negate()};
1600 Constraint * a=new Constraint(OR, 3, array);
1601 ADDCONSTRAINT(a, "equala");
1602 Constraint * a2=new Constraint(OR, 3, array2);
1603 ADDCONSTRAINT(a2, "equala2");
1604 Constraint * arrayb[]={var1, var2, vars[i]};
1605 Constraint * array2b[]={var2->negate(), var1->negate(), vars[i]};
1606 Constraint * b=new Constraint(OR, 3, arrayb);
1607 ADDCONSTRAINT(b, "equalb");
1608 Constraint *b2=new Constraint(OR, 3, array2b);
1609 ADDCONSTRAINT(b2, "equalb2");
1611 ADDCONSTRAINT(new Constraint(IMPLIES, new Constraint(AND, numvalvars, vars), outputtrue),"impequal1");
1613 ADDCONSTRAINT(new Constraint(IMPLIES, outputtrue, new Constraint(AND, numvalvars, vars)), "impequal2");
1617 Constraint * functionimplication=new Constraint(IMPLIES,generateEquivConstraint(numvalvars, valvar1, valvar2), outputtrue);
1618 ADDCONSTRAINT(functionimplication,"equalsimplspecial");
1619 Constraint * functionimplicationneg=new Constraint(IMPLIES,outputtrue, generateEquivConstraint(numvalvars, valvar1, valvar2));
1620 ADDCONSTRAINT(functionimplicationneg,"equalsimplspecialneg");
1625 if (inputs[0]==NULL && inputs[1]==NULL) {
1626 IntIterator *iit0=record->getSet(VC_BASEINDEX+0)->iterator();
1627 uint64_t constval=iit0->next();
1629 IntIterator *iit1=record->getSet(VC_BASEINDEX+1)->iterator();
1630 uint64_t constval2=iit1->next();
1633 if (constval==constval2) {
1634 ADDCONSTRAINT(outputtrue, "equalsconst");
1636 ADDCONSTRAINT(outputtrue->negate(), "equalsconst");
1641 if (inputs[0]==NULL ||
1643 int nullindex=inputs[0]==NULL?0:1;
1644 IntIterator *iit=record->getSet(VC_BASEINDEX+nullindex)->iterator();
1645 uint64_t constval=iit->next();
1648 record->getSet(VC_BASEINDEX+nullindex);
1649 EPRecord *r=inputs[1-nullindex];
1650 Constraint *l=getRetValueEncoding(r, constval);
1651 Constraint *functionimplication=new Constraint(IMPLIES, l, outputtrue);
1652 ADDCONSTRAINT(functionimplication,"equalsimpl");
1654 Constraint *l2=getRetValueEncoding(r, constval);
1655 Constraint *functionimplication2=new Constraint(IMPLIES, outputtrue, l2);
1656 ADDCONSTRAINT(functionimplication2,"equalsimpl");
1659 IntIterator *iit=record->getSet(VC_BASEINDEX)->iterator();
1660 while(iit->hasNext()) {
1661 uint64_t val1=iit->next();
1663 IntIterator *iit2=record->getSet(VC_BASEINDEX+1)->iterator();
1664 while(iit2->hasNext()) {
1665 uint64_t val2=iit2->next();
1666 Constraint *l=getRetValueEncoding(inputs[0], val1);
1667 Constraint *r=getRetValueEncoding(inputs[1], val2);
1668 Constraint *imp=(val1==val2)?outputtrue:outputtrue->negate();
1669 Constraint * functionimplication=new Constraint(IMPLIES, new Constraint(AND, l, r), imp);
1670 ADDCONSTRAINT(functionimplication,"equalsimpl");
1678 void ConstGen::processFence(EPRecord *record) {
1679 //do we already account for the fence?
1680 if (isAlwaysExecuted(record))
1682 ExecPoint * record_ep=record->getEP();
1683 thread_id_t tid=record_ep->get_tid();
1684 uint thread=id_to_int(tid);
1685 ModelVector<EPRecord *> *tvec=(*threadactions)[thread];
1686 uint size=tvec->size();
1688 EPRecord *prevstore=NULL;
1690 for(i=0;i<size;i++) {
1691 EPRecord *rec=(*tvec)[i];
1692 if (rec->getType()==STORE) {
1695 if (rec == record) {
1700 if (prevstore == NULL) {
1704 EPRecord *rec=(*tvec)[i];
1705 if (rec->getType()==LOAD) {
1706 Constraint * condition=getExecutionConstraint(record);
1707 Constraint * storeload=getOrderConstraint(prevstore, rec);
1708 Constraint * c=new Constraint(IMPLIES, condition, storeload);
1709 ADDCONSTRAINT(c, "fence");
1716 void ConstGen::processRecord(EPRecord *record) {
1717 switch (record->getType()) {
1719 processFunction(record);
1722 processEquals(record);
1725 processLoad(record);
1728 processStore(record);
1732 processFence(record);
1737 processFence(record);
1739 if (record->getOp()==ADD) {
1741 } else if (record->getOp()==CAS) {
1743 } else if (record->getOp()==EXC) {
1749 processYield(record);
1752 processBranch(record);
1759 void ConstGen::visitRecord(EPRecord *record) {
1760 switch (record->getType()) {
1762 recordExecCond(record);
1763 insertEquals(record);
1766 recordExecCond(record);
1767 insertFunction(record);
1771 recordExecCond(record);
1772 insertAction(record);
1776 recordExecCond(record);
1777 insertAction(record);
1778 groupMemoryOperations(record);
1781 recordExecCond(record);
1782 insertAction(record);
1783 groupMemoryOperations(record);
1786 recordExecCond(record);
1787 insertAction(record);
1788 groupMemoryOperations(record);
1791 recordExecCond(record);
1792 insertBranch(record);
1795 recordExecCond(record);
1798 recordExecCond(record);
1799 insertNonLocal(record);
1802 insertLabel(record);
1805 recordExecCond(record);
1812 void ConstGen::recordExecCond(EPRecord *record) {
1813 ExecPoint *eprecord=record->getEP();
1814 EPValue * branchval=record->getBranch();
1815 EPRecord * branch=(branchval==NULL)?NULL:branchval->getRecord();
1816 ExecPoint *epbranch= (branch==NULL) ? NULL : branch->getEP();
1817 RecordSet *srs=NULL;
1818 RecordIterator *sri=nonlocaltrans->iterator();
1819 while(sri->hasNext()) {
1820 EPRecord *nonlocal=sri->next();
1821 ExecPoint *epnl=nonlocal->getEP();
1822 if (epbranch!=NULL) {
1823 if (epbranch->compare(epnl)==CR_BEFORE) {
1824 //branch occurs after non local and thus will subsume condition
1825 //branch subsumes this condition
1829 if (eprecord->compare(epnl)==CR_BEFORE) {
1830 //record occurs after non-local, so add it to set
1832 srs=new RecordSet();
1838 execcondtable->put(record, srs);
1841 void ConstGen::insertNonLocal(EPRecord *record) {
1842 nonlocaltrans->add(record);
1845 void ConstGen::insertLabel(EPRecord *record) {
1846 RecordIterator *sri=nonlocaltrans->iterator();
1847 while(sri->hasNext()) {
1848 EPRecord *nonlocal=sri->next();
1849 if (nonlocal->getNextRecord()==record)
1856 void ConstGen::traverseRecord(EPRecord *record, bool initial) {
1859 visitRecord(record);
1861 processRecord(record);
1863 if (record->getType()==LOOPENTER) {
1864 workstack->push_back(record->getNextRecord());
1865 workstack->push_back(record->getChildRecord());
1868 if (record->getChildRecord()!=NULL) {
1869 workstack->push_back(record->getChildRecord());
1871 if (record->getType()==NONLOCALTRANS) {
1874 if (record->getType()==LOOPEXIT) {
1877 if (record->getType()==BRANCHDIR) {
1878 EPRecord *next=record->getNextRecord();
1880 workstack->push_back(next);
1881 for(uint i=0;i<record->numValues();i++) {
1882 EPValue *branchdir=record->getValue(i);
1884 //Could have an empty branch, so make sure the branch actually
1886 if (branchdir->getFirstRecord()!=NULL)
1887 workstack->push_back(branchdir->getFirstRecord());
1891 record=record->getNextRecord();
1892 } while(record!=NULL);
1895 unsigned int RecPairHash(RecPair *rp) {
1896 uintptr_t v=(uintptr_t) rp->epr1;
1897 uintptr_t v2=(uintptr_t) rp->epr2;
1900 return (uint)((x>>4)^(a));
1903 bool RecPairEquals(RecPair *r1, RecPair *r2) {
1904 return ((r1->epr1==r2->epr1)&&(r1->epr2==r2->epr2)) ||
1905 ((r1->epr1==r2->epr2)&&(r1->epr2==r2->epr1));