From: bdemsky Date: Sat, 1 Jun 2019 06:19:23 +0000 (-0700) Subject: Remove promises X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=51d58655a9a674d5e4b04f2dfcb5204a4342ef6d;p=c11tester.git Remove promises --- diff --git a/Makefile b/Makefile index 94109b4f..313445da 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 promise.o conditionvariable.o \ + snapshot.o malloc.o mymemory.o common.o mutex.o conditionvariable.o \ context.o execution.o libannotate.o pthread.o futex.o CPPFLAGS += -Iinclude -I. diff --git a/action.cc b/action.cc index 14160052..8395c885 100644 --- a/action.cc +++ b/action.cc @@ -39,7 +39,6 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, location(loc), value(value), reads_from(NULL), - reads_from_promise(NULL), last_fence_release(NULL), node(NULL), seq_number(ACTION_INITIAL_CLOCK), @@ -430,8 +429,6 @@ uint64_t ModelAction::get_reads_from_value() const ASSERT(is_read()); if (reads_from) return reads_from->get_write_value(); - else if (reads_from_promise) - return reads_from_promise->get_value(); return VALUE_NONE; /* Only for new actions with no reads-from */ } @@ -489,7 +486,6 @@ void ModelAction::set_read_from(const ModelAction *act) ASSERT(act); reads_from = act; - reads_from_promise = NULL; if (act->is_uninitialized()) { // WL uint64_t val = *((uint64_t *) location); @@ -506,17 +502,6 @@ void ModelAction::set_read_from(const ModelAction *act) } } -/** - * Set this action's read-from promise - * @param promise The promise to read from - */ -void ModelAction::set_read_from_promise(Promise *promise) -{ - ASSERT(is_read()); - reads_from_promise = promise; - reads_from = NULL; -} - /** * Synchronize the current thread with the thread corresponding to the * ModelAction parameter. @@ -601,13 +586,7 @@ void ModelAction::print() const if (is_read()) { if (reads_from) model_print(" %-3d", reads_from->get_seq_number()); - else if (reads_from_promise) { - int idx = reads_from_promise->get_index(); - if (idx >= 0) - model_print(" P%-2d", idx); - else - model_print(" P? "); - } else + else model_print(" ? "); } if (cv) { @@ -631,8 +610,6 @@ unsigned int ModelAction::hash() const if (is_read()) { if (reads_from) hash ^= reads_from->get_seq_number(); - else if (reads_from_promise) - hash ^= reads_from_promise->get_index(); hash ^= get_reads_from_value(); } return hash; @@ -651,19 +628,6 @@ bool ModelAction::may_read_from(const ModelAction *write) const return false; } -/** - * @brief Checks the NodeStack to see if a Promise is in our may-read-from set - * @param promise The Promise to check for - * @return True if the Promise is found; false otherwise - */ -bool ModelAction::may_read_from(const Promise *promise) const -{ - for (int i = 0; i < node->get_read_from_promise_size(); i++) - if (node->get_read_from_promise(i) == promise) - return true; - return false; -} - /** * Only valid for LOCK, TRY_LOCK, UNLOCK, and WAIT operations. * @return The mutex operated on by this action, if any; otherwise NULL diff --git a/action.h b/action.h index b0b3d51a..06d76c25 100644 --- a/action.h +++ b/action.h @@ -16,7 +16,6 @@ /* Forward declarations */ class ClockVector; class Thread; -class Promise; namespace cdsc { class mutex; @@ -111,14 +110,12 @@ public: uint64_t get_write_value() const; uint64_t get_return_value() const; const ModelAction * get_reads_from() const { return reads_from; } - Promise * get_reads_from_promise() const { return reads_from_promise; } cdsc::mutex * get_mutex() const; Node * get_node() const; void set_node(Node *n) { node = n; } void set_read_from(const ModelAction *act); - void set_read_from_promise(Promise *promise); /** Store the most recent fence-release from the same thread * @param fence The fence-release that occured prior to this */ @@ -186,10 +183,8 @@ public: unsigned int hash() const; bool equals(const ModelAction *x) const { return this == x; } - bool equals(const Promise *x) const { return false; } bool may_read_from(const ModelAction *write) const; - bool may_read_from(const Promise *promise) const; MEMALLOC void set_value(uint64_t val) { value = val; } @@ -227,13 +222,6 @@ private: */ const ModelAction *reads_from; - /** - * @brief The promise that this action reads from - * - * Only valid for reads - */ - Promise *reads_from_promise; - /** @brief The last fence release from the same thread */ const ModelAction *last_fence_release; diff --git a/cyclegraph.cc b/cyclegraph.cc index def51f96..439e6196 100644 --- a/cyclegraph.cc +++ b/cyclegraph.cc @@ -1,7 +1,6 @@ #include "cyclegraph.h" #include "action.h" #include "common.h" -#include "promise.h" #include "threads-model.h" /** Initializes a CycleGraph object. */ @@ -33,49 +32,12 @@ void CycleGraph::putNode(const ModelAction *act, CycleNode *node) #endif } -/** - * Add a CycleNode to the graph, corresponding to a Promise - * @param promise The Promise that should be added - * @param node The CycleNode that corresponds to the Promise - */ -void CycleGraph::putNode(const Promise *promise, CycleNode *node) -{ - promiseToNode.put(promise, node); -#if SUPPORT_MOD_ORDER_DUMP - nodeList.push_back(node); -#endif -} - -/** - * @brief Remove the Promise node from the graph - * @param promise The promise to remove from the graph - */ -void CycleGraph::erasePromiseNode(const Promise *promise) -{ - promiseToNode.put(promise, NULL); -#if SUPPORT_MOD_ORDER_DUMP - /* Remove the promise node from nodeList */ - CycleNode *node = getNode_noCreate(promise); - for (unsigned int i = 0; i < nodeList.size(); ) - if (nodeList[i] == node) - nodeList.erase(nodeList.begin() + i); - else - i++; -#endif -} - /** @return The corresponding CycleNode, if exists; otherwise NULL */ CycleNode * CycleGraph::getNode_noCreate(const ModelAction *act) const { return actionToNode.get(act); } -/** @return The corresponding CycleNode, if exists; otherwise NULL */ -CycleNode * CycleGraph::getNode_noCreate(const Promise *promise) const -{ - return promiseToNode.get(promise); -} - /** * @brief Returns the CycleNode corresponding to a given ModelAction * @@ -94,101 +56,6 @@ CycleNode * CycleGraph::getNode(const ModelAction *action) return node; } -/** - * @brief Returns a CycleNode corresponding to a promise - * - * Gets (or creates, if none exist) a CycleNode corresponding to a promised - * value. - * - * @param promise The Promise generated by a reader - * @return The CycleNode corresponding to the Promise - */ -CycleNode * CycleGraph::getNode(const Promise *promise) -{ - CycleNode *node = getNode_noCreate(promise); - if (node == NULL) { - node = new CycleNode(promise); - putNode(promise, node); - } - return node; -} - -/** - * Resolve/satisfy a Promise with a particular store ModelAction, taking care - * of the CycleGraph cleanups, including merging any necessary CycleNodes. - * - * @param promise The Promise to resolve - * @param writer The store that will resolve this Promise - * @return false if the resolution results in a cycle (or fails in some other - * way); true otherwise - */ -bool CycleGraph::resolvePromise(const Promise *promise, ModelAction *writer) -{ - CycleNode *promise_node = promiseToNode.get(promise); - CycleNode *w_node = actionToNode.get(writer); - ASSERT(promise_node); - - if (w_node) - return mergeNodes(w_node, promise_node); - /* No existing write-node; just convert the promise-node */ - promise_node->resolvePromise(writer); - erasePromiseNode(promise_node->getPromise()); - putNode(writer, promise_node); - return true; -} - -/** - * @brief Merge two CycleNodes that represent the same write - * - * Note that this operation cannot be rolled back. - * - * @param w_node The write ModelAction node with which to merge - * @param p_node The Promise node to merge. Will be destroyed after this - * function. - * - * @return false if the merge cannot succeed; true otherwise - */ -bool CycleGraph::mergeNodes(CycleNode *w_node, CycleNode *p_node) -{ - ASSERT(!w_node->is_promise()); - ASSERT(p_node->is_promise()); - - const Promise *promise = p_node->getPromise(); - if (!promise->is_compatible(w_node->getAction()) || - !promise->same_value(w_node->getAction())) - return false; - - /* Transfer the RMW */ - CycleNode *promise_rmw = p_node->getRMW(); - if (promise_rmw && promise_rmw != w_node->getRMW() && w_node->setRMW(promise_rmw)) - return false; - - /* Transfer back edges to w_node */ - while (p_node->getNumBackEdges() > 0) { - CycleNode *back = p_node->removeBackEdge(); - if (back == w_node) - continue; - addNodeEdge(back, w_node); - if (hasCycles) - return false; - } - - /* Transfer forward edges to w_node */ - while (p_node->getNumEdges() > 0) { - CycleNode *forward = p_node->removeEdge(); - if (forward == w_node) - continue; - addNodeEdge(w_node, forward); - if (hasCycles) - return false; - } - - erasePromiseNode(promise); - /* Not deleting p_node, to maintain consistency if mergeNodes() fails */ - - return !hasCycles; -} - /** * Adds an edge between two CycleNodes. * @param fromnode The edge comes from this CycleNode @@ -275,7 +142,6 @@ void CycleGraph::addRMWEdge(const T *from, const ModelAction *rmw) } /* Instantiate two forms of CycleGraph::addRMWEdge */ template void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw); -template void CycleGraph::addRMWEdge(const Promise *from, const ModelAction *rmw); /** * @brief Adds an edge between objects @@ -303,35 +169,16 @@ bool CycleGraph::addEdge(const T *from, const U *to) } /* Instantiate four forms of CycleGraph::addEdge */ template bool CycleGraph::addEdge(const ModelAction *from, const ModelAction *to); -template bool CycleGraph::addEdge(const ModelAction *from, const Promise *to); -template bool CycleGraph::addEdge(const Promise *from, const ModelAction *to); -template bool CycleGraph::addEdge(const Promise *from, const Promise *to); #if SUPPORT_MOD_ORDER_DUMP static void print_node(FILE *file, const CycleNode *node, int label) { - if (node->is_promise()) { - const Promise *promise = node->getPromise(); - int idx = promise->get_index(); - fprintf(file, "P%u", idx); - if (label) { - int first = 1; - fprintf(file, " [label=\"P%d, T", idx); - for (unsigned int i = 0 ; i < promise->max_available_thread_idx(); i++) - if (promise->thread_is_available(int_to_id(i))) { - fprintf(file, "%s%u", first ? "": ",", i); - first = 0; - } - fprintf(file, "\"]"); - } - } else { const ModelAction *act = node->getAction(); modelclock_t idx = act->get_seq_number(); fprintf(file, "N%u", idx); if (label) fprintf(file, " [label=\"N%u, T%u\"]", idx, act->get_tid()); - } } static void print_edge(FILE *file, const CycleNode *from, const CycleNode *to, const char *prop) @@ -358,7 +205,6 @@ void CycleGraph::dot_print_edge(FILE *file, const T *from, const U *to, const ch print_edge(file, fromnode, tonode, prop); } /* Instantiate two forms of CycleGraph::dot_print_edge */ -template void CycleGraph::dot_print_edge(FILE *file, const Promise *from, const ModelAction *to, const char *prop); template void CycleGraph::dot_print_edge(FILE *file, const ModelAction *from, const ModelAction *to, const char *prop); void CycleGraph::dumpNodes(FILE *file) const @@ -434,41 +280,6 @@ bool CycleGraph::checkReachable(const T *from, const U *to) const /* Instantiate four forms of CycleGraph::checkReachable */ template bool CycleGraph::checkReachable(const ModelAction *from, const ModelAction *to) const; -template bool CycleGraph::checkReachable(const ModelAction *from, - const Promise *to) const; -template bool CycleGraph::checkReachable(const Promise *from, - const ModelAction *to) const; -template bool CycleGraph::checkReachable(const Promise *from, - const Promise *to) const; - -/** @return True, if the promise has failed; false otherwise */ -bool CycleGraph::checkPromise(const ModelAction *fromact, Promise *promise) const -{ - discovered->reset(); - queue->clear(); - CycleNode *from = actionToNode.get(fromact); - - queue->push_back(from); - discovered->put(from, from); - while (!queue->empty()) { - const CycleNode *node = queue->back(); - queue->pop_back(); - - if (node->getPromise() == promise) - return true; - if (!node->is_promise()) - promise->eliminate_thread(node->getAction()->get_tid()); - - for (unsigned int i = 0; i < node->getNumEdges(); i++) { - CycleNode *next = node->getEdge(i); - if (!discovered->contains(next)) { - discovered->put(next, next); - queue->push_back(next); - } - } - } - return false; -} /** @brief Begin a new sequence of graph additions which can be rolled back */ void CycleGraph::startChanges() @@ -512,18 +323,6 @@ bool CycleGraph::checkForCycles() const */ CycleNode::CycleNode(const ModelAction *act) : action(act), - promise(NULL), - hasRMW(NULL) -{ -} - -/** - * @brief Constructor for a Promise CycleNode - * @param promise The Promise which was generated - */ -CycleNode::CycleNode(const Promise *promise) : - action(NULL), - promise(promise), hasRMW(NULL) { } @@ -640,19 +439,3 @@ bool CycleNode::setRMW(CycleNode *node) hasRMW = node; return false; } - -/** - * Convert a Promise CycleNode into a concrete-valued CycleNode. Should only be - * used when there's no existing ModelAction CycleNode for this write. - * - * @param writer The ModelAction which wrote the future value represented by - * this CycleNode - */ -void CycleNode::resolvePromise(const ModelAction *writer) -{ - ASSERT(is_promise()); - ASSERT(promise->is_compatible(writer)); - action = writer; - promise = NULL; - ASSERT(!is_promise()); -} diff --git a/cyclegraph.h b/cyclegraph.h index 7e7d180e..4f23e322 100644 --- a/cyclegraph.h +++ b/cyclegraph.h @@ -17,7 +17,6 @@ #include "mymemory.h" #include "stl-model.h" -class Promise; class CycleNode; class ModelAction; @@ -34,7 +33,6 @@ class CycleGraph { void addRMWEdge(const T *from, const ModelAction *rmw); bool checkForCycles() const; - bool checkPromise(const ModelAction *from, Promise *p) const; template bool checkReachable(const T *from, const U *to) const; @@ -51,18 +49,13 @@ class CycleGraph { void dot_print_edge(FILE *file, const T *from, const U *to, const char *prop); #endif - bool resolvePromise(const Promise *promise, ModelAction *writer); SNAPSHOTALLOC private: bool addNodeEdge(CycleNode *fromnode, CycleNode *tonode); void putNode(const ModelAction *act, CycleNode *node); - void putNode(const Promise *promise, CycleNode *node); - void erasePromiseNode(const Promise *promise); CycleNode * getNode(const ModelAction *act); - CycleNode * getNode(const Promise *promise); CycleNode * getNode_noCreate(const ModelAction *act) const; - CycleNode * getNode_noCreate(const Promise *promise) const; bool mergeNodes(CycleNode *node1, CycleNode *node2); HashTable *discovered; @@ -71,8 +64,6 @@ class CycleGraph { /** @brief A table for mapping ModelActions to CycleNodes */ HashTable actionToNode; - /** @brief A table for mapping Promises to CycleNodes */ - HashTable promiseToNode; #if SUPPORT_MOD_ORDER_DUMP SnapVector nodeList; @@ -90,13 +81,11 @@ class CycleGraph { }; /** - * @brief A node within a CycleGraph; corresponds either to one ModelAction or - * to a promised future value + * @brief A node within a CycleGraph; corresponds either to one ModelAction */ class CycleNode { public: CycleNode(const ModelAction *act); - CycleNode(const Promise *promise); bool addEdge(CycleNode *node); CycleNode * getEdge(unsigned int i) const; unsigned int getNumEdges() const; @@ -109,19 +98,12 @@ class CycleNode { CycleNode * getRMW() const; void clearRMW() { hasRMW = NULL; } const ModelAction * getAction() const { return action; } - const Promise * getPromise() const { return promise; } - bool is_promise() const { return !action; } - void resolvePromise(const ModelAction *writer); SNAPSHOTALLOC private: /** @brief The ModelAction that this node represents */ const ModelAction *action; - /** @brief The promise represented by this node; only valid when action - * is NULL */ - const Promise *promise; - /** @brief The edges leading out from this node */ SnapVector edges; diff --git a/execution.cc b/execution.cc index 8fdc9fbe..7a51bca6 100644 --- a/execution.cc +++ b/execution.cc @@ -11,7 +11,6 @@ #include "common.h" #include "clockvector.h" #include "cyclegraph.h" -#include "promise.h" #include "datarace.h" #include "threads-model.h" #include "bugmessage.h" @@ -28,8 +27,6 @@ struct model_snapshot_members { used_sequence_numbers(0), next_backtrack(NULL), bugs(), - failed_promise(false), - hard_failed_promise(false), too_many_reads(false), no_valid_reads(false), bad_synchronization(false), @@ -47,8 +44,6 @@ struct model_snapshot_members { modelclock_t used_sequence_numbers; ModelAction *next_backtrack; SnapVector bugs; - bool failed_promise; - bool hard_failed_promise; bool too_many_reads; bool no_valid_reads; /** @brief Incorrectly-ordered synchronization was made */ @@ -64,19 +59,18 @@ ModelExecution::ModelExecution(ModelChecker *m, const struct model_params *params, Scheduler *scheduler, NodeStack *node_stack) : + pthread_counter(0), model(m), params(params), scheduler(scheduler), action_trace(), thread_map(2), /* We'll always need at least 2 threads */ pthread_map(0), - pthread_counter(0), obj_map(), condvar_waiters_map(), obj_thrd_map(), mutex_map(), - promises(), - futurevalues(), + cond_map(), pending_rel_seqs(), thrd_last_action(1), thrd_last_fence_release(), @@ -97,9 +91,6 @@ ModelExecution::~ModelExecution() for (unsigned int i = 0; i < get_num_threads(); i++) delete get_thread(int_to_id(i)); - for (unsigned int i = 0; i < promises.size(); i++) - delete promises[i]; - delete mo_graph; delete priv; } @@ -635,30 +626,6 @@ bool ModelExecution::process_read(ModelAction *curr) updated = r_modification_order(curr, rf); read_from(curr, rf); mo_graph->commitChanges(); - mo_check_promises(curr, true); - break; - } - case READ_FROM_PROMISE: { - Promise *promise = curr->get_node()->get_read_from_promise(); - if (promise->add_reader(curr)) - priv->failed_promise = true; - curr->set_read_from_promise(promise); - mo_graph->startChanges(); - if (!check_recency(curr, promise)) - priv->too_many_reads = true; - updated = r_modification_order(curr, promise); - mo_graph->commitChanges(); - break; - } - case READ_FROM_FUTURE: { - /* Read from future value */ - struct future_value fv = node->get_future_value(); - Promise *promise = new Promise(this, curr, fv); - curr->set_read_from_promise(promise); - promises.push_back(promise); - mo_graph->startChanges(); - updated = r_modification_order(curr, promise); - mo_graph->commitChanges(); break; } default: @@ -770,67 +737,6 @@ bool ModelExecution::process_mutex(ModelAction *curr) return false; } -/** - * @brief Check if the current pending promises allow a future value to be sent - * - * It is unsafe to pass a future value back if there exists a pending promise Pr - * such that: - * - * reader --exec-> Pr --exec-> writer - * - * If such Pr exists, we must save the pending future value until Pr is - * resolved. - * - * @param writer The operation which sends the future value. Must be a write. - * @param reader The operation which will observe the value. Must be a read. - * @return True if the future value can be sent now; false if it must wait. - */ -bool ModelExecution::promises_may_allow(const ModelAction *writer, - const ModelAction *reader) const -{ - for (int i = promises.size() - 1; i >= 0; i--) { - ModelAction *pr = promises[i]->get_reader(0); - //reader is after promise...doesn't cross any promise - if (*reader > *pr) - return true; - //writer is after promise, reader before...bad... - if (*writer > *pr) - return false; - } - return true; -} - -/** - * @brief Add a future value to a reader - * - * This function performs a few additional checks to ensure that the future - * value can be feasibly observed by the reader - * - * @param writer The operation whose value is sent. Must be a write. - * @param reader The read operation which may read the future value. Must be a read. - */ -void ModelExecution::add_future_value(const ModelAction *writer, ModelAction *reader) -{ - /* Do more ambitious checks now that mo is more complete */ - if (!mo_may_allow(writer, reader)) - return; - - Node *node = reader->get_node(); - - /* Find an ancestor thread which exists at the time of the reader */ - Thread *write_thread = get_thread(writer); - while (id_to_int(write_thread->get_id()) >= node->get_num_threads()) - write_thread = write_thread->get_parent(); - - struct future_value fv = { - writer->get_write_value(), - writer->get_seq_number() + params->maxfuturedelay, - write_thread->get_id(), - }; - if (node->add_future_value(fv)) - set_latest_backtrack(reader); -} - /** * Process a write ModelAction * @param curr The ModelAction to process @@ -842,46 +748,13 @@ bool ModelExecution::process_write(ModelAction *curr, work_queue_t *work) /* Readers to which we may send our future value */ ModelVector send_fv; - const ModelAction *earliest_promise_reader; - bool updated_promises = false; - - bool updated_mod_order = w_modification_order(curr, &send_fv); - Promise *promise = pop_promise_to_resolve(curr); - - if (promise) { - earliest_promise_reader = promise->get_reader(0); - updated_promises = resolve_promise(curr, promise, work); - } else - earliest_promise_reader = NULL; - - for (unsigned int i = 0; i < send_fv.size(); i++) { - ModelAction *read = send_fv[i]; - - /* Don't send future values to reads after the Promise we resolve */ - if (!earliest_promise_reader || *read < *earliest_promise_reader) { - /* Check if future value can be sent immediately */ - if (promises_may_allow(curr, read)) { - add_future_value(curr, read); - } else { - futurevalues.push_back(PendingFutureValue(curr, read)); - } - } - } - /* Check the pending future values */ - for (int i = (int)futurevalues.size() - 1; i >= 0; i--) { - struct PendingFutureValue pfv = futurevalues[i]; - if (promises_may_allow(pfv.writer, pfv.reader)) { - add_future_value(pfv.writer, pfv.reader); - futurevalues.erase(futurevalues.begin() + i); - } - } + bool updated_mod_order = w_modification_order(curr); mo_graph->commitChanges(); - mo_check_promises(curr, false); get_thread(curr)->set_return_value(VALUE_NONE); - return updated_mod_order || updated_promises; + return updated_mod_order; } /** @@ -957,12 +830,6 @@ bool ModelExecution::process_thread_action(ModelAction *curr) curr->set_thread_operand(th); add_thread(th); th->set_creation(curr); - /* Promises can be satisfied by children */ - for (unsigned int i = 0; i < promises.size(); i++) { - Promise *promise = promises[i]; - if (promise->thread_is_available(curr->get_tid())) - promise->add_thread(th->get_id()); - } break; } case PTHREAD_CREATE: { @@ -978,13 +845,6 @@ bool ModelExecution::process_thread_action(ModelAction *curr) pthread_map.resize( pthread_counter ); pthread_map[ pthread_counter-1 ] = th; - /* Promises can be satisfied by children */ - for (unsigned int i = 0; i < promises.size(); i++) { - Promise *promise = promises[i]; - if (promise->thread_is_available(curr->get_tid())) - promise->add_thread(th->get_id()); - } - break; } case THREAD_JOIN: { @@ -1012,18 +872,10 @@ bool ModelExecution::process_thread_action(ModelAction *curr) scheduler->wake(waiting); } th->complete(); - /* Completed thread can't satisfy promises */ - for (unsigned int i = 0; i < promises.size(); i++) { - Promise *promise = promises[i]; - if (promise->thread_is_available(th->get_id())) - if (promise->eliminate_thread(th->get_id())) - priv->failed_promise = true; - } updated = true; /* trigger rel-seq checks */ break; } case THREAD_START: { - check_promises(curr->get_tid(), NULL, curr->get_cv()); break; } default: @@ -1107,9 +959,6 @@ bool ModelExecution::initialize_curr_action(ModelAction **curr) newcurr = process_rmw(*curr); delete *curr; - if (newcurr->is_rmw()) - compute_promises(newcurr); - *curr = newcurr; return false; } @@ -1146,9 +995,7 @@ bool ModelExecution::initialize_curr_action(ModelAction **curr) * Perform one-time actions when pushing new ModelAction onto * NodeStack */ - if (newcurr->is_write()) - compute_promises(newcurr); - else if (newcurr->is_relseq_fixup()) + if (newcurr->is_relseq_fixup()) compute_relseq_breakwrites(newcurr); else if (newcurr->is_wait()) newcurr->get_node()->set_misc_max(2); @@ -1207,39 +1054,9 @@ bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second) set_bad_synchronization(); return false; } - check_promises(first->get_tid(), second->get_cv(), first->get_cv()); return second->synchronize_with(first); } -/** - * Check promises and eliminate potentially-satisfying threads when a thread is - * blocked (e.g., join, lock). A thread which is waiting on another thread can - * no longer satisfy a promise generated from that thread. - * - * @param blocker The thread on which a thread is waiting - * @param waiting The waiting thread - */ -void ModelExecution::thread_blocking_check_promises(Thread *blocker, Thread *waiting) -{ - for (unsigned int i = 0; i < promises.size(); i++) { - Promise *promise = promises[i]; - if (!promise->thread_is_available(waiting->get_id())) - continue; - for (unsigned int j = 0; j < promise->get_num_readers(); j++) { - ModelAction *reader = promise->get_reader(j); - if (reader->get_tid() != blocker->get_id()) - continue; - if (promise->eliminate_thread(waiting->get_id())) { - /* Promise has failed */ - priv->failed_promise = true; - } else { - /* Only eliminate the 'waiting' thread once */ - return; - } - } - } -} - /** * @brief Check whether a model action is enabled. * @@ -1260,7 +1077,6 @@ bool ModelExecution::check_action_enabled(ModelAction *curr) { } else if (curr->is_thread_join()) { Thread *blocking = curr->get_thread_operand(); if (!blocking->is_complete()) { - thread_blocking_check_promises(blocking, get_thread(curr)); return false; } } else if (params->yieldblock && curr->is_yield()) { @@ -1350,23 +1166,17 @@ ModelAction * ModelExecution::check_current_action(ModelAction *curr) if (act->is_read()) { const ModelAction *rf = act->get_reads_from(); - const Promise *promise = act->get_reads_from_promise(); - if (rf) { - if (r_modification_order(act, rf)) - updated = true; - if (act->is_seqcst()) { - ModelAction *last_sc_write = get_last_seq_cst_write(act); - if (last_sc_write != NULL && rf->happens_before(last_sc_write)) { - set_bad_sc_read(); - } - } - } else if (promise) { - if (r_modification_order(act, promise)) - updated = true; + if (r_modification_order(act, rf)) + updated = true; + if (act->is_seqcst()) { + ModelAction *last_sc_write = get_last_seq_cst_write(act); + if (last_sc_write != NULL && rf->happens_before(last_sc_write)) { + set_bad_sc_read(); + } } } if (act->is_write()) { - if (w_modification_order(act, NULL)) + if (w_modification_order(act)) updated = true; } mo_graph->commitChanges(); @@ -1394,22 +1204,11 @@ void ModelExecution::check_curr_backtracking(ModelAction *curr) if ((parnode && !parnode->backtrack_empty()) || !currnode->misc_empty() || !currnode->read_from_empty() || - !currnode->promise_empty() || !currnode->relseq_break_empty()) { set_latest_backtrack(curr); } } -bool ModelExecution::promises_expired() const -{ - for (unsigned int i = 0; i < promises.size(); i++) { - Promise *promise = promises[i]; - if (promise->get_expiration() < priv->used_sequence_numbers) - return true; - } - return false; -} - /** * This is the strongest feasibility check available. * @return whether the current trace (partial or complete) must be a prefix of @@ -1431,8 +1230,6 @@ void ModelExecution::print_infeasibility(const char *prefix) const char *ptr = buf; if (mo_graph->checkForCycles()) ptr += sprintf(ptr, "[mo cycle]"); - if (priv->failed_promise || priv->hard_failed_promise) - ptr += sprintf(ptr, "[failed promise]"); if (priv->too_many_reads) ptr += sprintf(ptr, "[too many reads]"); if (priv->no_valid_reads) @@ -1441,10 +1238,6 @@ void ModelExecution::print_infeasibility(const char *prefix) const ptr += sprintf(ptr, "[bad sw ordering]"); if (priv->bad_sc_read) ptr += sprintf(ptr, "[bad sc read]"); - if (promises_expired()) - ptr += sprintf(ptr, "[promise expired]"); - if (promises.size() != 0) - ptr += sprintf(ptr, "[unresolved promise]"); if (ptr != buf) model_print("%s: %s", prefix ? prefix : "Infeasible", buf); } @@ -1455,7 +1248,7 @@ void ModelExecution::print_infeasibility(const char *prefix) const */ bool ModelExecution::is_feasible_prefix_ignore_relseq() const { - return !is_infeasible() && promises.size() == 0 && ! priv->failed_promise; + return !is_infeasible() ; } @@ -1471,9 +1264,7 @@ bool ModelExecution::is_infeasible() const priv->no_valid_reads || priv->too_many_reads || priv->bad_synchronization || - priv->bad_sc_read || - priv->hard_failed_promise || - promises_expired(); + priv->bad_sc_read; } /** Close out a RMWR by converting previous RMWR into a RMW or READ. */ @@ -1481,10 +1272,7 @@ ModelAction * ModelExecution::process_rmw(ModelAction *act) { ModelAction *lastread = get_last_action(act->get_tid()); lastread->process_rmw(act); if (act->is_rmw()) { - if (lastread->get_reads_from()) - mo_graph->addRMWEdge(lastread->get_reads_from(), lastread); - else - mo_graph->addRMWEdge(lastread->get_reads_from_promise(), lastread); + mo_graph->addRMWEdge(lastread->get_reads_from(), lastread); mo_graph->commitChanges(); } return lastread; @@ -1551,8 +1339,7 @@ bool ModelExecution::check_recency(ModelAction *curr, const T *rf) const return true; //NOTE: Next check is just optimization, not really necessary.... - if (curr->get_node()->get_read_from_past_size() + - curr->get_node()->get_read_from_promise_size() <= 1) + if (curr->get_node()->get_read_from_past_size() <= 1) return true; SnapVector *thrd_lists = obj_thrd_map.get(curr->get_location()); @@ -1572,12 +1359,9 @@ bool ModelExecution::check_recency(ModelAction *curr, const T *rf) const ModelAction *act = *ritcopy; if (!act->is_read()) return true; - if (act->get_reads_from_promise() && !act->get_reads_from_promise()->equals(rf)) - return true; if (act->get_reads_from() && !act->get_reads_from()->equals(rf)) return true; - if (act->get_node()->get_read_from_past_size() + - act->get_node()->get_read_from_promise_size() <= 1) + if (act->get_node()->get_read_from_past_size() <= 1) return true; } for (int i = 0; i < curr->get_node()->get_read_from_past_size(); i++) { @@ -1585,11 +1369,6 @@ bool ModelExecution::check_recency(ModelAction *curr, const T *rf) const if (should_read_instead(curr, rf, write)) return false; /* liveness failure */ } - for (int i = 0; i < curr->get_node()->get_read_from_promise_size(); i++) { - const Promise *promise = curr->get_node()->get_read_from_promise(i); - if (should_read_instead(curr, rf, promise)) - return false; /* liveness failure */ - } return true; } @@ -1682,13 +1461,8 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf) added = mo_graph->addEdge(act, rf) || added; } else { const ModelAction *prevrf = act->get_reads_from(); - const Promise *prevrf_promise = act->get_reads_from_promise(); - if (prevrf) { - if (!prevrf->equals(rf)) - added = mo_graph->addEdge(prevrf, rf) || added; - } else if (!prevrf_promise->equals(rf)) { - added = mo_graph->addEdge(prevrf_promise, rf) || added; - } + if (!prevrf->equals(rf)) + added = mo_graph->addEdge(prevrf, rf) || added; } break; } @@ -1699,9 +1473,6 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf) * All compatible, thread-exclusive promises must be ordered after any * concrete loads from the same thread */ - for (unsigned int i = 0; i < promises.size(); i++) - if (promises[i]->is_compatible_exclusive(curr)) - added = mo_graph->addEdge(rf, promises[i]) || added; return added; } @@ -1730,7 +1501,7 @@ bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf) * value. If NULL, then don't record any future values. * @return True if modification order edges were added; false otherwise */ -bool ModelExecution::w_modification_order(ModelAction *curr, ModelVector *send_fv) +bool ModelExecution::w_modification_order(ModelAction *curr) { SnapVector *thrd_lists = obj_thrd_map.get(curr->get_location()); unsigned int i; @@ -1804,10 +1575,7 @@ bool ModelExecution::w_modification_order(ModelAction *curr, ModelVectoraddEdge(act, curr) || added; else if (act->is_read()) { //if previous read accessed a null, just keep going - if (act->get_reads_from() == NULL) { - added = mo_graph->addEdge(act->get_reads_from_promise(), curr) || added; - } else - added = mo_graph->addEdge(act->get_reads_from(), curr) || added; + added = mo_graph->addEdge(act->get_reads_from(), curr) || added; } break; } else if (act->is_read() && !act->could_synchronize_with(curr) && @@ -1825,94 +1593,13 @@ bool ModelExecution::w_modification_order(ModelAction *curr, ModelVectorpush_back(act); - else if (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() && curr->get_reads_from() == act->get_reads_from()) - add_future_value(curr, act); - } } } } - /* - * All compatible, thread-exclusive promises must be ordered after any - * concrete stores to the same thread, or else they can be merged with - * this store later - */ - for (unsigned int i = 0; i < promises.size(); i++) - if (promises[i]->is_compatible_exclusive(curr)) - added = mo_graph->addEdge(curr, promises[i]) || added; - return added; } -//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;jget_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; -} - - -/** Arbitrary reads from the future are not allowed. Section 29.3 - * part 9 places some constraints. This method checks one result of constraint - * constraint. Others require compiler support. */ -bool ModelExecution::thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader) const -{ - if (!writer->is_rmw()) - return true; - - if (!reader->is_rmw()) - return true; - - for (const ModelAction *search = writer->get_reads_from(); search != NULL; search = search->get_reads_from()) { - if (search == reader) - return false; - if (search->get_tid() == reader->get_tid() && - search->happens_before(reader)) - break; - } - - return true; -} - /** * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places * some constraints. This method checks one the following constraint (others @@ -2414,177 +2101,6 @@ ClockVector * ModelExecution::get_cv(thread_id_t tid) const return get_parent_action(tid)->get_cv(); } -/** - * @brief Find the promise (if any) to resolve for the current action and - * remove it from the pending promise vector - * @param curr The current ModelAction. Should be a write. - * @return The Promise to resolve, if any; otherwise NULL - */ -Promise * ModelExecution::pop_promise_to_resolve(const ModelAction *curr) -{ - for (unsigned int i = 0; i < promises.size(); i++) - if (curr->get_node()->get_promise(i)) { - Promise *ret = promises[i]; - promises.erase(promises.begin() + i); - return ret; - } - return NULL; -} - -/** - * Resolve a Promise with a current write. - * @param write The ModelAction that is fulfilling Promises - * @param promise The Promise to resolve - * @param work The work queue, for adding new fixup work - * @return True if the Promise was successfully resolved; false otherwise - */ -bool ModelExecution::resolve_promise(ModelAction *write, Promise *promise, - work_queue_t *work) -{ - ModelVector actions_to_check; - - for (unsigned int i = 0; i < promise->get_num_readers(); i++) { - ModelAction *read = promise->get_reader(i); - if (read_from(read, write)) { - /* Propagate the changed clock vector */ - propagate_clockvector(read, work); - } - actions_to_check.push_back(read); - } - /* Make sure the promise's value matches the write's value */ - ASSERT(promise->is_compatible(write) && promise->same_value(write)); - if (!mo_graph->resolvePromise(promise, write)) - priv->hard_failed_promise = true; - - /** - * @todo It is possible to end up in an inconsistent state, where a - * "resolved" promise may still be referenced if - * CycleGraph::resolvePromise() failed, so don't delete 'promise'. - * - * Note that the inconsistency only matters when dumping mo_graph to - * file. - * - * delete promise; - */ - - //Check whether reading these writes has made threads unable to - //resolve promises - for (unsigned int i = 0; i < actions_to_check.size(); i++) { - ModelAction *read = actions_to_check[i]; - mo_check_promises(read, true); - } - - return true; -} - -/** - * Compute the set of promises that could potentially be satisfied by this - * action. Note that the set computation actually appears in the Node, not in - * ModelExecution. - * @param curr The ModelAction that may satisfy promises - */ -void ModelExecution::compute_promises(ModelAction *curr) -{ - for (unsigned int i = 0; i < promises.size(); i++) { - Promise *promise = promises[i]; - if (!promise->is_compatible(curr) || !promise->same_value(curr)) - continue; - - bool satisfy = true; - for (unsigned int j = 0; j < promise->get_num_readers(); j++) { - const ModelAction *act = promise->get_reader(j); - if (act->happens_before(curr) || - act->could_synchronize_with(curr)) { - satisfy = false; - break; - } - } - if (satisfy) - curr->get_node()->set_promise(i); - } -} - -/** Checks promises in response to change in ClockVector Threads. */ -void ModelExecution::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]; - if (!promise->thread_is_available(tid)) - continue; - for (unsigned int j = 0; j < promise->get_num_readers(); j++) { - const ModelAction *act = promise->get_reader(j); - if ((!old_cv || !old_cv->synchronized_since(act)) && - merge_cv->synchronized_since(act)) { - if (promise->eliminate_thread(tid)) { - /* Promise has failed */ - priv->failed_promise = true; - return; - } - } - } - } -} - -void ModelExecution::check_promises_thread_disabled() -{ - for (unsigned int i = 0; i < promises.size(); i++) { - Promise *promise = promises[i]; - if (promise->has_failed()) { - priv->failed_promise = true; - return; - } - } -} - -/** - * @brief Checks promises in response to addition to modification order for - * threads. - * - * We test whether threads are still available for satisfying promises after an - * addition to our modification order constraints. Those that are unavailable - * are "eliminated". Once all threads are eliminated from satisfying a promise, - * that promise has failed. - * - * @param act The ModelAction which updated the modification order - * @param is_read_check Should be true if act is a read and we must check for - * updates to the store from which it read (there is a distinction here for - * RMW's, which are both a load and a store) - */ -void ModelExecution::mo_check_promises(const ModelAction *act, bool is_read_check) -{ - const ModelAction *write = is_read_check ? act->get_reads_from() : act; - - for (unsigned int i = 0; i < promises.size(); i++) { - Promise *promise = promises[i]; - - // Is this promise on the same location? - if (!promise->same_location(write)) - continue; - - for (unsigned int j = 0; j < promise->get_num_readers(); j++) { - const ModelAction *pread = promise->get_reader(j); - if (!pread->happens_before(act)) - continue; - if (mo_graph->checkPromise(write, promise)) { - priv->hard_failed_promise = true; - return; - } - break; - } - - // Don't do any lookups twice for the same thread - if (!promise->thread_is_available(act->get_tid())) - continue; - - if (mo_graph->checkReachable(promise, write)) { - if (mo_graph->checkPromise(write, promise)) { - priv->hard_failed_promise = true; - return; - } - } - } -} - /** * Compute the set of writes that may break the current pending release * sequence. This information is extracted from previou release sequence @@ -2661,20 +2177,6 @@ void ModelExecution::build_may_read_from(ModelAction *curr) } } - /* Inherit existing, promised future values */ - for (i = 0; i < promises.size(); i++) { - const Promise *promise = promises[i]; - const ModelAction *promise_read = promise->get_reader(0); - if (promise_read->same_var(curr)) { - /* Only add feasible future-values */ - mo_graph->startChanges(); - r_modification_order(curr, promise); - if (!is_infeasible()) - curr->get_node()->add_read_from_promise(promise_read); - mo_graph->rollbackChanges(); - } - } - /* We may find no valid may-read-from only if the execution is doomed */ if (!curr->get_node()->read_from_size()) { priv->no_valid_reads = true; @@ -2761,16 +2263,10 @@ void ModelExecution::dumpGraph(char *filename) const ModelAction *act = *it; if (act->is_read()) { mo_graph->dot_print_node(file, act); - if (act->get_reads_from()) - mo_graph->dot_print_edge(file, + mo_graph->dot_print_edge(file, act->get_reads_from(), act, "label=\"rf\", color=red, weight=2"); - else - mo_graph->dot_print_edge(file, - act->get_reads_from_promise(), - act, - "label=\"rf\", color=red"); } if (thread_array[act->get_tid()]) { mo_graph->dot_print_edge(file, @@ -2813,14 +2309,6 @@ void ModelExecution::print_summary() const print_list(&action_trace); model_print("\n"); - if (!promises.empty()) { - model_print("Pending promises:\n"); - for (unsigned int i = 0; i < promises.size(); i++) { - model_print(" [P%u] ", i); - promises[i]->print(); - } - model_print("\n"); - } } /** @@ -2871,26 +2359,6 @@ Thread * ModelExecution::get_pthread(pthread_t pid) { else return NULL; } -/** - * @brief Get a Promise's "promise number" - * - * A "promise number" is an index number that is unique to a promise, valid - * only for a specific snapshot of an execution trace. Promises may come and go - * as they are generated an resolved, so an index only retains meaning for the - * current snapshot. - * - * @param promise The Promise to check - * @return The promise index, if the promise still is valid; otherwise -1 - */ -int ModelExecution::get_promise_number(const Promise *promise) const -{ - for (unsigned int i = 0; i < promises.size(); i++) - if (promises[i] == promise) - return i; - /* Not found */ - return -1; -} - /** * @brief Check if a Thread is currently enabled * @param t The Thread to check diff --git a/execution.h b/execution.h index fdc226b4..579e9b7c 100644 --- a/execution.h +++ b/execution.h @@ -23,7 +23,6 @@ class Node; class NodeStack; class CycleGraph; -class Promise; class Scheduler; class Thread; class ClockVector; @@ -87,8 +86,6 @@ public: void incr_pthread_counter() { pthread_counter++; } Thread * get_pthread(pthread_t pid); - int get_promise_number(const Promise *promise) const; - bool is_enabled(Thread *t) const; bool is_enabled(thread_id_t tid) const; @@ -97,7 +94,6 @@ public: ClockVector * get_cv(thread_id_t tid) const; ModelAction * get_parent_action(thread_id_t tid) const; - void check_promises_thread_disabled(); bool isfeasibleprefix() const; action_list_t * get_actions_on_obj(void * obj, thread_id_t tid) const; @@ -125,10 +121,9 @@ public: action_list_t * get_action_trace() { return &action_trace; } CycleGraph * const get_mo_graph() { return mo_graph; } - - HashTable mutex_map; - HashTable cond_map; - + HashTable * getCondMap() {return &cond_map;} + HashTable * getMutexMap() {return &mutex_map;} + SNAPSHOTALLOC private: int get_execution_number() const; @@ -144,10 +139,8 @@ private: bool sleep_can_read_from(ModelAction *curr, const ModelAction *write); bool thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader) const; bool mo_may_allow(const ModelAction *writer, const ModelAction *reader); - bool promises_may_allow(const ModelAction *writer, const ModelAction *reader) const; void set_bad_synchronization(); void set_bad_sc_read(); - bool promises_expired() const; bool should_wake_up(const ModelAction *curr, const Thread *thread) const; void wake_up_sleeping_actions(ModelAction *curr); modelclock_t get_next_seq_num(); @@ -175,16 +168,8 @@ private: ModelAction * get_last_conflict(ModelAction *act) const; void set_backtracking(ModelAction *act); bool set_latest_backtrack(ModelAction *act); - Promise * pop_promise_to_resolve(const ModelAction *curr); - bool resolve_promise(ModelAction *curr, Promise *promise, - work_queue_t *work); - void compute_promises(ModelAction *curr); void compute_relseq_breakwrites(ModelAction *curr); - void check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv); - void mo_check_promises(const ModelAction *act, bool is_read_check); - void thread_blocking_check_promises(Thread *blocker, Thread *waiting); - void check_curr_backtracking(ModelAction *curr); void add_action_to_lists(ModelAction *act); ModelAction * get_last_fence_release(thread_id_t tid) const; @@ -197,13 +182,12 @@ private: template bool r_modification_order(ModelAction *curr, const rf_type *rf); - bool w_modification_order(ModelAction *curr, ModelVector *send_fv); + bool w_modification_order(ModelAction *curr); void get_release_seq_heads(ModelAction *acquire, ModelAction *read, rel_heads_list_t *release_heads); bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads, struct release_seq *pending) const; void propagate_clockvector(ModelAction *acquire, work_queue_t *work); bool resolve_release_sequences(void *location, work_queue_t *work_queue); void add_future_value(const ModelAction *writer, ModelAction *reader); - bool check_coherence_promise(const ModelAction *write, const ModelAction *read); ModelAction * get_uninitialized_action(const ModelAction *curr) const; action_list_t action_trace; @@ -220,16 +204,8 @@ private: HashTable *, uintptr_t, 4> obj_thrd_map; -// HashTable mutex_map; - - /** - * @brief List of currently-pending promises - * - * Promises are sorted by the execution order of the read(s) which - * created them - */ - SnapVector promises; - SnapVector futurevalues; + HashTable mutex_map; + HashTable cond_map; /** * List of pending release sequences. Release sequences might be diff --git a/futex.cc b/futex.cc index 64ec6b4a..fa32e9a2 100644 --- a/futex.cc +++ b/futex.cc @@ -48,8 +48,8 @@ _GLIBCXX_BEGIN_NAMESPACE_VERSION cdsc::condition_variable *v = new cdsc::condition_variable(); cdsc::mutex *m = new cdsc::mutex(); - execution->cond_map.put( (pthread_cond_t *) __addr, v); - execution->mutex_map.put( (pthread_mutex_t *) __addr, m); + execution->getCondMap()->put( (pthread_cond_t *) __addr, v); + execution->getMutexMap()->put( (pthread_mutex_t *) __addr, m); v->wait(*m); return true; @@ -60,7 +60,7 @@ _GLIBCXX_BEGIN_NAMESPACE_VERSION { // INT_MAX wakes all the waiters at the address __addr ModelExecution *execution = model->get_execution(); - cdsc::condition_variable *v = execution->cond_map.get( (pthread_cond_t *) __addr); + cdsc::condition_variable *v = execution->getCondMap()->get( (pthread_cond_t *) __addr); v->notify_all(); } diff --git a/model.cc b/model.cc index c4bcaf9b..6f6ba3ec 100644 --- a/model.cc +++ b/model.cc @@ -471,7 +471,6 @@ void ModelChecker::do_restart() /** @brief Run ModelChecker for the user program */ void ModelChecker::run() { - bool has_next; int i = 0; do { thrd_t user_thread; @@ -541,7 +540,7 @@ void ModelChecker::run() t = execution->take_step(curr); } while (!should_terminate_execution()); - has_next = next_execution(); + next_execution(); i++; } while (i<2); // while (has_next); diff --git a/model.h b/model.h index cdc317c9..18fcf0be 100644 --- a/model.h +++ b/model.h @@ -20,7 +20,6 @@ class Node; class NodeStack; class CycleGraph; -class Promise; class Scheduler; class Thread; class ClockVector; diff --git a/nodestack.cc b/nodestack.cc index fed7545f..e3bccc99 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -42,12 +42,6 @@ Node::Node(const struct model_params *params, ModelAction *act, Node *par, enabled_array(NULL), read_from_past(), read_from_past_idx(0), - read_from_promises(), - read_from_promise_idx(-1), - future_values(), - future_index(-1), - resolve_promise(), - resolve_promise_idx(-1), relseq_break_writes(), relseq_break_index(0), misc_index(0), @@ -180,17 +174,6 @@ void Node::print() const model_print("[%d]", read_from_past[i]->get_seq_number()); model_print("\n"); - model_print(" read-from promises: %s", read_from_promise_empty() ? "empty" : "non-empty "); - for (int i = read_from_promise_idx + 1; i < (int)read_from_promises.size(); i++) - model_print("[%d]", read_from_promises[i]->get_seq_number()); - model_print("\n"); - - model_print(" future values: %s", future_value_empty() ? "empty" : "non-empty "); - for (int i = future_index + 1; i < (int)future_values.size(); i++) - model_print("[%#" PRIx64 "]", future_values[i].value); - model_print("\n"); - - model_print(" promises: %s\n", promise_empty() ? "empty" : "non-empty"); model_print(" misc: %s\n", misc_empty() ? "empty" : "non-empty"); model_print(" rel seq break: %s\n", relseq_break_empty() ? "empty" : "non-empty"); } @@ -292,68 +275,6 @@ void Node::clear_backtracking() /************************** end threads backtracking **************************/ -/*********************************** promise **********************************/ - -/** - * Sets a promise to explore meeting with the given node. - * @param i is the promise index. - */ -void Node::set_promise(unsigned int i) -{ - if (i >= resolve_promise.size()) - resolve_promise.resize(i + 1, false); - resolve_promise[i] = true; -} - -/** - * Looks up whether a given promise should be satisfied by this node. - * @param i The promise index. - * @return true if the promise should be satisfied by the given ModelAction. - */ -bool Node::get_promise(unsigned int i) const -{ - return (i < resolve_promise.size()) && (int)i == resolve_promise_idx; -} - -/** - * Increments to the next promise to resolve. - * @return true if we have a valid combination. - */ -bool Node::increment_promise() -{ - DBG(); - if (resolve_promise.empty()) - return false; - int prev_idx = resolve_promise_idx; - resolve_promise_idx++; - for ( ; resolve_promise_idx < (int)resolve_promise.size(); resolve_promise_idx++) - if (resolve_promise[resolve_promise_idx]) - return true; - resolve_promise_idx = prev_idx; - return false; -} - -/** - * Returns whether the promise set is empty. - * @return true if we have explored all promise combinations. - */ -bool Node::promise_empty() const -{ - for (int i = resolve_promise_idx + 1; i < (int)resolve_promise.size(); i++) - if (i >= 0 && resolve_promise[i]) - return false; - return true; -} - -/** @brief Clear any promise-resolution information for this Node */ -void Node::clear_promise_resolutions() -{ - resolve_promise.clear(); - resolve_promise_idx = -1; -} - -/******************************* end promise **********************************/ - void Node::set_misc_max(int i) { misc_max = i; @@ -409,7 +330,7 @@ bool Node::has_priority_over(thread_id_t tid1, thread_id_t tid2) const /** * Get the current state of the may-read-from set iteration - * @return The read-from type we should currently be checking (past or future) + * @return The read-from type we should currently be checking (past) */ read_from_type_t Node::get_read_from_status() { @@ -425,16 +346,9 @@ read_from_type_t Node::get_read_from_status() */ bool Node::increment_read_from() { - clear_promise_resolutions(); if (increment_read_from_past()) { read_from_status = READ_FROM_PAST; return true; - } else if (increment_read_from_promise()) { - read_from_status = READ_FROM_PROMISE; - return true; - } else if (increment_future_value()) { - read_from_status = READ_FROM_FUTURE; - return true; } read_from_status = READ_FROM_NONE; return false; @@ -445,21 +359,16 @@ bool Node::increment_read_from() */ bool Node::read_from_empty() const { - return read_from_past_empty() && - read_from_promise_empty() && - future_value_empty(); + return read_from_past_empty(); } /** - * Get the total size of the may-read-from set, including both past and future - * values + * Get the total size of the may-read-from set, including both past * @return The size of may-read-from */ unsigned int Node::read_from_size() const { - return read_from_past.size() + - read_from_promises.size() + - future_values.size(); + return read_from_past.size(); } /******************************* end read from ********************************/ @@ -533,151 +442,6 @@ bool Node::increment_read_from_past() /************************** end read from past ********************************/ -/***************************** read_from_promises *****************************/ - -/** - * Add an action to the read_from_promises set. - * @param reader The read which generated the Promise; we use the ModelAction - * instead of the Promise because the Promise does not last across executions - */ -void Node::add_read_from_promise(const ModelAction *reader) -{ - read_from_promises.push_back(reader); -} - -/** - * Gets the next 'read-from-promise' from this Node. Only valid for a node - * where this->action is a 'read'. - * @return The current element in read_from_promises - */ -Promise * Node::get_read_from_promise() const -{ - ASSERT(read_from_promise_idx >= 0 && read_from_promise_idx < ((int)read_from_promises.size())); - return read_from_promises[read_from_promise_idx]->get_reads_from_promise(); -} - -/** - * Gets a particular 'read-from-promise' form this Node. Only vlaid for a node - * where this->action is a 'read'. - * @param i The index of the Promise to get - * @return The Promise at index i, if the Promise is still available; NULL - * otherwise - */ -Promise * Node::get_read_from_promise(int i) const -{ - return read_from_promises[i]->get_reads_from_promise(); -} - -/** @return The size of the read-from-promise set */ -int Node::get_read_from_promise_size() const -{ - return read_from_promises.size(); -} - -/** - * Checks whether the read_from_promises set for this node is empty. - * @return true if the read_from_promises set is empty. - */ -bool Node::read_from_promise_empty() const -{ - return ((read_from_promise_idx + 1) >= ((int)read_from_promises.size())); -} - -/** - * Increments the index into the read_from_promises set to explore the next item. - * @return Returns false if we have explored all promises. - */ -bool Node::increment_read_from_promise() -{ - DBG(); - if (read_from_promise_idx < ((int)read_from_promises.size())) { - read_from_promise_idx++; - return (read_from_promise_idx < ((int)read_from_promises.size())); - } - return false; -} - -/************************* end read_from_promises *****************************/ - -/****************************** future values *********************************/ - -/** - * Adds a value from a weakly ordered future write to backtrack to. This - * operation may "fail" if the future value has already been run (within some - * sloppiness window of this expiration), or if the futurevalues set has - * reached its maximum. - * @see model_params.maxfuturevalues - * - * @param value is the value to backtrack to. - * @return True if the future value was successully added; false otherwise - */ -bool Node::add_future_value(struct future_value fv) -{ - uint64_t value = fv.value; - modelclock_t expiration = fv.expiration; - thread_id_t tid = fv.tid; - int idx = -1; /* Highest index where value is found */ - for (unsigned int i = 0; i < future_values.size(); i++) { - if (future_values[i].value == value && future_values[i].tid == tid) { - if (expiration <= future_values[i].expiration) - return false; - idx = i; - } - } - if (idx > future_index) { - /* Future value hasn't been explored; update expiration */ - future_values[idx].expiration = expiration; - return true; - } else if (idx >= 0 && expiration <= future_values[idx].expiration + get_params()->expireslop) { - /* Future value has been explored and is within the "sloppy" window */ - return false; - } - - /* Limit the size of the future-values set */ - if (get_params()->maxfuturevalues > 0 && - (int)future_values.size() >= get_params()->maxfuturevalues) - return false; - - future_values.push_back(fv); - return true; -} - -/** - * Gets the next 'future_value' from this Node. Only valid for a node where - * this->action is a 'read'. - * @return The first element in future_values - */ -struct future_value Node::get_future_value() const -{ - ASSERT(future_index >= 0 && future_index < ((int)future_values.size())); - return future_values[future_index]; -} - -/** - * Checks whether the future_values set for this node is empty. - * @return true if the future_values set is empty. - */ -bool Node::future_value_empty() const -{ - return ((future_index + 1) >= ((int)future_values.size())); -} - -/** - * Increments the index into the future_values set to explore the next item. - * @return Returns false if we have explored all values. - */ -bool Node::increment_future_value() -{ - DBG(); - if (future_index < ((int)future_values.size())) { - future_index++; - return (future_index < ((int)future_values.size())); - } - return false; -} - -/************************** end future values *********************************/ - /*********************** breaking release sequences ***************************/ /** @@ -743,9 +507,6 @@ bool Node::increment_behaviors() /* satisfy a different misc_index values */ if (increment_misc()) return true; - /* satisfy a different set of promises */ - if (increment_promise()) - return true; /* read from a different value */ if (increment_read_from()) return true; diff --git a/nodestack.h b/nodestack.h index 6ae96be8..b7e630b0 100644 --- a/nodestack.h +++ b/nodestack.h @@ -10,7 +10,6 @@ #include "mymemory.h" #include "schedule.h" -#include "promise.h" #include "stl-model.h" class ModelAction; @@ -31,8 +30,6 @@ struct fairness_info { */ typedef enum { READ_FROM_PAST, /**< @brief Read from a prior, existing store */ - READ_FROM_PROMISE, /**< @brief Read from an existing promised future value */ - READ_FROM_FUTURE, /**< @brief Read from a newly-asserted future value */ READ_FROM_NONE, /**< @brief A NULL state, which should not be reached */ } read_from_type_t; @@ -94,20 +91,6 @@ public: const ModelAction * get_read_from_past(int i) const; int get_read_from_past_size() const; - void add_read_from_promise(const ModelAction *reader); - Promise * get_read_from_promise() const; - Promise * get_read_from_promise(int i) const; - int get_read_from_promise_size() const; - - bool add_future_value(struct future_value fv); - struct future_value get_future_value() const; - - void set_promise(unsigned int i); - bool get_promise(unsigned int i) const; - bool increment_promise(); - bool promise_empty() const; - void clear_promise_resolutions(); - enabled_type_t *get_enabled_array() {return enabled_array;} void set_misc_max(int i); @@ -130,8 +113,6 @@ private: int get_yield_data(int tid1, int tid2) const; bool read_from_past_empty() const; bool increment_read_from_past(); - bool read_from_promise_empty() const; - bool increment_read_from_promise(); bool future_value_empty() const; bool increment_future_value(); read_from_type_t read_from_status; @@ -159,15 +140,6 @@ private: ModelVector read_from_past; unsigned int read_from_past_idx; - ModelVector read_from_promises; - int read_from_promise_idx; - - ModelVector future_values; - int future_index; - - ModelVector resolve_promise; - int resolve_promise_idx; - ModelVector relseq_break_writes; int relseq_break_index; diff --git a/promise.cc b/promise.cc deleted file mode 100644 index a98403bb..00000000 --- a/promise.cc +++ /dev/null @@ -1,204 +0,0 @@ -#define __STDC_FORMAT_MACROS -#include - -#include "promise.h" -#include "execution.h" -#include "schedule.h" -#include "action.h" -#include "threads-model.h" - -/** - * @brief Promise constructor - * @param execution The execution which is creating this Promise - * @param read The read which reads from a promised future value - * @param fv The future value that is promised - */ -Promise::Promise(const ModelExecution *execution, ModelAction *read, struct future_value fv) : - execution(execution), - num_available_threads(0), - num_was_available_threads(0), - fv(fv), - readers(1, read), - write(NULL) -{ - add_thread(fv.tid); - eliminate_thread(read->get_tid()); -} - -/** - * Add a reader that reads from this Promise. Must be added in an order - * consistent with execution order. - * - * @param reader The ModelAction that reads from this promise. Must be a read. - * @return True if this new reader has invalidated the promise; false otherwise - */ -bool Promise::add_reader(ModelAction *reader) -{ - readers.push_back(reader); - return eliminate_thread(reader->get_tid()); -} - -/** - * Access a reader that read from this Promise. Readers must be inserted in - * order by execution order, so they can be returned in this order. - * - * @param i The index of the reader to return - * @return The i'th reader of this Promise - */ -ModelAction * Promise::get_reader(unsigned int i) const -{ - return i < readers.size() ? readers[i] : NULL; -} - -/** - * Eliminate a thread which no longer can satisfy this promise. Once all - * enabled threads have been eliminated, this promise is unresolvable. - * - * @param tid The thread ID of the thread to eliminate - * @return True, if this elimination has invalidated the promise; false - * otherwise - */ -bool Promise::eliminate_thread(thread_id_t tid) -{ - unsigned int id = id_to_int(tid); - if (!thread_is_available(tid)) - return false; - - available_thread[id] = false; - num_available_threads--; - return has_failed(); -} - -/** - * Add a thread which may resolve this promise - * - * @param tid The thread ID - */ -void Promise::add_thread(thread_id_t tid) -{ - unsigned int id = id_to_int(tid); - if (id >= available_thread.size()) - available_thread.resize(id + 1, false); - if (!available_thread[id]) { - available_thread[id] = true; - num_available_threads++; - } - if (id >= was_available_thread.size()) - was_available_thread.resize(id + 1, false); - if (!was_available_thread[id]) { - was_available_thread[id] = true; - num_was_available_threads++; - } -} - -/** - * Check if a thread is available for resolving this promise. That is, the - * thread must have been previously marked for resolving this promise, and it - * cannot have been eliminated due to synchronization, etc. - * - * @param tid Thread ID of the thread to check - * @return True if the thread is available; false otherwise - */ -bool Promise::thread_is_available(thread_id_t tid) const -{ - unsigned int id = id_to_int(tid); - if (id >= available_thread.size()) - return false; - return available_thread[id]; -} - -bool Promise::thread_was_available(thread_id_t tid) const -{ - unsigned int id = id_to_int(tid); - if (id >= was_available_thread.size()) - return false; - return was_available_thread[id]; -} - -/** - * @brief Get an upper bound on the number of available threads - * - * Gets an upper bound on the number of threads in the available threads set, - * useful for iterating over "thread_is_available()". - * - * @return The upper bound - */ -unsigned int Promise::max_available_thread_idx() const -{ - return available_thread.size(); -} - -/** @brief Print debug info about the Promise */ -void Promise::print() const -{ - model_print("Promised value %#" PRIx64 ", first read from thread %d, available threads to resolve: ", - fv.value, id_to_int(get_reader(0)->get_tid())); - bool failed = true; - for (unsigned int i = 0; i < available_thread.size(); i++) - if (available_thread[i]) { - model_print("[%d]", i); - failed = false; - } - if (failed) - model_print("(none)"); - model_print("\n"); -} - -/** - * Check if this promise has failed. A promise can fail when all threads which - * could possibly satisfy the promise have been eliminated. - * - * @return True, if this promise has failed; false otherwise - */ -bool Promise::has_failed() const -{ - return num_available_threads == 0; -} - -/** - * @brief Check if an action's thread and location are compatible for resolving - * this promise - * @param act The action to check against - * @return True if we are compatible; false otherwise - */ -bool Promise::is_compatible(const ModelAction *act) const -{ - return thread_is_available(act->get_tid()) && get_reader(0)->same_var(act); -} - -/** - * @brief Check if an action's thread and location are compatible for resolving - * this promise, and that the promise is thread-exclusive - * @param act The action to check against - * @return True if we are compatible and exclusive; false otherwise - */ -bool Promise::is_compatible_exclusive(const ModelAction *act) const -{ - return get_num_available_threads() == 1 && is_compatible(act); -} - -/** - * @brief Check if a store's value matches this Promise - * @param write The store to check - * @return True if the store's written value matches this Promise - */ -bool Promise::same_value(const ModelAction *write) const -{ - return get_value() == write->get_write_value(); -} - -/** - * @brief Check if a ModelAction's location matches this Promise - * @param act The ModelAction to check - * @return True if the action's location matches this Promise - */ -bool Promise::same_location(const ModelAction *act) const -{ - return get_reader(0)->same_var(act); -} - -/** @brief Get this Promise's index within the execution's promise array */ -int Promise::get_index() const -{ - return execution->get_promise_number(this); -} diff --git a/promise.h b/promise.h deleted file mode 100644 index e306e14a..00000000 --- a/promise.h +++ /dev/null @@ -1,78 +0,0 @@ -/** @file promise.h - * - * @brief Promise class --- tracks future obligations for execution - * related to weakly ordered writes. - */ - -#ifndef __PROMISE_H__ -#define __PROMISE_H__ - -#include - -#include "modeltypes.h" -#include "mymemory.h" -#include "stl-model.h" - -class ModelAction; -class ModelExecution; - -struct future_value { - uint64_t value; - modelclock_t expiration; - thread_id_t tid; -}; - -class Promise { - public: - Promise(const ModelExecution *execution, ModelAction *read, struct future_value fv); - bool add_reader(ModelAction *reader); - ModelAction * get_reader(unsigned int i) const; - unsigned int get_num_readers() const { return readers.size(); } - bool eliminate_thread(thread_id_t tid); - void add_thread(thread_id_t tid); - bool thread_is_available(thread_id_t tid) const; - bool thread_was_available(thread_id_t tid) const; - unsigned int max_available_thread_idx() const; - bool has_failed() const; - void set_write(const ModelAction *act) { write = act; } - const ModelAction * get_write() const { return write; } - int get_num_available_threads() const { return num_available_threads; } - int get_num_was_available_threads() const { return num_was_available_threads; } - bool is_compatible(const ModelAction *act) const; - bool is_compatible_exclusive(const ModelAction *act) const; - bool same_value(const ModelAction *write) const; - bool same_location(const ModelAction *act) const; - - modelclock_t get_expiration() const { return fv.expiration; } - uint64_t get_value() const { return fv.value; } - struct future_value get_fv() const { return fv; } - - int get_index() const; - - void print() const; - - bool equals(const Promise *x) const { return this == x; } - bool equals(const ModelAction *x) const { return false; } - - SNAPSHOTALLOC - private: - /** @brief The execution which created this Promise */ - const ModelExecution *execution; - - /** @brief Thread ID(s) for thread(s) that potentially can satisfy this - * promise */ - SnapVector available_thread; - SnapVector was_available_thread; - - int num_available_threads; - int num_was_available_threads; - - const future_value fv; - - /** @brief The action(s) which read the promised future value */ - SnapVector readers; - - const ModelAction *write; -}; - -#endif diff --git a/pthread.cc b/pthread.cc index dec0ddf7..723e60b5 100644 --- a/pthread.cc +++ b/pthread.cc @@ -93,7 +93,7 @@ int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t *) { cdsc::mutex *m = new cdsc::mutex(); ModelExecution *execution = model->get_execution(); - execution->mutex_map.put(p_mutex, m); + execution->getMutexMap()->put(p_mutex, m); return 0; } @@ -103,11 +103,11 @@ int pthread_mutex_lock(pthread_mutex_t *p_mutex) { /* to protect the case where PTHREAD_MUTEX_INITIALIZER is used instead of pthread_mutex_init, or where *p_mutex is not stored in the execution->mutex_map for some reason. */ - if (!execution->mutex_map.contains(p_mutex)) { + if (!execution->getMutexMap()->contains(p_mutex)) { pthread_mutex_init(p_mutex, NULL); } - cdsc::mutex *m = execution->mutex_map.get(p_mutex); + cdsc::mutex *m = execution->getMutexMap()->get(p_mutex); if (m != NULL) { m->lock(); @@ -120,12 +120,12 @@ int pthread_mutex_lock(pthread_mutex_t *p_mutex) { int pthread_mutex_trylock(pthread_mutex_t *p_mutex) { ModelExecution *execution = model->get_execution(); - cdsc::mutex *m = execution->mutex_map.get(p_mutex); + cdsc::mutex *m = execution->getMutexMap()->get(p_mutex); return m->try_lock(); } int pthread_mutex_unlock(pthread_mutex_t *p_mutex) { ModelExecution *execution = model->get_execution(); - cdsc::mutex *m = execution->mutex_map.get(p_mutex); + cdsc::mutex *m = execution->getMutexMap()->get(p_mutex); if (m != NULL) { m->unlock(); @@ -172,17 +172,17 @@ int pthread_cond_init(pthread_cond_t *p_cond, const pthread_condattr_t *attr) { cdsc::condition_variable *v = new cdsc::condition_variable(); ModelExecution *execution = model->get_execution(); - execution->cond_map.put(p_cond, v); + execution->getCondMap()->put(p_cond, v); return 0; } int pthread_cond_wait(pthread_cond_t *p_cond, pthread_mutex_t *p_mutex) { ModelExecution *execution = model->get_execution(); - if ( !execution->cond_map.contains(p_cond) ) + if ( !execution->getCondMap()->contains(p_cond) ) pthread_cond_init(p_cond, NULL); - cdsc::condition_variable *v = execution->cond_map.get(p_cond); - cdsc::mutex *m = execution->mutex_map.get(p_mutex); + cdsc::condition_variable *v = execution->getCondMap()->get(p_cond); + cdsc::mutex *m = execution->getMutexMap()->get(p_mutex); v->wait(*m); return 0; @@ -193,13 +193,13 @@ int pthread_cond_timedwait(pthread_cond_t *p_cond, // implement cond_timedwait as a noop and let the scheduler decide which thread goes next ModelExecution *execution = model->get_execution(); - if ( !execution->cond_map.contains(p_cond) ) + if ( !execution->getCondMap()->contains(p_cond) ) pthread_cond_init(p_cond, NULL); - if ( !execution->mutex_map.contains(p_mutex) ) + if ( !execution->getMutexMap()->contains(p_mutex) ) pthread_mutex_init(p_mutex, NULL); - cdsc::condition_variable *v = execution->cond_map.get(p_cond); - cdsc::mutex *m = execution->mutex_map.get(p_mutex); + cdsc::condition_variable *v = execution->getCondMap()->get(p_cond); + cdsc::mutex *m = execution->getMutexMap()->get(p_mutex); model->switch_to_master(new ModelAction(NOOP, std::memory_order_seq_cst, v, NULL)); // v->wait(*m); @@ -210,10 +210,10 @@ int pthread_cond_timedwait(pthread_cond_t *p_cond, int pthread_cond_signal(pthread_cond_t *p_cond) { // notify only one blocked thread ModelExecution *execution = model->get_execution(); - if ( !execution->cond_map.contains(p_cond) ) + if ( !execution->getCondMap()->contains(p_cond) ) pthread_cond_init(p_cond, NULL); - cdsc::condition_variable *v = execution->cond_map.get(p_cond); + cdsc::condition_variable *v = execution->getCondMap()->get(p_cond); v->notify_one(); return 0; diff --git a/schedule.cc b/schedule.cc index 2a02e307..63204f54 100644 --- a/schedule.cc +++ b/schedule.cc @@ -66,8 +66,6 @@ void Scheduler::set_enabled(Thread *t, enabled_type_t enabled_status) { enabled_len = threadid + 1; } enabled[threadid] = enabled_status; - if (enabled_status == THREAD_DISABLED) - execution->check_promises_thread_disabled(); } /** diff --git a/test/userprog.c b/test/userprog.c index 0ff8f125..415eb248 100644 --- a/test/userprog.c +++ b/test/userprog.c @@ -24,7 +24,7 @@ static void b(void *obj) printf("r2=%d\n",r2); } -int main(int argc, char **argv) +int user_main(int argc, char **argv) { thrd_t t1, t2;