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),
position(NULL),
reads_from(NULL),
last_fence_release(NULL),
- node(NULL),
+ uninitaction(NULL),
cv(NULL),
rf_cv(NULL),
value(value),
position(position),
reads_from(NULL),
last_fence_release(NULL),
- node(NULL),
+ uninitaction(NULL),
cv(NULL),
rf_cv(NULL),
value(value),
position(position),
reads_from(NULL),
last_fence_release(NULL),
- node(NULL),
+ uninitaction(NULL),
cv(NULL),
rf_cv(NULL),
value(value),
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
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(ModelAction *act);
/** Store the most recent fence-release from the same thread
/* 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;
/** @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
*
*/
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;
#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 */
/**
* 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
ModelAction *newcurr = *curr;
newcurr->set_seq_number(get_next_seq_num());
- node_stack->add_action(newcurr);
/* Always compute new clock vector */
newcurr->create_cv(get_parent_action(newcurr->get_tid()));
/**
* @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;
/** @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 r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> *priorset, bool *canprune);
void w_modification_order(ModelAction *curr);
ClockVector * get_hb_from_write(ModelAction *rf) const;
- ModelAction * get_uninitialized_action(const ModelAction *curr) const;
+ ModelAction * get_uninitialized_action(ModelAction *curr) const;
action_list_t action_trace;
SnapVector<Thread *> thread_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 */
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);
public:
Fuzzer() {}
int selectWrite(ModelAction *read, SnapVector<ModelAction *>* rf_set);
- Thread * selectThread(Node *n, int * threadlist, int numthreads);
+ Thread * selectThread(int * threadlist, int numthreads);
Thread * selectNotify(action_list_t * waiters);
MEMALLOC
private:
#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();
}
/**
/** The scheduler to use: tracks the running/ready Threads */
Scheduler * const scheduler;
- NodeStack * const node_stack;
ModelExecution *execution;
Thread * init_thread;
ModelHistory *history;
+++ /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. */
-void NodeStack::add_action(ModelAction *act)
-{
- DBG();
-
- node_list.push_back(new Node(act));
- head_idx++;
-}
-
-
-/** 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);
- void add_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__ */
#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;
projects / c11tester.git / commitdiff