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
#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] = {
/* --- 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) {
__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 */
--- /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;
+ };
#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() :
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());
}
/**
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
Scheduler * const scheduler;
NodeStack * const node_stack;
ModelExecution *execution;
+ Thread * init_thread;
+ ModelHistory *history;
int execution_number;
projects / c11tester.git / commitdiff