#include "clockvector.h"
#include "common.h"
-ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int value)
+ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int value) :
+ type(type),
+ order(order),
+ location(loc),
+ value(value),
+ cv(NULL)
{
Thread *t = thread_current();
- ModelAction *act = this;
-
- act->type = type;
- act->order = order;
- act->location = loc;
- act->tid = t->get_id();
- act->value = value;
- act->seq_number = model->get_next_seq_num();
-
- cv = NULL;
+ this->tid = t->get_id();
+ this->seq_number = model->get_next_seq_num();
}
ModelAction::~ModelAction()
bool ModelAction::is_write() const
{
- return type == ATOMIC_WRITE;
+ return type == ATOMIC_WRITE || type == ATOMIC_INIT;
}
bool ModelAction::is_rmw() const
return type == ATOMIC_RMW;
}
+bool ModelAction::is_initialization() const
+{
+ return type == ATOMIC_INIT;
+}
+
bool ModelAction::is_acquire() const
{
switch (order) {
return false;
}
-void ModelAction::create_cv(ModelAction *parent)
+void ModelAction::create_cv(const ModelAction *parent)
{
ASSERT(cv == NULL);
cv = new ClockVector(NULL, this);
}
-void ModelAction::read_from(ModelAction *act)
+void ModelAction::read_from(const ModelAction *act)
{
ASSERT(cv);
if (act->is_release() && this->is_acquire())
* @return true if this action's thread has synchronized with act's thread
* since the execution of act, false otherwise.
*/
-bool ModelAction::happens_before(ModelAction *act)
+bool ModelAction::happens_before(const ModelAction *act) const
{
return act->cv->synchronized_since(this);
}
case ATOMIC_RMW:
type_str = "atomic rmw";
break;
+ case ATOMIC_INIT:
+ type_str = "init atomic";
+ break;
default:
type_str = "unknown type";
}
#define VALUE_NONE -1
+/** @brief Represents an action type, identifying one of several types of
+ * ModelAction */
typedef enum action_type {
- THREAD_CREATE,
- THREAD_YIELD,
- THREAD_JOIN,
- ATOMIC_READ,
- ATOMIC_WRITE,
- ATOMIC_RMW
+ THREAD_CREATE, /**< A thread creation action */
+ THREAD_YIELD, /**< A thread yield action */
+ THREAD_JOIN, /**< A thread join action */
+ ATOMIC_READ, /**< An atomic read action */
+ ATOMIC_WRITE, /**< An atomic write action */
+ ATOMIC_RMW, /**< An atomic read-modify-write action */
+ ATOMIC_INIT /**< Initialization of an atomic object (e.g.,
+ * atomic_init()) */
} action_type_t;
/* Forward declaration */
bool is_read() const;
bool is_write() const;
bool is_rmw() const;
+ bool is_initialization() const;
bool is_acquire() const;
bool is_release() const;
bool is_seqcst() const;
bool same_thread(const ModelAction *act) const;
bool is_synchronizing(const ModelAction *act) const;
- void create_cv(ModelAction *parent = NULL);
+ void create_cv(const ModelAction *parent = NULL);
ClockVector * get_cv() const { return cv; }
- void read_from(ModelAction *act);
+ void read_from(const ModelAction *act);
- bool happens_before(ModelAction *act);
+ bool happens_before(const ModelAction *act) const;
inline bool operator <(const ModelAction& act) const {
return get_seq_number() < act.get_seq_number();
ClockVector *cv;
};
-typedef std::list<class ModelAction *> action_list_t;
+typedef std::list<ModelAction *> action_list_t;
#endif /* __ACTION_H__ */
* thread, false otherwise. That is, this function returns:
* <BR><CODE>act <= cv[act->tid]</CODE>
*/
-bool ClockVector::synchronized_since(ModelAction *act) const
+bool ClockVector::synchronized_since(const ModelAction *act) const
{
int i = id_to_int(act->get_tid());
ClockVector(ClockVector *parent = NULL, ModelAction *act = NULL);
~ClockVector();
void merge(ClockVector *cv);
- bool synchronized_since(ModelAction *act) const;
+ bool synchronized_since(const ModelAction *act) const;
void print() const;
modelclock_t getClock(thread_id_t thread);
#include "cyclegraph.h"
+#include "action.h"
CycleGraph::CycleGraph() {
hasCycles=false;
}
bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) {
- std::vector<class CycleNode *> queue;
- HashTable<class CycleNode *, class CycleNode *, uintptr_t, 4> discovered;
-
+ std::vector<CycleNode *> queue;
+ HashTable<CycleNode *, CycleNode *, uintptr_t, 4> discovered;
+
queue.push_back(from);
discovered.put(from, from);
while(!queue.empty()) {
- class CycleNode * node=queue.back();
+ CycleNode * node=queue.back();
queue.pop_back();
if (node==to)
return true;
-
+
for(unsigned int i=0;i<node->getEdges()->size();i++) {
CycleNode *next=(*node->getEdges())[i];
if (!discovered.contains(next)) {
action=modelaction;
}
-std::vector<class CycleNode *> * CycleNode::getEdges() {
+std::vector<CycleNode *> * CycleNode::getEdges() {
return &edges;
}
#define CYCLEGRAPH_H
#include "hashtable.h"
-#include "action.h"
#include <vector>
#include <inttypes.h>
class CycleNode;
+class ModelAction;
/** @brief A graph of Model Actions for tracking cycles. */
class CycleGraph {
private:
CycleNode * getNode(ModelAction *);
- HashTable<class ModelAction *, class CycleNode *, uintptr_t, 4> actionToNode;
+ HashTable<ModelAction *, CycleNode *, uintptr_t, 4> actionToNode;
bool checkReachable(CycleNode *from, CycleNode *to);
-
+
bool hasCycles;
};
public:
CycleNode(ModelAction *action);
void addEdge(CycleNode * node);
- std::vector<class CycleNode *> * getEdges();
+ std::vector<CycleNode *> * getEdges();
private:
ModelAction *action;
- std::vector<class CycleNode *> edges;
+ std::vector<CycleNode *> edges;
};
#endif
void atomic_init(struct atomic_object *obj, int value)
{
+ DBG();
obj->value = value;
+ model->switch_to_master(new ModelAction(ATOMIC_INIT, memory_order_relaxed, obj, value));
}
extern "C" {
#endif
+ /** @brief The memory orders specified by the C11/C++11 memory models */
typedef enum memory_order {
memory_order_relaxed,
memory_order_consume,
diverge(NULL),
nextThread(THREAD_ID_T_NONE),
action_trace(new action_list_t()),
- thread_map(new std::map<int, class Thread *>),
+ thread_map(new std::map<int, Thread *>),
obj_thrd_map(new std::map<void *, std::vector<action_list_t> >()),
thrd_last_action(new std::vector<ModelAction *>(1)),
node_stack(new NodeStack()),
/** @brief Destructor */
ModelChecker::~ModelChecker()
{
- std::map<int, class Thread *>::iterator it;
+ std::map<int, Thread *>::iterator it;
for (it = thread_map->begin(); it != thread_map->end(); it++)
delete (*it).second;
delete thread_map;
ASSERT(curr->is_read());
+ /* Track whether this object has been initialized */
+ bool initialized = false;
+
for (i = 0; i < thrd_lists->size(); i++) {
action_list_t *list = &(*thrd_lists)[i];
action_list_t::reverse_iterator rit;
}
curr->get_node()->add_read_from(act);
- /* Include at most one act that "happens before" curr */
- if (act->happens_before(curr))
+ /* Include at most one act per-thread that "happens before" curr */
+ if (act->happens_before(curr)) {
+ initialized = true;
break;
+ }
}
}
+
+ if (!initialized) {
+ /* TODO: need a more informative way of reporting errors */
+ printf("ERROR: may read from uninitialized atomic\n");
+ }
+
+ if (DBG_ENABLED() || !initialized) {
+ printf("Reached read action:\n");
+ curr->print();
+ printf("Printing may_read_from\n");
+ curr->get_node()->print_may_read_from();
+ printf("End printing may_read_from\n");
+ }
+
+ ASSERT(initialized);
}
static void print_list(action_list_t *list)
~ModelChecker();
/** The scheduler to use: tracks the running/ready Threads */
- class Scheduler *scheduler;
+ Scheduler *scheduler;
/** Stores the context for the main model-checking system thread (call
* once)
/** @returns the context for the main model-checking system thread */
ucontext_t * get_system_context(void) { return system_context; }
- /**
- * Stores the ModelAction for the current thread action. Call this
- * immediately before switching from user- to system-context to pass
- * data between them.
- * @param act The ModelAction created by the user-thread action
- */
- void set_current_action(ModelAction *act) { current_action = act; }
void check_current_action(void);
void print_summary(void);
Thread * schedule_next_thread();
modelclock_t used_sequence_numbers;
int num_executions;
+ /**
+ * Stores the ModelAction for the current thread action. Call this
+ * immediately before switching from user- to system-context to pass
+ * data between them.
+ * @param act The ModelAction created by the user-thread action
+ */
+ void set_current_action(ModelAction *act) { current_action = act; }
+
ModelAction * get_last_conflict(ModelAction *act);
void set_backtracking(ModelAction *act);
thread_id_t get_next_replay_thread();
ucontext_t *system_context;
action_list_t *action_trace;
- std::map<int, class Thread *> *thread_map;
+ std::map<int, Thread *> *thread_map;
std::map<void *, std::vector<action_list_t> > *obj_thrd_map;
std::vector<ModelAction *> *thrd_last_action;
- class NodeStack *node_stack;
+ NodeStack *node_stack;
ModelAction *next_backtrack;
};
printf("******** empty action ********\n");
}
+/** @brief Prints info about may_read_from set */
+void Node::print_may_read_from()
+{
+ readfrom_set_t::iterator it;
+ for (it = may_read_from.begin(); it != may_read_from.end(); it++)
+ (*it)->print();
+}
+
/**
* Checks if the Thread associated with this thread ID has been explored from
* this Node already.
* Add an action to the may_read_from set.
* @param act is the action to add
*/
-void Node::add_read_from(ModelAction *act)
+void Node::add_read_from(const ModelAction *act)
{
- may_read_from.insert(act);
+ may_read_from.push_back(act);
}
void Node::explore(thread_id_t tid)
#include <list>
#include <vector>
-#include <set>
#include <cstddef>
#include "threads.h"
#include "mymemory.h"
class ModelAction;
-typedef std::set< ModelAction *, std::less< ModelAction *>, MyAlloc< ModelAction * > > action_set_t;
+typedef std::list< const ModelAction *, MyAlloc< const ModelAction * > > readfrom_set_t;
/**
* @brief A single node in a NodeStack
* occurred previously in the stack. */
Node * get_parent() const { return parent; }
- void add_read_from(ModelAction *act);
+ void add_read_from(const ModelAction *act);
void print();
+ void print_may_read_from();
MEMALLOC
private:
/** The set of ModelActions that this the action at this Node may read
* from. Only meaningful if this Node represents a 'read' action. */
- action_set_t may_read_from;
+ readfrom_set_t may_read_from;
};
-typedef std::list<class Node *, MyAlloc< class Node * > > node_list_t;
+typedef std::list< Node *, MyAlloc< Node * > > node_list_t;
/**
* @brief A stack of nodes
Thread * thread_current(void)
{
+ ASSERT(model);
return model->scheduler->get_current_thread();
}
}
}
-Thread::Thread(thrd_t *t, void (*func)(void *), void *a) {
+Thread::Thread(thrd_t *t, void (*func)(void *), void *a) :
+ last_action_val(VALUE_NONE)
+{
int ret;
user_thread = t;
#define THREAD_ID_T_NONE -1
+/** @brief Represents the state of a user Thread */
typedef enum thread_state {
+ /** Thread was just created and hasn't run yet */
THREAD_CREATED,
+ /** Thread is running */
THREAD_RUNNING,
+ /**
+ * Thread has yielded to the model-checker but is ready to run. Used
+ * during an action that caused a context switch to the model-checking
+ * context.
+ */
THREAD_READY,
+ /** Thread has completed its execution */
THREAD_COMPLETED
} thread_state;
void set_creation(ModelAction *act) { creation = act; }
ModelAction * get_creation() { return creation; }
+ /**
+ * Set a return value for the last action in this thread (e.g., for an
+ * atomic read).
+ * @param value The value to return
+ */
+ void set_return_value(int value) { last_action_val = value; }
+
+ /**
+ * Retrieve a return value for the last action in this thread. Used,
+ * for instance, for an atomic read to return the 'read' value. Should
+ * be called from a user context.
+ * @return The value 'returned' by the action
+ */
+ int get_return_value() { return last_action_val; }
+
friend void thread_startup();
SNAPSHOTALLOC
thrd_t *user_thread;
thread_id_t id;
thread_state state;
+
+ /**
+ * The value returned by the last action in this thread
+ * @see Thread::set_return_value()
+ * @see Thread::get_return_value()
+ */
+ int last_action_val;
};
Thread * thread_current();
projects / model-checker.git / commitdiff