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.
location(loc),
value(value),
reads_from(NULL),
- reads_from_promise(NULL),
last_fence_release(NULL),
node(NULL),
seq_number(ACTION_INITIAL_CLOCK),
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 */
}
ASSERT(act);
reads_from = act;
- reads_from_promise = NULL;
if (act->is_uninitialized()) { // WL
uint64_t val = *((uint64_t *) location);
}
}
-/**
- * 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.
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) {
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;
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
/* Forward declarations */
class ClockVector;
class Thread;
-class Promise;
namespace cdsc {
class mutex;
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 */
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; }
*/
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;
#include "cyclegraph.h"
#include "action.h"
#include "common.h"
-#include "promise.h"
#include "threads-model.h"
/** Initializes a CycleGraph object. */
#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
*
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
}
/* 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
}
/* 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)
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
/* 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()
*/
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)
{
}
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());
-}
#include "mymemory.h"
#include "stl-model.h"
-class Promise;
class CycleNode;
class ModelAction;
void addRMWEdge(const T *from, const ModelAction *rmw);
bool checkForCycles() const;
- bool checkPromise(const ModelAction *from, Promise *p) const;
template <typename T, typename U>
bool checkReachable(const T *from, const U *to) const;
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<const CycleNode *, const CycleNode *, uintptr_t, 4, model_malloc, model_calloc, model_free> *discovered;
/** @brief A table for mapping ModelActions to CycleNodes */
HashTable<const ModelAction *, CycleNode *, uintptr_t, 4> actionToNode;
- /** @brief A table for mapping Promises to CycleNodes */
- HashTable<const Promise *, CycleNode *, uintptr_t, 4> promiseToNode;
#if SUPPORT_MOD_ORDER_DUMP
SnapVector<CycleNode *> nodeList;
};
/**
- * @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;
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<CycleNode *> edges;
#include "common.h"
#include "clockvector.h"
#include "cyclegraph.h"
-#include "promise.h"
#include "datarace.h"
#include "threads-model.h"
#include "bugmessage.h"
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),
modelclock_t used_sequence_numbers;
ModelAction *next_backtrack;
SnapVector<bug_message *> bugs;
- bool failed_promise;
- bool hard_failed_promise;
bool too_many_reads;
bool no_valid_reads;
/** @brief Incorrectly-ordered synchronization was made */
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(),
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;
}
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:
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
/* Readers to which we may send our future value */
ModelVector<ModelAction *> 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;
}
/**
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: {
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: {
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:
newcurr = process_rmw(*curr);
delete *curr;
- if (newcurr->is_rmw())
- compute_promises(newcurr);
-
*curr = newcurr;
return false;
}
* 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);
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.
*
} 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()) {
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();
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
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)
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);
}
*/
bool ModelExecution::is_feasible_prefix_ignore_relseq() const
{
- return !is_infeasible() && promises.size() == 0 && ! priv->failed_promise;
+ return !is_infeasible() ;
}
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. */
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;
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<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
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++) {
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;
}
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;
}
* 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;
}
* 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<ModelAction *> *send_fv)
+bool ModelExecution::w_modification_order(ModelAction *curr)
{
SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
unsigned int i;
added = mo_graph->addEdge(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) &&
*/
- if (send_fv && thin_air_constraint_may_allow(curr, act) && check_coherence_promise(curr, act)) {
- if (!is_infeasible())
- send_fv->push_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;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;
-}
-
-
-/** 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
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<ModelAction *> 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
}
}
- /* 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;
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,
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");
- }
}
/**
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
class Node;
class NodeStack;
class CycleGraph;
-class Promise;
class Scheduler;
class Thread;
class ClockVector;
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;
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;
action_list_t * get_action_trace() { return &action_trace; }
CycleGraph * const get_mo_graph() { return mo_graph; }
-
- HashTable<pthread_mutex_t *, cdsc::mutex *, uintptr_t, 4> mutex_map;
- HashTable<pthread_cond_t *, cdsc::condition_variable *, uintptr_t, 4> cond_map;
-
+ HashTable<pthread_cond_t *, cdsc::condition_variable *, uintptr_t, 4> * getCondMap() {return &cond_map;}
+ HashTable<pthread_mutex_t *, cdsc::mutex *, uintptr_t, 4> * getMutexMap() {return &mutex_map;}
+
SNAPSHOTALLOC
private:
int get_execution_number() const;
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();
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;
template <typename rf_type>
bool r_modification_order(ModelAction *curr, const rf_type *rf);
- bool w_modification_order(ModelAction *curr, ModelVector<ModelAction *> *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;
HashTable<void *, SnapVector<action_list_t> *, uintptr_t, 4> obj_thrd_map;
-// HashTable<pthread_mutex_t *, cdsc::mutex *, uintptr_t, 4> mutex_map;
-
- /**
- * @brief List of currently-pending promises
- *
- * Promises are sorted by the execution order of the read(s) which
- * created them
- */
- SnapVector<Promise *> promises;
- SnapVector<struct PendingFutureValue> futurevalues;
+ HashTable<pthread_mutex_t *, cdsc::mutex *, uintptr_t, 4> mutex_map;
+ HashTable<pthread_cond_t *, cdsc::condition_variable *, uintptr_t, 4> cond_map;
/**
* List of pending release sequences. Release sequences might be
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;
{
// 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();
}
/** @brief Run ModelChecker for the user program */
void ModelChecker::run()
{
- bool has_next;
int i = 0;
do {
thrd_t user_thread;
t = execution->take_step(curr);
} while (!should_terminate_execution());
- has_next = next_execution();
+ next_execution();
i++;
} while (i<2); // while (has_next);
class Node;
class NodeStack;
class CycleGraph;
-class Promise;
class Scheduler;
class Thread;
class ClockVector;
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),
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");
}
/************************** 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;
/**
* 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()
{
*/
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;
*/
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 ********************************/
/************************** 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 ***************************/
/**
/* 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;
#include "mymemory.h"
#include "schedule.h"
-#include "promise.h"
#include "stl-model.h"
class ModelAction;
*/
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;
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);
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;
ModelVector<const ModelAction *> read_from_past;
unsigned int read_from_past_idx;
- ModelVector<const ModelAction *> read_from_promises;
- int read_from_promise_idx;
-
- ModelVector<struct future_value> future_values;
- int future_index;
-
- ModelVector<bool> resolve_promise;
- int resolve_promise_idx;
-
ModelVector<const ModelAction *> relseq_break_writes;
int relseq_break_index;
+++ /dev/null
-#define __STDC_FORMAT_MACROS
-#include <inttypes.h>
-
-#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);
-}
+++ /dev/null
-/** @file promise.h
- *
- * @brief Promise class --- tracks future obligations for execution
- * related to weakly ordered writes.
- */
-
-#ifndef __PROMISE_H__
-#define __PROMISE_H__
-
-#include <inttypes.h>
-
-#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<bool> available_thread;
- SnapVector<bool> 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<ModelAction *> readers;
-
- const ModelAction *write;
-};
-
-#endif
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;
}
/* 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();
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();
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;
// 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);
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;
enabled_len = threadid + 1;
}
enabled[threadid] = enabled_status;
- if (enabled_status == THREAD_DISABLED)
- execution->check_promises_thread_disabled();
}
/**
printf("r2=%d\n",r2);
}
-int main(int argc, char **argv)
+int user_main(int argc, char **argv)
{
thrd_t t1, t2;
projects / c11tester.git / commitdiff