include common.mk
OBJECTS := libthreads.o schedule.o model.o threads.o librace.o action.o \
- nodestack.o clockvector.o main.o snapshot-interface.o cyclegraph.o \
+ 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 conditionvariable.o \
context.o execution.o libannotate.o plugins.o pthread.o futex.o fuzzer.o \
#include "clockvector.h"
#include "common.h"
#include "threads-model.h"
-#include "nodestack.h"
#include "wildcard.h"
#define ACTION_INITIAL_CLOCK 0
position(NULL),
reads_from(NULL),
last_fence_release(NULL),
- node(NULL),
+ uninitaction(NULL),
cv(NULL),
+ rf_cv(NULL),
value(value),
type(type),
order(order),
position(NULL),
reads_from(NULL),
last_fence_release(NULL),
- node(NULL),
+ uninitaction(NULL),
cv(NULL),
+ rf_cv(NULL),
value(value),
type(type),
order(order),
position(position),
reads_from(NULL),
last_fence_release(NULL),
- node(NULL),
+ uninitaction(NULL),
cv(NULL),
+ rf_cv(NULL),
value(value),
type(type),
order(order),
position(position),
reads_from(NULL),
last_fence_release(NULL),
- node(NULL),
+ uninitaction(NULL),
cv(NULL),
+ rf_cv(NULL),
value(value),
type(type),
order(order),
return value;
}
-/** @return The Node associated with this ModelAction */
-Node * ModelAction::get_node() const
-{
- /* UNINIT actions do not have a Node */
- ASSERT(!is_uninitialized());
- return node;
-}
-
/**
* Update the model action's read_from action
* @param act The action to read from; should be a write
*/
-void ModelAction::set_read_from(const ModelAction *act)
+void ModelAction::set_read_from(ModelAction *act)
{
ASSERT(act);
uint64_t val = *((uint64_t *) location);
ModelAction * act_initialized = (ModelAction *)act;
act_initialized->set_value(val);
- reads_from = (const ModelAction *)act_initialized;
+ reads_from = act_initialized;
// disabled by WL, because LLVM IR is unable to detect atomic init
/* model->assert_bug("May read from uninitialized atomic:\n"
uint64_t get_reads_from_value() const;
uint64_t get_write_value() const;
uint64_t get_return_value() const;
- const ModelAction * get_reads_from() const { return reads_from; }
+ ModelAction * get_reads_from() const { return reads_from; }
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(ModelAction *act);
/** Store the most recent fence-release from the same thread
* @param fence The fence-release that occured prior to this */
Thread * get_thread_operand() const;
void create_cv(const ModelAction *parent = NULL);
ClockVector * get_cv() const { return cv; }
+ ClockVector * get_rfcv() const { return rf_cv; }
+ void set_rfcv(ClockVector * rfcv) { rf_cv = rfcv; }
bool synchronize_with(const ModelAction *act);
bool has_synchronized_with(const ModelAction *act) const;
/* to accomodate pthread create and join */
Thread * thread_operand;
void set_thread_operand(Thread *th) { thread_operand = th; }
+ void set_uninit_action(ModelAction *act) { uninitaction = act; }
+ ModelAction * get_uninit_action() { return uninitaction; }
SNAPSHOTALLOC
private:
const char * get_type_str() const;
*
* Only valid for reads
*/
- const ModelAction *reads_from;
+ ModelAction *reads_from;
int size;
};
/** @brief The last fence release from the same thread */
const ModelAction *last_fence_release;
-
- /**
- * @brief A back reference to a Node in NodeStack
- *
- * Only set if this ModelAction is saved on the NodeStack. (A
- * ModelAction can be thrown away before it ever enters the NodeStack.)
- */
- Node *node;
+ ModelAction * uninitaction;
/**
* @brief The clock vector for this operation
* vectors for all operations.
*/
ClockVector *cv;
+ ClockVector *rf_cv;
/** @brief The value written (for write or RMW; undefined for read) */
uint64_t value;
class ModelChecker;
class ModelExecution;
class ModelHistory;
-class Node;
-class NodeStack;
class Scheduler;
class Thread;
class TraceAnalysis;
struct bug_message;
typedef SnapList<ModelAction *> action_list_t;
typedef SnapList<uint32_t> func_id_list_t;
+
+extern volatile int forklock;
#endif
*/
ClockVector::ClockVector(ClockVector *parent, const ModelAction *act)
{
- ASSERT(act);
- num_threads = int_to_id(act->get_tid()) + 1;
+ num_threads = act != NULL ? int_to_id(act->get_tid()) + 1 : 0;
if (parent && parent->num_threads > num_threads)
num_threads = parent->num_threads;
if (parent)
std::memcpy(clock, parent->clock, parent->num_threads * sizeof(modelclock_t));
- clock[id_to_int(act->get_tid())] = act->get_seq_number();
+ if (act != NULL)
+ clock[id_to_int(act->get_tid())] = act->get_seq_number();
}
/** @brief Destructor */
#include "printf.h"
extern int model_out;
-extern int switch_alloc;
#define model_print(fmt, ...) do { \
- switch_alloc = 1; \
- char mprintbuf[256]; \
- int printbuflen=snprintf_(mprintbuf, 256, fmt, ## __VA_ARGS__); \
- int lenleft = printbuflen < 256 ?printbuflen:256; \
- int totalwritten = 0;\
- while(lenleft) { \
- int byteswritten=write(model_out, &mprintbuf[totalwritten], lenleft);\
- lenleft-=byteswritten; \
- totalwritten+=byteswritten; \
- } \
- switch_alloc = 0; \
- } while (0)
+ char mprintbuf[256]; \
+ int printbuflen=snprintf_(mprintbuf, 256, fmt, ## __VA_ARGS__); \
+ int lenleft = printbuflen < 256 ? printbuflen : 256; \
+ int totalwritten = 0; \
+ while(lenleft) { \
+ int byteswritten=write(model_out, &mprintbuf[totalwritten], lenleft); \
+ lenleft-=byteswritten; \
+ totalwritten+=byteswritten; \
+ } \
+} while (0)
#ifdef CONFIG_DEBUG
#define DEBUG(fmt, ...) do { model_print("*** %15s:%-4d %25s() *** " fmt, __FILE__, __LINE__, __func__, ## __VA_ARGS__); } while (0)
/** Enable debugging assertions (via ASSERT()) */
#define CONFIG_ASSERT
+/** Enable mitigations against fork handlers that call into locks... */
+#define FORK_HANDLER_HACK
+
#endif
#include "model.h"
#include "execution.h"
#include "action.h"
-#include "nodestack.h"
#include "schedule.h"
#include "common.h"
#include "clockvector.h"
};
/** @brief Constructor */
-ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler, NodeStack *node_stack) :
+ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
model(m),
params(NULL),
scheduler(scheduler),
mutex_map(),
thrd_last_action(1),
thrd_last_fence_release(),
- node_stack(node_stack),
priv(new struct model_snapshot_members ()),
mo_graph(new CycleGraph()),
fuzzer(new Fuzzer()),
model_thread = new Thread(get_next_id());
add_thread(model_thread);
scheduler->register_engine(this);
- node_stack->register_engine(this);
}
/** @brief Destructor */
return tmp;
}
-static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, SnapVector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
+static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<
const void *, SnapVector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
{
SnapVector<action_list_t> *tmp = hash->get(ptr);
if (tmp == NULL) {
* @param rf_set is the set of model actions we can possibly read from
* @return True if processing this read updates the mo_graph.
*/
-void ModelExecution::process_read(ModelAction *curr, SnapVector<const ModelAction *> * rf_set)
+void ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
{
SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
while(true) {
int index = fuzzer->selectWrite(curr, rf_set);
- const ModelAction *rf = (*rf_set)[index];
+ ModelAction *rf = (*rf_set)[index];
ASSERT(rf);
continue;
/* Establish hypothetical release sequences */
- rel_heads_list_t release_heads;
- get_release_seq_heads(curr, act, &release_heads);
- for (unsigned int i = 0;i < release_heads.size();i++)
- synchronize(release_heads[i], curr);
- if (release_heads.size() != 0)
+ ClockVector *cv = get_hb_from_write(act);
+ if (curr->get_cv()->merge(cv))
updated = true;
}
}
/**
* Initialize the current action by performing one or more of the following
- * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
- * in the NodeStack, manipulating backtracking sets, allocating and
+ * actions, as appropriate: merging RMWR and RMWC/RMW actions,
+ * manipulating backtracking sets, allocating and
* initializing clock vectors, and computing the promises to fulfill.
*
* @param curr The current action, as passed from the user context; may be
*/
bool ModelExecution::initialize_curr_action(ModelAction **curr)
{
- ModelAction *newcurr;
-
if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
- newcurr = process_rmw(*curr);
+ ModelAction *newcurr = process_rmw(*curr);
delete *curr;
*curr = newcurr;
return false;
- }
-
- (*curr)->set_seq_number(get_next_seq_num());
-
- newcurr = node_stack->explore_action(*curr);
- if (newcurr) {
- /* First restore type and order in case of RMW operation */
- if ((*curr)->is_rmwr())
- newcurr->copy_typeandorder(*curr);
-
- ASSERT((*curr)->get_location() == newcurr->get_location());
- newcurr->copy_from_new(*curr);
-
- /* Discard duplicate ModelAction; use action from NodeStack */
- delete *curr;
-
- /* Always compute new clock vector */
- newcurr->create_cv(get_parent_action(newcurr->get_tid()));
-
- *curr = newcurr;
- return false; /* Action was explored previously */
} else {
- newcurr = *curr;
+ ModelAction *newcurr = *curr;
+ newcurr->set_seq_number(get_next_seq_num());
/* Always compute new clock vector */
newcurr->create_cv(get_parent_action(newcurr->get_tid()));
* @return True if this read established synchronization
*/
-bool ModelExecution::read_from(ModelAction *act, const ModelAction *rf)
+void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
{
ASSERT(rf);
ASSERT(rf->is_write());
act->set_read_from(rf);
if (act->is_acquire()) {
- rel_heads_list_t release_heads;
- get_release_seq_heads(act, act, &release_heads);
- int num_heads = release_heads.size();
- for (unsigned int i = 0;i < release_heads.size();i++)
- if (!synchronize(release_heads[i], act))
- num_heads--;
- return num_heads > 0;
+ ClockVector *cv = get_hb_from_write(rf);
+ if (cv == NULL)
+ return;
+ act->get_cv()->merge(cv);
}
- return false;
}
/**
if (!second_part_of_rmw && curr->get_type() != NOOP)
add_action_to_lists(curr);
- SnapVector<const ModelAction *> * rf_set = NULL;
+ if (curr->is_write())
+ add_write_to_lists(curr);
+
+ SnapVector<ModelAction *> * rf_set = NULL;
/* Build may_read_from set for newly-created actions */
if (newly_explored && curr->is_read())
rf_set = build_may_read_from(curr);
mo_graph->addEdge(act->get_reads_from(), curr, force_edge);
}
break;
- } else if (act->is_read() && !act->could_synchronize_with(curr) &&
- !act->same_thread(curr)) {
- /* We have an action that:
- (1) did not happen before us
- (2) is a read and we are a write
- (3) cannot synchronize with us
- (4) is in a different thread
- =>
- that read could potentially read from our write. Note that
- these checks are overly conservative at this point, we'll
- do more checks before actually removing the
- pendingfuturevalue.
-
- */
-
}
}
}
}
/**
- * Finds the head(s) of the release sequence(s) containing a given ModelAction.
- * The ModelAction under consideration is expected to be taking part in
- * release/acquire synchronization as an object of the "reads from" relation.
- * Note that this can only provide release sequence support for RMW chains
- * which do not read from the future, as those actions cannot be traced until
- * their "promise" is fulfilled. Similarly, we may not even establish the
- * presence of a release sequence with certainty, as some modification order
- * constraints may be decided further in the future. Thus, this function
- * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
- * and a boolean representing certainty.
+ * Computes the clock vector that happens before propagates from this write.
*
* @param rf The action that might be part of a release sequence. Must be a
* write.
- * @param release_heads A pass-by-reference style return parameter. After
- * execution of this function, release_heads will contain the heads of all the
- * relevant release sequences, if any exists with certainty
- * @return true, if the ModelExecution is certain that release_heads is complete;
- * false otherwise
+ * @return ClockVector of happens before relation.
*/
-bool ModelExecution::release_seq_heads(const ModelAction *rf, rel_heads_list_t *release_heads) const
-{
+ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
+ SnapVector<ModelAction *> * processset = NULL;
for ( ;rf != NULL;rf = rf->get_reads_from()) {
ASSERT(rf->is_write());
+ if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
+ break;
+ if (processset == NULL)
+ processset = new SnapVector<ModelAction *>();
+ processset->push_back(rf);
+ }
- if (rf->is_release())
- release_heads->push_back(rf);
- else if (rf->get_last_fence_release())
- release_heads->push_back(rf->get_last_fence_release());
- if (!rf->is_rmw())
- break;/* End of RMW chain */
-
- /** @todo Need to be smarter here... In the linux lock
- * example, this will run to the beginning of the program for
- * every acquire. */
- /** @todo The way to be smarter here is to keep going until 1
- * thread has a release preceded by an acquire and you've seen
- * both. */
-
- /* acq_rel RMW is a sufficient stopping condition */
- if (rf->is_acquire() && rf->is_release())
- return true;/* complete */
- };
- ASSERT(rf); // Needs to be real write
-
- if (rf->is_release())
- return true;/* complete */
-
- /* else relaxed write
- * - check for fence-release in the same thread (29.8, stmt. 3)
- * - check modification order for contiguous subsequence
- * -> rf must be same thread as release */
-
- const ModelAction *fence_release = rf->get_last_fence_release();
- /* Synchronize with a fence-release unconditionally; we don't need to
- * find any more "contiguous subsequence..." for it */
- if (fence_release)
- release_heads->push_back(fence_release);
-
- return true; /* complete */
-}
+ int i = (processset == NULL) ? 0 : processset->size();
-/**
- * An interface for getting the release sequence head(s) with which a
- * given ModelAction must synchronize. This function only returns a non-empty
- * result when it can locate a release sequence head with certainty. Otherwise,
- * it may mark the internal state of the ModelExecution so that it will handle
- * the release sequence at a later time, causing @a acquire to update its
- * synchronization at some later point in execution.
- *
- * @param acquire The 'acquire' action that may synchronize with a release
- * sequence
- * @param read The read action that may read from a release sequence; this may
- * be the same as acquire, or else an earlier action in the same thread (i.e.,
- * when 'acquire' is a fence-acquire)
- * @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 ModelExecution::release_seq_heads
- */
-void ModelExecution::get_release_seq_heads(ModelAction *acquire,
- ModelAction *read, rel_heads_list_t *release_heads)
-{
- const ModelAction *rf = read->get_reads_from();
-
- release_seq_heads(rf, release_heads);
+ ClockVector * vec = NULL;
+ while(true) {
+ if (rf->get_rfcv() != NULL) {
+ vec = rf->get_rfcv();
+ } else if (rf->is_acquire() && rf->is_release()) {
+ vec = rf->get_cv();
+ } else if (rf->is_release() && !rf->is_rmw()) {
+ vec = rf->get_cv();
+ } else if (rf->is_release()) {
+ //have rmw that is release and doesn't have a rfcv
+ (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
+ rf->set_rfcv(vec);
+ } else {
+ //operation that isn't release
+ if (rf->get_last_fence_release()) {
+ if (vec == NULL)
+ vec = rf->get_last_fence_release()->get_cv();
+ else
+ (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
+ }
+ rf->set_rfcv(vec);
+ }
+ i--;
+ if (i >= 0) {
+ rf = (*processset)[i];
+ } else
+ break;
+ }
+ if (processset != NULL)
+ delete processset;
+ return vec;
}
/**
uninit = get_uninitialized_action(act);
uninit_id = id_to_int(uninit->get_tid());
list->push_front(uninit);
+ SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
+ if (uninit_id >= (int)vec->size())
+ vec->resize(uninit_id + 1);
+ (*vec)[uninit_id].push_front(uninit);
}
list->push_back(act);
+ // Update action trace, a total order of all actions
action_trace.push_back(act);
if (uninit)
action_trace.push_front(uninit);
+ // Update obj_thrd_map, a per location, per thread, order of actions
SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
if (tid >= (int)vec->size())
vec->resize(priv->next_thread_id);
if (uninit)
(*vec)[uninit_id].push_front(uninit);
+ // Update thrd_last_action, the last action taken by each thrad
if ((int)thrd_last_action.size() <= tid)
thrd_last_action.resize(get_num_threads());
thrd_last_action[tid] = act;
if (uninit)
thrd_last_action[uninit_id] = uninit;
+ // Update thrd_last_fence_release, the last release fence taken by each thread
if (act->is_fence() && act->is_release()) {
if ((int)thrd_last_fence_release.size() <= tid)
thrd_last_fence_release.resize(get_num_threads());
}
}
+void ModelExecution::add_write_to_lists(ModelAction *write) {
+ // Update seq_cst map
+ if (write->is_seqcst())
+ obj_last_sc_map.put(write->get_location(), write);
+
+ SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
+ int tid = id_to_int(write->get_tid());
+ if (tid >= (int)vec->size())
+ vec->resize(priv->next_thread_id);
+ (*vec)[tid].push_back(write);
+}
+
/**
* @brief Get the last action performed by a particular Thread
* @param tid The thread ID of the Thread in question
ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
{
void *location = curr->get_location();
- action_list_t *list = obj_map.get(location);
- /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
- action_list_t::reverse_iterator rit;
- for (rit = list->rbegin();(*rit) != curr;rit++)
- ;
- rit++; /* Skip past curr */
- for ( ;rit != list->rend();rit++)
- if ((*rit)->is_write() && (*rit)->is_seqcst())
- return *rit;
- return NULL;
+ return obj_last_sc_map.get(location);
}
/**
* @param curr is the current ModelAction that we are exploring; it must be a
* 'read' operation.
*/
-SnapVector<const ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
+SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
{
- SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
+ SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
unsigned int i;
ASSERT(curr->is_read());
if (curr->is_seqcst())
last_sc_write = get_last_seq_cst_write(curr);
- SnapVector<const ModelAction *> * rf_set = new SnapVector<const ModelAction *>();
+ SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
/* Iterate over all threads */
for (i = 0;i < thrd_lists->size();i++) {
action_list_t *list = &(*thrd_lists)[i];
action_list_t::reverse_iterator rit;
for (rit = list->rbegin();rit != list->rend();rit++) {
- const ModelAction *act = *rit;
-
- /* Only consider 'write' actions */
- if (!act->is_write()) {
- if (act != curr && act->is_read() && act->happens_before(curr)) {
- const ModelAction *tmp = act->get_reads_from();
- if (((unsigned int) id_to_int(tmp->get_tid()))==i)
- act = tmp;
- else
- break;
- } else
- continue;
- }
+ ModelAction *act = *rit;
if (act == curr)
continue;
/**
* @brief Get an action representing an uninitialized atomic
*
- * This function may create a new one or try to retrieve one from the NodeStack
+ * This function may create a new one.
*
* @param curr The current action, which prompts the creation of an UNINIT action
* @return A pointer to the UNINIT ModelAction
*/
-ModelAction * ModelExecution::get_uninitialized_action(const ModelAction *curr) const
+ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const
{
- Node *node = curr->get_node();
- ModelAction *act = node->get_uninit_action();
+ ModelAction *act = curr->get_uninit_action();
if (!act) {
act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
- node->set_uninit_action(act);
+ curr->set_uninit_action(act);
}
act->create_cv(NULL);
return act;
#include <condition_variable>
#include "classlist.h"
-/** @brief Shorthand for a list of release sequence heads */
-typedef ModelVector<const ModelAction *> rel_heads_list_t;
typedef SnapList<ModelAction *> action_list_t;
struct PendingFutureValue {
ModelAction *reader;
};
-/** @brief Records information regarding a single pending release sequence */
-struct release_seq {
- /** @brief The acquire operation */
- ModelAction *acquire;
- /** @brief The read operation that may read from a release sequence;
- * may be the same as acquire, or else an earlier action in the same
- * thread (i.e., when 'acquire' is a fence-acquire) */
- const ModelAction *read;
- /** @brief The head of the RMW chain from which 'read' reads; may be
- * equal to 'release' */
- const ModelAction *rf;
- /** @brief The head of the potential longest release sequence chain */
- const ModelAction *release;
- /** @brief The write(s) that may break the release sequence */
- SnapVector<const ModelAction *> writes;
-};
-
/** @brief The central structure for model-checking */
class ModelExecution {
public:
- ModelExecution(ModelChecker *m,
- Scheduler *scheduler,
- NodeStack *node_stack);
+ ModelExecution(ModelChecker *m, Scheduler *scheduler);
~ModelExecution();
struct model_params * get_params() const { return params; }
bool next_execution();
bool initialize_curr_action(ModelAction **curr);
- void process_read(ModelAction *curr, SnapVector<const ModelAction *> * rf_set);
+ void process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set);
void process_write(ModelAction *curr);
bool process_fence(ModelAction *curr);
bool process_mutex(ModelAction *curr);
bool process_thread_action(ModelAction *curr);
- bool read_from(ModelAction *act, const ModelAction *rf);
+ void read_from(ModelAction *act, ModelAction *rf);
bool synchronize(const ModelAction *first, ModelAction *second);
void add_action_to_lists(ModelAction *act);
+ void add_write_to_lists(ModelAction *act);
ModelAction * get_last_fence_release(thread_id_t tid) const;
ModelAction * get_last_seq_cst_write(ModelAction *curr) const;
ModelAction * get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const;
ModelAction * get_last_unlock(ModelAction *curr) const;
- SnapVector<const ModelAction *> * build_may_read_from(ModelAction *curr);
+ SnapVector<ModelAction *> * build_may_read_from(ModelAction *curr);
ModelAction * process_rmw(ModelAction *curr);
bool r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> *priorset, bool *canprune);
void 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) const;
- ModelAction * get_uninitialized_action(const ModelAction *curr) const;
+ ClockVector * get_hb_from_write(ModelAction *rf) const;
+ ModelAction * get_uninitialized_action(ModelAction *curr) const;
action_list_t action_trace;
SnapVector<Thread *> thread_map;
* to a trace of all actions performed on the object. */
HashTable<const void *, action_list_t *, uintptr_t, 4> condvar_waiters_map;
- HashTable<void *, SnapVector<action_list_t> *, uintptr_t, 4> obj_thrd_map;
+ HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 4> obj_thrd_map;
+
+ HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 4> obj_wr_thrd_map;
+
+ HashTable<const void *, ModelAction *, uintptr_t, 4> obj_last_sc_map;
+
HashTable<pthread_mutex_t *, cdsc::snapmutex *, uintptr_t, 4> mutex_map;
HashTable<pthread_cond_t *, cdsc::snapcondition_variable *, uintptr_t, 4> cond_map;
SnapVector<ModelAction *> thrd_last_action;
SnapVector<ModelAction *> thrd_last_fence_release;
- NodeStack * const node_stack;
/** A special model-checker Thread; used for associating with
* model-checker-related ModelAcitons */
#include "threads-model.h"
#include "model.h"
-int Fuzzer::selectWrite(ModelAction *read, SnapVector<const ModelAction *> * rf_set) {
+int Fuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set) {
int random_index = random() % rf_set->size();
return random_index;
}
-Thread * Fuzzer::selectThread(Node *n, int * threadlist, int numthreads) {
+Thread * Fuzzer::selectThread(int * threadlist, int numthreads) {
int random_index = random() % numthreads;
int thread = threadlist[random_index];
thread_id_t curr_tid = int_to_id(thread);
class Fuzzer {
public:
Fuzzer() {}
- int selectWrite(ModelAction *read, SnapVector<const ModelAction *>* rf_set);
- Thread * selectThread(Node *n, int * threadlist, int numthreads);
+ int selectWrite(ModelAction *read, SnapVector<ModelAction *>* rf_set);
+ Thread * selectThread(int * threadlist, int numthreads);
Thread * selectNotify(action_list_t * waiters);
MEMALLOC
private:
#define _ATOMIC_LOAD_( __a__, __x__ ) \
({ volatile __typeof__((__a__)->__f__)* __p__ = &((__a__)->__f__); \
- __typeof__((__a__)->__f__)__r__ = (__typeof__((__a__)->__f__))model_read_action((void *)__p__, __x__); \
+ __typeof__((__a__)->__f__) __r__ = (__typeof__((__a__)->__f__))model_read_action((void *)__p__, __x__); \
__r__; })
#define _ATOMIC_STORE_( __a__, __m__, __x__ ) \
({ volatile __typeof__((__a__)->__f__)* __p__ = &((__a__)->__f__); \
- __typeof__(__m__)__v__ = (__m__); \
+ __typeof__(__m__) __v__ = (__m__); \
model_write_action((void *) __p__, __x__, (uint64_t) __v__); \
__v__ = __v__; /* Silence clang (-Wunused-value) */ \
})
#define _ATOMIC_INIT_( __a__, __m__ ) \
({ volatile __typeof__((__a__)->__f__)* __p__ = &((__a__)->__f__); \
- __typeof__(__m__)__v__ = (__m__); \
+ __typeof__(__m__) __v__ = (__m__); \
model_init_action((void *) __p__, (uint64_t) __v__); \
__v__ = __v__; /* Silence clang (-Wunused-value) */ \
})
#define _ATOMIC_MODIFY_( __a__, __o__, __m__, __x__ ) \
({ volatile __typeof__((__a__)->__f__)* __p__ = &((__a__)->__f__); \
- __typeof__((__a__)->__f__)__old__=(__typeof__((__a__)->__f__))model_rmwr_action((void *)__p__, __x__); \
- __typeof__(__m__)__v__ = (__m__); \
- __typeof__((__a__)->__f__)__copy__= __old__; \
+ __typeof__((__a__)->__f__) __old__=(__typeof__((__a__)->__f__))model_rmwr_action((void *)__p__, __x__); \
+ __typeof__(__m__) __v__ = (__m__); \
+ __typeof__((__a__)->__f__) __copy__= __old__; \
__copy__ __o__ __v__; \
model_rmw_action((void *)__p__, __x__, (uint64_t) __copy__); \
__old__ = __old__; /* Silence clang (-Wunused-value) */ \
#define _ATOMIC_CMPSWP_( __a__, __e__, __m__, __x__ ) \
({ volatile __typeof__((__a__)->__f__)* __p__ = &((__a__)->__f__); \
- __typeof__(__e__)__q__ = (__e__); \
- __typeof__(__m__)__v__ = (__m__); \
+ __typeof__(__e__) __q__ = (__e__); \
+ __typeof__(__m__) __v__ = (__m__); \
bool __r__; \
- __typeof__((__a__)->__f__)__t__=(__typeof__((__a__)->__f__))model_rmwrcas_action((void *)__p__, __x__, (uint64_t) *__q__, sizeof((__a__)->__f__)); \
+ __typeof__((__a__)->__f__) __t__=(__typeof__((__a__)->__f__))model_rmwrcas_action((void *)__p__, __x__, (uint64_t) *__q__, sizeof((__a__)->__f__)); \
if (__t__ == *__q__ ) {; \
model_rmw_action((void *)__p__, __x__, (uint64_t) __v__); __r__ = true; } \
else { model_rmwc_action((void *)__p__, __x__); *__q__ = __t__; __r__ = false;} \
( volatile atomic_address* __a__, ptrdiff_t __m__, memory_order __x__ )
{
volatile __typeof__((__a__)->__f__)* __p__ = &((__a__)->__f__);
- __typeof__((__a__)->__f__)__old__=(__typeof__((__a__)->__f__))model_rmwr_action((void *)__p__, __x__);
- __typeof__((__a__)->__f__)__copy__= __old__;
+ __typeof__((__a__)->__f__) __old__=(__typeof__((__a__)->__f__))model_rmwr_action((void *)__p__, __x__);
+ __typeof__((__a__)->__f__) __copy__= __old__;
__copy__ = (void *) (((char *)__copy__) + __m__);
model_rmw_action((void *)__p__, __x__, (uint64_t) __copy__);
return __old__;
( volatile atomic_address* __a__, ptrdiff_t __m__, memory_order __x__ )
{
volatile __typeof__((__a__)->__f__)* __p__ = &((__a__)->__f__);
- __typeof__((__a__)->__f__)__old__=(__typeof__((__a__)->__f__))model_rmwr_action((void *)__p__, __x__);
- __typeof__((__a__)->__f__)__copy__= __old__;
+ __typeof__((__a__)->__f__) __old__=(__typeof__((__a__)->__f__))model_rmwr_action((void *)__p__, __x__);
+ __typeof__((__a__)->__f__) __copy__= __old__;
__copy__ = (void *) (((char *)__copy__) - __m__);
model_rmw_action((void *)__p__, __x__, (uint64_t) __copy__);
return __old__;
#define is_normal_mo(x) ((x >= memory_order_relaxed && x <= memory_order_seq_cst) || x == memory_order_normal)
#define assert_infer(x) for (int i = 0;i <= wildcardNum;i++) \
- ASSERT(is_normal_mo_infer((x[i])));
+ ASSERT(is_normal_mo_infer((x[i])));
#define assert_infers(x) for (ModelList<memory_order *>::iterator iter = \
(x)->begin();iter != (x)->end();iter++) \
- assert_infer((*iter));
+ assert_infer((*iter));
#define relaxed memory_order_relaxed
#define release memory_order_release
#include "model.h"
#include "action.h"
-#include "nodestack.h"
#include "schedule.h"
#include "snapshot-interface.h"
#include "common.h"
params(),
restart_flag(false),
scheduler(new Scheduler()),
- node_stack(new NodeStack()),
- execution(new ModelExecution(this, scheduler, node_stack)),
+ execution(new ModelExecution(this, scheduler)),
history(new ModelHistory()),
execution_number(1),
trace_analyses(),
/** @brief Destructor */
ModelChecker::~ModelChecker()
{
- delete node_stack;
delete scheduler;
}
* Have we completed exploring the preselected path? Then let the
* scheduler decide
*/
- return scheduler->select_next_thread(node_stack->get_head());
+ return scheduler->select_next_thread();
}
/**
bugs->size(),
bugs->size() > 1 ? "s" : "");
for (unsigned int i = 0;i < bugs->size();i++)
- (*bugs)[i] -> print();
+ (*bugs)[i]->print();
}
/**
*/
void ModelChecker::record_stats()
{
- stats.num_total ++;
+ stats.num_total++;
if (!execution->isfeasibleprefix())
- stats.num_infeasible ++;
+ stats.num_infeasible++;
else if (execution->have_bug_reports())
- stats.num_buggy_executions ++;
+ stats.num_buggy_executions++;
else if (execution->is_complete_execution())
- stats.num_complete ++;
+ stats.num_complete++;
else {
- stats.num_redundant ++;
+ stats.num_redundant++;
/**
* @todo We can violate this ASSERT() when fairness/sleep sets
return true;
}
// test code
- execution_number ++;
+ execution_number++;
reset_to_initial_state();
return false;
}
/** @brief Run trace analyses on complete trace */
void ModelChecker::run_trace_analyses() {
- for (unsigned int i = 0;i < trace_analyses.size();i ++)
- trace_analyses[i] -> analyze(execution->get_action_trace());
+ for (unsigned int i = 0;i < trace_analyses.size();i++)
+ trace_analyses[i]->analyze(execution->get_action_trace());
}
/**
*/
uint64_t ModelChecker::switch_to_master(ModelAction *act)
{
+ if (forklock) {
+ static bool fork_message_printed = false;
+
+ if (!fork_message_printed) {
+ model_print("Fork handler trying to call into model checker...\n");
+ fork_message_printed = true;
+ }
+ delete act;
+ return 0;
+ }
DBG();
Thread *old = thread_current();
scheduler->set_current_thread(NULL);
/** The scheduler to use: tracks the running/ready Threads */
Scheduler * const scheduler;
- NodeStack * const node_stack;
ModelExecution *execution;
Thread * init_thread;
ModelHistory *history;
size_t allocatedReqs[REQUESTS_BEFORE_ALLOC] = { 0 };
int nextRequest = 0;
int howManyFreed = 0;
-int switch_alloc = 0;
#if !USE_MPROTECT_SNAPSHOT
static mspace sStaticSpace = NULL;
#endif
void *malloc(size_t size)
{
if (user_snapshot_space) {
- if (switch_alloc) {
- return model_malloc(size);
- }
/* Only perform user allocations from user context */
ASSERT(!model || thread_current());
return user_malloc(size);
void free(void * ptr)
{
if (!DontFree(ptr)) {
- if (switch_alloc) {
- return model_free(ptr);
- }
mspace_free(user_snapshot_space, ptr);
}
}
+++ /dev/null
-#define __STDC_FORMAT_MACROS
-#include <inttypes.h>
-#include <cstdlib>
-
-#include <string.h>
-
-#include "nodestack.h"
-#include "action.h"
-#include "common.h"
-#include "threads-model.h"
-#include "modeltypes.h"
-#include "execution.h"
-#include "params.h"
-
-/**
- * @brief Node constructor
- *
- * Constructs a single Node for use in a NodeStack. Each Node is associated
- * with exactly one ModelAction (exception: the first Node should be created
- * as an empty stub, to represent the first thread "choice") and up to one
- * parent.
- *
- * @param act The ModelAction to associate with this Node. May be NULL.
- * @param nthreads The number of threads which exist at this point in the
- * execution trace.
- */
-Node::Node(ModelAction *act) :
- action(act),
- uninit_action(NULL)
-{
- ASSERT(act);
- act->set_node(this);
-}
-
-/** @brief Node desctructor */
-Node::~Node()
-{
- delete action;
- if (uninit_action)
- delete uninit_action;
-}
-
-/** Prints debugging info for the ModelAction associated with this Node */
-void Node::print() const
-{
- action->print();
-}
-
-NodeStack::NodeStack() :
- node_list(),
- head_idx(-1)
-{
-}
-
-NodeStack::~NodeStack()
-{
- for (unsigned int i = 0;i < node_list.size();i++)
- delete node_list[i];
-}
-
-/**
- * @brief Register the model-checker object with this NodeStack
- * @param exec The execution structure for the ModelChecker
- */
-void NodeStack::register_engine(const ModelExecution *exec)
-{
- this->execution = exec;
-}
-
-const struct model_params * NodeStack::get_params() const
-{
- return execution->get_params();
-}
-
-void NodeStack::print() const
-{
- model_print("............................................\n");
- model_print("NodeStack printing node_list:\n");
- for (unsigned int it = 0;it < node_list.size();it++) {
- if ((int)it == this->head_idx)
- model_print("vvv following action is the current iterator vvv\n");
- node_list[it]->print();
- }
- model_print("............................................\n");
-}
-
-/** Note: The is_enabled set contains what actions were enabled when
- * act was chosen. */
-ModelAction * NodeStack::explore_action(ModelAction *act)
-{
- DBG();
-
- node_list.push_back(new Node(act));
- head_idx++;
- return NULL;
-}
-
-
-/** Reset the node stack. */
-void NodeStack::full_reset()
-{
- for (unsigned int i = 0;i < node_list.size();i++)
- delete node_list[i];
- node_list.clear();
- reset_execution();
-}
-
-Node * NodeStack::get_head() const
-{
- if (node_list.empty() || head_idx < 0)
- return NULL;
- return node_list[head_idx];
-}
-
-Node * NodeStack::get_next() const
-{
- if (node_list.empty()) {
- DEBUG("Empty\n");
- return NULL;
- }
- unsigned int it = head_idx + 1;
- if (it == node_list.size()) {
- DEBUG("At end\n");
- return NULL;
- }
- return node_list[it];
-}
-
-void NodeStack::reset_execution()
-{
- head_idx = -1;
-}
+++ /dev/null
-/** @file nodestack.h
- * @brief Stack of operations for use in backtracking.
- */
-
-#ifndef __NODESTACK_H__
-#define __NODESTACK_H__
-
-#include <cstddef>
-#include <inttypes.h>
-
-#include "mymemory.h"
-#include "schedule.h"
-#include "stl-model.h"
-#include "classlist.h"
-
-/**
- * @brief A single node in a NodeStack
- *
- * Represents a single node in the NodeStack. Each Node is associated with up
- * to one action and up to one parent node. A node holds information
- * regarding the last action performed (the "associated action"), the thread
- * choices that have been explored (explored_children) and should be explored
- * (backtrack), and the actions that the last action may read from.
- */
-class Node {
-public:
- Node(ModelAction *act);
- ~Node();
-
- ModelAction * get_action() const { return action; }
- void set_uninit_action(ModelAction *act) { uninit_action = act; }
- ModelAction * get_uninit_action() const { return uninit_action; }
- void print() const;
-
- SNAPSHOTALLOC
-private:
- ModelAction * const action;
-
- /** @brief ATOMIC_UNINIT action which was created at this Node */
- ModelAction *uninit_action;
-};
-
-typedef SnapVector<Node *> node_list_t;
-
-/**
- * @brief A stack of nodes
- *
- * Holds a Node linked-list that can be used for holding backtracking,
- * may-read-from, and replay information. It is used primarily as a
- * stack-like structure, in that backtracking points and replay nodes are
- * only removed from the top (most recent).
- */
-class NodeStack {
-public:
- NodeStack();
- ~NodeStack();
-
- void register_engine(const ModelExecution *exec);
- ModelAction * explore_action(ModelAction *act);
- Node * get_head() const;
- Node * get_next() const;
- void reset_execution();
- void full_reset();
- void print() const;
-
- SNAPSHOTALLOC
-private:
- node_list_t node_list;
- const struct model_params * get_params() const;
-
- /** @brief The model-checker execution object */
- const ModelExecution *execution;
-
- /**
- * @brief the index position of the current head Node
- *
- * This index is relative to node_list. The index should point to the
- * current head Node. It is negative when the list is empty.
- */
- int head_idx;
-};
-
-#endif /* __NODESTACK_H__ */
(void)character; (void)buffer; (void)idx; (void)maxlen;\r
}\r
\r
-\r
// internal _putchar wrapper\r
static inline void _out_char(char character, void* buffer, size_t idx, size_t maxlen)\r
{\r
(void)buffer; (void)idx; (void)maxlen;\r
if (character) {\r
- _putchar(character);\r
+ // _putchar(character);\r
}\r
}\r
\r
// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell\r
// copies of the Software, and to permit persons to whom the Software is\r
// furnished to do so, subject to the following conditions:\r
-// \r
+//\r
// The above copyright notice and this permission notice shall be included in\r
// all copies or substantial portions of the Software.\r
-// \r
+//\r
// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR\r
// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,\r
// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE\r
* This function is declared here only. You have to write your custom implementation somewhere\r
* \param character Character to output\r
*/\r
-void _putchar(char character);\r
+//void _putchar(char character);\r
\r
\r
/**\r
#endif\r
\r
\r
-#endif // _PRINTF_H_\r
+#endif // _PRINTF_H_\r
#include "schedule.h"
#include "common.h"
#include "model.h"
-#include "nodestack.h"
#include "execution.h"
#include "fuzzer.h"
/**
* @brief Select a Thread to run via round-robin
*
- * @param n The current Node, holding priority information for the next thread
- * selection
*
* @return The next Thread to run
*/
-Thread * Scheduler::select_next_thread(Node *n)
+Thread * Scheduler::select_next_thread()
{
int avail_threads = 0;
int thread_list[enabled_len];
if (avail_threads == 0)
return NULL;// No threads availablex
- Thread * thread = execution->getFuzzer()->selectThread(n, thread_list, avail_threads);
+ Thread * thread = execution->getFuzzer()->selectThread(thread_list, avail_threads);
curr_thread_index = id_to_int(thread->get_id());
return thread;
}
void remove_thread(Thread *t);
void sleep(Thread *t);
void wake(Thread *t);
- Thread * select_next_thread(Node *n);
+ Thread * select_next_thread();
void set_current_thread(Thread *t);
Thread * get_current_thread() const;
void print() const;
model_snapshot_space = create_mspace(numheappages * PAGESIZE, 1);
}
+volatile int forklock = 0;
+
static void fork_loop() {
/* switch back here when takesnapshot is called */
snapshotid = fork_snap->currSnapShotID;
while (true) {
pid_t forkedID;
fork_snap->currSnapShotID = snapshotid + 1;
+
+ forklock = 1;
forkedID = fork();
+ forklock = 0;
if (0 == forkedID) {
setcontext(&fork_snap->shared_ctxt);
projects / c11tester.git / commitdiff