cv = new ClockVector(NULL, this);
}
-
/** Update the model action's read_from action */
void ModelAction::read_from(const ModelAction *act)
{
ASSERT(cv);
if (act!=NULL && act->is_release() && this->is_acquire()) {
- synchronized(act);
- cv->merge(act->cv);
+ synchronize_with(act);
}
reads_from = act;
}
-
-/** Synchronize the current thread with the thread corresponding to
- * the ModelAction parameter. */
-
-void ModelAction::synchronized(const ModelAction *act) {
+/**
+ * Synchronize the current thread with the thread corresponding to the
+ * ModelAction parameter.
+ * @param act The ModelAction to synchronize with
+ */
+void ModelAction::synchronize_with(const ModelAction *act) {
model->check_promises(cv, act->cv);
cv->merge(act->cv);
}
void create_cv(const ModelAction *parent = NULL);
ClockVector * get_cv() const { return cv; }
void read_from(const ModelAction *act);
- void synchronized(const ModelAction *act);
-
bool happens_before(const ModelAction *act) const;
MEMALLOC
private:
+ void synchronize_with(const ModelAction *act);
/** Type of action (read, write, thread create, thread yield, thread join) */
action_type type;
int thrd_create(thrd_t *t, thrd_start_t start_routine, void *arg)
{
Thread *thread;
- int ret;
DBG();
thread = new Thread(t, start_routine, arg);
- ret = model->add_thread(thread);
+ model->add_thread(thread);
DEBUG("create thread %d\n", id_to_int(thrd_to_id(*t)));
/* seq_cst is just a 'don't care' parameter */
model->switch_to_master(new ModelAction(THREAD_CREATE, std::memory_order_seq_cst, thread, VALUE_NONE));
- return ret;
+ return 0;
}
int thrd_join(thrd_t t)
#include "model.h"
#include "snapshot-interface.h"
-/**
- * The thread_system_next function takes the next step in the execution, if
- * possible.
- * @return Returns 0 (success) if there is another step and non-zero otherwise.
- */
-static int thread_system_next(void) {
- Thread *curr, *next;
-
- curr = thread_current();
- if (curr) {
- if (curr->get_state() == THREAD_READY) {
- model->check_current_action();
- model->scheduler->add_thread(curr);
- } else if (curr->get_state() == THREAD_RUNNING) {
- /* Stopped while running; i.e., completed */
- curr->complete();
- } else {
- ASSERT(false);
- }
- }
- next = model->scheduler->next_thread();
-
- /* Infeasible -> don't take any more steps */
- if (!model->isfeasible())
- return 1;
-
- if (next)
- next->set_state(THREAD_RUNNING);
- DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1);
-
- /* next == NULL -> don't take any more steps */
- if (!next)
- return 1;
- /* Return non-zero only if swap fails with an error */
- return Thread::swap(model->get_system_context(), next);
-}
-
-/** The thread_wait_finish method runs the current execution until we
- * have no more steps to take.
- */
-static void thread_wait_finish(void) {
- DBG();
-
- while (!thread_system_next());
-}
-
static void parse_options(struct model_params *params, int argc, char **argv) {
}
/** The real_main function contains the main model checking loop. */
static void real_main() {
thrd_t user_thread;
- ucontext_t main_context;
struct model_params params;
parse_options(¶ms, main_argc, main_argv);
model = new ModelChecker(params);
- if (getcontext(&main_context))
- return;
-
- model->set_system_context(&main_context);
-
snapshotObject->snapshotStep(0);
do {
/* Start user program */
model->add_thread(new Thread(&user_thread, (void (*)(void *)) &user_main, NULL));
/* Wait for all threads to complete */
- thread_wait_finish();
+ model->finish_execution();
} while (model->next_execution());
delete model;
printf("\n");
}
-int ModelChecker::add_thread(Thread *t)
+/**
+ * Add a Thread to the system for the first time. Should only be called once
+ * per thread.
+ * @param t The Thread to add
+ */
+void ModelChecker::add_thread(Thread *t)
{
thread_map->put(id_to_int(t->get_id()), t);
scheduler->add_thread(t);
- return 0;
}
void ModelChecker::remove_thread(Thread *t)
Thread * old = thread_current();
set_current_action(act);
old->set_state(THREAD_READY);
- return Thread::swap(old, get_system_context());
+ return Thread::swap(old, &system_context);
+}
+
+/**
+ * Takes the next step in the execution, if possible.
+ * @return Returns true (success) if a step was taken and false otherwise.
+ */
+bool ModelChecker::take_step() {
+ Thread *curr, *next;
+
+ curr = thread_current();
+ if (curr) {
+ if (curr->get_state() == THREAD_READY) {
+ check_current_action();
+ scheduler->add_thread(curr);
+ } else if (curr->get_state() == THREAD_RUNNING) {
+ /* Stopped while running; i.e., completed */
+ curr->complete();
+ } else {
+ ASSERT(false);
+ }
+ }
+ next = scheduler->next_thread();
+
+ /* Infeasible -> don't take any more steps */
+ if (!isfeasible())
+ return false;
+
+ if (next)
+ next->set_state(THREAD_RUNNING);
+ DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1);
+
+ /* next == NULL -> don't take any more steps */
+ if (!next)
+ return false;
+ /* Return false only if swap fails with an error */
+ return (Thread::swap(&system_context, next) == 0);
+}
+
+/** Runs the current execution until threre are no more steps to take. */
+void ModelChecker::finish_execution() {
+ DBG();
+
+ while (take_step());
}
ModelChecker(struct model_params params);
~ModelChecker();
- /** The scheduler to use: tracks the running/ready Threads */
- Scheduler *scheduler;
-
- /** Stores the context for the main model-checking system thread (call
- * once)
- * @param ctxt The system context structure
- */
- void set_system_context(ucontext_t *ctxt) { system_context = ctxt; }
-
/** @returns the context for the main model-checking system thread */
- ucontext_t * get_system_context(void) { return system_context; }
-
- void check_current_action(void);
+ ucontext_t * get_system_context() { return &system_context; }
/** Prints an execution summary with trace information. */
void print_summary();
Thread * schedule_next_thread();
- int add_thread(Thread *t);
+ void add_thread(Thread *t);
void remove_thread(Thread *t);
Thread * get_thread(thread_id_t tid) { return thread_map->get(id_to_int(tid)); }
int get_num_threads();
modelclock_t get_next_seq_num();
+ /** @return The currently executing Thread. */
+ Thread * get_current_thread() { return scheduler->get_current_thread(); }
+
int switch_to_master(ModelAction *act);
ClockVector * get_cv(thread_id_t tid);
bool next_execution();
bool isfinalfeasible();
void check_promises(ClockVector *old_cv, ClockVector * merge_cv);
+ void finish_execution();
+
MEMALLOC
private:
+ /** The scheduler to use: tracks the running/ready Threads */
+ Scheduler *scheduler;
+
int next_thread_id;
modelclock_t used_sequence_numbers;
int num_executions;
* @param act The ModelAction created by the user-thread action
*/
void set_current_action(ModelAction *act) { current_action = act; }
+ void check_current_action();
+
+ bool take_step();
ModelAction * get_last_conflict(ModelAction *act);
void set_backtracking(ModelAction *act);
ModelAction *diverge;
thread_id_t nextThread;
- ucontext_t *system_context;
+ ucontext_t system_context;
action_list_t *action_trace;
HashTable<int, Thread *, int> *thread_map;
#include "common.h"
#include "model.h"
+/** Constructor */
Scheduler::Scheduler() :
current(NULL)
{
}
+/**
+ * Add a Thread to the scheduler's ready list.
+ * @param t The Thread to add
+ */
void Scheduler::add_thread(Thread *t)
{
DEBUG("thread %d\n", t->get_id());
readyList.push_back(t);
}
+/**
+ * Remove a given Thread from the scheduler.
+ * @param t The Thread to remove
+ */
void Scheduler::remove_thread(Thread *t)
{
if (current == t)
readyList.remove(t);
}
-Thread * Scheduler::next_thread(void)
+/**
+ * Remove one Thread from the scheduler. This implementation performs FIFO.
+ * @return The next Thread to run
+ */
+Thread * Scheduler::next_thread()
{
Thread *t = model->schedule_next_thread();
return t;
}
-Thread * Scheduler::get_current_thread(void)
+/**
+ * @return The currently-running Thread
+ */
+Thread * Scheduler::get_current_thread() const
{
return current;
}
-void Scheduler::print()
+/**
+ * Print debugging information about the current state of the scheduler. Only
+ * prints something if debugging is enabled.
+ */
+void Scheduler::print() const
{
if (current)
DEBUG("Current thread: %d\n", current->get_id());
DEBUG("No current thread\n");
DEBUG("Num. threads in ready list: %zu\n", readyList.size());
- std::list<Thread *, MyAlloc< Thread * > >::iterator it;
+ std::list<Thread *, MyAlloc< Thread * > >::const_iterator it;
for (it = readyList.begin(); it != readyList.end(); it++)
DEBUG("In ready list: thread %d\n", (*it)->get_id());
}
Scheduler();
void add_thread(Thread *t);
void remove_thread(Thread *t);
- Thread * next_thread(void);
- Thread * get_current_thread(void);
- void print();
+ Thread * next_thread();
+ Thread * get_current_thread() const;
+ void print() const;
SNAPSHOTALLOC
private:
+ /** The list of available Threads that are not currently running */
std::list<Thread *> readyList;
+
+ /** The currently-running Thread */
Thread *current;
};
}
/** Return the currently executing thread. */
-
Thread * thread_current(void)
{
ASSERT(model);
- return model->scheduler->get_current_thread();
+ return model->get_current_thread();
}
/**
curr_thread->start_routine(curr_thread->arg);
}
-/** Create a thread context for a new thread so we can use
- * setcontext/getcontext/swapcontext to swap it out.
- * @return 0 on success.
+/**
+ * Create a thread context for a new thread so we can use
+ * setcontext/getcontext/swapcontext to swap it out.
+ * @return 0 on success; otherwise, non-zero error condition
*/
-
int Thread::create_context()
{
int ret;
/**
* Swaps the current context to another thread of execution. This form switches
* from a user Thread to a system context.
- * @param t Thread representing the current context
- * @param ctxt Context to switch to
+ * @param t Thread representing the currently-running thread. The current
+ * context is saved here.
+ * @param ctxt Context to which we will swap. Must hold a valid system context.
* @return Does not return, unless we return to Thread t's context. See
* swapcontext(3) (returns 0 for success, -1 for failure).
*/
/**
* Swaps the current context to another thread of execution. This form switches
* from a system context to a user Thread.
- * @param t Thread representing the current context
- * @param ctxt Context to switch to
- * @return Does not return, unless we return to Thread t's context. See
+ * @param ctxt System context variable to which to save the current context.
+ * @param t Thread to which we will swap. Must hold a valid user context.
+ * @return Does not return, unless we return to the system context (ctxt). See
* swapcontext(3) (returns 0 for success, -1 for failure).
*/
int Thread::swap(ucontext_t *ctxt, Thread *t)
}
}
-/** Create a new thread.
- * Takes the following parameters:
- * @param t The thread identifier of the newly created thread.
- * @param func The function that the thread will call.
- * @param a The parameter to pass to this function. */
-
+/**
+ * Construct a new thread.
+ * @param t The thread identifier of the newly created thread.
+ * @param func The function that the thread will call.
+ * @param a The parameter to pass to this function.
+ */
Thread::Thread(thrd_t *t, void (*func)(void *), void *a) :
start_routine(func),
arg(a),
parent = thread_current();
}
+/** Destructor */
Thread::~Thread()
{
complete();
model->remove_thread(this);
}
-/** Return the thread_id_t corresponding to this Thread object. */
-
+/** @return The thread_id_t corresponding to this Thread object. */
thread_id_t Thread::get_id()
{
return id;
projects / model-checker.git / commitdiff