#include <stdio.h>
#include <algorithm>
-#include <mutex>
#include <new>
#include <stdarg.h>
#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),
too_many_reads(false),
no_valid_reads(false),
bad_synchronization(false),
+ bad_sc_read(false),
asserted(false)
{ }
modelclock_t used_sequence_numbers;
ModelAction *next_backtrack;
SnapVector<bug_message *> bugs;
- bool failed_promise;
bool too_many_reads;
bool no_valid_reads;
/** @brief Incorrectly-ordered synchronization was made */
bool bad_synchronization;
+ bool bad_sc_read;
bool asserted;
SNAPSHOTALLOC
/** @brief Constructor */
ModelExecution::ModelExecution(ModelChecker *m,
- struct model_params *params,
+ 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),
obj_map(),
condvar_waiters_map(),
obj_thrd_map(),
- promises(),
- futurevalues(),
+ mutex_map(),
+ cond_map(),
pending_rel_seqs(),
thrd_last_action(1),
thrd_last_fence_release(),
mo_graph(new CycleGraph())
{
/* Initialize a model-checker thread, for special ModelActions */
- model_thread = new Thread(get_next_id());
- add_thread(model_thread);
+ model_thread = new Thread(get_next_id()); // L: Create model thread
+ add_thread(model_thread); // L: Add model thread to scheduler
scheduler->register_engine(this);
+ node_stack->register_engine(this);
}
/** @brief Destructor */
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;
}
priv->bad_synchronization = true;
}
+/** @brief Alert the model-checker that an incorrectly-ordered
+ * synchronization was made */
+void ModelExecution::set_bad_sc_read()
+{
+ priv->bad_sc_read = true;
+}
+
bool ModelExecution::assert_bug(const char *msg)
{
priv->bugs.push_back(new bug_message(msg));
return blocking_threads;
}
+/**
+ * @brief Check if we are yield-blocked
+ *
+ * A program can be "yield-blocked" if all threads are ready to execute a
+ * yield.
+ *
+ * @return True if the program is yield-blocked; false otherwise
+ */
+bool ModelExecution::is_yieldblocked() const
+{
+ if (!params->yieldblock)
+ return false;
+
+ for (unsigned int i = 0; i < get_num_threads(); i++) {
+ thread_id_t tid = int_to_id(i);
+ Thread *t = get_thread(tid);
+ if (t->get_pending() && t->get_pending()->is_yield())
+ return true;
+ }
+ return false;
+}
+
/**
* Check if this is a complete execution. That is, have all thread completed
* execution (rather than exiting because sleep sets have forced a redundant
*/
bool ModelExecution::is_complete_execution() const
{
+ if (is_yieldblocked())
+ return false;
for (unsigned int i = 0; i < get_num_threads(); i++)
if (is_enabled(int_to_id(i)))
return false;
ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
{
switch (act->get_type()) {
- /* case ATOMIC_FENCE: fences don't directly cause backtracking */
+ case ATOMIC_FENCE:
+ /* Only seq-cst fences can (directly) cause backtracking */
+ if (!act->is_seqcst())
+ break;
case ATOMIC_READ:
case ATOMIC_WRITE:
case ATOMIC_RMW: {
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
+ if (prev == act)
+ continue;
if (prev->could_synchronize_with(act)) {
ret = prev;
break;
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:
*/
bool ModelExecution::process_mutex(ModelAction *curr)
{
- std::mutex *mutex = curr->get_mutex();
- struct std::mutex_state *state = NULL;
+ cdsc::mutex *mutex = curr->get_mutex();
+ struct cdsc::mutex_state *state = NULL;
if (mutex)
state = mutex->get_state();
action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
int wakeupthread = curr->get_node()->get_misc();
action_list_t::iterator it = waiters->begin();
+
+ // WL
+ if (it == waiters->end())
+ break;
+
advance(it, wakeupthread);
scheduler->wake(get_thread(*it));
waiters->erase(it);
return false;
}
-/**
- * @brief Check if the current pending promises allow a future value to be sent
- *
- * If one of the following is true:
- * (a) there are no pending promises
- * (b) the reader and writer do not cross any promises
- * Then, it is safe to pass a future value back now.
- *
- * Otherwise, we must save the pending future value until (a) or (b) is true
- *
- * @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
-{
- if (promises.empty())
- return true;
- 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
+ * @param work The work queue, for adding fixup work
* @return True if the mo_graph was updated or promises were resolved
*/
-bool ModelExecution::process_write(ModelAction *curr)
+bool ModelExecution::process_write(ModelAction *curr, work_queue_t *work)
{
/* 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);
- } 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;
}
/**
thrd_t *thrd = (thrd_t *)curr->get_location();
struct thread_params *params = (struct thread_params *)curr->get_value();
Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(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: {
+ (*(pthread_t *)curr->get_location()) = pthread_counter++;
+
+ struct pthread_params *params = (struct pthread_params *)curr->get_value();
+ Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
+ curr->set_thread_operand(th);
+ add_thread(th);
+ th->set_creation(curr);
+
+ if ( pthread_map.size() < pthread_counter )
+ pthread_map.resize( pthread_counter );
+ pthread_map[ pthread_counter-1 ] = th;
+
break;
}
case THREAD_JOIN: {
updated = true; /* trigger rel-seq checks */
break;
}
+ case PTHREAD_JOIN: {
+ Thread *blocking = curr->get_thread_operand();
+ ModelAction *act = get_last_action(blocking->get_id());
+ synchronize(act, curr);
+ updated = true; /* trigger rel-seq checks */
+ break; // WL: to be add (modified)
+ }
+
case THREAD_FINISH: {
Thread *th = get_thread(curr);
/* Wake up any joining threads */
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:
/* Must synchronize */
if (!synchronize(release, acquire))
return;
- /* Re-check all pending release sequences */
- work_queue->push_back(CheckRelSeqWorkEntry(NULL));
- /* Re-check act for mo_graph edges */
- work_queue->push_back(MOEdgeWorkEntry(acquire));
-
- /* propagate synchronization to later actions */
- action_list_t::reverse_iterator rit = action_trace.rbegin();
- for (; (*rit) != acquire; rit++) {
- ModelAction *propagate = *rit;
- if (acquire->happens_before(propagate)) {
- synchronize(acquire, propagate);
- /* Re-check 'propagate' for mo_graph edges */
- work_queue->push_back(MOEdgeWorkEntry(propagate));
- }
- }
+
+ /* Propagate the changed clock vector */
+ propagate_clockvector(acquire, work_queue);
} else {
/* Break release sequence with new edges:
* release --mo--> write --mo--> rf */
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);
*
* @return True if this read established synchronization
*/
+
bool ModelExecution::read_from(ModelAction *act, const ModelAction *rf)
{
ASSERT(rf);
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.
*
- * Checks whether a lock or join operation would be successful (i.e., is the
- * lock already locked, or is the joined thread already complete). If not, put
- * the action in a waiter list.
+ * Checks whether an operation would be successful (i.e., is a lock already
+ * locked, or is the joined thread already complete).
+ *
+ * For yield-blocking, yields are never enabled.
*
* @param curr is the ModelAction to check whether it is enabled.
* @return a bool that indicates whether the action is enabled.
*/
bool ModelExecution::check_action_enabled(ModelAction *curr) {
if (curr->is_lock()) {
- std::mutex *lock = curr->get_mutex();
- struct std::mutex_state *state = lock->get_state();
+ cdsc::mutex *lock = curr->get_mutex();
+ struct cdsc::mutex_state *state = lock->get_state();
if (state->locked)
return false;
} 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()) {
+ return false;
}
return true;
*
* @param curr The current action to process
* @return The ModelAction that is actually executed; may be different than
- * curr; may be NULL, if the current action is not enabled to run
+ * curr
*/
ModelAction * ModelExecution::check_current_action(ModelAction *curr)
{
if (act->is_read() && !second_part_of_rmw && process_read(act))
update = true;
- if (act->is_write() && process_write(act))
+ if (act->is_write() && process_write(act, &work_queue))
update = true;
if (act->is_fence() && process_fence(act))
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;
- } 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)
- ptr += sprintf(ptr, "[failed promise]");
if (priv->too_many_reads)
ptr += sprintf(ptr, "[too many reads]");
if (priv->no_valid_reads)
ptr += sprintf(ptr, "[no valid reads-from]");
if (priv->bad_synchronization)
ptr += sprintf(ptr, "[bad sw ordering]");
- if (promises_expired())
- ptr += sprintf(ptr, "[promise expired]");
- if (promises.size() != 0)
- ptr += sprintf(ptr, "[unresolved promise]");
+ if (priv->bad_sc_read)
+ ptr += sprintf(ptr, "[bad sc read]");
if (ptr != buf)
- model_print("%s: %s\n", prefix ? prefix : "Infeasible", buf);
+ model_print("%s: %s", prefix ? prefix : "Infeasible", buf);
}
/**
*/
bool ModelExecution::is_feasible_prefix_ignore_relseq() const
{
- return !is_infeasible() && promises.size() == 0;
+ return !is_infeasible() ;
+
}
/**
{
return mo_graph->checkForCycles() ||
priv->no_valid_reads ||
- priv->failed_promise ||
priv->too_many_reads ||
priv->bad_synchronization ||
- 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;
}
}
}
- /* C++, Section 29.3 statement 3 (second subpoint) */
- if (curr->is_seqcst() && last_sc_write && act == last_sc_write) {
- added = mo_graph->addEdge(act, rf) || added;
- break;
- }
-
/*
* Include at most one act per-thread that "happens
* before" curr
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)
- continue;
- 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) &&
pendingfuturevalue.
*/
- if (send_fv && thin_air_constraint_may_allow(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;
}
-/** 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
* require compiler support):
*
* If X --hb-> Y --mo-> Z, then X should not read from Z.
+ * If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
*/
bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
{
}
}
+/**
+ * @brief Propagate a modified clock vector to actions later in the execution
+ * order
+ *
+ * After an acquire operation lazily completes a release-sequence
+ * synchronization, we must update all clock vectors for operations later than
+ * the acquire in the execution order.
+ *
+ * @param acquire The ModelAction whose clock vector must be propagated
+ * @param work The work queue to which we can add work items, if this
+ * propagation triggers more updates (e.g., to the modification order)
+ */
+void ModelExecution::propagate_clockvector(ModelAction *acquire, work_queue_t *work)
+{
+ /* Re-check all pending release sequences */
+ work->push_back(CheckRelSeqWorkEntry(NULL));
+ /* Re-check read-acquire for mo_graph edges */
+ work->push_back(MOEdgeWorkEntry(acquire));
+
+ /* propagate synchronization to later actions */
+ action_list_t::reverse_iterator rit = action_trace.rbegin();
+ for (; (*rit) != acquire; rit++) {
+ ModelAction *propagate = *rit;
+ if (acquire->happens_before(propagate)) {
+ synchronize(acquire, propagate);
+ /* Re-check 'propagate' for mo_graph edges */
+ work->push_back(MOEdgeWorkEntry(propagate));
+ }
+ }
+}
+
/**
* Attempt to resolve all stashed operations that might synchronize with a
* release sequence for a given location. This implements the "lazy" portion of
updated = true;
if (updated) {
- /* Re-check all pending release sequences */
- work_queue->push_back(CheckRelSeqWorkEntry(NULL));
- /* Re-check read-acquire for mo_graph edges */
- if (acquire->is_read())
- work_queue->push_back(MOEdgeWorkEntry(acquire));
-
- /* propagate synchronization to later actions */
- action_list_t::reverse_iterator rit = action_trace.rbegin();
- for (; (*rit) != acquire; rit++) {
- ModelAction *propagate = *rit;
- if (acquire->happens_before(propagate)) {
- synchronize(acquire, propagate);
- /* Re-check 'propagate' for mo_graph edges */
- work_queue->push_back(MOEdgeWorkEntry(propagate));
- }
- }
+ /* Propagate the changed clock vector */
+ propagate_clockvector(acquire, work_queue);
}
if (complete) {
it = pending_rel_seqs.erase(it);
ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
{
void *location = curr->get_location();
+
action_list_t *list = obj_map.get(location);
/* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
action_list_t::reverse_iterator rit;
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
- * @return True if the Promise was successfully resolved; false otherwise
- */
-bool ModelExecution::resolve_promise(ModelAction *write, Promise *promise)
-{
- ModelVector<ModelAction *> actions_to_check;
-
- for (unsigned int i = 0; i < promise->get_num_readers(); i++) {
- ModelAction *read = promise->get_reader(i);
- read_from(read, write);
- 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->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->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->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;
{
action_list_t::const_iterator it;
- model_print("---------------------------------------------------------------------\n");
+ model_print("------------------------------------------------------------------------------------\n");
+ model_print("# t Action type MO Location Value Rf CV\n");
+ model_print("------------------------------------------------------------------------------------\n");
unsigned int hash = 0;
hash = hash^(hash<<3)^((*it)->hash());
}
model_print("HASH %u\n", hash);
- model_print("---------------------------------------------------------------------\n");
+ model_print("------------------------------------------------------------------------------------\n");
}
#if SUPPORT_MOD_ORDER_DUMP
mo_graph->dumpNodes(file);
ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
- for (action_list_t::iterator it = action_trace.begin(); it != action_trace.end(); it++) {
+ for (action_list_t::const_iterator it = action_trace.begin(); it != action_trace.end(); it++) {
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,
dumpGraph(buffername);
#endif
- model_print("Execution %d:", get_execution_number());
+ model_print("Execution trace %d:", get_execution_number());
if (isfeasibleprefix()) {
+ if (is_yieldblocked())
+ model_print(" YIELD BLOCKED");
if (scheduler->all_threads_sleeping())
model_print(" SLEEP-SET REDUNDANT");
- model_print("\n");
+ if (have_bug_reports())
+ model_print(" DETECTED BUG(S)");
} else
print_infeasibility(" INFEASIBLE");
+ model_print("\n");
+
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");
- }
+
}
/**
}
/**
- * @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
+ * @brief Get a Thread reference by its pthread ID
+ * @param index The pthread's ID
+ * @return A Thread reference
*/
-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;
+Thread * ModelExecution::get_pthread(pthread_t pid) {
+ if (pid < pthread_counter + 1) return pthread_map[pid];
+ else return NULL;
}
/**
/* Do not split atomic RMW */
if (curr->is_rmwr())
return get_thread(curr);
+ if (curr->is_write()) {
+// std::memory_order order = curr->get_mo();
+// switch(order) {
+// case std::memory_order_relaxed:
+// return get_thread(curr);
+// case std::memory_order_release:
+// return get_thread(curr);
+// defalut:
+// return NULL;
+// }
+ return NULL;
+ }
+
/* Follow CREATE with the created thread */
+ /* which is not needed, because model.cc takes care of this */
if (curr->get_type() == THREAD_CREATE)
+ return curr->get_thread_operand();
+ if (curr->get_type() == PTHREAD_CREATE) {
return curr->get_thread_operand();
+ }
return NULL;
}
{
while (!pending_rel_seqs.empty() &&
is_feasible_prefix_ignore_relseq() &&
- !unrealizedraces.empty()) {
+ haveUnrealizedRaces()) {
model_print("*** WARNING: release sequence fixup action "
"(%zu pending release seuqence(s)) ***\n",
pending_rel_seqs.size());
projects / c11tester.git / blobdiff