From: Brian Demsky <bdemsky@uci.edu>
Date: Thu, 4 Oct 2012 08:21:11 +0000 (-0700)
Subject: local commit... bug that prunes too many executions
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=c832cb55af09e735821ae3463bc37c29d3fa27c8;p=cdsspec-compiler.git
local commit... bug that prunes too many executions
---
diff --git a/Makefile b/Makefile
index 3a3d826..d530fee 100644
--- a/Makefile
+++ b/Makefile
@@ -3,7 +3,7 @@ include common.mk
OBJECTS = libthreads.o schedule.o model.o threads.o librace.o action.o \
nodestack.o clockvector.o main.o snapshot-interface.o cyclegraph.o \
datarace.o impatomic.o cmodelint.o \
- snapshot.o malloc.o mymemory.o common.o mutex.o
+ snapshot.o malloc.o mymemory.o common.o mutex.o promise.o
CPPFLAGS += -Iinclude -I. -rdynamic
LDFLAGS = -ldl -lrt
diff --git a/action.cc b/action.cc
index 20777f9..c6504cd 100644
--- a/action.cc
+++ b/action.cc
@@ -281,7 +281,7 @@ bool ModelAction::read_from(const ModelAction *act)
bool ModelAction::synchronize_with(const ModelAction *act) {
if (*this < *act && type != THREAD_JOIN && type != ATOMIC_LOCK)
return false;
- model->check_promises(cv, act->cv);
+ model->check_promises(act->get_tid(), cv, act->cv);
cv->merge(act->cv);
return true;
}
diff --git a/cyclegraph.cc b/cyclegraph.cc
index f4d3b93..2280e76 100644
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -1,6 +1,8 @@
#include "cyclegraph.h"
#include "action.h"
#include "common.h"
+#include "promise.h"
+#include "model.h"
/** Initializes a CycleGraph object. */
CycleGraph::CycleGraph() :
@@ -195,6 +197,33 @@ bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) {
return false;
}
+bool CycleGraph::checkPromise(const ModelAction *fromact, Promise *promise) {
+ std::vector<CycleNode *, ModelAlloc<CycleNode *> > queue;
+ HashTable<CycleNode *, CycleNode *, uintptr_t, 4, model_malloc, model_calloc, model_free> discovered(64);
+ CycleNode *from = actionToNode.get(fromact);
+
+
+ queue.push_back(from);
+ discovered.put(from, from);
+ while(!queue.empty()) {
+ CycleNode * node=queue.back();
+ queue.pop_back();
+
+ if (promise->increment_threads(node->getAction()->get_tid())) {
+ return true;
+ }
+
+ for(unsigned int i=0;i<node->getEdges()->size();i++) {
+ CycleNode *next=(*node->getEdges())[i];
+ if (!discovered.contains(next)) {
+ discovered.put(next,next);
+ queue.push_back(next);
+ }
+ }
+ }
+ return false;
+}
+
void CycleGraph::startChanges() {
ASSERT(rollbackvector.size()==0);
ASSERT(rmwrollbackvector.size()==0);
diff --git a/cyclegraph.h b/cyclegraph.h
index 42866a3..1cc0d06 100644
--- a/cyclegraph.h
+++ b/cyclegraph.h
@@ -11,6 +11,7 @@
#include "config.h"
#include "mymemory.h"
+class Promise;
class CycleNode;
class ModelAction;
@@ -23,7 +24,7 @@ class CycleGraph {
bool checkForCycles();
bool checkForRMWViolation();
void addRMWEdge(const ModelAction *from, const ModelAction *rmw);
-
+ bool checkPromise(const ModelAction *from, Promise *p);
bool checkReachable(const ModelAction *from, const ModelAction *to);
void startChanges();
void commitChanges();
diff --git a/model.cc b/model.cc
index e3d9203..824e1e4 100644
--- a/model.cc
+++ b/model.cc
@@ -52,7 +52,7 @@ ModelChecker::ModelChecker(struct model_params params) :
/** @brief Destructor */
ModelChecker::~ModelChecker()
{
- for (int i = 0; i < get_num_threads(); i++)
+ for (unsigned int i = 0; i < get_num_threads(); i++)
delete thread_map->get(i);
delete thread_map;
@@ -95,7 +95,7 @@ thread_id_t ModelChecker::get_next_id()
}
/** @return the number of user threads created during this execution */
-int ModelChecker::get_num_threads()
+unsigned int ModelChecker::get_num_threads()
{
return priv->next_thread_id;
}
@@ -377,6 +377,8 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
curr->read_from(reads_from);
mo_graph->commitChanges();
+ mo_check_promises(curr->get_tid(), reads_from);
+
updated |= r_status;
} else if (!second_part_of_rmw) {
/* Read from future value */
@@ -474,6 +476,8 @@ bool ModelChecker::process_write(ModelAction *curr)
}
mo_graph->commitChanges();
+ mo_check_promises(curr->get_tid(), curr);
+
get_thread(curr)->set_return_value(VALUE_NONE);
return updated_mod_order || updated_promises;
}
@@ -526,7 +530,7 @@ bool ModelChecker::process_thread_action(ModelAction *curr)
break;
}
case THREAD_START: {
- check_promises(NULL, curr->get_cv());
+ check_promises(curr->get_tid(), NULL, curr->get_cv());
break;
}
default:
@@ -1503,6 +1507,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
post_r_modification_order(read, write);
//Make sure the promise's value matches the write's value
ASSERT(promise->get_value() == write->get_value());
+ mo_check_promises(read->get_tid(), write);
delete(promise);
promises->erase(promises->begin() + promise_index);
@@ -1535,16 +1540,14 @@ void ModelChecker::compute_promises(ModelAction *curr)
}
/** Checks promises in response to change in ClockVector Threads. */
-void ModelChecker::check_promises(ClockVector *old_cv, ClockVector *merge_cv)
+void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv)
{
for (unsigned int i = 0; i < promises->size(); i++) {
Promise *promise = (*promises)[i];
const ModelAction *act = promise->get_action();
if ((old_cv == NULL || !old_cv->synchronized_since(act)) &&
merge_cv->synchronized_since(act)) {
- //This thread is no longer able to send values back to satisfy the promise
- int num_synchronized_threads = promise->increment_threads();
- if (num_synchronized_threads == get_num_threads()) {
+ if (promise->increment_threads(tid)) {
//Promise has failed
failed_promise = true;
return;
@@ -1553,6 +1556,40 @@ void ModelChecker::check_promises(ClockVector *old_cv, ClockVector *merge_cv)
}
}
+/** Checks promises in response to change in ClockVector Threads. */
+void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) {
+ void * location = write->get_location();
+ for (unsigned int i = 0; i < promises->size(); i++) {
+ Promise *promise = (*promises)[i];
+ const ModelAction *act = promise->get_action();
+
+ //Is this promise on the same location?
+ if ( act->get_location() != location )
+ continue;
+
+ if ( act->get_tid()==tid) {
+ if (promise->get_write() == NULL ) {
+ promise->set_write(write);
+ }
+ if (mo_graph->checkPromise(write, promise)) {
+ failed_promise = true;
+ return;
+ }
+ }
+
+ //Don't do any lookups twice for the same thread
+ if (promise->has_sync_thread(tid))
+ continue;
+
+ if (mo_graph->checkReachable(promise->get_write(), write)) {
+ if (promise->increment_threads(tid)) {
+ failed_promise = true;
+ return;
+ }
+ }
+ }
+}
+
/**
* Build up an initial set of all past writes that this 'read' action may read
* from. This set is determined by the clock vector's "happens before"
diff --git a/model.h b/model.h
index d8dce07..dfc8e36 100644
--- a/model.h
+++ b/model.h
@@ -49,7 +49,7 @@ struct PendingFutureValue {
*/
struct model_snapshot_members {
ModelAction *current_action;
- int next_thread_id;
+ unsigned int next_thread_id;
modelclock_t used_sequence_numbers;
Thread *nextThread;
ModelAction *next_backtrack;
@@ -76,7 +76,7 @@ public:
Thread * get_thread(ModelAction *act) const;
thread_id_t get_next_id();
- int get_num_threads();
+ unsigned int get_num_threads();
Thread * get_current_thread();
int switch_to_master(ModelAction *act);
@@ -86,7 +86,8 @@ public:
bool isfeasible();
bool isfeasibleotherthanRMW();
bool isfinalfeasible();
- void check_promises(ClockVector *old_cv, ClockVector * merge_cv);
+ void mo_check_promises(thread_id_t tid, const ModelAction *write);
+ void check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector * merge_cv);
void get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads);
void finish_execution();
bool isfeasibleprefix();
@@ -97,6 +98,7 @@ public:
void set_bad_synchronization() { bad_synchronization = true; }
const model_params params;
+ Scheduler * get_scheduler() { return scheduler;}
MEMALLOC
private:
diff --git a/promise.cc b/promise.cc
new file mode 100644
index 0000000..259ba05
--- /dev/null
+++ b/promise.cc
@@ -0,0 +1,21 @@
+#include "promise.h"
+#include "model.h"
+#include "schedule.h"
+
+bool Promise::increment_threads(thread_id_t tid) {
+ unsigned int id=id_to_int(tid);
+ if (id>=synced_thread.size()) {
+ synced_thread.resize(id+1, false);
+ }
+ if (synced_thread[id])
+ return false;
+
+ synced_thread[id]=true;
+ bool * enabled=model->get_scheduler()->get_enabled();
+
+ for(unsigned int i=0;i<model->get_num_threads();i++) {
+ if (!synced_thread[id] && enabled[id])
+ return false;
+ }
+ return true;
+}
diff --git a/promise.h b/promise.h
index 11719fc..2ce3e29 100644
--- a/promise.h
+++ b/promise.h
@@ -8,25 +8,40 @@
#define __PROMISE_H__
#include <inttypes.h>
+#include "threads.h"
-class ModelAction;
+#include "model.h"
class Promise {
public:
Promise(ModelAction *act, uint64_t value, modelclock_t expiration) :
- value(value), expiration(expiration), read(act), numthreads(1)
- { }
+ value(value), expiration(expiration), read(act), write(NULL)
+ {
+ increment_threads(act->get_tid());
+ }
modelclock_t get_expiration() const {return expiration;}
ModelAction * get_action() const { return read; }
- int increment_threads() { return ++numthreads; }
+ bool increment_threads(thread_id_t tid);
+
+ bool has_sync_thread(thread_id_t tid) {
+ unsigned int id=id_to_int(tid);
+ if (id>=synced_thread.size()) {
+ return false;
+ }
+ return synced_thread[id];
+ }
+
uint64_t get_value() const { return value; }
+ void set_write(const ModelAction *act) { write = act; }
+ const ModelAction * get_write() { return write; }
SNAPSHOTALLOC
private:
+ std::vector<bool> synced_thread;
const uint64_t value;
const modelclock_t expiration;
ModelAction * const read;
- unsigned int numthreads;
+ const ModelAction * write;
};
#endif
diff --git a/threads.h b/threads.h
index b69f426..a379494 100644
--- a/threads.h
+++ b/threads.h
@@ -81,6 +81,14 @@ public:
*/
void push_wait_list(ModelAction *act) { wait_list.push_back(act); }
+ unsigned int num_wait_list() {
+ return wait_list.size();
+ }
+
+ ModelAction * get_waiter(unsigned int i) {
+ return wait_list[i];
+ }
+
ModelAction * get_pending() { return pending; }
void set_pending(ModelAction *act) { pending = act; }
/**