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()==BRANCHDIR) {
352 EPRecord *next=record->getNextRecord();
354 workstack->push_back(next);
355 for(uint i=0;i<record->numValues();i++) {
356 EPValue *branchdir=record->getValue(i);
358 //Could have an empty branch, so make sure the branch actually
360 if (branchdir->getFirstRecord()!=NULL) {
361 workstack->push_back(branchdir->getFirstRecord());
362 dprintf(file, "%lu->%lu[color=blue];\n", (uintptr_t) record, (uintptr_t) branchdir->getFirstRecord());
367 record=record->getNextRecord();
368 } while(record!=NULL);
372 /* This function traverses a thread's graph in execution order. */
374 void ConstGen::traverse(bool initial) {
375 EPRecord *first=execution->getEPRecord(MCID_FIRST);
376 traverseRecord(first, initial);
377 while(!workstack->empty()) {
378 EPRecord *record=workstack->back();
379 workstack->pop_back();
380 traverseRecord(record, initial);
384 /** This method looks for all other memory operations that could
385 potentially share a location, and build partitions of memory
386 locations such that all memory locations that can share the same
387 address are in the same group.
389 These memory operations should share an encoding of addresses and
393 void ConstGen::groupMemoryOperations(EPRecord *op) {
394 /** Handle our first address */
395 IntHashSet *addrset=op->getSet(VC_ADDRINDEX);
396 IntIterator *ait=addrset->iterator();
398 void *iaddr=(void *) ait->next();
399 StoreLoadSet *isls=storeloadtable->get(iaddr);
401 isls=new StoreLoadSet();
402 storeloadtable->put(iaddr, isls);
406 while(ait->hasNext()) {
407 void *addr=(void *)ait->next();
408 StoreLoadSet *sls=storeloadtable->get(addr);
410 storeloadtable->put(addr, isls);
411 } else if (sls!=isls) {
413 mergeSets(isls, sls);
420 RecordSet * ConstGen::computeConflictSet(EPRecord *store, EPRecord *load, RecordSet * baseset) {
421 //See if we can determine addresses that store/load may use
422 IntIterator * storeaddr=store->getSet(VC_ADDRINDEX)->iterator();
423 int numaddr=0;void *commonaddr=NULL;
424 while(storeaddr->hasNext()) {
425 void *addr=(void *) storeaddr->next();
426 if (load->getSet(VC_ADDRINDEX)->contains((uint64_t)addr)) {
437 RecordSet *srscopy=baseset->copy();
438 RecordIterator *sri=srscopy->iterator();
439 while(sri->hasNext()) {
440 bool pruneconflictstore=false;
441 EPRecord *conflictstore=sri->next();
442 bool conflictafterstore=getOrderConstraint(store,conflictstore)->isTrue();
443 bool conflictbeforeload=getOrderConstraint(conflictstore,load)->isTrue();
445 if (conflictafterstore) {
446 RecordIterator *sricheck=srscopy->iterator();
447 while(sricheck->hasNext()) {
448 EPRecord *checkstore=sricheck->next();
449 bool checkafterstore=getOrderConstraint(store, checkstore)->isTrue();
450 if (!checkafterstore)
452 bool checkbeforeconflict=getOrderConstraint(checkstore,conflictstore)->isTrue();
453 if (!checkbeforeconflict)
456 //See if the checkstore must store to the relevant address
457 IntHashSet * storeaddr=checkstore->getSet(VC_ADDRINDEX);
459 if (storeaddr->getSize()!=1 || !storeaddr->contains((uint64_t)commonaddr))
463 if (subsumesExecutionConstraint(checkstore, conflictstore)) {
464 pruneconflictstore=true;
471 if (conflictbeforeload && !pruneconflictstore) {
472 RecordIterator *sricheck=srscopy->iterator();
473 while(sricheck->hasNext()) {
474 EPRecord *checkstore=sricheck->next();
476 bool checkafterconflict=getOrderConstraint(conflictstore, checkstore)->isTrue();
477 if (!checkafterconflict)
480 bool checkbeforeload=getOrderConstraint(checkstore, load)->isTrue();
481 if (!checkbeforeload)
484 //See if the checkstore must store to the relevant address
485 IntHashSet * storeaddr=checkstore->getSet(VC_ADDRINDEX);
486 if (storeaddr->getSize()!=1 || !storeaddr->contains((uint64_t)commonaddr))
490 if (subsumesExecutionConstraint(checkstore, conflictstore)) {
491 pruneconflictstore=true;
497 if (pruneconflictstore) {
498 //This store is redundant
508 /** This method returns all stores that a load may read from. */
510 RecordSet * ConstGen::getMayReadFromSet(EPRecord *load) {
511 if (load->getSet(VC_ADDRINDEX)->getSize()==1)
512 return getMayReadFromSetOpt(load);
514 RecordSet *srs=loadtable->get(load);
515 ExecPoint *epload=load->getEP();
516 thread_id_t loadtid=epload->get_tid();
519 loadtable->put(load, srs);
521 IntHashSet *addrset=load->getSet(VC_ADDRINDEX);
522 IntIterator *ait=addrset->iterator();
524 while(ait->hasNext()) {
525 void *addr=(void *)ait->next();
526 RecordSet *rs=execution->getStoreTable(addr);
530 RecordIterator * rit=rs->iterator();
531 while(rit->hasNext()) {
532 EPRecord *rec=rit->next();
533 ExecPoint *epstore=rec->getEP();
534 thread_id_t storetid=epstore->get_tid();
535 if (storetid != loadtid ||
536 epstore->compare(epload) == CR_AFTER)
547 RecordSet * ConstGen::getMayReadFromSetOpt(EPRecord *load) {
548 RecordSet *srs=loadtable->get(load);
549 ExecPoint *epload=load->getEP();
550 thread_id_t loadtid=epload->get_tid();
553 loadtable->put(load, srs);
555 IntHashSet *addrset=load->getSet(VC_ADDRINDEX);
556 IntIterator *ait=addrset->iterator();
557 void *addr=(void *)ait->next();
560 RecordSet *rs=execution->getStoreTable(addr);
561 RecordIterator * rit=rs->iterator();
562 ExecPoint *latest=NULL;
563 while(rit->hasNext()) {
564 EPRecord *store=rit->next();
565 ExecPoint *epstore=store->getEP();
566 thread_id_t storetid=epstore->get_tid();
567 if (storetid == loadtid && isAlwaysExecuted(store) &&
568 store->getSet(VC_ADDRINDEX)->getSize()==1 &&
569 epstore->compare(epload) == CR_AFTER &&
570 (latest==NULL || latest->compare(epstore) == CR_AFTER)) {
576 while(rit->hasNext()) {
577 EPRecord *store=rit->next();
578 ExecPoint *epstore=store->getEP();
579 thread_id_t storetid=epstore->get_tid();
580 if (storetid == loadtid) {
581 if (epstore->compare(epload) == CR_AFTER &&
582 (latest==NULL || epstore->compare(latest) != CR_AFTER))
593 /** This function merges two recordsets and updates the storeloadtable
596 void ConstGen::mergeSets(StoreLoadSet *to, StoreLoadSet *from) {
597 RecordIterator * sri=from->iterator();
598 while(sri->hasNext()) {
599 EPRecord *rec=sri->next();
601 IntHashSet *addrset=rec->getSet(VC_ADDRINDEX);
602 IntIterator *ait=addrset->iterator();
603 while(ait->hasNext()) {
604 void *addr=(void *)ait->next();
605 storeloadtable->put(addr, to);
614 /** This function creates ordering variables between stores and loads
615 * in same thread for TSO. */
617 void ConstGen::insertTSOAction(EPRecord *load) {
618 if (load->getType() != LOAD)
620 ExecPoint *load_ep=load->getEP();
621 thread_id_t tid=load_ep->get_tid();
622 uint thread=id_to_int(tid);
623 ModelVector<EPRecord *> * vector=(*threadactions)[thread];
624 uint j=vector->size()-1;
626 EPRecord *oldrec=(*vector)[--j];
627 EventType oldrec_t=oldrec->getType();
629 if (((oldrec_t == RMW) || (oldrec_t==FENCE)) &&
630 isAlwaysExecuted(oldrec)) {
632 } else if (oldrec_t == STORE) {
633 /* Only generate variables for things that can actually both run */
635 createOrderConstraint(oldrec, load);
640 void ConstGen::genTSOTransOrderConstraints() {
641 for(uint t1=0;t1<threadactions->size();t1++) {
642 ModelVector<EPRecord *> *tvec=(*threadactions)[t1];
643 uint size=tvec->size();
644 EPRecord *laststore=NULL;
645 for(uint store_i=0;store_i<size;store_i++) {
646 EPRecord *store=(*tvec)[store_i];
647 EventType store_t=store->getType();
648 if (store_t != STORE)
650 EPRecord *lastload=NULL;
651 for(uint load_i=store_i+1;load_i<size;load_i++) {
652 EPRecord *rec=(*tvec)[store_i];
653 //Hit fence, don't need more stuff
654 EventType rec_t=rec->getType();
655 if (((rec_t == RMW) || (rec_t == FENCE)) &&
656 isAlwaysExecuted(rec))
660 if (laststore != NULL) {
661 Constraint * storeload=getOrderConstraint(store, rec);
662 Constraint * earlystoreload=getOrderConstraint(laststore, rec);
663 Constraint * c=new Constraint(IMPLIES, storeload, earlystoreload);
664 ADDCONSTRAINT(c, "earylstore");
666 if (lastload != NULL) {
667 Constraint * storeearlyload=getOrderConstraint(store, lastload);
668 Constraint * storeload=getOrderConstraint(store, rec);
669 Constraint * c=new Constraint(IMPLIES, storeearlyload, storeload);
670 ADDCONSTRAINT(c, "earylload");
680 /** This function creates ordering constraints to implement SC for
681 memory operations. */
683 void ConstGen::insertAction(EPRecord *record) {
684 thread_id_t tid=record->getEP()->get_tid();
685 uint thread=id_to_int(tid);
686 if (threadactions->size()<=thread) {
687 uint oldsize=threadactions->size();
688 threadactions->resize(thread+1);
689 for(;oldsize<=thread;oldsize++) {
690 (*threadactions)[oldsize]=new ModelVector<EPRecord *>();
694 (*threadactions)[thread]->push_back(record);
696 for(uint i=0;i<threadactions->size();i++) {
699 ModelVector<EPRecord *> * vector=(*threadactions)[i];
700 for(uint j=0;j<vector->size();j++) {
701 EPRecord *oldrec=(*vector)[j];
702 createOrderConstraint(oldrec, record);
706 insertTSOAction(record);
710 void ConstGen::genTransOrderConstraints() {
711 for(uint t1=0;t1<threadactions->size();t1++) {
712 ModelVector<EPRecord *> *t1vec=(*threadactions)[t1];
713 for(uint t2=0;t2<t1;t2++) {
714 ModelVector<EPRecord *> *t2vec=(*threadactions)[t2];
715 genTransOrderConstraints(t1vec, t2vec);
716 genTransOrderConstraints(t2vec, t1vec);
717 for(uint t3=0;t3<t2;t3++) {
718 ModelVector<EPRecord *> *t3vec=(*threadactions)[t3];
719 genTransOrderConstraints(t1vec, t2vec, t3vec);
725 void ConstGen::genTransOrderConstraints(ModelVector<EPRecord *> * t1vec, ModelVector<EPRecord *> *t2vec) {
726 for(uint t1i=0;t1i<t1vec->size();t1i++) {
727 EPRecord *t1rec=(*t1vec)[t1i];
728 for(uint t2i=0;t2i<t2vec->size();t2i++) {
729 EPRecord *t2rec=(*t2vec)[t2i];
731 /* Note: One only really needs to generate the first constraint
732 in the first loop and the last constraint in the last loop.
733 I tried this and performance suffered on linuxrwlocks and
734 linuxlocks at the current time. BD - August 2014*/
735 Constraint *c21=getOrderConstraint(t2rec, t1rec);
737 /* short circuit for the trivial case */
741 for(uint t3i=t2i+1;t3i<t2vec->size();t3i++) {
742 EPRecord *t3rec=(*t2vec)[t3i];
743 Constraint *c13=getOrderConstraint(t1rec, t3rec);
745 Constraint *c32=getOrderConstraint(t3rec, t2rec);
746 Constraint * array[]={c21, c32, c13};
747 Constraint *intratransorder=new Constraint(OR, 3, array);
749 Constraint *intratransorder=new Constraint(OR, c21, c13);
751 ADDCONSTRAINT(intratransorder,"intratransorder");
754 for(uint t0i=0;t0i<t1i;t0i++) {
755 EPRecord *t0rec=(*t1vec)[t0i];
756 Constraint *c02=getOrderConstraint(t0rec, t2rec);
758 Constraint *c10=getOrderConstraint(t1rec, t0rec);
759 Constraint * array[]={c10, c21, c02};
760 Constraint *intratransorder=new Constraint(OR, 3, array);
762 Constraint *intratransorder=new Constraint(OR, c21, c02);
764 ADDCONSTRAINT(intratransorder,"intratransorder");
771 void ConstGen::genTransOrderConstraints(ModelVector<EPRecord *> * t1vec, ModelVector<EPRecord *> *t2vec, ModelVector<EPRecord *> * t3vec) {
772 for(uint t1i=0;t1i<t1vec->size();t1i++) {
773 EPRecord *t1rec=(*t1vec)[t1i];
774 for(uint t2i=0;t2i<t2vec->size();t2i++) {
775 EPRecord *t2rec=(*t2vec)[t2i];
776 for(uint t3i=0;t3i<t3vec->size();t3i++) {
777 EPRecord *t3rec=(*t3vec)[t3i];
778 genTransOrderConstraint(t1rec, t2rec, t3rec);
784 void ConstGen::genTransOrderConstraint(EPRecord *t1rec, EPRecord *t2rec, EPRecord *t3rec) {
785 Constraint *c21=getOrderConstraint(t2rec, t1rec);
786 Constraint *c32=getOrderConstraint(t3rec, t2rec);
787 Constraint *c13=getOrderConstraint(t1rec, t3rec);
788 Constraint * cimpl1[]={c21, c32, c13};
789 Constraint * c1=new Constraint(OR, 3, cimpl1);
790 ADDCONSTRAINT(c1, "intertransorder");
792 Constraint *c12=getOrderConstraint(t1rec, t2rec);
793 Constraint *c23=getOrderConstraint(t2rec, t3rec);
794 Constraint *c31=getOrderConstraint(t3rec, t1rec);
795 Constraint * cimpl2[]={c12, c23, c31};
796 Constraint *c2=new Constraint(OR, 3, cimpl2);
797 ADDCONSTRAINT(c2, "intertransorder");
800 void ConstGen::addGoal(EPRecord *r, Constraint *c) {
801 rectoint->put(r, goalset->size());
802 goalset->push_back(c);
805 void ConstGen::addBranchGoal(EPRecord *r, Constraint *c) {
806 has_untaken_branches=true;
807 rectoint->put(r, goalset->size());
808 goalset->push_back(c);
811 void ConstGen::achievedGoal(EPRecord *r) {
812 if (rectoint->contains(r)) {
813 uint index=rectoint->get(r);
814 //if (goalvararray[index] != NULL)
815 //model_print("Run Clearing goal index %d\n",index);
816 goalvararray[index]=NULL;
820 void ConstGen::addConstraint(Constraint *c) {
821 ModelVector<Constraint *> *vec=c->simplify();
822 for(uint i=0;i<vec->size();i++) {
823 Constraint *simp=(*vec)[i];
824 if (simp->type==TRUE)
826 ASSERT(simp->type!=FALSE);
827 simp->printDIMACS(this);
828 #ifdef VERBOSE_CONSTRAINTS
838 void ConstGen::printNegConstraint(uint value) {
840 solver->addClauseLiteral(val);
843 void ConstGen::printConstraint(uint value) {
844 solver->addClauseLiteral(value);
847 bool * ConstGen::runSolver() {
848 int solution=solver->solve();
849 if (solution == IS_UNSAT) {
851 } else if (solution == IS_SAT) {
852 bool * assignments=(bool *)model_malloc(sizeof(bool)*(varindex+1));
853 for(uint i=0;i<=varindex;i++)
854 assignments[i]=solver->getValue(i);
859 dprintf(2, "INDETER\n");
860 model_print("INDETER\n");
866 Constraint * ConstGen::getOrderConstraint(EPRecord *first, EPRecord *second) {
868 if (first->getEP()->get_tid()==second->getEP()->get_tid()) {
869 if (first->getEP()->compare(second->getEP())==CR_AFTER)
876 RecPair rp(first, second);
877 RecPair *rpc=rpt->get(&rp);
880 first->getEP()->get_tid()==second->getEP()->get_tid()) {
881 if (first->getEP()->compare(second->getEP())==CR_AFTER)
890 Constraint *c=rpc->constraint;
891 if (rpc->epr1!=first) {
892 //have to flip arguments
899 bool ConstGen::getOrder(EPRecord *first, EPRecord *second, bool * satsolution) {
900 RecPair rp(first, second);
901 RecPair *rpc=rpt->get(&rp);
904 first->getEP()->get_tid()==second->getEP()->get_tid()) {
905 if (first->getEP()->compare(second->getEP())==CR_AFTER)
915 Constraint *c=rpc->constraint;
916 CType type=c->getType();
921 else if (type==FALSE)
924 uint index=c->getVar();
925 order=satsolution[index];
927 if (rpc->epr1==first)
933 /** This function determines whether events first and second are
934 * ordered by start and join operations. */
936 bool ConstGen::orderThread(EPRecord *first, EPRecord *second) {
937 ExecPoint * ep1=first->getEP();
938 ExecPoint * ep2=second->getEP();
939 thread_id_t thr1=ep1->get_tid();
940 thread_id_t thr2=ep2->get_tid();
941 Thread *tr2=execution->get_thread(thr2);
942 EPRecord *thr2start=tr2->getParentRecord();
943 if (thr2start!=NULL) {
944 ExecPoint *epthr2start=thr2start->getEP();
945 if (epthr2start->get_tid()==thr1 &&
946 ep1->compare(epthr2start)==CR_AFTER)
949 ModelVector<EPRecord *> * joinvec=execution->getJoins();
950 for(uint i=0;i<joinvec->size();i++) {
951 EPRecord *join=(*joinvec)[i];
952 ExecPoint *jp=join->getEP();
953 if (jp->get_tid()==thr2 &&
954 jp->compare(ep2)==CR_AFTER)
960 /** This function generates an ordering constraint for two events. */
962 void ConstGen::createOrderConstraint(EPRecord *first, EPRecord *second) {
963 RecPair * rp=new RecPair(first, second);
964 if (!rpt->contains(rp)) {
965 if (orderThread(first, second))
966 rp->constraint=&ctrue;
967 else if (orderThread(second, first))
968 rp->constraint=&cfalse;
970 rp->constraint=getNewVar();
978 Constraint * ConstGen::getNewVar() {
980 if (varindex>vars->size()) {
981 var=new Constraint(VAR, varindex);
982 Constraint *varneg=new Constraint(NOTVAR, varindex);
985 vars->push_back(var);
987 var=(*vars)[varindex-1];
993 /** Gets an array of new variables. */
995 void ConstGen::getArrayNewVars(uint num, Constraint **carray) {
996 for(uint i=0;i<num;i++)
997 carray[i]=getNewVar();
1000 StoreLoadSet * ConstGen::getStoreLoadSet(EPRecord *record) {
1001 IntIterator *it=record->getSet(VC_ADDRINDEX)->iterator();
1002 void *addr=(void *)it->next();
1004 return storeloadtable->get(addr);
1007 /** Returns a constraint that is true if the output of record has the
1010 Constraint * ConstGen::getRetValueEncoding(EPRecord *record, uint64_t value) {
1011 switch(record->getType()) {
1013 return equalstable->get(record)->getValueEncoding(value);
1015 return functiontable->get(record)->getValueEncoding(value);
1017 return getStoreLoadSet(record)->getValueEncoding(this, record, value);
1020 return getStoreLoadSet(record)->getRMWRValueEncoding(this, record, value);
1028 Constraint * ConstGen::getMemValueEncoding(EPRecord *record, uint64_t value) {
1029 switch(record->getType()) {
1031 return getStoreLoadSet(record)->getValueEncoding(this, record, value);
1033 return getStoreLoadSet(record)->getValueEncoding(this, record, value);
1040 /** Return true if the execution of record implies the execution of
1043 bool ConstGen::subsumesExecutionConstraint(EPRecord *recordsubsumes, EPRecord *record) {
1044 EPValue *branch=record->getBranch();
1045 EPValue *branchsubsumes=recordsubsumes->getBranch();
1046 if (branchsubsumes != NULL) {
1047 bool branchsubsumed=false;
1048 while(branch!=NULL) {
1049 if (branchsubsumes==branch) {
1050 branchsubsumed=true;
1053 branch=branch->getRecord()->getBranch();
1055 if (!branchsubsumed)
1058 RecordSet *srs=execcondtable->get(recordsubsumes);
1061 RecordIterator *sri=srs->iterator();
1062 while(sri->hasNext()) {
1063 EPRecord *rec=sri->next();
1065 if (!getOrderConstraint(rec, record)->isTrue()) {
1075 Constraint * ConstGen::getExecutionConstraint(EPRecord *record) {
1076 EPValue *branch=record->getBranch();
1077 RecordSet *srs=execcondtable->get(record);
1078 int size=srs==NULL?0:srs->getSize();
1082 Constraint *array[size];
1085 RecordIterator *sri=srs->iterator();
1086 while(sri->hasNext()) {
1087 EPRecord *rec=sri->next();
1088 EPValue *recbranch=rec->getBranch();
1089 BranchRecord *guardbr=branchtable->get(recbranch->getRecord());
1090 array[index++]=guardbr->getBranch(recbranch)->negate();
1095 BranchRecord *guardbr=branchtable->get(branch->getRecord());
1096 array[index++]=guardbr->getBranch(branch);
1103 return new Constraint(AND, index, array);
1106 bool ConstGen::isAlwaysExecuted(EPRecord *record) {
1107 EPValue *branch=record->getBranch();
1108 RecordSet *srs=execcondtable->get(record);
1109 int size=srs==NULL?0:srs->getSize();
1116 void ConstGen::insertBranch(EPRecord *record) {
1117 uint numvalue=record->numValues();
1118 /** need one value for new directions */
1119 if (numvalue<record->getLen())
1121 /** need extra value to represent that branch wasn't executed. **/
1122 bool alwaysexecuted=isAlwaysExecuted(record);
1123 if (!alwaysexecuted)
1125 uint numbits=NUMBITS(numvalue-1);
1126 Constraint *bits[numbits];
1127 getArrayNewVars(numbits, bits);
1128 BranchRecord *br=new BranchRecord(record, numbits, bits, alwaysexecuted);
1129 branchtable->put(record, br);
1132 void ConstGen::processBranch(EPRecord *record) {
1133 BranchRecord *br=branchtable->get(record);
1134 if (record->numValues()<record->getLen()) {
1135 Constraint *goal=br->getNewBranch();
1136 ADDBRANCHGOAL(record, goal,"newbranch");
1139 /** Insert criteria of parent branch going the right way. **/
1140 Constraint *baseconstraint=getExecutionConstraint(record);
1142 if (!isAlwaysExecuted(record)) {
1143 Constraint *parentbranch=new Constraint(IMPLIES, br->getAnyBranch(), baseconstraint);
1144 ADDCONSTRAINT(parentbranch, "parentbranch");
1147 /** Insert criteria for directions */
1148 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1149 ASSERT(depvec->size()==1);
1150 EPRecord * val_record=(*depvec)[0];
1151 for(unsigned int i=0;i<record->numValues();i++) {
1152 EPValue * branchval=record->getValue(i);
1153 uint64_t val=branchval->getValue();
1156 Constraint *execconstraint=getExecutionConstraint(record);
1157 Constraint *br_false=new Constraint(IMPLIES,
1158 new Constraint(AND, execconstraint,
1159 getRetValueEncoding(val_record, val)), br->getBranch(branchval));
1160 ADDCONSTRAINT(br_false, "br_false");
1162 if (record->getBranchAnyValue()) {
1163 if (getRetValueEncoding(val_record, 0)!=NULL) {
1164 Constraint *execconstraint=getExecutionConstraint(record);
1165 Constraint *br_true1=new Constraint(IMPLIES, new Constraint(AND, getRetValueEncoding(val_record, 0)->negate(),
1167 br->getBranch(branchval));
1168 ADDCONSTRAINT(br_true1, "br_true1");
1170 for(unsigned int j=0;j<val_record->numValues();j++) {
1171 EPValue * epval=val_record->getValue(j);
1172 Constraint *execconstraint=getExecutionConstraint(record);
1173 Constraint *valuematches=getRetValueEncoding(val_record, epval->getValue());
1174 Constraint *br_true2=new Constraint(IMPLIES, new Constraint(AND, execconstraint, valuematches), br->getBranch(branchval));
1175 ADDCONSTRAINT(br_true2, "br_true2");
1179 Constraint *execconstraint=getExecutionConstraint(record);
1180 Constraint *br_val=new Constraint(IMPLIES, new Constraint(AND, execconstraint, getRetValueEncoding(val_record, val)), br->getBranch(branchval));
1181 ADDCONSTRAINT(br_val, "br_val");
1187 void ConstGen::insertFunction(EPRecord *record) {
1188 FunctionRecord * fr=new FunctionRecord(this, record);
1189 functiontable->put(record, fr);
1192 void ConstGen::insertEquals(EPRecord *record) {
1193 EqualsRecord * fr=new EqualsRecord(this, record);
1194 equalstable->put(record, fr);
1197 void ConstGen::processLoad(EPRecord *record) {
1198 LoadRF * lrf=new LoadRF(record, this);
1199 lrf->genConstraints(this);
1201 processAddresses(record);
1204 /** This procedure generates the constraints that set the address
1205 variables for load/store/rmw operations. */
1207 void ConstGen::processAddresses(EPRecord *record) {
1208 StoreLoadSet *sls=getStoreLoadSet(record);
1209 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_ADDRINDEX);
1211 //we have a hard coded address
1212 const void *addr=record->getValue(0)->getAddr();
1213 Constraint *addrenc=sls->getAddressEncoding(this, record, addr);
1214 ADDCONSTRAINT(addrenc,"fixedaddress");
1216 //we take as input an address and have to generate implications
1217 //for each possible input address
1218 ASSERT(depvec->size()==1);
1219 EPRecord *src=(*depvec)[0];
1220 IntIterator *it=record->getSet(VC_ADDRINDEX)->iterator();
1222 uintptr_t offset=record->getOffset();
1224 while(it->hasNext()) {
1225 uint64_t addr=it->next();
1226 Constraint *srcenc=getRetValueEncoding(src, addr-offset);
1227 Constraint *addrenc=sls->getAddressEncoding(this, record, (void *) addr);
1228 Constraint *addrmatch=new Constraint(IMPLIES, srcenc, addrenc);
1229 ADDCONSTRAINT(addrmatch,"setaddress");
1235 void ConstGen::processCAS(EPRecord *record) {
1237 LoadRF * lrf=new LoadRF(record, this);
1238 lrf->genConstraints(this);
1240 //Next see if we are successful
1241 Constraint *eq=getNewVar();
1242 ModelVector<EPRecord *> * depveccas=execution->getRevDependences(record, VC_OLDVALCASINDEX);
1243 if (depveccas==NULL) {
1244 //Hard coded old value
1245 IntIterator *iit=record->getSet(VC_OLDVALCASINDEX)->iterator();
1246 uint64_t valcas=iit->next();
1248 Constraint *rmwr=getStoreLoadSet(record)->getRMWRValueEncoding(this, record, valcas);
1250 Constraint *cascond=eq->negate();
1251 ADDCONSTRAINT(cascond, "cascond");
1253 Constraint *cascond=generateEquivConstraint(eq, rmwr);
1254 ADDCONSTRAINT(cascond, "cascond");
1257 ASSERT(depveccas->size()==1);
1258 EPRecord *src=(*depveccas)[0];
1259 IntIterator *it=getStoreLoadSet(record)->getValues()->iterator();
1261 while(it->hasNext()) {
1262 uint64_t valcas=it->next();
1263 Constraint *srcenc=getRetValueEncoding(src, valcas);
1264 Constraint *storeenc=getStoreLoadSet(record)->getRMWRValueEncoding(this, record, valcas);
1266 if (srcenc!=NULL && storeenc!=NULL) {
1267 Constraint *cond=new Constraint(AND,
1268 new Constraint(IMPLIES, srcenc->clone(), eq),
1269 new Constraint(IMPLIES, eq, srcenc));
1270 Constraint *cas=new Constraint(IMPLIES, storeenc, cond);
1271 ADDCONSTRAINT(cas, "cas");
1272 } else if (srcenc==NULL) {
1273 Constraint *casfail=new Constraint(IMPLIES, storeenc, eq->negate());
1274 ADDCONSTRAINT(casfail,"casfail_eq");
1276 //srcenc must be non-null and store-encoding must be null
1281 IntIterator *iit=record->getSet(VC_OLDVALCASINDEX)->iterator();
1282 while(iit->hasNext()) {
1283 uint64_t val=iit->next();
1284 if (!getStoreLoadSet(record)->getValues()->contains(val)) {
1285 Constraint *srcenc=getRetValueEncoding(src, val);
1286 Constraint *casfail=new Constraint(IMPLIES, srcenc, eq->negate());
1287 ADDCONSTRAINT(casfail,"casfailretval");
1293 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1295 IntIterator *iit=record->getSet(VC_BASEINDEX)->iterator();
1296 uint64_t val=iit->next();
1298 Constraint *storeenc=getMemValueEncoding(record, val);
1299 Constraint *casmemsuc=new Constraint(IMPLIES, eq, storeenc);
1300 ADDCONSTRAINT(casmemsuc, "casmemsuc");
1302 ASSERT(depvec->size()==1);
1303 EPRecord *src=(*depvec)[0];
1304 IntIterator *it=record->getStoreSet()->iterator();
1306 while(it->hasNext()) {
1307 uint64_t val=it->next();
1308 Constraint *srcenc=getRetValueEncoding(src, val);
1310 //this can happen for values that are in the store set because
1311 //we re-stored them on a failed CAS
1314 Constraint *storeenc=getMemValueEncoding(record, val);
1315 Constraint *storevalue=new Constraint(IMPLIES, new Constraint(AND, eq, srcenc), storeenc);
1316 ADDCONSTRAINT(storevalue,"casmemsuc");
1320 StoreLoadSet *sls=getStoreLoadSet(record);
1322 Constraint *repeatval=generateEquivConstraint(sls->getNumValVars(), sls->getValVars(this, record), sls->getRMWRValVars(this, record));
1323 Constraint *failcas=new Constraint(IMPLIES, eq->negate(), repeatval);
1324 ADDCONSTRAINT(failcas,"casmemfail");
1326 processAddresses(record);
1329 void ConstGen::processEXC(EPRecord *record) {
1331 LoadRF * lrf=new LoadRF(record, this);
1332 lrf->genConstraints(this);
1335 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1337 IntIterator *iit=record->getSet(VC_BASEINDEX)->iterator();
1338 uint64_t val=iit->next();
1340 Constraint *storeenc=getMemValueEncoding(record, val);
1341 ADDCONSTRAINT(storeenc, "excmemsuc");
1343 ASSERT(depvec->size()==1);
1344 EPRecord *src=(*depvec)[0];
1345 IntIterator *it=record->getStoreSet()->iterator();
1347 while(it->hasNext()) {
1348 uint64_t val=it->next();
1349 Constraint *srcenc=getRetValueEncoding(src, val);
1350 Constraint *storeenc=getMemValueEncoding(record, val);
1351 Constraint *storevalue=new Constraint(IMPLIES, srcenc, storeenc);
1352 ADDCONSTRAINT(storevalue,"excmemsuc");
1357 processAddresses(record);
1360 void ConstGen::processAdd(EPRecord *record) {
1362 LoadRF * lrf=new LoadRF(record, this);
1363 lrf->genConstraints(this);
1365 Constraint *var=getNewVar();
1366 Constraint *newadd=new Constraint(AND, var, getExecutionConstraint(record));
1367 ADDGOAL(record, newadd, "newadd");
1369 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1371 IntIterator *valit=record->getSet(VC_BASEINDEX)->iterator();
1372 uint64_t val=valit->next();
1374 IntHashSet *valset=getStoreLoadSet(record)->getValues();
1375 IntIterator *sis=valset->iterator();
1376 while(sis->hasNext()) {
1377 uint64_t memval=sis->next();
1378 uint64_t sumval=(memval+val)&getmask(record->getLen());
1380 if (valset->contains(sumval)) {
1382 Constraint *loadenc=getStoreLoadSet(record)->getRMWRValueEncoding(this, record, memval);
1383 Constraint *storeenc=getMemValueEncoding(record, sumval);
1384 Constraint *notvar=var->negate();
1385 Constraint *addinputfix=new Constraint(IMPLIES, loadenc, new Constraint(AND, storeenc, notvar));
1386 ADDCONSTRAINT(addinputfix, "addinputfix");
1392 ASSERT(depvec->size()==1);
1393 EPRecord *src=(*depvec)[0];
1394 IntIterator *it=record->getStoreSet()->iterator();
1395 IntHashSet *valset=getStoreLoadSet(record)->getValues();
1397 while(it->hasNext()) {
1398 uint64_t val=it->next();
1399 IntIterator *sis=valset->iterator();
1400 while(sis->hasNext()) {
1401 uint64_t memval=sis->next();
1402 uint64_t sum=(memval+val)&getmask(record->getLen());
1403 if (valset->contains(sum)) {
1404 Constraint *srcenc=getRetValueEncoding(src, val);
1405 Constraint *loadenc=getStoreLoadSet(record)->getRMWRValueEncoding(this, record, memval);
1406 Constraint *storeenc=getMemValueEncoding(record, sum);
1407 Constraint *notvar=var->negate();
1408 Constraint *addop=new Constraint(IMPLIES, new Constraint(AND, srcenc, loadenc),
1409 new Constraint(AND, notvar, storeenc));
1410 ADDCONSTRAINT(addop,"addinputvar");
1418 processAddresses(record);
1421 /** This function ensures that the value of a store's SAT variables
1422 matches the store's input value.
1424 TODO: Could optimize the case where the encodings are the same...
1427 void ConstGen::processStore(EPRecord *record) {
1428 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, VC_BASEINDEX);
1430 //We have a hard coded value
1431 uint64_t val=record->getValue(0)->getValue();
1432 Constraint *storeenc=getMemValueEncoding(record, val);
1433 ADDCONSTRAINT(storeenc,"storefix");
1435 //We have a value from an input
1436 ASSERT(depvec->size()==1);
1437 EPRecord *src=(*depvec)[0];
1438 IntIterator *it=record->getStoreSet()->iterator();
1440 while(it->hasNext()) {
1441 uint64_t val=it->next();
1442 Constraint *srcenc=getRetValueEncoding(src, val);
1443 Constraint *storeenc=getMemValueEncoding(record, val);
1444 Constraint *storevalue=new Constraint(IMPLIES, srcenc, storeenc);
1445 ADDCONSTRAINT(storevalue,"storevar");
1449 processAddresses(record);
1452 /** Handle yields by just forbidding them via the SAT formula. */
1454 void ConstGen::processYield(EPRecord *record) {
1455 if (model->params.noyields &&
1456 record->getBranch()!=NULL) {
1457 Constraint * noyield=getExecutionConstraint(record)->negate();
1458 ADDCONSTRAINT(noyield, "noyield");
1462 void ConstGen::processLoopPhi(EPRecord *record) {
1463 EPRecordIDSet *phiset=record->getPhiLoopTable();
1464 EPRecordIDIterator *rit=phiset->iterator();
1466 while(rit->hasNext()) {
1467 struct RecordIDPair *rip=rit->next();
1468 EPRecord *input=rip->idrecord;
1470 IntIterator * it=record->getSet(VC_BASEINDEX)->iterator();
1471 while(it->hasNext()) {
1472 uint64_t value=it->next();
1473 Constraint * inputencoding=getRetValueEncoding(input, value);
1474 if (inputencoding==NULL)
1476 Constraint * branchconstraint=getExecutionConstraint(rip->record);
1477 Constraint * outputencoding=getRetValueEncoding(record, value);
1478 Constraint * phiimplication=new Constraint(IMPLIES, new Constraint(AND, inputencoding, branchconstraint), outputencoding);
1479 ADDCONSTRAINT(phiimplication,"philoop");
1486 void ConstGen::processPhi(EPRecord *record) {
1487 ModelVector<EPRecord *> * inputs=execution->getRevDependences(record, VC_BASEINDEX);
1488 for(uint i=0;i<inputs->size();i++) {
1489 EPRecord * input=(*inputs)[i];
1491 IntIterator * it=record->getSet(VC_BASEINDEX)->iterator();
1492 while(it->hasNext()) {
1493 uint64_t value=it->next();
1494 Constraint * inputencoding=getRetValueEncoding(input, value);
1495 if (inputencoding==NULL)
1497 Constraint * branchconstraint=getExecutionConstraint(input);
1498 Constraint * outputencoding=getRetValueEncoding(record, value);
1499 Constraint * phiimplication=new Constraint(IMPLIES, new Constraint(AND, inputencoding, branchconstraint), outputencoding);
1500 ADDCONSTRAINT(phiimplication,"phi");
1506 void ConstGen::processFunction(EPRecord *record) {
1507 if (record->getLoopPhi()) {
1508 processLoopPhi(record);
1510 } else if (record->getPhi()) {
1515 CGoalSet *knownbehaviors=record->completedGoalSet();
1516 CGoalIterator *cit=knownbehaviors->iterator();
1517 uint numinputs=record->getNumFuncInputs();
1518 EPRecord * inputs[numinputs];
1519 for(uint i=0;i<numinputs;i++) {
1520 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, i+VC_BASEINDEX);
1521 ASSERT(depvec->size()==1);
1522 inputs[i]=(*depvec)[0];
1524 while(cit->hasNext()) {
1525 CGoal *goal=cit->next();
1526 Constraint *carray[numinputs];
1527 if (record->isSharedGoals()) {
1528 bool badvalue=false;
1529 for(uint i=0;i<numinputs;i++) {
1530 uint64_t inputval=goal->getValue(i+VC_BASEINDEX);
1531 if (!record->getSet(i+VC_BASEINDEX)->contains(inputval)) {
1540 /* Build up constraints for each input */
1541 for(uint i=0;i<numinputs;i++) {
1542 uint64_t inputval=goal->getValue(i+VC_BASEINDEX);
1543 Constraint * inputc=getRetValueEncoding(inputs[i], inputval);
1544 ASSERT(inputc!=NULL);
1547 Constraint * outputconstraint=getRetValueEncoding(record, goal->getOutput());
1549 ADDCONSTRAINT(outputconstraint,"functionimpl");
1551 Constraint * functionimplication=new Constraint(IMPLIES, new Constraint(AND, numinputs, carray), outputconstraint);
1552 ADDCONSTRAINT(functionimplication,"functionimpl");
1557 FunctionRecord *fr=functiontable->get(record);
1558 Constraint *goal=fr->getNoValueEncoding();
1559 Constraint *newfunc=new Constraint(AND, goal, getExecutionConstraint(record));
1560 ADDGOAL(record, newfunc, "newfunc");
1563 void ConstGen::processEquals(EPRecord *record) {
1564 ASSERT (record->getNumFuncInputs() == 2);
1565 EPRecord * inputs[2];
1567 for(uint i=0;i<2;i++) {
1568 ModelVector<EPRecord *> * depvec=execution->getRevDependences(record, i+VC_BASEINDEX);
1571 } else if (depvec->size()==1) {
1572 inputs[i]=(*depvec)[0];
1573 } else ASSERT(false);
1576 //rely on this being a variable
1577 Constraint * outputtrue=getRetValueEncoding(record, 1);
1578 ASSERT(outputtrue->getType()==VAR);
1580 if (inputs[0]!=NULL && inputs[1]!=NULL &&
1581 (inputs[0]->getType()==LOAD || inputs[0]->getType()==RMW) &&
1582 (inputs[1]->getType()==LOAD || inputs[1]->getType()==RMW) &&
1583 (getStoreLoadSet(inputs[0])==getStoreLoadSet(inputs[1]))) {
1584 StoreLoadSet * sls=getStoreLoadSet(inputs[0]);
1585 int numvalvars=sls->getNumValVars();
1586 Constraint **valvar1=(inputs[0]->getType()==RMW)?sls->getRMWRValVars(this, inputs[0]):sls->getValVars(this, inputs[0]);
1587 Constraint **valvar2=(inputs[1]->getType()==RMW)?sls->getRMWRValVars(this, inputs[1]):sls->getValVars(this, inputs[1]);
1590 Constraint *vars[numvalvars];
1591 for(int i=0;i<numvalvars;i++) {
1592 vars[i]=getNewVar();
1593 Constraint *var1=valvar1[i];
1594 Constraint *var2=valvar2[i];
1595 Constraint * array[]={var1, var2->negate(), vars[i]->negate()};
1596 Constraint * array2[]={var2, var1->negate(), vars[i]->negate()};
1597 Constraint * a=new Constraint(OR, 3, array);
1598 ADDCONSTRAINT(a, "equala");
1599 Constraint * a2=new Constraint(OR, 3, array2);
1600 ADDCONSTRAINT(a2, "equala2");
1601 Constraint * arrayb[]={var1, var2, vars[i]};
1602 Constraint * array2b[]={var2->negate(), var1->negate(), vars[i]};
1603 Constraint * b=new Constraint(OR, 3, arrayb);
1604 ADDCONSTRAINT(b, "equalb");
1605 Constraint *b2=new Constraint(OR, 3, array2b);
1606 ADDCONSTRAINT(b2, "equalb2");
1608 ADDCONSTRAINT(new Constraint(IMPLIES, new Constraint(AND, numvalvars, vars), outputtrue),"impequal1");
1610 ADDCONSTRAINT(new Constraint(IMPLIES, outputtrue, new Constraint(AND, numvalvars, vars)), "impequal2");
1614 Constraint * functionimplication=new Constraint(IMPLIES,generateEquivConstraint(numvalvars, valvar1, valvar2), outputtrue);
1615 ADDCONSTRAINT(functionimplication,"equalsimplspecial");
1616 Constraint * functionimplicationneg=new Constraint(IMPLIES,outputtrue, generateEquivConstraint(numvalvars, valvar1, valvar2));
1617 ADDCONSTRAINT(functionimplicationneg,"equalsimplspecialneg");
1622 if (inputs[0]==NULL && inputs[1]==NULL) {
1623 IntIterator *iit0=record->getSet(VC_BASEINDEX+0)->iterator();
1624 uint64_t constval=iit0->next();
1626 IntIterator *iit1=record->getSet(VC_BASEINDEX+1)->iterator();
1627 uint64_t constval2=iit1->next();
1630 if (constval==constval2) {
1631 ADDCONSTRAINT(outputtrue, "equalsconst");
1633 ADDCONSTRAINT(outputtrue->negate(), "equalsconst");
1638 if (inputs[0]==NULL ||
1640 int nullindex=inputs[0]==NULL?0:1;
1641 IntIterator *iit=record->getSet(VC_BASEINDEX+nullindex)->iterator();
1642 uint64_t constval=iit->next();
1645 record->getSet(VC_BASEINDEX+nullindex);
1646 EPRecord *r=inputs[1-nullindex];
1647 Constraint *l=getRetValueEncoding(r, constval);
1648 Constraint *functionimplication=new Constraint(IMPLIES, l, outputtrue);
1649 ADDCONSTRAINT(functionimplication,"equalsimpl");
1651 Constraint *l2=getRetValueEncoding(r, constval);
1652 Constraint *functionimplication2=new Constraint(IMPLIES, outputtrue, l2);
1653 ADDCONSTRAINT(functionimplication2,"equalsimpl");
1656 IntIterator *iit=record->getSet(VC_BASEINDEX)->iterator();
1657 while(iit->hasNext()) {
1658 uint64_t val1=iit->next();
1660 IntIterator *iit2=record->getSet(VC_BASEINDEX+1)->iterator();
1661 while(iit2->hasNext()) {
1662 uint64_t val2=iit2->next();
1663 Constraint *l=getRetValueEncoding(inputs[0], val1);
1664 Constraint *r=getRetValueEncoding(inputs[1], val2);
1665 Constraint *imp=(val1==val2)?outputtrue:outputtrue->negate();
1666 Constraint * functionimplication=new Constraint(IMPLIES, new Constraint(AND, l, r), imp);
1667 ADDCONSTRAINT(functionimplication,"equalsimpl");
1675 void ConstGen::processFence(EPRecord *record) {
1676 //do we already account for the fence?
1677 if (isAlwaysExecuted(record))
1679 ExecPoint * record_ep=record->getEP();
1680 thread_id_t tid=record_ep->get_tid();
1681 uint thread=id_to_int(tid);
1682 ModelVector<EPRecord *> *tvec=(*threadactions)[thread];
1683 uint size=tvec->size();
1685 EPRecord *prevstore=NULL;
1687 for(i=0;i<size;i++) {
1688 EPRecord *rec=(*tvec)[i];
1689 if (rec->getType()==STORE) {
1692 if (rec == record) {
1697 if (prevstore == NULL) {
1701 EPRecord *rec=(*tvec)[i];
1702 if (rec->getType()==LOAD) {
1703 Constraint * condition=getExecutionConstraint(record);
1704 Constraint * storeload=getOrderConstraint(prevstore, rec);
1705 Constraint * c=new Constraint(IMPLIES, condition, storeload);
1706 ADDCONSTRAINT(c, "fence");
1713 void ConstGen::processRecord(EPRecord *record) {
1714 switch (record->getType()) {
1716 processFunction(record);
1719 processEquals(record);
1722 processLoad(record);
1725 processStore(record);
1729 processFence(record);
1734 processFence(record);
1736 if (record->getOp()==ADD) {
1738 } else if (record->getOp()==CAS) {
1740 } else if (record->getOp()==EXC) {
1746 processYield(record);
1749 processBranch(record);
1756 void ConstGen::visitRecord(EPRecord *record) {
1757 switch (record->getType()) {
1759 recordExecCond(record);
1760 insertEquals(record);
1763 recordExecCond(record);
1764 insertFunction(record);
1768 recordExecCond(record);
1769 insertAction(record);
1773 recordExecCond(record);
1774 insertAction(record);
1775 groupMemoryOperations(record);
1778 recordExecCond(record);
1779 insertAction(record);
1780 groupMemoryOperations(record);
1783 recordExecCond(record);
1784 insertAction(record);
1785 groupMemoryOperations(record);
1788 recordExecCond(record);
1789 insertBranch(record);
1792 recordExecCond(record);
1793 insertNonLocal(record);
1796 insertLabel(record);
1799 recordExecCond(record);
1806 void ConstGen::recordExecCond(EPRecord *record) {
1807 ExecPoint *eprecord=record->getEP();
1808 EPValue * branchval=record->getBranch();
1809 EPRecord * branch=(branchval==NULL)?NULL:branchval->getRecord();
1810 ExecPoint *epbranch= (branch==NULL) ? NULL : branch->getEP();
1811 RecordSet *srs=NULL;
1812 RecordIterator *sri=nonlocaltrans->iterator();
1813 while(sri->hasNext()) {
1814 EPRecord *nonlocal=sri->next();
1815 ExecPoint *epnl=nonlocal->getEP();
1816 if (epbranch!=NULL) {
1817 if (epbranch->compare(epnl)==CR_BEFORE) {
1818 //branch occurs after non local and thus will subsume condition
1819 //branch subsumes this condition
1823 if (eprecord->compare(epnl)==CR_BEFORE) {
1824 //record occurs after non-local, so add it to set
1826 srs=new RecordSet();
1832 execcondtable->put(record, srs);
1835 void ConstGen::insertNonLocal(EPRecord *record) {
1836 nonlocaltrans->add(record);
1839 void ConstGen::insertLabel(EPRecord *record) {
1840 RecordIterator *sri=nonlocaltrans->iterator();
1841 while(sri->hasNext()) {
1842 EPRecord *nonlocal=sri->next();
1843 if (nonlocal->getNextRecord()==record)
1850 void ConstGen::traverseRecord(EPRecord *record, bool initial) {
1853 visitRecord(record);
1855 processRecord(record);
1857 if (record->getType()==LOOPENTER) {
1858 workstack->push_back(record->getNextRecord());
1859 workstack->push_back(record->getChildRecord());
1862 if (record->getChildRecord()!=NULL) {
1863 workstack->push_back(record->getChildRecord());
1865 if (record->getType()==NONLOCALTRANS) {
1868 if (record->getType()==BRANCHDIR) {
1869 EPRecord *next=record->getNextRecord();
1871 workstack->push_back(next);
1872 for(uint i=0;i<record->numValues();i++) {
1873 EPValue *branchdir=record->getValue(i);
1875 //Could have an empty branch, so make sure the branch actually
1877 if (branchdir->getFirstRecord()!=NULL)
1878 workstack->push_back(branchdir->getFirstRecord());
1882 record=record->getNextRecord();
1883 } while(record!=NULL);
1886 unsigned int RecPairHash(RecPair *rp) {
1887 uintptr_t v=(uintptr_t) rp->epr1;
1888 uintptr_t v2=(uintptr_t) rp->epr2;
1891 return (uint)((x>>4)^(a));
1894 bool RecPairEquals(RecPair *r1, RecPair *r2) {
1895 return ((r1->epr1==r2->epr1)&&(r1->epr2==r2->epr2)) ||
1896 ((r1->epr1==r2->epr2)&&(r1->epr2==r2->epr1));