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 \
- sleeps.o history.o funcnode.o funcinst.o printf.o
+ sleeps.o history.o funcnode.o funcinst.o predicate.o printf.o
CPPFLAGS += -Iinclude -I.
LDFLAGS := -ldl -lrt -rdynamic -lpthread
}
+/**
+ * @brief Construct a new ModelAction for sleep actions
+ *
+ * @param type The type of action: THREAD_SLEEP
+ * @param order The memory order of this action. A "don't care" for non-ATOMIC
+ * actions (e.g., THREAD_* or MODEL_* actions).
+ * @param loc The location that this action acts upon
+ * @param value The time duration a thread is scheduled to sleep.
+ * @param _time The this sleep action is constructed
+ */
+ModelAction::ModelAction(action_type_t type, memory_order order, uint64_t value, uint64_t _time) :
+ location(NULL),
+ position(NULL),
+ time(_time),
+ last_fence_release(NULL),
+ uninitaction(NULL),
+ cv(NULL),
+ rf_cv(NULL),
+ value(value),
+ type(type),
+ order(order),
+ original_order(order),
+ seq_number(ACTION_INITIAL_CLOCK)
+{
+ Thread *t = thread_current();
+ this->tid = t!= NULL ? t->get_id() : -1;
+}
+
/**
* @brief Construct a new ModelAction
*
Thread *t = thread ? thread : thread_current();
this->tid = t->get_id();
- // model_print("position: %s\n", position);
}
return type == ATOMIC_LOCK;
}
+bool ModelAction::is_sleep() const
+{
+ return type == THREAD_SLEEP;
+}
+
bool ModelAction::is_wait() const {
return type == ATOMIC_WAIT;
}
ASSERT(act);
reads_from = act;
-
if (act->is_uninitialized()) { // WL
uint64_t val = *((uint64_t *) location);
ModelAction * act_uninitialized = (ModelAction *)act;
case THREAD_YIELD: return "thread yield";
case THREAD_JOIN: return "thread join";
case THREAD_FINISH: return "thread finish";
+ case THREAD_SLEEP: return "thread sleep";
case THREADONLY_FINISH: return "pthread_exit finish";
case PTHREAD_CREATE: return "pthread create";
THREADONLY_FINISH, // < A thread completion action
PTHREAD_CREATE, // < A pthread creation action
PTHREAD_JOIN, // < A pthread join action
+ THREAD_SLEEP, // < A sleep operation
ATOMIC_UNINIT, // < Represents an uninitialized atomic
NONATOMIC_WRITE, // < Represents a non-atomic store
ATOMIC_INIT, // < Initialization of an atomic object (e.g., atomic_init())
ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value = VALUE_NONE, Thread *thread = NULL);
ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value, int size);
ModelAction(action_type_t type, const char * position, memory_order order, void *loc, uint64_t value, int size);
+ ModelAction(action_type_t type, memory_order order, uint64_t value, uint64_t time);
ModelAction(action_type_t type, const char * position, memory_order order, void *loc, uint64_t value = VALUE_NONE, Thread *thread = NULL);
~ModelAction();
void print() const;
uint64_t get_write_value() const;
uint64_t get_return_value() const;
ModelAction * get_reads_from() const { return reads_from; }
+ uint64_t get_time() const {return time;}
cdsc::mutex * get_mutex() const;
void set_read_from(ModelAction *act);
bool is_thread_join() const;
bool is_mutex_op() const;
bool is_lock() const;
+ bool is_sleep() const;
bool is_trylock() const;
bool is_unlock() const;
bool is_wait() const;
*/
ModelAction *reads_from;
int size;
+ uint64_t time; //used for sleep
};
/** @brief The last fence release from the same thread */
#define CLASSLIST_H
#include <inttypes.h>
#include "stl-model.h"
+#include "hashset.h"
class ClockVector;
class CycleGraph;
class Fuzzer;
class FuncNode;
class FuncInst;
+class Predicate;
struct model_snapshot_members;
struct bug_message;
typedef SnapList<ModelAction *> action_list_t;
typedef SnapList<uint32_t> func_id_list_t;
typedef SnapList<FuncInst *> func_inst_list_t;
+typedef HSIterator<Predicate *, uintptr_t, 0, model_malloc, model_calloc, model_free> PredSetIter;
+typedef HashSet<Predicate *, uintptr_t, 0, model_malloc, model_calloc, model_free> PredSet;
+typedef HSIterator<uint64_t, uint64_t, 0, model_malloc, model_calloc, model_free> write_set_iter;
+typedef HashSet<uint64_t, uint64_t, 0, model_malloc, model_calloc, model_free> write_set_t;
extern volatile int modellock;
#endif
#include "threads-model.h"
#include "datarace.h"
-memory_order orders[8] = {
+memory_order orders[7] = {
memory_order_relaxed, memory_order_consume, memory_order_acquire,
memory_order_release, memory_order_acq_rel, memory_order_seq_cst,
};
*/
void cds_func_entry(const char * funcName) {
- if (!model) return;
-
+ ensureModel();
Thread * th = thread_current();
uint32_t func_id;
}
void cds_func_exit(const char * funcName) {
- if (!model) return;
-
+ ensureModel();
Thread * th = thread_current();
uint32_t func_id;
*
* This function should only be called once.
*/
+char filename[256];
+
void redirect_output()
{
/* Save stdout for later use */
perror("dup");
exit(EXIT_FAILURE);
}
-
- /* Redirect program output to a pipe */
- int pipefd[2];
- if (pipe(pipefd) < 0) {
- perror("pipe");
- exit(EXIT_FAILURE);
- }
- if (dup2(pipefd[1], STDOUT_FILENO) < 0) {
+ snprintf_(filename, sizeof(filename), "C11FuzzerTmp%d", getpid());
+ fd_user_out = open(filename, O_CREAT | O_TRUNC| O_RDWR, S_IRWXU);
+ if (dup2(fd_user_out, STDOUT_FILENO) < 0) {
perror("dup2");
exit(EXIT_FAILURE);
}
- close(pipefd[1]);
- /* Save the "read" side of the pipe for use later */
- if (fcntl(pipefd[0], F_SETFL, O_NONBLOCK) < 0) {
- perror("fcntl");
- exit(EXIT_FAILURE);
- }
- fd_user_out = pipefd[0];
}
/**
void clear_program_output()
{
fflush(stdout);
- char buf[200];
- while (read_to_buf(fd_user_out, buf, sizeof(buf))) ;
+ close(fd_user_out);
+ unlink(filename);
}
/** @brief Print out any pending program output */
/* Gather all program output */
fflush(stdout);
+ lseek(fd_user_out, 0, SEEK_SET);
/* Read program output pipe and write to (real) stdout */
ssize_t ret;
while (1) {
}
}
+ close(fd_user_out);
+ unlink(filename);
+
model_print("---- END PROGRAM OUTPUT ----\n");
}
#endif /* ! CONFIG_DEBUG */
LIB_NAME := model
LIB_SO := lib$(LIB_NAME).so
-CPPFLAGS += -Wall -g -O0
+CPPFLAGS += -Wall -g -O3
# Mac OSX options
ifeq ($(UNAME), Darwin)
mo_graph(new CycleGraph()),
fuzzer(new Fuzzer()),
thrd_func_list(),
- thrd_func_inst_lists(),
+ thrd_func_act_lists(),
isfinished(false)
{
/* Initialize a model-checker thread, for special ModelActions */
if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
return true;
}
+ if (asleep->is_sleep()) {
+ if (fuzzer->shouldWake(asleep))
+ return true;
+ }
+
return false;
}
add_normal_write_to_lists(act);
add_write_to_lists(act);
w_modification_order(act);
+ model->get_history()->process_action(act, act->get_tid());
return act;
}
if (!blocking->is_complete()) {
return false;
}
+ } else if (curr->is_sleep()) {
+ if (!fuzzer->shouldSleep(curr))
+ return false;
}
return true;
curr = check_current_action(curr);
ASSERT(curr);
- /* Process this action in ModelHistory for records*/
- // model->get_history()->process_action( curr, curr->get_tid() );
+ /* Process this action in ModelHistory for records */
+ model->get_history()->process_action( curr, curr->get_tid() );
if (curr_thrd->is_blocked() || curr_thrd->is_complete())
scheduler->remove_thread(curr_thrd);
ModelAction * check_current_action(ModelAction *curr);
SnapVector<func_id_list_t> * get_thrd_func_list() { return &thrd_func_list; }
- SnapVector< SnapList<func_inst_list_t *> *> * get_thrd_func_inst_lists() { return &thrd_func_inst_lists; }
+ SnapVector< SnapList<action_list_t *> *> * get_thrd_func_act_lists() { return &thrd_func_act_lists; }
bool isFinished() {return isfinished;}
void setFinished() {isfinished = true;}
/* Keeps track of atomic actions that thread i has performed in some
* function. Index of SnapVector is thread id. SnapList simulates
* the call stack.
- *
- * This data structure is handled by ModelHistory
*/
- SnapVector< SnapList< func_inst_list_t *> *> thrd_func_inst_lists;
+ SnapVector< SnapList<action_list_t *> *> thrd_func_act_lists;
bool isfinished;
};
#include "funcinst.h"
FuncInst::FuncInst(ModelAction *act, FuncNode *func_node) :
- collisions()
+ single_location(true)
{
ASSERT(act);
ASSERT(func_node);
this->position = act->get_position();
this->location = act->get_location();
this->type = act->get_type();
+ this->order = act->get_mo();
this->func_node = func_node;
}
return true;
}
+/*
FuncInst * FuncInst::search_in_collision(ModelAction *act)
{
action_type type = act->get_type();
- mllnode<FuncInst*>* it;
- for (it = collisions.begin();it != NULL;it=it->getNext()) {
+ mllnode<FuncInst*> * it;
+ for (it = collisions.begin(); it != NULL; it = it->getNext()) {
FuncInst * inst = it->getVal();
- if ( inst->get_type() == type )
+ if (inst->get_type() == type)
return inst;
}
return NULL;
}
+*/
bool FuncInst::is_read() const
{
- return type == ATOMIC_READ || type == ATOMIC_RMWR || type == ATOMIC_RMWRCAS; /* type == ATOMIC_RMW ? */
+ return type == ATOMIC_READ || type == ATOMIC_RMWR || type == ATOMIC_RMWRCAS || type == ATOMIC_RMW;
}
bool FuncInst::is_write() const
return type == ATOMIC_WRITE || type == ATOMIC_RMW || type == ATOMIC_INIT || type == ATOMIC_UNINIT || type == NONATOMIC_WRITE;
}
+void FuncInst::print()
+{
+ model_print("func inst - pos: %s, loc: %p, type: %d,\n", position, location, type);
+}
FuncInst(ModelAction *act, FuncNode *func_node);
~FuncInst();
- //ModelAction * get_action() const { return action; }
const char * get_position() const { return position; }
+
void * get_location() const { return location; }
+ void set_location(void * loc) { location = loc; }
+ void reset_location() { location = NULL; }
+
action_type get_type() const { return type; }
+ memory_order get_mo() const { return order; }
FuncNode * get_func_node() const { return func_node; }
bool add_pred(FuncInst * other);
bool add_succ(FuncInst * other);
- FuncInst * search_in_collision(ModelAction *act);
+ //FuncInst * search_in_collision(ModelAction *act);
+ //func_inst_list_mt * get_collisions() { return &collisions; }
- func_inst_list_mt * get_collisions() { return &collisions; }
func_inst_list_mt * get_preds() { return &predecessors; }
func_inst_list_mt * get_succs() { return &successors; }
bool is_read() const;
bool is_write() const;
+ bool is_single_location() { return single_location; }
+ void not_single_location() { single_location = false; }
+
+ void print();
MEMALLOC
private:
- //ModelAction * const action;
const char * position;
+
+ /* Atomic operations with the same source line number may act at different
+ * memory locations, such as the next field of the head pointer in ms-queue.
+ * location only stores the memory location when this FuncInst was constructed.
+ */
void * location;
action_type type;
+ memory_order order;
FuncNode * func_node;
- /* collisions store a list of FuncInsts with the same position
+ bool single_location;
+
+ /* Currently not in use. May remove this field later
+ *
+ * collisions store a list of FuncInsts with the same position
* but different action types. For example, CAS is broken down
* as three different atomic operations in cmodelint.cc */
- func_inst_list_mt collisions;
+ // func_inst_list_mt collisions;
func_inst_list_mt predecessors;
func_inst_list_mt successors;
#include "funcnode.h"
-#include "predicate.h"
-FuncNode::FuncNode() :
+FuncNode::FuncNode(ModelHistory * history) :
+ history(history),
+ predicate_tree_initialized(false),
+ predicate_tree_entry(new Predicate(NULL, true)),
+ exit_count(0),
func_inst_map(),
inst_list(),
entry_insts(),
thrd_read_map(),
- read_locations()
-{}
+ action_list_buffer()
+{
+ predicate_tree_entry->add_predicate_expr(NOPREDICATE, NULL, true);
+}
+
+void FuncNode::set_new_exec_flag()
+{
+ for (uint i = 0; i < thrd_read_map.size(); i++)
+ thrd_read_map[i] = new read_map_t();
+
+ for (mllnode<FuncInst *> * it = inst_list.begin(); it != NULL; it = it->getNext()) {
+ FuncInst * inst = it->getVal();
+ inst->reset_location();
+ }
+}
/* Check whether FuncInst with the same type, position, and location
- * as act has been added to func_inst_map or not. If so, return it;
- * if not, add it and return it.
+ * as act has been added to func_inst_map or not. If not, add it.
*
- * @return FuncInst with the same type, position, and location as act */
-FuncInst * FuncNode::get_or_add_action(ModelAction *act)
+ * Note: currently, actions with the same position are filtered out by process_action,
+ * so the collision list of FuncInst is not used. May remove it later.
+ */
+void FuncNode::add_inst(ModelAction *act)
{
ASSERT(act);
const char * position = act->get_position();
- /* Actions THREAD_CREATE, THREAD_START, THREAD_YIELD, THREAD_JOIN,
- * THREAD_FINISH, PTHREAD_CREATE, PTHREAD_JOIN,
- * ATOMIC_LOCK, ATOMIC_TRYLOCK, and ATOMIC_UNLOCK are not tagged with their
- * source line numbers
+ /* THREAD* actions, ATOMIC_LOCK, ATOMIC_TRYLOCK, and ATOMIC_UNLOCK
+ * actions are not tagged with their source line numbers
*/
if (position == NULL)
- return NULL;
+ return;
if ( func_inst_map.contains(position) ) {
FuncInst * inst = func_inst_map.get(position);
- if (inst->get_type() != act->get_type() ) {
- // model_print("action with a different type occurs at line number %s\n", position);
- FuncInst * func_inst = inst->search_in_collision(act);
+ ASSERT(inst->get_type() == act->get_type());
- if (func_inst != NULL) {
- // return the FuncInst found in the collision list
- return func_inst;
- }
-
- func_inst = new FuncInst(act, this);
- inst->get_collisions()->push_back(func_inst);
- inst_list.push_back(func_inst); // delete?
+ // locations are set to NULL when new executions start
+ if (inst->get_location() == NULL)
+ inst->set_location(act->get_location());
- return func_inst;
- }
+ if (inst->get_location() != act->get_location())
+ inst->not_single_location();
- return inst;
+ return;
}
FuncInst * func_inst = new FuncInst(act, this);
func_inst_map.put(position, func_inst);
inst_list.push_back(func_inst);
+}
+
+/* Get the FuncInst with the same type, position, and location
+ * as act
+ *
+ * @return FuncInst with the same type, position, and location as act */
+FuncInst * FuncNode::get_inst(ModelAction *act)
+{
+ ASSERT(act);
+ const char * position = act->get_position();
+
+ /* THREAD* actions, ATOMIC_LOCK, ATOMIC_TRYLOCK, and ATOMIC_UNLOCK
+ * actions are not tagged with their source line numbers
+ */
+ if (position == NULL)
+ return NULL;
- return func_inst;
+ FuncInst * inst = func_inst_map.get(position);
+ if (inst == NULL)
+ return NULL;
+
+ action_type inst_type = inst->get_type();
+ action_type act_type = act->get_type();
+
+ // else if branch: an RMWRCAS action is converted to a RMW or READ action
+ if (inst_type == act_type)
+ return inst;
+ else if (inst_type == ATOMIC_RMWRCAS &&
+ (act_type == ATOMIC_RMW || act_type == ATOMIC_READ))
+ return inst;
+
+ return NULL;
}
+
void FuncNode::add_entry_inst(FuncInst * inst)
{
if (inst == NULL)
return;
- mllnode<FuncInst*>* it;
- for (it = entry_insts.begin();it != NULL;it=it->getNext()) {
+ mllnode<FuncInst *> * it;
+ for (it = entry_insts.begin(); it != NULL; it = it->getNext()) {
if (inst == it->getVal())
return;
}
entry_insts.push_back(inst);
}
-/* @param inst_list a list of FuncInsts; this argument comes from ModelExecution
- * Link FuncInsts in a list - add one FuncInst to another's predecessors and successors
+/**
+ * @brief Convert ModelAdtion list to FuncInst list
+ * @param act_list A list of ModelActions
+ */
+void FuncNode::update_tree(action_list_t * act_list)
+{
+ if (act_list == NULL || act_list->size() == 0)
+ return;
+
+ /* build inst_list from act_list for later processing */
+ func_inst_list_t inst_list;
+ action_list_t read_act_list;
+
+ for (sllnode<ModelAction *> * it = act_list->begin(); it != NULL; it = it->getNext()) {
+ ModelAction * act = it->getVal();
+ FuncInst * func_inst = get_inst(act);
+
+ if (func_inst == NULL)
+ continue;
+
+ inst_list.push_back(func_inst);
+
+ if (func_inst->is_read())
+ read_act_list.push_back(act);
+ }
+
+// model_print("function %s\n", func_name);
+ update_inst_tree(&inst_list);
+ update_predicate_tree(&read_act_list);
+// deep_update(predicate_tree_entry);
+
+// print_predicate_tree();
+}
+
+/**
+ * @brief Link FuncInsts in inst_list - add one FuncInst to another's predecessors and successors
+ * @param inst_list A list of FuncInsts
*/
-void FuncNode::link_insts(func_inst_list_t * inst_list)
+void FuncNode::update_inst_tree(func_inst_list_t * inst_list)
{
if (inst_list == NULL)
return;
+ else if (inst_list->size() == 0)
+ return;
+ /* start linking */
sllnode<FuncInst *>* it = inst_list->begin();
sllnode<FuncInst *>* prev;
- if (inst_list->size() == 0)
- return;
-
/* add the first instruction to the list of entry insts */
FuncInst * entry_inst = it->getVal();
add_entry_inst(entry_inst);
- it=it->getNext();
+ it = it->getNext();
while (it != NULL) {
- prev = it;
prev = it->getPrev();
FuncInst * prev_inst = prev->getVal();
prev_inst->add_succ(curr_inst);
curr_inst->add_pred(prev_inst);
- it=it->getNext();
+ it = it->getNext();
}
}
uint64_t read_from_val = act->get_reads_from_value();
/* resize and initialize */
+
uint32_t old_size = thrd_read_map.size();
if (old_size <= tid) {
thrd_read_map.resize(tid + 1);
- for (uint32_t i = old_size;i < tid + 1;i++)
+ for (uint32_t i = old_size; i < tid + 1;i++)
thrd_read_map[i] = new read_map_t();
}
read_map->put(location, read_from_val);
/* Store the memory locations where atomic reads happen */
- bool push_loc = true;
- mllnode<void *> * it;
- for (it = read_locations.begin();it != NULL;it=it->getNext()) {
- if (location == it->getVal()) {
- push_loc = false;
- break;
- }
- }
-
- if (push_loc)
- read_locations.push_back(location);
+ // read_locations.add(location);
}
uint64_t FuncNode::query_last_read(void * location, uint32_t tid)
{
if (thrd_read_map.size() <= tid)
- return 0xdeadbeef;
+ return VALUE_NONE;
read_map_t * read_map = thrd_read_map[tid];
/* last read value not found */
if ( !read_map->contains(location) )
- return 0xdeadbeef;
+ return VALUE_NONE;
uint64_t read_val = read_map->get(location);
return read_val;
thrd_read_map[tid]->reset();
}
-void FuncNode::generate_predicate(FuncInst *func_inst)
+void FuncNode::update_predicate_tree(action_list_t * act_list)
+{
+ if (act_list == NULL || act_list->size() == 0)
+ return;
+/*
+ if (predicate_tree_initialized) {
+ return;
+ }
+ predicate_tree_initialized = true;
+*/
+ /* map a FuncInst to the its predicate */
+ HashTable<FuncInst *, Predicate *, uintptr_t, 0> inst_pred_map(128);
+
+ // number FuncInsts to detect loops
+ HashTable<FuncInst *, uint32_t, uintptr_t, 0> inst_id_map(128);
+ uint32_t inst_counter = 0;
+
+ HashTable<void *, ModelAction *, uintptr_t, 0> loc_act_map(128);
+ HashTable<FuncInst *, ModelAction *, uintptr_t, 0> inst_act_map(128);
+
+ sllnode<ModelAction *> *it = act_list->begin();
+ Predicate * curr_pred = predicate_tree_entry;
+ while (it != NULL) {
+ ModelAction * next_act = it->getVal();
+ FuncInst * next_inst = get_inst(next_act);
+ SnapVector<Predicate *> * unset_predicates = new SnapVector<Predicate *>();
+
+ bool branch_found = follow_branch(&curr_pred, next_inst, next_act, &inst_act_map, unset_predicates);
+
+ // no predicate expressions, follow the only branch
+ if (!branch_found && unset_predicates->size() != 0) {
+ ASSERT(unset_predicates->size() == 1);
+ Predicate * one_branch = (*unset_predicates)[0];
+ curr_pred = one_branch;
+ branch_found = true;
+ }
+
+ delete unset_predicates;
+
+ // detect loops
+ if (!branch_found && inst_id_map.contains(next_inst)) {
+ FuncInst * curr_inst = curr_pred->get_func_inst();
+ uint32_t curr_id = inst_id_map.get(curr_inst);
+ uint32_t next_id = inst_id_map.get(next_inst);
+
+ if (curr_id >= next_id) {
+ Predicate * old_pred = inst_pred_map.get(next_inst);
+ Predicate * back_pred = old_pred->get_parent();
+
+ curr_pred->add_backedge(back_pred);
+ curr_pred = back_pred;
+
+ continue;
+ }
+ }
+
+ if (!branch_found) {
+ if ( loc_act_map.contains(next_act->get_location()) ) {
+ ModelAction * last_act = loc_act_map.get(next_act->get_location());
+ FuncInst * last_inst = get_inst(last_act);
+
+ Predicate * new_pred1 = new Predicate(next_inst);
+ new_pred1->add_predicate_expr(EQUALITY, last_inst, true);
+
+ Predicate * new_pred2 = new Predicate(next_inst);
+ new_pred2->add_predicate_expr(EQUALITY, last_inst, false);
+
+ curr_pred->add_child(new_pred1);
+ curr_pred->add_child(new_pred2);
+ new_pred1->set_parent(curr_pred);
+ new_pred2->set_parent(curr_pred);
+
+ uint64_t last_read = last_act->get_reads_from_value();
+ uint64_t next_read = next_act->get_reads_from_value();
+
+ if ( last_read == next_read )
+ curr_pred = new_pred1;
+ else
+ curr_pred = new_pred2;
+ } else if (!next_inst->is_single_location()) {
+ Predicate * new_pred1 = new Predicate(next_inst);
+ new_pred1->add_predicate_expr(NULLITY, NULL, true);
+
+ Predicate * new_pred2 = new Predicate(next_inst);
+ new_pred2->add_predicate_expr(NULLITY, NULL, false);
+
+ curr_pred->add_child(new_pred1);
+ curr_pred->add_child(new_pred2);
+ new_pred1->set_parent(curr_pred);
+ new_pred2->set_parent(curr_pred);
+
+ uint64_t next_read = next_act->get_reads_from_value();
+ bool isnull = ((void*)next_read == NULL);
+ if (isnull)
+ curr_pred = new_pred1;
+ else
+ curr_pred = new_pred2;
+ } else {
+ Predicate * new_pred = new Predicate(next_inst);
+ curr_pred->add_child(new_pred);
+ new_pred->set_parent(curr_pred);
+
+ if (curr_pred->is_entry_predicate())
+ new_pred->add_predicate_expr(NOPREDICATE, NULL, true);
+
+ curr_pred = new_pred;
+ }
+ }
+
+ inst_pred_map.put(next_inst, curr_pred);
+ if (!inst_id_map.contains(next_inst))
+ inst_id_map.put(next_inst, inst_counter++);
+
+ loc_act_map.put(next_act->get_location(), next_act);
+ inst_act_map.put(next_inst, next_act);
+ it = it->getNext();
+ }
+}
+
+void FuncNode::deep_update(Predicate * curr_pred)
+{
+ FuncInst * func_inst = curr_pred->get_func_inst();
+ if (func_inst != NULL && !func_inst->is_single_location()) {
+ bool has_null_pred = false;
+ PredExprSet * pred_expressions = curr_pred->get_pred_expressions();
+ PredExprSetIter * pred_expr_it = pred_expressions->iterator();
+ while (pred_expr_it->hasNext()) {
+ pred_expr * pred_expression = pred_expr_it->next();
+ if (pred_expression->token == NULLITY) {
+ has_null_pred = true;
+ break;
+ }
+ }
+
+ if (!has_null_pred) {
+// func_inst->print();
+ Predicate * another_branch = new Predicate(func_inst);
+ another_branch->copy_predicate_expr(curr_pred);
+ another_branch->add_predicate_expr(NULLITY, NULL, 1);
+ curr_pred->add_predicate_expr(NULLITY, NULL, 0);
+
+ Predicate * parent = curr_pred->get_parent();
+ parent->add_child(another_branch);
+ }
+ }
+
+ ModelVector<Predicate *> * branches = curr_pred->get_children();
+ for (uint i = 0; i < branches->size(); i++) {
+ Predicate * branch = (*branches)[i];
+ deep_update(branch);
+ }
+}
+
+/* Given curr_pred and next_inst, find the branch following curr_pred that
+ * contains next_inst and the correct predicate.
+ * @return true if branch found, false otherwise.
+ */
+bool FuncNode::follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act,
+ HashTable<FuncInst *, ModelAction *, uintptr_t, 0> * inst_act_map,
+ SnapVector<Predicate *> * unset_predicates)
{
+ /* check if a branch with func_inst and corresponding predicate exists */
+ bool branch_found = false;
+ ModelVector<Predicate *> * branches = (*curr_pred)->get_children();
+ for (uint i = 0; i < branches->size(); i++) {
+ Predicate * branch = (*branches)[i];
+ if (branch->get_func_inst() != next_inst)
+ continue;
+
+ /* check against predicate expressions */
+ bool predicate_correct = true;
+ PredExprSet * pred_expressions = branch->get_pred_expressions();
+ PredExprSetIter * pred_expr_it = pred_expressions->iterator();
+
+ if (pred_expressions->getSize() == 0) {
+ predicate_correct = false;
+ unset_predicates->push_back(branch);
+ }
+ while (pred_expr_it->hasNext()) {
+ pred_expr * pred_expression = pred_expr_it->next();
+ uint64_t last_read, next_read;
+ bool equality;
+
+ switch(pred_expression->token) {
+ case NOPREDICATE:
+ predicate_correct = true;
+ break;
+ case EQUALITY:
+ FuncInst * to_be_compared;
+ ModelAction * last_act;
+
+ to_be_compared = pred_expression->func_inst;
+ last_act = inst_act_map->get(to_be_compared);
+
+ last_read = last_act->get_reads_from_value();
+ next_read = next_act->get_reads_from_value();
+ equality = (last_read == next_read);
+ if (equality != pred_expression->value)
+ predicate_correct = false;
+
+ break;
+ case NULLITY:
+ next_read = next_act->get_reads_from_value();
+ equality = ((void*)next_read == NULL);
+ if (equality != pred_expression->value)
+ predicate_correct = false;
+ break;
+ default:
+ predicate_correct = false;
+ model_print("unkown predicate token\n");
+ break;
+ }
+ }
+
+ if (predicate_correct) {
+ *curr_pred = branch;
+ branch_found = true;
+ break;
+ }
+ }
+
+ return branch_found;
+}
+
+void FuncNode::print_predicate_tree()
+{
+ model_print("digraph function_%s {\n", func_name);
+ predicate_tree_entry->print_pred_subtree();
+ model_print("}\n"); // end of graph
}
/* @param tid thread id
* Print the values read by the last read actions for each memory location
*/
+/*
void FuncNode::print_last_read(uint32_t tid)
{
ASSERT(thrd_read_map.size() > tid);
model_print("last read of thread %d at %p: 0x%x\n", tid, it->getVal(), read_val);
}
}
+*/
#include "action.h"
#include "funcinst.h"
#include "hashtable.h"
+#include "hashset.h"
+#include "predicate.h"
+#include "history.h"
typedef ModelList<FuncInst *> func_inst_list_mt;
-typedef HashTable<void *, uint64_t, uintptr_t, 4, model_malloc, model_calloc, model_free> read_map_t;
+typedef HashTable<void *, uint64_t, uintptr_t, 4> read_map_t;
class FuncNode {
public:
- FuncNode();
+ FuncNode(ModelHistory * history);
~FuncNode();
uint32_t get_func_id() { return func_id; }
const char * get_func_name() { return func_name; }
void set_func_id(uint32_t id) { func_id = id; }
void set_func_name(const char * name) { func_name = name; }
+ void set_new_exec_flag();
- FuncInst * get_or_add_action(ModelAction *act);
+ void add_inst(ModelAction *act);
+ FuncInst * get_inst(ModelAction *act);
HashTable<const char *, FuncInst *, uintptr_t, 4, model_malloc, model_calloc, model_free> * getFuncInstMap() { return &func_inst_map; }
func_inst_list_mt * get_inst_list() { return &inst_list; }
func_inst_list_mt * get_entry_insts() { return &entry_insts; }
void add_entry_inst(FuncInst * inst);
- void link_insts(func_inst_list_t * inst_list);
+
+ void update_tree(action_list_t * act_list);
+ void update_inst_tree(func_inst_list_t * inst_list);
void store_read(ModelAction * act, uint32_t tid);
uint64_t query_last_read(void * location, uint32_t tid);
void clear_read_map(uint32_t tid);
/* TODO: generate EQUALITY or NULLITY predicate based on write_history in history.cc */
- void generate_predicate(FuncInst * func_inst);
+ void update_predicate_tree(action_list_t * act_list);
+ void deep_update(Predicate * pred);
+ bool follow_branch(Predicate ** curr_pred, FuncInst * next_inst, ModelAction * next_act, HashTable<FuncInst *, ModelAction *, uintptr_t, 0>* inst_act_map, SnapVector<Predicate *> * unset_predicates);
+
+ void incr_exit_count() { exit_count++; }
+ uint32_t get_exit_count() { return exit_count; }
+
+ ModelList<action_list_t *> * get_action_list_buffer() { return &action_list_buffer; }
+ void print_predicate_tree();
void print_last_read(uint32_t tid);
MEMALLOC
private:
uint32_t func_id;
const char * func_name;
+ ModelHistory * history;
+ bool predicate_tree_initialized;
+ Predicate * predicate_tree_entry; // a dummy node whose children are the real entries
+
+ uint32_t exit_count;
/* Use source line number as the key of hashtable, to check if
* atomic operation with this line number has been added or not
/* Store the values read by atomic read actions per memory location for each thread */
ModelVector<read_map_t *> thrd_read_map;
- ModelList<void *> read_locations;
+
+ ModelList<action_list_t *> action_list_buffer;
};
-#endif /* __FUNCNODE_H__ */
+#endif /* __FUNCNODE_H__ */
#include <stdlib.h>
#include "threads-model.h"
#include "model.h"
+#include "action.h"
int Fuzzer::selectWrite(ModelAction *read, SnapVector<ModelAction *> * rf_set) {
int random_index = random() % rf_set->size();
waiters->erase(it);
return thread;
}
+
+bool Fuzzer::shouldSleep(const ModelAction *sleep) {
+ return true;
+}
+
+bool Fuzzer::shouldWake(const ModelAction *sleep) {
+ struct timespec currtime;
+ clock_gettime(CLOCK_MONOTONIC, &currtime);
+ uint64_t lcurrtime = currtime.tv_sec * 1000000000 + currtime.tv_nsec;
+
+ return ((sleep->get_time()+sleep->get_value()) >= lcurrtime);
+}
int selectWrite(ModelAction *read, SnapVector<ModelAction *>* rf_set);
Thread * selectThread(int * threadlist, int numthreads);
Thread * selectNotify(action_list_t * waiters);
+ bool shouldSleep(const ModelAction *sleep);
+ bool shouldWake(const ModelAction *sleep);
MEMALLOC
private:
};
LinkNode<_Key> *next;
};
-template<typename _Key, typename _KeyInt, int _Shift, void *
- (* _malloc)(size_t), void * (* _calloc)(size_t, size_t), void (*_free)(void *), unsigned int (*hash_function
- )(_Key), bool (*equals)(_Key, _Key)>
+template<typename _Key, typename _KeyInt, int _Shift, void * (* _malloc)(size_t), void * (* _calloc)(size_t, size_t), void (*_free)(void *), unsigned int (*hash_function)(_Key), bool (*equals)(_Key, _Key)>
class HashSet;
template<typename _Key, typename _KeyInt, int _Shift, void * (* _malloc)(size_t), void * (* _calloc)(size_t, size_t), void (*_free)(void *), unsigned int (*hash_function)(_Key) = default_hash_function<_Key, _Shift, _KeyInt>, bool (*equals)(_Key, _Key) = default_equals<_Key> >
func_map(),
func_map_rev(),
func_nodes(),
- write_history()
+ write_history(),
+ write_locations()
{}
void ModelHistory::enter_function(const uint32_t func_id, thread_id_t tid)
{
//model_print("thread %d entering func %d\n", tid, func_id);
- uint32_t id = id_to_int(tid);
+ uint id = id_to_int(tid);
SnapVector<func_id_list_t> * thrd_func_list = model->get_execution()->get_thrd_func_list();
- SnapVector< SnapList<func_inst_list_t *> *> *
- thrd_func_inst_lists = model->get_execution()->get_thrd_func_inst_lists();
+ SnapVector< SnapList<action_list_t *> *> *
+ thrd_func_act_lists = model->get_execution()->get_thrd_func_act_lists();
if ( thrd_func_list->size() <= id ) {
uint oldsize = thrd_func_list->size();
thrd_func_list->resize( id + 1 );
- for(uint i=oldsize;i<id+1;i++) {
- new(&(*thrd_func_list)[i]) func_id_list_t();
+ for (uint i = oldsize; i < id + 1; i++) {
+ new (&(*thrd_func_list)[i]) func_id_list_t();
+ // push 0 as a dummy function id to a void seg fault
+ (*thrd_func_list)[i].push_back(0);
}
- thrd_func_inst_lists->resize( id + 1 );
- }
- SnapList<func_inst_list_t *> * func_inst_lists = thrd_func_inst_lists->at(id);
-
- if (func_inst_lists == NULL) {
- func_inst_lists = new SnapList< func_inst_list_t *>();
- thrd_func_inst_lists->at(id) = func_inst_lists;
+ thrd_func_act_lists->resize( id + 1 );
+ for (uint i = oldsize; i < id + 1; i++) {
+ (*thrd_func_act_lists)[i] = new SnapList<action_list_t *>();
+ }
}
+ SnapList<action_list_t *> * func_act_lists = (*thrd_func_act_lists)[id];
+
(*thrd_func_list)[id].push_back(func_id);
- func_inst_lists->push_back( new func_inst_list_t() );
+ func_act_lists->push_back( new action_list_t() );
if ( func_nodes.size() <= func_id )
resize_func_nodes( func_id + 1 );
{
uint32_t id = id_to_int(tid);
SnapVector<func_id_list_t> * thrd_func_list = model->get_execution()->get_thrd_func_list();
- SnapVector< SnapList<func_inst_list_t *> *> *
- thrd_func_inst_lists = model->get_execution()->get_thrd_func_inst_lists();
+ SnapVector< SnapList<action_list_t *> *> *
+ thrd_func_act_lists = model->get_execution()->get_thrd_func_act_lists();
- SnapList<func_inst_list_t *> * func_inst_lists = thrd_func_inst_lists->at(id);
+ SnapList<action_list_t *> * func_act_lists = (*thrd_func_act_lists)[id];
uint32_t last_func_id = (*thrd_func_list)[id].back();
if (last_func_id == func_id) {
FuncNode * func_node = func_nodes[func_id];
func_node->clear_read_map(tid);
- func_inst_list_t * curr_inst_list = func_inst_lists->back();
- func_node->link_insts(curr_inst_list);
+ action_list_t * curr_act_list = func_act_lists->back();
+
+ func_node->incr_exit_count();
+
+ /* defer the processing of curr_act_list until the function has exits a few times
+ * (currently 2 times) so that more information can be gathered to infer nullity predicates.
+ */
+ if (func_node->get_exit_count() >= 2) {
+ ModelList<action_list_t *> * action_list_buffer = func_node->get_action_list_buffer();
+ while (action_list_buffer->size() > 0) {
+ action_list_t * act_list = action_list_buffer->back();
+ action_list_buffer->pop_back();
+ func_node->update_tree(act_list);
+ }
+
+ func_node->update_tree(curr_act_list);
+ } else
+ func_node->get_action_list_buffer()->push_front(curr_act_list);
(*thrd_func_list)[id].pop_back();
- func_inst_lists->pop_back();
+ func_act_lists->pop_back();
} else {
model_print("trying to exit with a wrong function id\n");
model_print("--- last_func: %d, func_id: %d\n", last_func_id, func_id);
for (uint32_t id = old_size;id < new_size;id++) {
const char * func_name = func_map_rev[id];
- FuncNode * func_node = new FuncNode();
+ FuncNode * func_node = new FuncNode(this);
func_node->set_func_id(id);
func_node->set_func_name(func_name);
func_nodes[id] = func_node;
/* return if thread i has not entered any function or has exited
from all functions */
SnapVector<func_id_list_t> * thrd_func_list = model->get_execution()->get_thrd_func_list();
- SnapVector< SnapList<func_inst_list_t *> *> *
- thrd_func_inst_lists = model->get_execution()->get_thrd_func_inst_lists();
+ SnapVector< SnapList<action_list_t *> *> *
+ thrd_func_act_lists = model->get_execution()->get_thrd_func_act_lists();
uint32_t id = id_to_int(tid);
if ( thrd_func_list->size() <= id )
/* get the function id that thread i is currently in */
uint32_t func_id = (*thrd_func_list)[id].back();
- SnapList<func_inst_list_t *> * func_inst_lists = thrd_func_inst_lists->at(id);
+ SnapList<action_list_t *> * func_act_lists = (*thrd_func_act_lists)[id];
- if ( func_nodes.size() <= func_id )
+ if (act->is_write())
+ add_to_write_history(act->get_location(), act->get_write_value());
+
+ if (func_id == 0)
+ return;
+ else if ( func_nodes.size() <= func_id )
resize_func_nodes( func_id + 1 );
FuncNode * func_node = func_nodes[func_id];
- ASSERT (func_node != NULL);
- /* add corresponding FuncInst to func_node */
- FuncInst * inst = func_node->get_or_add_action(act);
+ /* do not care about actions without a position */
- if (inst == NULL)
+ if (act->get_position() == NULL)
return;
- // if (inst->is_read())
- // func_node->store_read(act, tid);
-
- if (inst->is_write())
- add_to_write_history(act->get_location(), act->get_write_value());
+ if (act->is_read())
+ func_node->store_read(act, tid);
/* add to curr_inst_list */
- func_inst_list_t * curr_inst_list = func_inst_lists->back();
- ASSERT(curr_inst_list != NULL);
- curr_inst_list->push_back(inst);
+
+ bool second_part_of_rmw = act->is_rmwc() || act->is_rmw();
+ if (!second_part_of_rmw) {
+ action_list_t * curr_act_list = func_act_lists->back();
+ ASSERT(curr_act_list != NULL);
+
+ ModelAction * last_act;
+ if (curr_act_list->size() != 0)
+ last_act = curr_act_list->back();
+
+ // do not add actions with the same sequence number twice
+ if (last_act != NULL && last_act->get_seq_number() == act->get_seq_number())
+ return;
+
+ curr_act_list->push_back(act);
+ func_node->add_inst(act);
+ }
}
/* return the FuncNode given its func_id */
FuncNode * ModelHistory::get_func_node(uint32_t func_id)
{
- if (func_nodes.size() <= func_id) // this node has not been added
+ if (func_nodes.size() <= func_id) // this node has not been added to func_nodes
return NULL;
return func_nodes[func_id];
void ModelHistory::add_to_write_history(void * location, uint64_t write_val)
{
- if ( !write_history.contains(location) )
- write_history.put(location, new write_set_t() );
-
write_set_t * write_set = write_history.get(location);
+
+ if (write_set == NULL) {
+ write_set = new write_set_t();
+ write_history.put(location, write_set);
+ }
+
write_set->add(write_val);
+ write_locations.add(location);
+}
+
+void ModelHistory::set_new_exec_flag()
+{
+ for (uint i = 1; i < func_nodes.size(); i++) {
+ FuncNode * func_node = func_nodes[i];
+ func_node->set_new_exec_flag();
+ }
}
-void ModelHistory::print()
+void ModelHistory::print_write()
+{
+}
+
+void ModelHistory::print_func_node()
{
/* function id starts with 1 */
- for (uint32_t i = 1;i < func_nodes.size();i++) {
+ for (uint32_t i = 1; i < func_nodes.size(); i++) {
FuncNode * func_node = func_nodes[i];
func_inst_list_mt * entry_insts = func_node->get_entry_insts();
FuncInst *inst = it->getVal();
model_print("type: %d, at: %s\n", inst->get_type(), inst->get_position());
}
-
/*
func_inst_list_mt * inst_list = funcNode->get_inst_list();
FuncInst *inst = *it;
model_print("type: %d, at: %s\n", inst->get_type(), inst->get_position());
}
- */
+*/
}
}
#include "hashset.h"
#include "threads-model.h"
-typedef HashSet<uint64_t, uint64_t, 0, model_malloc, model_calloc, model_free> write_set_t;
class ModelHistory {
public:
uint64_t query_last_read(void * location, thread_id_t tid);
void add_to_write_history(void * location, uint64_t write_val);
+ HashTable<void *, write_set_t *, uintptr_t, 4> * getWriteHistory() { return &write_history; }
- void print();
+ void set_new_exec_flag();
+ void print_write();
+ void print_func_node();
MEMALLOC
private:
ModelVector<const char *> func_map_rev;
ModelVector<FuncNode *> func_nodes;
- HashTable<void *, write_set_t *, uintptr_t, 4, model_malloc, model_calloc, model_free> write_history;
+
+ HashTable<void *, write_set_t *, uintptr_t, 4> write_history;
+ HashSet<void *, uintptr_t, 4> write_locations;
};
#endif /* __HISTORY_H__ */
int user_main(int, char**);
}
-void check();
#endif
return *((uint64_t *)addr);
}
-// helper functions used by CdsPass
-// The CdsPass implementation does not replace normal load/stores with cds load/stores,
-// but inserts cds load/stores to check dataraces. Thus, the cds load/stores do not
-// return anything.
+/**
+ * Helper functions used by CDSPass
+ * The CDSPass implementation does not replace normal load/stores with cds load/stores,
+ * but inserts cds load/stores to check dataraces. Thus, the cds load/stores do not
+ * return anything.
+ */
void cds_store8(void *addr)
{
params->uninitvalue = 0;
params->maxexecutions = 10;
params->nofork = false;
+ params->threadsnocleanup = false;
}
static void print_usage(const char *program_name, struct model_params *params)
" Default: %u\n"
" -o help for a list of options\n"
"-n No fork\n"
+#ifdef TLS
+ "-d Don't allow threads to cleanup\n"
+#endif
" -- Program arguments follow.\n\n",
program_name,
params->verbose,
static void parse_options(struct model_params *params, int argc, char **argv)
{
- const char *shortopts = "hnt:o:u:x:v::";
+ const char *shortopts = "hdnt:o:u:x:v::";
const struct option longopts[] = {
{"help", no_argument, NULL, 'h'},
{"verbose", optional_argument, NULL, 'v'},
case 'h':
print_usage(argv[0], params);
break;
+ case 'd':
+ params->threadsnocleanup = true;
+ break;
case 'n':
params->nofork = true;
break;
"Distributed under the GPLv2\n"
"Written by Weiyu Luo, Brian Norris, and Brian Demsky\n\n");
- /* Configure output redirection for the model-checker */
- redirect_output();
//Initialize snapshotting library and model checker object
if (!model) {
model->startChecker();
}
+ /* Configure output redirection for the model-checker */
+ redirect_output();
+
register_plugins();
//Parse command line options
// test code
execution_number ++;
reset_to_initial_state();
+ history->set_new_exec_flag();
return false;
}
main_thread_startup();
}
-static bool is_nonsc_write(const ModelAction *act) {
- if (act->get_type() == ATOMIC_WRITE) {
- std::memory_order order = act->get_mo();
- switch(order) {
- case std::memory_order_relaxed:
- case std::memory_order_release:
- return true;
- default:
- return false;
- }
- }
- return false;
-}
-
/** @brief Run ModelChecker for the user program */
void ModelChecker::run()
{
/* Have the trace analyses dump their output. */
for (unsigned int i = 0;i < trace_analyses.size();i++)
trace_analyses[i]->finish();
+
+ /* unlink tmp file created by last child process */
+ char filename[256];
+ snprintf_(filename, sizeof(filename), "C11FuzzerTmp%d", getpid());
+ unlink(filename);
}
void startMainThread();
void startChecker();
Thread * getInitThread() {return init_thread;}
+ Scheduler * getScheduler() {return scheduler;}
MEMALLOC
private:
/** Flag indicates whether to restart the model checker. */
unsigned int uninitvalue;
int maxexecutions;
bool nofork;
+ bool threadsnocleanup;
/** @brief Verbosity (0 = quiet; 1 = noisy; 2 = noisier) */
int verbose;
#include "predicate.h"
-inline bool operator==(const predicate_expr& expr_A, const predicate_expr& expr_B)
+Predicate::Predicate(FuncInst * func_inst, bool is_entry) :
+ func_inst(func_inst),
+ entry_predicate(is_entry),
+ pred_expressions(16),
+ children(),
+ parent(NULL),
+ backedges(16)
+{}
+
+unsigned int pred_expr_hash(struct pred_expr * expr)
{
- if (expr_A.token != expr_B.token)
- return false;
+ return (unsigned int)((uintptr_t)expr);
+}
- if (expr_A.token == EQUALITY && expr_A.location != expr_B.location)
+bool pred_expr_equal(struct pred_expr * p1, struct pred_expr * p2)
+{
+ if (p1->token != p2->token)
return false;
-
- if (expr_A.value != expr_B.value)
+ if (p1->token == EQUALITY && p1->func_inst != p2->func_inst)
+ return false;
+ if (p1->value != p2->value)
return false;
-
return true;
}
-void Predicate::add_predicate(predicate_expr predicate)
+void Predicate::add_predicate_expr(token_t token, FuncInst * func_inst, bool value)
+{
+ struct pred_expr *ptr = new pred_expr(token, func_inst, value);
+ pred_expressions.add(ptr);
+}
+
+void Predicate::add_child(Predicate * child)
+{
+ /* check duplication? */
+ children.push_back(child);
+}
+
+void Predicate::copy_predicate_expr(Predicate * other)
+{
+ PredExprSet * other_pred_expressions = other->get_pred_expressions();
+ PredExprSetIter * it = other_pred_expressions->iterator();
+
+ while (it->hasNext()) {
+ struct pred_expr * ptr = it->next();
+ struct pred_expr * copy = new pred_expr(ptr->token, ptr->func_inst, ptr->value);
+ pred_expressions.add(copy);
+ }
+}
+
+void Predicate::print_predicate()
+{
+ model_print("\"%p\" [shape=box, label=\"\n", this);
+ if (entry_predicate) {
+ model_print("entry node\"];\n");
+ return;
+ }
+
+ func_inst->print();
+
+ PredExprSetIter * it = pred_expressions.iterator();
+
+ if (pred_expressions.getSize() == 0)
+ model_print("predicate unset\n");
+
+ while (it->hasNext()) {
+ struct pred_expr * expr = it->next();
+ FuncInst * inst = expr->func_inst;
+ switch (expr->token) {
+ case NOPREDICATE:
+ break;
+ case EQUALITY:
+ model_print("predicate token: equality, position: %s, value: %d\n", inst->get_position(), expr->value);
+ break;
+ case NULLITY:
+ model_print("predicate token: nullity, value: %d\n", expr->value);
+ break;
+ default:
+ model_print("unknown predicate token\n");
+ break;
+ }
+ }
+ model_print("\"];\n");
+}
+
+void Predicate::print_pred_subtree()
{
- ModelList<predicate_expr>::iterator it;
- for (it = predicates.begin();it != predicates.end();it++) {
- if (predicate == *it)
- return;
+ print_predicate();
+ for (uint i = 0; i < children.size(); i++) {
+ Predicate * child = children[i];
+ child->print_pred_subtree();
+ model_print("\"%p\" -> \"%p\"\n", this, child);
}
- predicates.push_back(predicate);
+ PredSetIter * it = backedges.iterator();
+ while (it->hasNext()) {
+ Predicate * backedge = it->next();
+ model_print("\"%p\" -> \"%p\"[style=dashed, color=grey]\n", this, backedge);
+ }
}
+#ifndef __PREDICTAE_H__
+#define __PREDICATE_H__
+
#include "funcinst.h"
+#include "hashset.h"
+
+unsigned int pred_expr_hash (struct pred_expr *);
+bool pred_expr_equal(struct pred_expr *, struct pred_expr *);
+typedef HashSet<struct pred_expr *, uintptr_t, 0, model_malloc, model_calloc, model_free, pred_expr_hash, pred_expr_equal> PredExprSet;
+typedef HSIterator<struct pred_expr *, uintptr_t, 0, model_malloc, model_calloc, model_free, pred_expr_hash, pred_expr_equal> PredExprSetIter;
typedef enum predicate_token {
- EQUALITY, NULLITY
+ NOPREDICATE, EQUALITY, NULLITY
} token_t;
/* If token is EQUALITY, then the predicate asserts whether
* this load should read the same value as the last value
* read at memory location specified in predicate_expr.
*/
-struct predicate_expr {
+struct pred_expr {
+ pred_expr(token_t token, FuncInst * inst, bool value) :
+ token(token),
+ func_inst(inst),
+ value(value)
+ {}
+
token_t token;
- void * location;
+ FuncInst * func_inst;
bool value;
+
+ MEMALLOC
};
+
class Predicate {
public:
- Predicate();
+ Predicate(FuncInst * func_inst, bool is_entry = false);
~Predicate();
FuncInst * get_func_inst() { return func_inst; }
- ModelList<predicate_expr> * get_predicates() { return &predicates; }
- void add_predicate(predicate_expr predicate);
+ PredExprSet * get_pred_expressions() { return &pred_expressions; }
+
+ void add_predicate_expr(token_t token, FuncInst * func_inst, bool value);
+ void add_child(Predicate * child);
+ void set_parent(Predicate * parent_pred) { parent = parent_pred; }
+ void add_backedge(Predicate * back_pred) { backedges.add(back_pred); }
+ void copy_predicate_expr(Predicate * other);
+
+ ModelVector<Predicate *> * get_children() { return &children; }
+ Predicate * get_parent() { return parent; }
+ PredSet * get_backedges() { return &backedges; }
+
+ bool is_entry_predicate() { return entry_predicate; }
+ void set_entry_predicate() { entry_predicate = true; }
+
+ void print_predicate();
+ void print_pred_subtree();
MEMALLOC
private:
FuncInst * func_inst;
- /* may have multiple precicates */
- ModelList<predicate_expr> predicates;
+ bool entry_predicate;
+
+ /* may have multiple predicate expressions */
+ PredExprSet pred_expressions;
+ ModelVector<Predicate *> children;
+
+ /* only a single parent may exist */
+ Predicate * parent;
+
+ /* may have multiple back edges, e.g. nested loops */
+ PredSet backedges;
};
+
+#endif /* __PREDICATE_H__ */
#include "mutex.h"
#include <condition_variable>
-#include <assert.h>
/* global "model" object */
#include "model.h"
#include "execution.h"
+extern "C" {
+int nanosleep(const struct timespec *rqtp, struct timespec *rmtp);
+}
+
+int nanosleep(const struct timespec *rqtp, struct timespec *rmtp) {
+ if (model) {
+ uint64_t time = rqtp->tv_sec * 1000000000 + rqtp->tv_nsec;
+ struct timespec currtime;
+ clock_gettime(CLOCK_MONOTONIC, &currtime);
+ uint64_t lcurrtime = currtime.tv_sec * 1000000000 + currtime.tv_nsec;
+ model->switch_to_master(new ModelAction(THREAD_SLEEP, std::memory_order_seq_cst, time, lcurrtime));
+ if (rmtp != NULL) {
+ clock_gettime(CLOCK_MONOTONIC, &currtime);
+ uint64_t lendtime = currtime.tv_sec * 1000000000 + currtime.tv_nsec;
+ uint64_t elapsed = lendtime - lcurrtime;
+ rmtp->tv_sec = elapsed / 1000000000;
+ rmtp->tv_nsec = elapsed - rmtp->tv_sec * 1000000000;
+ }
+ }
+ return 0;
+}
int pthread_create(pthread_t *t, const pthread_attr_t * attr,
pthread_start_t start_routine, void * arg) {
}
int pthread_join(pthread_t t, void **value_ptr) {
-// Thread *th = model->get_pthread(t);
ModelExecution *execution = model->get_execution();
Thread *th = execution->get_pthread(t);
}
int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t *) {
- cdsc::snapmutex *m = new cdsc::snapmutex();
-
if (!model) {
snapshot_system_init(10000, 1024, 1024, 40000);
model = new ModelChecker();
model->startChecker();
}
+ cdsc::snapmutex *m = new cdsc::snapmutex();
ModelExecution *execution = model->get_execution();
execution->getMutexMap()->put(p_mutex, m);
model->startChecker();
}
-
ModelExecution *execution = model->get_execution();
/* to protect the case where PTHREAD_MUTEX_INITIALIZER is used
pthread_mutex_init(p_mutex, NULL);
cdsc::snapcondition_variable *v = execution->getCondMap()->get(p_cond);
- cdsc::snapmutex *m = execution->getMutexMap()->get(p_mutex);
+// cdsc::snapmutex *m = execution->getMutexMap()->get(p_mutex);
model->switch_to_master(new ModelAction(NOOP, std::memory_order_seq_cst, v));
// v->wait(*m);
v->notify_all();
return 0;
}
+
+int pthread_cond_destroy(pthread_cond_t *p_cond) {
+ ModelExecution *execution = model->get_execution();
+
+ if (execution->getCondMap()->contains(p_cond)) {
+ cdsc::snapcondition_variable *v = execution->getCondMap()->get(p_cond);
+ delete v;
+ execution->getCondMap()->remove(p_cond);
+ }
+ return 0;
+}
#include "context.h"
#include "model.h"
+
+#if USE_MPROTECT_SNAPSHOT
+
/** PageAlignedAdressUpdate return a page aligned address for the
* address being added as a side effect the numBytes are also changed.
*/
return (void *)((((uintptr_t)addr) + PAGESIZE - 1) & ~(PAGESIZE - 1));
}
-#if USE_MPROTECT_SNAPSHOT
-
/* Each SnapShotRecord lists the firstbackingpage that must be written to
* revert to that snapshot */
struct SnapShotRecord {
/* global "model" object */
#include "model.h"
#include "execution.h"
+#include "schedule.h"
#ifdef TLS
#include <dlfcn.h>
if (stack)
stack_free(stack);
#ifdef TLS
- if (this != model->getInitThread()) {
+ if (this != model->getInitThread() && !model->getParams()->threadsnocleanup) {
modellock = 1;
+ ASSERT(thread_current()==NULL);
+ Thread * curr_thread = model->getScheduler()->get_current_thread();
+ //Make any current_thread calls work in code to free
+ model->getScheduler()->set_current_thread(this);
real_pthread_mutex_unlock(&mutex2);
real_pthread_join(thread, NULL);
+ model->getScheduler()->set_current_thread(curr_thread);
modellock = 0;
}
#endif
projects / c11tester.git / commitdiff