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
++ sleeps.o history.o
CPPFLAGS += -Iinclude -I.
LDFLAGS := -ldl -lrt -rdynamic
malloc.o: malloc.c
$(CC) -fPIC -c malloc.c -DMSPACES -DONLY_MSPACES -DHAVE_MMAP=0 $(CPPFLAGS) -Wno-unused-variable
+ futex.o: futex.cc
+ $(CXX) -fPIC -c futex.cc -std=c++11 $(CPPFLAGS)
%.o : %.cc
$(CXX) -MMD -MF .$@.d -fPIC -c $< $(CPPFLAGS)
public:
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, const char * position, memory_order order, void *loc, uint64_t value = VALUE_NONE, Thread *thread = NULL);
~ModelAction();
void print() const;
/* to accomodate pthread create and join */
Thread * thread_operand;
void set_thread_operand(Thread *th) { thread_operand = th; }
- MEMALLOC
+ SNAPSHOTALLOC
private:
const char * get_type_str() const;
const char * get_mo_str() const;
#include <stdio.h>
+ #include <string>
+
#include "model.h"
#include "execution.h"
#include "action.h"
+ #include "history.h"
#include "cmodelint.h"
+#include "snapshot-interface.h"
#include "threads-model.h"
memory_order orders[6] = {
memory_order_release, memory_order_acq_rel, memory_order_seq_cst
};
+#define ensureModel(action) \
+ if (!modelchecker_started) { \
+ if (!model) { \
+ snapshot_system_init(10000, 1024, 1024, 40000); \
+ model = new ModelChecker(); \
+ } \
+ model->get_execution()->check_current_action(action); \
+ }else { \
+ model->switch_to_master(action); \
+ }
+
+
+#define ensureModelValue(action, type) \
+ if (!modelchecker_started) { \
+ if (!model) { \
+ snapshot_system_init(10000, 1024, 1024, 40000); \
+ model = new ModelChecker(); \
+ } \
+ model->get_execution()->check_current_action(action); \
+ return (type) thread_current()->get_return_value(); \
+ } else { \
+ return (type) model->switch_to_master(action); \
+ }
+
/** Performs a read action.*/
uint64_t model_read_action(void * obj, memory_order ord) {
return model->switch_to_master(new ModelAction(ATOMIC_READ, ord, obj));
/* --- helper functions --- */
uint64_t model_rmwrcas_action_helper(void *obj, int atomic_index, uint64_t oldval, int size, const char *position) {
- ensureModelValue(new ModelAction(ATOMIC_RMWRCAS, position, orders[atomic_index], obj), uint64_t);
- return model->switch_to_master(
- new ModelAction(ATOMIC_RMWRCAS, position, orders[atomic_index], obj, oldval, size)
++ ensureModelValue(
++ new ModelAction(ATOMIC_RMWRCAS, position, orders[atomic_index], obj, oldval, size), uint64_t
+ );
}
uint64_t model_rmwr_action_helper(void *obj, int atomic_index, const char *position) {
- return model->switch_to_master(
- new ModelAction(ATOMIC_RMWR, position, orders[atomic_index], obj)
- );
+ ensureModelValue(new ModelAction(ATOMIC_RMWR, position, orders[atomic_index], obj), uint64_t);
}
void model_rmw_action_helper(void *obj, uint64_t val, int atomic_index, const char * position) {
- model->switch_to_master(
- new ModelAction(ATOMIC_RMW, position, orders[atomic_index], obj, val)
- );
+ ensureModel(new ModelAction(ATOMIC_RMW, position, orders[atomic_index], obj, val));
}
void model_rmwc_action_helper(void *obj, int atomic_index, const char *position) {
- model->switch_to_master(
- new ModelAction(ATOMIC_RMWC, position, orders[atomic_index], obj)
- );
+ ensureModel(new ModelAction(ATOMIC_RMWC, position, orders[atomic_index], obj));
}
// cds atomic inits
void cds_atomic_init8(void * obj, uint8_t val, const char * position) {
- model->switch_to_master(
+ ensureModel(
new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
);
}
void cds_atomic_init16(void * obj, uint16_t val, const char * position) {
- model->switch_to_master(
+ ensureModel(
new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
);
}
void cds_atomic_init32(void * obj, uint32_t val, const char * position) {
- model->switch_to_master(
+ ensureModel(
new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, (uint64_t) val)
);
}
void cds_atomic_init64(void * obj, uint64_t val, const char * position) {
- model->switch_to_master(
+ ensureModel(
new ModelAction(ATOMIC_INIT, position, memory_order_relaxed, obj, val)
);
}
// cds atomic loads
uint8_t cds_atomic_load8(void * obj, int atomic_index, const char * position) {
- return (uint8_t) ( model->switch_to_master(
- new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj))
- );
+ ensureModelValue(
+ new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj), uint8_t);
}
uint16_t cds_atomic_load16(void * obj, int atomic_index, const char * position) {
- return (uint16_t) ( model->switch_to_master(
- new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj))
- );
+ ensureModelValue(
+ new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj), uint16_t);
}
uint32_t cds_atomic_load32(void * obj, int atomic_index, const char * position) {
- return (uint32_t) ( model->switch_to_master(
- new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj))
- );
+ ensureModelValue(
+ new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj), uint32_t
+ );
}
uint64_t cds_atomic_load64(void * obj, int atomic_index, const char * position) {
- return model->switch_to_master(
- new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj)
- );
+ ensureModelValue(
+ new ModelAction(ATOMIC_READ, position, orders[atomic_index], obj), uint64_t);
}
// cds atomic stores
void cds_atomic_store8(void * obj, uint8_t val, int atomic_index, const char * position) {
- model->switch_to_master(
+ ensureModel(
new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)
);
}
void cds_atomic_store16(void * obj, uint16_t val, int atomic_index, const char * position) {
- model->switch_to_master(
+ ensureModel(
new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)
);
}
void cds_atomic_store32(void * obj, uint32_t val, int atomic_index, const char * position) {
- model->switch_to_master(
+ ensureModel(
new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)
);
}
void cds_atomic_store64(void * obj, uint64_t val, int atomic_index, const char * position) {
- model->switch_to_master(
+ ensureModel(
new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, val)
);
}
__old__ = __old__; Silence clang (-Wunused-value) \
})
*/
- Thread * th = thread_current();
+
+ void cds_func_entry(const char * funcName) {
+ if (!model) return;
+
- Thread * th = thread_current();
++ Thread * th = thread_current();
+ uint32_t func_id;
+
+ ModelHistory *history = model->get_history();
+ if ( !history->getFuncMap()->contains(funcName) ) {
+ func_id = history->get_func_counter();
+ history->incr_func_counter();
+
+ history->getFuncMap()->put(funcName, func_id);
+ } else {
+ func_id = history->getFuncMap()->get(funcName);
+ }
+
+ history->enter_function(func_id, th->get_id());
+ }
+
+ void cds_func_exit(const char * funcName) {
+ if (!model) return;
+
++ Thread * th = thread_current();
+ uint32_t func_id;
+
+ ModelHistory *history = model->get_history();
+ func_id = history->getFuncMap()->get(funcName);
+
+ history->exit_function(func_id, th->get_id());
+ }
thrd_last_fence_release(),
node_stack(node_stack),
priv(new struct model_snapshot_members ()),
-- mo_graph(new CycleGraph()),
++ mo_graph(new CycleGraph()),
fuzzer(new Fuzzer())
{
/* Initialize a model-checker thread, for special ModelActions */
/* Last SC fence in the current thread */
ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
- ModelAction *last_sc_write = NULL;
- if (curr->is_seqcst())
- last_sc_write = get_last_seq_cst_write(curr);
int tid = curr->get_tid();
ModelAction *prev_same_thread = NULL;
--- /dev/null
- func_id(1), /* function id starts with 1 */
+ #include <inttypes.h>
+ #include "history.h"
+ #include "action.h"
+
+ ModelHistory::ModelHistory() :
++ func_id(1), /* function id starts with 1 */
+ func_map(),
+ func_history(),
+ work_list()
+ {}
+
+ void ModelHistory::enter_function(const uint32_t func_id, thread_id_t tid)
+ {
+ if ( !work_list.contains(tid) ) {
+ // This thread has not been pushed to work_list
+ SnapList<uint32_t> * func_list = new SnapList<uint32_t>();
+ func_list->push_back(func_id);
+ work_list.put(tid, func_list);
+ } else {
+ SnapList<uint32_t> * func_list = work_list.get(tid);
+ func_list->push_back(func_id);
+ }
+ }
+
+ void ModelHistory::exit_function(const uint32_t func_id, thread_id_t tid)
+ {
+ SnapList<uint32_t> * func_list = work_list.get(tid);
+ uint32_t last_func_id = func_list->back();
+
+ if (last_func_id == func_id) {
+ func_list->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);
+ }
+ }
--- /dev/null
-
+ #include "stl-model.h"
+ #include "common.h"
+ #include "hashtable.h"
+ #include "modeltypes.h"
+
+ /* forward declaration */
+ class ModelAction;
+
+ typedef ModelList<ModelAction *> action_mlist_t;
+
+ class ModelHistory {
+ public:
+ ModelHistory();
- uint32_t get_func_counter() { return func_id; }
- void incr_func_counter() { func_id++; }
++
+ void enter_function(const uint32_t func_id, thread_id_t tid);
+ void exit_function(const uint32_t func_id, thread_id_t tid);
+
- HashTable<const char *, uint32_t, uintptr_t, 4> * getFuncMap() { return &func_map; }
++ uint32_t get_func_counter() { return func_id; }
++ void incr_func_counter() { func_id++; }
+
- /* map function names to integer ids */
- HashTable<const char *, uint32_t, uintptr_t, 4> func_map;
++ HashTable<const char *, uint32_t, uintptr_t, 4> * getFuncMap() { return &func_map; }
+ HashTable<uint32_t, action_mlist_t *, uintptr_t, 4> * getFuncHistory() { return &func_history; }
+
+ void print();
+
+ private:
+ uint32_t func_id;
+
- * the functions that thread i has entered and yet to exit from
++ /* map function names to integer ids */
++ HashTable<const char *, uint32_t, uintptr_t, 4> func_map;
+
+ HashTable<uint32_t, action_mlist_t *, uintptr_t, 4> func_history;
+
+ /* work_list stores a list of function ids for each thread
+ * SnapList<uint32_t> is intended to be used as a stack storing
++ * the functions that thread i has entered and yet to exit from
+ */
+ HashTable<thread_id_t, SnapList<uint32_t> *, uintptr_t, 4> work_list;
+ };
#if __cplusplus
using std::memory_order;
extern "C" {
+#else
+typedef int bool;
#endif
+
uint64_t model_read_action(void * obj, memory_order ord);
void model_write_action(void * obj, memory_order ord, uint64_t val);
void model_init_action(void * obj, uint64_t val);
// cds atomic thread fence
void cds_atomic_thread_fence(int atomic_index, const char * position);
+ void cds_func_entry(const char * funcName);
+ void cds_func_exit(const char * funcName);
+
#if __cplusplus
}
#endif
#include "output.h"
#include "traceanalysis.h"
#include "execution.h"
+ #include "history.h"
#include "bugmessage.h"
+#include "params.h"
-ModelChecker *model;
+ModelChecker *model = NULL;
+bool modelchecker_started = false;
+
+/** Wrapper to run the user's main function, with appropriate arguments */
+void user_main_wrapper(void *)
+{
+ user_main(model->params.argc, model->params.argv);
+}
/** @brief Constructor */
ModelChecker::ModelChecker() :
scheduler(new Scheduler()),
node_stack(new NodeStack()),
execution(new ModelExecution(this, scheduler, node_stack)),
+ history(new ModelHistory()),
execution_number(1),
trace_analyses(),
inspect_plugin(NULL)
{
memset(&stats,0,sizeof(struct execution_stats));
+ init_thread = new Thread(execution->get_next_id(), (thrd_t *) malloc(sizeof(thrd_t)), &user_main_wrapper, NULL, NULL); // L: user_main_wrapper passes the user program
+ execution->add_thread(init_thread);
+ scheduler->set_current_thread(init_thread);
+ execution->setParams(¶ms);
+ param_defaults(¶ms);
}
/** @brief Destructor */
}
/** Method to set parameters */
-void ModelChecker::setParams(struct model_params params) {
- this->params = params;
- execution->setParams(¶ms);
+model_params * ModelChecker::getParams() {
+ return ¶ms;
}
/**
*/
void ModelChecker::reset_to_initial_state()
{
- DEBUG("+++ Resetting to initial state +++\n");
- node_stack->reset_execution();
/**
* FIXME: if we utilize partial rollback, we will need to free only
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();
- node_stack->full_reset();
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());
}
/**
Thread *old = thread_current();
scheduler->set_current_thread(NULL);
ASSERT(!old->get_pending());
-/* W: No plugin
- if (inspect_plugin != NULL) {
- inspect_plugin->inspectModelAction(act);
- }*/
+
+ if (inspect_plugin != NULL) {
+ inspect_plugin->inspectModelAction(act);
+ }
+
old->set_pending(act);
if (Thread::swap(old, &system_context) < 0) {
perror("swap threads");
return old->get_return_value();
}
-/** Wrapper to run the user's main function, with appropriate arguments */
-void user_main_wrapper(void *)
-{
- user_main(model->params.argc, model->params.argv);
-}
-
bool ModelChecker::should_terminate_execution()
{
/* Infeasible -> don't take any more steps */
{
restart_flag = false;
reset_to_initial_state();
- node_stack->full_reset();
memset(&stats,0,sizeof(struct execution_stats));
execution_number = 1;
}
char random_state[256];
initstate(423121, random_state, sizeof(random_state));
-- for(int exec = 0;exec < params.maxexecutions;exec++) {
- thrd_t user_thread;
- Thread *t = new Thread(execution->get_next_id(), &user_thread, &user_main_wrapper, NULL, NULL); // L: user_main_wrapper passes the user program
- execution->add_thread(t);
- //Need to seed random number generator, otherwise its state gets reset
++ for(int exec = 0;exec < params.maxexecutions;exec ++) {
+ Thread * t = init_thread;
+
do {
/*
* Stash next pending action(s) for thread(s). There
public:
ModelChecker();
~ModelChecker();
- void setParams(struct model_params params);
+ model_params * getParams();
void run();
/** Restart the model checker, intended for pluggins. */
ucontext_t * get_system_context() { return &system_context; }
ModelExecution * get_execution() const { return execution; }
+ ModelHistory * get_history() const { return history; }
int get_execution_number() const { return execution_number; }
model_params params;
void add_trace_analysis(TraceAnalysis *a) { trace_analyses.push_back(a); }
void set_inspect_plugin(TraceAnalysis *a) { inspect_plugin=a; }
+
MEMALLOC
private:
/** Flag indicates whether to restart the model checker. */
Scheduler * const scheduler;
NodeStack * const node_stack;
ModelExecution *execution;
+ Thread * init_thread;
+ ModelHistory *history;
int execution_number;
};
extern ModelChecker *model;
-
+extern bool modelchecker_started;
#endif /* __MODEL_H__ */
projects / c11tester.git / commitdiff