+//This procedure uses cohere to prune future values that are
+//guaranteed to generate a coherence violation.
+//
+//need to see if there is (1) a promise for thread write, (2)
+//the promise is sb before write, (3) the promise can only be
+//resolved by the thread read, and (4) the promise has same
+//location as read/write
+
+bool ModelExecution::check_coherence_promise(const ModelAction * write, const ModelAction *read) {
+ thread_id_t write_tid=write->get_tid();
+ for(unsigned int i = promises.size(); i>0; i--) {
+ Promise *pr=promises[i-1];
+ if (!pr->same_location(write))
+ continue;
+ //the reading thread is the only thread that can resolve the promise
+ if (pr->get_num_was_available_threads()==1 && pr->thread_was_available(read->get_tid())) {
+ for(unsigned int j=0;j<pr->get_num_readers();j++) {
+ ModelAction *prreader=pr->get_reader(j);
+ //the writing thread reads from the promise before the write
+ if (prreader->get_tid()==write_tid &&
+ (*prreader)<(*write)) {
+ if ((*read)>(*prreader)) {
+ //check that we don't have a read between the read and promise
+ //from the same thread as read
+ bool okay=false;
+ for(const ModelAction *tmp=read;tmp!=prreader;) {
+ tmp=tmp->get_node()->get_parent()->get_action();
+ if (tmp->is_read() && tmp->same_thread(read)) {
+ okay=true;
+ break;
+ }
+ }
+ if (okay)
+ continue;
+ }
+ return false;
+ }
+ }
+ }
+ }
+ return true;
+}
+
+