#include "memoryorder.h"
#include "modeltypes.h"
#include "pthread.h"
-
-/* Forward declarations */
-class ClockVector;
-class Thread;
+#include "classlist.h"
namespace cdsc {
class mutex;
NOOP
} action_type_t;
-/* Forward declaration */
-class Node;
-class ClockVector;
/**
* @brief Represents a single atomic action
--- /dev/null
+#ifndef CLASSLIST_H
+#define CLASSLIST_H
+class ClockVector;
+class CycleGraph;
+class CycleNode;
+class ModelAction;
+class ModelChecker;
+class ModelExecution;
+class Node;
+class NodeStack;
+class Scheduler;
+class Thread;
+class TraceAnalysis;
+
+struct model_snapshot_members;
+struct bug_message;
+
+#endif
#include "mymemory.h"
#include "modeltypes.h"
-
-/* Forward declaration */
-class ModelAction;
+#include "classlist.h"
class ClockVector {
public:
#include "config.h"
#include "mymemory.h"
#include "stl-model.h"
-
-class CycleNode;
-class ModelAction;
+#include "classlist.h"
/** @brief A graph of Model Actions for tracking cycles. */
class CycleGraph {
#include "config.h"
#include <stdint.h>
#include "modeltypes.h"
-
-/* Forward declaration */
-class ModelAction;
+#include "classlist.h"
struct ShadowTable {
void * array[65536];
/** @brief Constructor */
ModelExecution::ModelExecution(ModelChecker *m,
- const struct model_params *params,
Scheduler *scheduler,
NodeStack *node_stack) :
model(m),
- params(params),
+ params(NULL),
scheduler(scheduler),
action_trace(),
thread_map(2), /* We'll always need at least 2 threads */
return NULL;
}
-/** @return True if the execution has taken too many steps */
-bool ModelExecution::too_many_steps() const
-{
- return params->bound != 0 && priv->used_sequence_numbers > params->bound;
-}
-
/**
* Takes the next step in the execution, if possible.
* @param curr The current step to take
#include "mutex.h"
#include <condition_variable>
-
-/* Forward declaration */
-class Node;
-class NodeStack;
-class CycleGraph;
-class Scheduler;
-class Thread;
-class ClockVector;
-struct model_snapshot_members;
-class ModelChecker;
-struct bug_message;
+#include "classlist.h"
/** @brief Shorthand for a list of release sequence heads */
typedef ModelVector<const ModelAction *> rel_heads_list_t;
class ModelExecution {
public:
ModelExecution(ModelChecker *m,
- const struct model_params *params,
- Scheduler *scheduler,
+ Scheduler *scheduler,
NodeStack *node_stack);
~ModelExecution();
- const struct model_params * get_params() const { return params; }
-
+ struct model_params * get_params() const { return params; }
+ void setParams(struct model_params * _params) {params = _params;}
+
Thread * take_step(ModelAction *curr);
void print_summary() const;
void print_infeasibility(const char *prefix) const;
bool is_infeasible() const;
bool is_deadlocked() const;
- bool too_many_steps() const;
action_list_t * get_action_trace() { return &action_trace; }
ModelChecker *model;
- const model_params * const params;
+ struct model_params * params;
/** The scheduler to use: tracks the running/ready Threads */
Scheduler * const scheduler;
static void param_defaults(struct model_params *params)
{
- params->enabledcount = 1;
- params->bound = 0;
params->verbose = !!DBG_ENABLED();
params->uninitvalue = 0;
- params->maxexecutions = 0;
+ params->maxexecutions = 10;
}
static void print_usage(const char *program_name, struct model_params *params)
"\n"
"Model-checker options:\n"
"-h, --help Display this help message and exit\n"
-"-e, --enabled=COUNT Enabled count.\n"
-" Default: %d\n"
-"-b, --bound=MAX Upper length bound.\n"
-" Default: %d\n"
"-v[NUM], --verbose[=NUM] Print verbose execution information. NUM is optional:\n"
" 0 is quiet; 1 shows valid executions; 2 is noisy;\n"
" 3 is noisier.\n"
" -o help for a list of options\n"
" -- Program arguments follow.\n\n",
program_name,
- params->enabledcount,
- params->bound,
params->verbose,
params->uninitvalue,
params->maxexecutions);
static void parse_options(struct model_params *params, int argc, char **argv)
{
- const char *shortopts = "ht:o:e:b:u:x:v::";
+ const char *shortopts = "ht:o:u:x:v::";
const struct option longopts[] = {
{"help", no_argument, NULL, 'h'},
- {"enabled", required_argument, NULL, 'e'},
- {"bound", required_argument, NULL, 'b'},
{"verbose", optional_argument, NULL, 'v'},
{"uninitialized", required_argument, NULL, 'u'},
{"analysis", required_argument, NULL, 't'},
case 'x':
params->maxexecutions = atoi(optarg);
break;
- case 'e':
- params->enabledcount = atoi(optarg);
- break;
- case 'b':
- params->bound = atoi(optarg);
- break;
case 'v':
params->verbose = optarg ? atoi(optarg) : 1;
break;
snapshot_stack_init();
- model = new ModelChecker(params);
+ if (!model)
+ model = new ModelChecker();
+ model->setParams(params);
install_trace_analyses(model->get_execution());
snapshot_record(0);
ModelChecker *model;
/** @brief Constructor */
-ModelChecker::ModelChecker(struct model_params params) :
+ModelChecker::ModelChecker() :
/* Initialize default scheduler */
- params(params),
+ params(),
restart_flag(false),
- exit_flag(false),
scheduler(new Scheduler()),
node_stack(new NodeStack()),
- execution(new ModelExecution(this, &this->params, scheduler, node_stack)),
+ execution(new ModelExecution(this, scheduler, node_stack)),
execution_number(1),
- diverge(NULL),
- earliest_diverge(NULL),
trace_analyses(),
inspect_plugin(NULL)
{
delete scheduler;
}
+/** Method to set parameters */
+void ModelChecker::setParams(struct model_params params) {
+ this->params = params;
+ execution->setParams(¶ms);
+}
+
/**
* Restores user program to initial state and resets all model-checker data
* structures.
model_print("Number of buggy executions: %d\n", stats.num_buggy_executions);
model_print("Number of infeasible executions: %d\n", stats.num_infeasible);
model_print("Total executions: %d\n", stats.num_total);
- if (params.verbose)
- model_print("Total nodes created: %d\n", node_stack->get_total_nodes());
}
/**
print_program_output();
if (params.verbose >= 3) {
- model_print("\nEarliest divergence point since last feasible execution:\n");
- if (earliest_diverge)
- earliest_diverge->print();
- else
- model_print("(Not set)\n");
-
- model_print("\n");
print_stats();
}
execution_number++;
reset_to_initial_state();
node_stack->full_reset();
- diverge = NULL;
return false;
-/* test
- if (complete)
- earliest_diverge = NULL;
-
- if (exit_flag)
- return false;
-
-// diverge = execution->get_next_backtrack();
- if (diverge == NULL) {
- execution_number++;
- reset_to_initial_state();
- model_print("Does not diverge\n");
- return false;
- }
-
- if (DBG_ENABLED()) {
- model_print("Next execution will diverge at:\n");
- diverge->print();
- }
-
- execution_number++;
-
- if (params.maxexecutions != 0 && stats.num_complete >= params.maxexecutions)
- return false;
-
- reset_to_initial_state();
- return true;
-*/
-
}
/** @brief Run trace analyses on complete trace */
execution->set_assert();
return true;
}
-
- if (execution->too_many_steps())
- return true;
return false;
}
-/** @brief Exit ModelChecker upon returning to the run loop of the
- * model checker. */
-void ModelChecker::exit_model_checker()
-{
- exit_flag = true;
-}
-
/** @brief Restart ModelChecker upon returning to the run loop of the
* model checker. */
void ModelChecker::restart()
void ModelChecker::do_restart()
{
restart_flag = false;
- diverge = NULL;
- earliest_diverge = NULL;
reset_to_initial_state();
node_stack->full_reset();
memset(&stats,0,sizeof(struct execution_stats));
/** @brief Run ModelChecker for the user program */
void ModelChecker::run()
{
- int i = 0;
//Need to initial random number generator state to avoid resets on rollback
char random_state[256];
initstate(423121, random_state, sizeof(random_state));
- do {
+
+ 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);
t = execution->take_step(curr);
} while (!should_terminate_execution());
next_execution();
- i++;
//restore random number generator state after rollback
setstate(random_state);
- } while (i<5); // while (has_next);
+ }
model_print("******* Model-checking complete: *******\n");
print_stats();
#include "stl-model.h"
#include "context.h"
#include "params.h"
-
-/* Forward declaration */
-class Node;
-class NodeStack;
-class CycleGraph;
-class Scheduler;
-class Thread;
-class ClockVector;
-class TraceAnalysis;
-class ModelExecution;
-class ModelAction;
+#include "classlist.h"
typedef SnapList<ModelAction *> action_list_t;
/** @brief The central structure for model-checking */
class ModelChecker {
public:
- ModelChecker(struct model_params params);
+ ModelChecker();
~ModelChecker();
-
+ void setParams(struct model_params params);
void run();
/** Restart the model checker, intended for pluggins. */
/** Exit the model checker, intended for pluggins. */
void exit_model_checker();
- /** Check the exit_flag. */
- bool get_exit_flag() const { return exit_flag; }
-
/** @returns the context for the main model-checking system thread */
ucontext_t * get_system_context() { return &system_context; }
bool assert_bug(const char *msg, ...);
void assert_user_bug(const char *msg);
- const model_params params;
+ 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. */
bool restart_flag;
- /** Flag indicates whether to exit the model checker. */
- bool exit_flag;
/** The scheduler to use: tracks the running/ready Threads */
Scheduler * const scheduler;
Thread * get_next_thread();
void reset_to_initial_state();
- ModelAction *diverge;
- ModelAction *earliest_diverge;
-
ucontext_t system_context;
ModelVector<TraceAnalysis *> trace_analyses;
* parent.
*
* @param act The ModelAction to associate with this Node. May be NULL.
- * @param par The parent Node in the NodeStack. May be NULL if there is no
- * parent.
* @param nthreads The number of threads which exist at this point in the
* execution trace.
*/
-Node::Node(ModelAction *act, Node *par, int nthreads) :
+Node::Node(ModelAction *act) :
action(act),
- uninit_action(NULL),
- parent(par),
- num_threads(nthreads)
+ uninit_action(NULL)
{
ASSERT(act);
act->set_node(this);
NodeStack::NodeStack() :
node_list(),
- head_idx(-1),
- total_nodes(0)
+ head_idx(-1)
{
- total_nodes++;
}
NodeStack::~NodeStack()
{
DBG();
- /* Record action */
- Node *head = get_head();
-
- int next_threads = execution->get_num_threads();
- if (act->get_type() == THREAD_CREATE || act->get_type() == PTHREAD_CREATE ) // may need to be changed
- next_threads++;
- node_list.push_back(new Node(act, head, next_threads));
- total_nodes++;
+ node_list.push_back(new Node(act));
head_idx++;
return NULL;
}
delete node_list[i];
node_list.clear();
reset_execution();
- total_nodes = 1;
}
Node * NodeStack::get_head() const
#include "mymemory.h"
#include "schedule.h"
#include "stl-model.h"
-
-class ModelAction;
-class Thread;
-
-struct fairness_info {
- unsigned int enabled_count;
- unsigned int turns;
- bool priority;
-};
-
+#include "classlist.h"
/**
* @brief A single node in a NodeStack
*/
class Node {
public:
- Node(ModelAction *act, Node *par,
- int nthreads);
+ Node(ModelAction *act);
~Node();
- bool is_enabled(Thread *t) const;
- bool is_enabled(thread_id_t tid) const;
-
ModelAction * get_action() const { return action; }
void set_uninit_action(ModelAction *act) { uninit_action = act; }
ModelAction * get_uninit_action() const { return uninit_action; }
-
- int get_num_threads() const { return num_threads; }
- /** @return the parent Node to this Node; that is, the action that
- * occurred previously in the stack. */
- Node * get_parent() const { return parent; }
-
-
-
void print() const;
MEMALLOC
/** @brief ATOMIC_UNINIT action which was created at this Node */
ModelAction *uninit_action;
- Node * const parent;
- const int num_threads;
};
typedef ModelVector<Node *> node_list_t;
~NodeStack();
void register_engine(const ModelExecution *exec);
-
ModelAction * explore_action(ModelAction *act);
Node * get_head() const;
Node * get_next() const;
void reset_execution();
void full_reset();
- int get_total_nodes() { return total_nodes; }
-
void print() const;
MEMALLOC
private:
node_list_t node_list;
-
const struct model_params * get_params() const;
/** @brief The model-checker execution object */
* current head Node. It is negative when the list is empty.
*/
int head_idx;
-
- int total_nodes;
};
#endif /* __NODESTACK_H__ */
* the model checker.
*/
struct model_params {
- unsigned int enabledcount;
- unsigned int bound;
unsigned int uninitvalue;
int maxexecutions;
#include "model.h"
#include "execution.h"
-static void param_defaults(struct model_params *params)
-{
- params->enabledcount = 1;
- params->bound = 0;
- params->verbose = !!DBG_ENABLED();
- params->uninitvalue = 0;
- params->maxexecutions = 0;
-}
-
-static void model_main()
-{
- struct model_params params;
-
- param_defaults(¶ms);
-
- //parse_options(¶ms, main_argc, main_argv);
-
- //Initialize race detector
- initRaceDetector();
-
- snapshot_stack_init();
-
- model = new ModelChecker(params); // L: Model thread is created
-// install_trace_analyses(model->get_execution()); L: disable plugin
-
- snapshot_record(0);
- model->run();
- delete model;
-
- DEBUG("Exiting\n");
-}
-
int pthread_create(pthread_t *t, const pthread_attr_t * attr,
pthread_start_t start_routine, void * arg) {
struct pthread_params params = { start_routine, arg };
int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t *) {
if (!model) {
- snapshot_system_init(10000, 1024, 1024, 40000, &model_main);
+ model = new ModelChecker();
}
cdsc::mutex *m = new cdsc::mutex();
#include "mymemory.h"
#include "modeltypes.h"
-
-/* Forward declaration */
-class Thread;
-class Node;
-class ModelExecution;
+#include "classlist.h"
typedef enum enabled_type {
THREAD_DISABLED,
printf("r2=%d\n",r2);
}
-int main(int argc, char **argv)
+int user_main(int argc, char **argv)
{
thrd_t t1, t2;
#include "modeltypes.h"
#include "stl-model.h"
#include "context.h"
+#include "classlist.h"
struct thread_params {
thrd_start_t func;
THREAD_COMPLETED
} thread_state;
-class ModelAction;
/** @brief A Thread is created for each user-space thread */
class Thread {
projects / c11tester.git / commitdiff