#include "action.h"
#include "clockvector.h"
#include "common.h"
+#include "threads.h"
#define ACTION_INITIAL_CLOCK 0
value=VALUE_TRYFAILED;
}
-/** Update the model action's read_from action */
-void ModelAction::read_from(const ModelAction *act)
+/**
+ * Update the model action's read_from action
+ * @param act The action to read from; should be a write
+ * @return True if this read established synchronization
+ */
+bool ModelAction::read_from(const ModelAction *act)
{
ASSERT(cv);
reads_from = act;
if (act != NULL && this->is_acquire()) {
rel_heads_list_t release_heads;
model->get_release_seq_heads(this, &release_heads);
+ int num_heads = release_heads.size();
for (unsigned int i = 0; i < release_heads.size(); i++)
- if (!synchronize_with(release_heads[i]))
+ if (!synchronize_with(release_heads[i])) {
model->set_bad_synchronization();
+ num_heads--;
+ }
+ return num_heads > 0;
}
+ return false;
}
/**
return act->cv->synchronized_since(this);
}
-/**
- * Print nicely-formatted info about this ModelAction
- *
- * @param print_cv True if we want to print clock vector data. Might be false,
- * for instance, in situations where the clock vector might be invalid
- */
-void ModelAction::print(bool print_cv) const
+/** @brief Print nicely-formatted info about this ModelAction */
+void ModelAction::print() const
{
const char *type_str, *mo_str;
switch (this->type) {
else
printf(" Rf: ?");
}
- if (cv && print_cv) {
+ if (cv) {
printf("\t");
cv->print();
} else
#include <list>
#include <cstddef>
+#include <inttypes.h>
-#include "threads.h"
#include "mymemory.h"
-#include "clockvector.h"
#include "memoryorder.h"
+#include "modeltypes.h"
+
+class ClockVector;
using std::memory_order;
using std::memory_order_relaxed;
public:
ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value = VALUE_NONE);
~ModelAction();
- void print(bool print_cv = true) const;
+ void print() const;
thread_id_t get_tid() const { return tid; }
action_type get_type() const { return type; }
void create_cv(const ModelAction *parent = NULL);
ClockVector * get_cv() const { return cv; }
- void read_from(const ModelAction *act);
+ bool read_from(const ModelAction *act);
bool synchronize_with(const ModelAction *act);
bool has_synchronized_with(const ModelAction *act) const;
#include "action.h"
#include "clockvector.h"
#include "common.h"
+#include "threads.h"
/**
* Constructs a new ClockVector, given a parent ClockVector and a first
#ifndef __CLOCKVECTOR_H__
#define __CLOCKVECTOR_H__
-#include "threads.h"
#include "mymemory.h"
+#include "modeltypes.h"
-typedef unsigned int modelclock_t;
/* Forward declaration */
class ModelAction;
#include "model.h"
#include "cmodelint.h"
+#include "threads.h"
/** Performs a read action.*/
uint64_t model_read_action(void * obj, memory_order ord) {
#include <stdio.h>
#include <cstring>
#include "mymemory.h"
+#include "clockvector.h"
struct ShadowTable *root;
std::vector<struct DataRace *> unrealizedraces;
void printRace(struct DataRace * race) {
printf("Datarace detected\n");
printf("Location %p\n", race->address);
- printf("Initial access: thread %u clock %u, iswrite %u\n",race->oldthread,race->oldclock, race->isoldwrite);
- printf("Second access: thread %u clock %u, iswrite %u\n", race->newaction->get_tid(), race->newaction->get_seq_number() , race->isnewwrite);
+ printf("Initial access: thread %u clock %u, iswrite %u\n", id_to_int(race->oldthread), race->oldclock, race->isoldwrite);
+ printf("Second access: thread %u clock %u, iswrite %u\n", id_to_int(race->newaction->get_tid()), race->newaction->get_seq_number(), race->isnewwrite);
}
/** This function does race detection for a write on an expanded record. */
#ifndef DATARACE_H
#include "config.h"
#include <stdint.h>
-#include "clockvector.h"
#include <vector>
+#include "modeltypes.h"
+
+/* Forward declaration */
+class ClockVector;
+class ModelAction;
struct ShadowTable {
void * array[65536];
#include "impatomic.h"
#include "common.h"
#include "model.h"
+#include "threads.h"
namespace std {
#include "common.h"
#include "datarace.h"
#include "model.h"
+#include "threads.h"
void store_8(void *addr, uint8_t val)
{
int thrd_join(thrd_t t)
{
Thread *th = model->get_thread(thrd_to_id(t));
- model->switch_to_master(new ModelAction(THREAD_JOIN, std::memory_order_seq_cst, th, thrd_to_id(t)));
+ model->switch_to_master(new ModelAction(THREAD_JOIN, std::memory_order_seq_cst, th, id_to_int(thrd_to_id(t))));
return 0;
}
#include "promise.h"
#include "datarace.h"
#include "mutex.h"
+#include "threads.h"
#define INITIAL_THREAD_ID 0
return priv->next_thread_id;
}
+/** @return The currently executing Thread. */
+Thread * ModelChecker::get_current_thread()
+{
+ return scheduler->get_current_thread();
+}
+
/** @return a sequence number for a new ModelAction */
modelclock_t ModelChecker::get_next_seq_num()
{
} else {
tid = next->get_tid();
}
- DEBUG("*** ModelChecker chose next thread = %d ***\n", tid);
+ DEBUG("*** ModelChecker chose next thread = %d ***\n", id_to_int(tid));
ASSERT(tid != THREAD_ID_T_NONE);
return thread_map->get(id_to_int(tid));
}
if (isfinalfeasible()) {
printf("Earliest divergence point since last feasible execution:\n");
if (earliest_diverge)
- earliest_diverge->print(false);
+ earliest_diverge->print();
else
printf("(Not set)\n");
if (!node->set_backtrack(tid))
continue;
DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
- prev->get_tid(), t->get_id());
+ id_to_int(prev->get_tid()),
+ id_to_int(t->get_id()));
if (DBG_ENABLED()) {
prev->print();
act->print();
/** Close out a RMWR by converting previous RMWR into a RMW or READ. */
ModelAction * ModelChecker::process_rmw(ModelAction *act) {
- int tid = id_to_int(act->get_tid());
- ModelAction *lastread = get_last_action(tid);
+ ModelAction *lastread = get_last_action(act->get_tid());
lastread->process_rmw(act);
if (act->is_rmw() && lastread->get_reads_from()!=NULL) {
mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
* @return true, if the ModelChecker is certain that release_heads is complete;
* false otherwise
*/
-bool ModelChecker::release_seq_head(const ModelAction *rf, rel_heads_list_t *release_heads) const
+bool ModelChecker::release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const
{
/* Only check for release sequences if there are no cycles */
if (mo_graph->checkForCycles())
ModelAction *last = get_last_action(int_to_id(i));
if (last && (rf->happens_before(last) ||
- last->get_type() == THREAD_FINISH))
+ get_thread(int_to_id(i))->is_complete()))
future_ordered = true;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
* @param act The 'acquire' action that may read from a release sequence
* @param release_heads A pass-by-reference return parameter. Will be filled
* with the head(s) of the release sequence(s), if they exists with certainty.
- * @see ModelChecker::release_seq_head
+ * @see ModelChecker::release_seq_heads
*/
void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads)
{
const ModelAction *rf = act->get_reads_from();
bool complete;
- complete = release_seq_head(rf, release_heads);
+ complete = release_seq_heads(rf, release_heads);
if (!complete) {
/* add act to 'lazy checking' list */
pending_acq_rel_seq->push_back(act);
const ModelAction *rf = act->get_reads_from();
rel_heads_list_t release_heads;
bool complete;
- complete = release_seq_head(rf, &release_heads);
+ complete = release_seq_heads(rf, &release_heads);
for (unsigned int i = 0; i < release_heads.size(); i++) {
if (!act->has_synchronized_with(release_heads[i])) {
if (act->synchronize_with(release_heads[i]))
scheduler->remove_thread(t);
}
+/**
+ * @brief Get a Thread reference by its ID
+ * @param tid The Thread's ID
+ * @return A Thread reference
+ */
+Thread * ModelChecker::get_thread(thread_id_t tid) const
+{
+ return thread_map->get(id_to_int(tid));
+}
+
+/**
+ * @brief Get a reference to the Thread in which a ModelAction was executed
+ * @param act The ModelAction
+ * @return A Thread reference
+ */
+Thread * ModelChecker::get_thread(ModelAction *act) const
+{
+ return get_thread(act->get_tid());
+}
+
/**
* Switch from a user-context to the "master thread" context (a.k.a. system
* context). This switch is made with the intention of exploring a particular
* model-checking action (described by a ModelAction object). Must be called
* from a user-thread context.
- * @param act The current action that will be explored. Must not be NULL.
+ *
+ * @param act The current action that will be explored. May be NULL only if
+ * trace is exiting via an assertion (see ModelChecker::set_assert and
+ * ModelChecker::has_asserted).
* @return Return status from the 'swap' call (i.e., success/fail, 0/-1)
*/
int ModelChecker::switch_to_master(ModelAction *act)
if (has_asserted())
return false;
- Thread * curr = thread_current();
+ Thread *curr = thread_current();
if (curr) {
if (curr->get_state() == THREAD_READY) {
ASSERT(priv->current_action);
ASSERT(false);
}
}
- Thread * next = scheduler->next_thread(priv->nextThread);
+ Thread *next = scheduler->next_thread(priv->nextThread);
/* Infeasible -> don't take any more steps */
if (!isfeasible())
return false;
- if (next)
- next->set_state(THREAD_RUNNING);
- DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1);
+ DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1,
+ next ? id_to_int(next->get_id()) : -1);
/* next == NULL -> don't take any more steps */
if (!next)
return false;
- if ( next->get_pending() != NULL ) {
- //restart a pending action
+ next->set_state(THREAD_RUNNING);
+
+ if (next->get_pending() != NULL) {
+ /* restart a pending action */
set_current_action(next->get_pending());
next->set_pending(NULL);
next->set_state(THREAD_READY);
#include <cstddef>
#include <ucontext.h>
-#include "schedule.h"
#include "mymemory.h"
-#include "libthreads.h"
-#include "threads.h"
#include "action.h"
-#include "clockvector.h"
#include "hashtable.h"
#include "workqueue.h"
#include "config.h"
+#include "modeltypes.h"
/* Forward declaration */
class NodeStack;
class CycleGraph;
class Promise;
+class Scheduler;
+class Thread;
/** @brief Shorthand for a list of release sequence heads */
typedef std::vector< const ModelAction *, ModelAlloc<const ModelAction *> > rel_heads_list_t;
void add_thread(Thread *t);
void remove_thread(Thread *t);
- Thread * get_thread(thread_id_t tid) { return thread_map->get(id_to_int(tid)); }
- Thread * get_thread(ModelAction *act) { return get_thread(act->get_tid()); }
+ Thread * get_thread(thread_id_t tid) const;
+ Thread * get_thread(ModelAction *act) const;
thread_id_t get_next_id();
int get_num_threads();
-
- /** @return The currently executing Thread. */
- Thread * get_current_thread() { return scheduler->get_current_thread(); }
+ Thread * get_current_thread();
int switch_to_master(ModelAction *act);
ClockVector * get_cv(thread_id_t tid);
void post_r_modification_order(ModelAction *curr, const ModelAction *rf);
bool r_modification_order(ModelAction *curr, const ModelAction *rf);
bool w_modification_order(ModelAction *curr);
- bool release_seq_head(const ModelAction *rf, rel_heads_list_t *release_heads) const;
+ bool release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const;
bool resolve_release_sequences(void *location, work_queue_t *work_queue);
void do_complete_join(ModelAction *join);
--- /dev/null
+#ifndef __MODELTYPES_H__
+#define __MODELTYPES_H__
+
+typedef int thread_id_t;
+
+#define THREAD_ID_T_NONE -1
+
+typedef unsigned int modelclock_t;
+
+#endif /* __MODELTYPES_H__ */
#include "mutex.h"
#include "model.h"
+#include "threads.h"
+#include "clockvector.h"
namespace std {
mutex::mutex() {
#ifndef MUTEX_H
#define MUTEX_H
-#include "threads.h"
-#include "clockvector.h"
+
+#include "modeltypes.h"
namespace std {
struct mutex_state {
#include "action.h"
#include "common.h"
#include "model.h"
+#include "threads.h"
/**
* @brief Node constructor
return thread_id < num_threads && enabled_array[thread_id];
}
+bool Node::has_priority(thread_id_t tid)
+{
+ return fairness[id_to_int(tid)].priority;
+}
+
/**
* Add an action to the may_read_from set.
* @param act is the action to add
#include <list>
#include <vector>
#include <cstddef>
-#include "threads.h"
+#include <inttypes.h>
+
#include "mymemory.h"
-#include "clockvector.h"
+#include "modeltypes.h"
class ModelAction;
+class Thread;
/**
* A flag used for the promise counting/combination problem within a node,
bool is_enabled(Thread *t);
bool is_enabled(thread_id_t tid);
ModelAction * get_action() { return action; }
- bool has_priority(thread_id_t tid) {return fairness[id_to_int(tid)].priority;}
+ bool has_priority(thread_id_t tid);
int get_num_threads() {return num_threads;}
/** @return the parent Node to this Node; that is, the action that
* occurred previously in the stack. */
*/
void Scheduler::add_thread(Thread *t)
{
- DEBUG("thread %d\n", t->get_id());
+ DEBUG("thread %d\n", id_to_int(t->get_id()));
set_enabled(t, true);
}
void Scheduler::print() const
{
if (current)
- DEBUG("Current thread: %d\n", current->get_id());
+ DEBUG("Current thread: %d\n", id_to_int(current->get_id()));
else
DEBUG("No current thread\n");
}
void Thread::complete()
{
if (!is_complete()) {
- DEBUG("completed thread %d\n", get_id());
+ DEBUG("completed thread %d\n", id_to_int(get_id()));
state = THREAD_COMPLETED;
if (stack)
stack_free(stack);
#include "mymemory.h"
#include "libthreads.h"
-
-typedef int thread_id_t;
-
-#define THREAD_ID_T_NONE -1
+#include "modeltypes.h"
/** @brief Represents the state of a user Thread */
typedef enum thread_state {