Rewrite code such that most thread data is kept internally, not within the user
program.
void atomic_store_explicit(struct atomic_object *obj, int value, memory_order order)
{
void atomic_store_explicit(struct atomic_object *obj, int value, memory_order order)
{
- thread_switch_to_master(new ModelAction(ATOMIC_WRITE, order, obj, value));
+ thread_current()->switch_to_master(new ModelAction(ATOMIC_WRITE, order, obj, value));
}
int atomic_load_explicit(struct atomic_object *obj, memory_order order)
{
}
int atomic_load_explicit(struct atomic_object *obj, memory_order order)
{
- thread_switch_to_master(new ModelAction(ATOMIC_READ, order, obj, VALUE_NONE));
+ thread_current()->switch_to_master(new ModelAction(ATOMIC_READ, order, obj, VALUE_NONE));
-static int create_context(struct thread *t)
+Thread *thread_current(void)
+{
+ return model->scheduler->get_current_thread();
+}
+
+int Thread::create_context()
- memset(&t->context, 0, sizeof(t->context));
- ret = getcontext(&t->context);
+ ret = getcontext(&context);
- /* t->start_routine == NULL means this is our initial context */
- if (!t->start_routine)
+ /* start_routine == NULL means this is our initial context */
+ if (!start_routine)
return 0;
/* Initialize new managed context */
return 0;
/* Initialize new managed context */
- t->stack = stack_allocate(STACK_SIZE);
- t->context.uc_stack.ss_sp = t->stack;
- t->context.uc_stack.ss_size = STACK_SIZE;
- t->context.uc_stack.ss_flags = 0;
- t->context.uc_link = &model->system_thread->context;
- makecontext(&t->context, t->start_routine, 1, t->arg);
+ stack = stack_allocate(STACK_SIZE);
+ context.uc_stack.ss_sp = stack;
+ context.uc_stack.ss_size = STACK_SIZE;
+ context.uc_stack.ss_flags = 0;
+ context.uc_link = &model->system_thread->context;
+ makecontext(&context, start_routine, 1, arg);
-static int create_initial_thread(struct thread *t)
+int Thread::swap(Thread *t)
- memset(t, 0, sizeof(*t));
- model->assign_id(t);
- return create_context(t);
+ return swapcontext(&this->context, &t->context);
-static int thread_swap(struct thread *t1, struct thread *t2)
- return swapcontext(&t1->context, &t2->context);
-}
-
-static void thread_dispose(struct thread *t)
-{
- DEBUG("completed thread %d\n", thread_current()->id);
- t->state = THREAD_COMPLETED;
- stack_free(t->stack);
+ DEBUG("completed thread %d\n", thread_current()->get_id());
+ state = THREAD_COMPLETED;
+ stack_free(stack);
*/
static int thread_system_next(void)
{
*/
static int thread_system_next(void)
{
- struct thread *curr, *next;
curr = thread_current();
model->check_current_action();
if (curr) {
curr = thread_current();
model->check_current_action();
if (curr) {
- if (curr->state == THREAD_READY)
+ if (curr->get_state() == THREAD_READY)
model->scheduler->add_thread(curr);
model->scheduler->add_thread(curr);
- else if (curr->state == THREAD_RUNNING)
+ else if (curr->get_state() == THREAD_RUNNING)
/* Stopped while running; i.e., completed */
/* Stopped while running; i.e., completed */
else
DEBUG("ERROR: current thread in unexpected state??\n");
}
next = model->scheduler->next_thread();
if (next)
else
DEBUG("ERROR: current thread in unexpected state??\n");
}
next = model->scheduler->next_thread();
if (next)
- next->state = THREAD_RUNNING;
- DEBUG("(%d, %d)\n", curr ? curr->id : -1, next ? next->id : -1);
+ next->set_state(THREAD_RUNNING);
+ DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1);
- return thread_swap(model->system_thread, next);
+ return model->system_thread->swap(next);
}
static void thread_wait_finish(void)
}
static void thread_wait_finish(void)
while (!thread_system_next());
}
while (!thread_system_next());
}
-int thread_switch_to_master(ModelAction *act)
+int Thread::switch_to_master(ModelAction *act)
- struct thread *old, *next;
DBG();
model->set_current_action(act);
DBG();
model->set_current_action(act);
- old = thread_current();
- old->state = THREAD_READY;
next = model->system_thread;
next = model->system_thread;
- return thread_swap(old, next);
-/*
- * User program API functions
- */
-int thread_create(struct thread *t, void (*start_routine)(), void *arg)
-{
- int ret = 0;
-
- DBG();
-
- memset(t, 0, sizeof(*t));
- model->assign_id(t);
- DEBUG("create thread %d\n", t->id);
+Thread::Thread(thrd_t *t, void (*func)(), void *a) {
+ int ret;
- t->start_routine = start_routine;
- t->arg = arg;
+ user_thread = t;
+ start_routine = func;
+ arg = a;
- ret = create_context(t);
+ ret = create_context();
+ printf("Error in create_context\n");
- t->state = THREAD_CREATED;
+ state = THREAD_CREATED;
+ model->assign_id(this);
+ model->scheduler->add_thread(this);
+}
- model->scheduler->add_thread(t);
- return 0;
+Thread::Thread(thrd_t *t) {
+ /* system thread */
+ user_thread = t;
+ state = THREAD_CREATED;
+ model->assign_id(this);
+ create_context();
+ model->add_system_thread(this);
-int thread_join(struct thread *t)
+static thread_id_t thrd_to_id(thrd_t t)
+{
+ return t;
+}
+
+thread_id_t Thread::get_id()
+{
+ return thrd_to_id(*user_thread);
+}
+
+/*
+ * User program API functions
+ */
+int thrd_create(thrd_t *t, void (*start_routine)(), void *arg)
+{
+ int ret;
+ DBG();
+ ret = model->add_thread(new Thread(t, start_routine, arg));
+ DEBUG("create thread %d\n", thrd_to_id(*t));
+ return ret;
+}
+
+int thrd_join(thrd_t t)
- while (t->state != THREAD_COMPLETED && !ret)
+ Thread *th = model->get_thread(thrd_to_id(t));
+ while (th->get_state() != THREAD_COMPLETED && !ret)
/* seq_cst is just a 'don't care' parameter */
/* seq_cst is just a 'don't care' parameter */
- ret = thread_switch_to_master(new ModelAction(THREAD_JOIN, memory_order_seq_cst, NULL, VALUE_NONE));
+ ret = thread_current()->switch_to_master(new ModelAction(THREAD_JOIN, memory_order_seq_cst, NULL, VALUE_NONE));
{
/* seq_cst is just a 'don't care' parameter */
{
/* seq_cst is just a 'don't care' parameter */
- return thread_switch_to_master(new ModelAction(THREAD_YIELD, memory_order_seq_cst, NULL, VALUE_NONE));
+ return thread_current()->switch_to_master(new ModelAction(THREAD_YIELD, memory_order_seq_cst, NULL, VALUE_NONE));
-struct thread *thread_current(void)
+thrd_t thrd_current(void)
- return model->scheduler->get_current_thread();
+ return thread_current()->get_thrd_t();
- struct thread user_thread;
- struct thread *main_thread;
+ thrd_t user_thread, main_thread;
+ Thread *th;
model = new ModelChecker();
model = new ModelChecker();
- main_thread = (struct thread *)myMalloc(sizeof(*main_thread));
- create_initial_thread(main_thread);
- model->add_system_thread(main_thread);
+ th = new Thread(&main_thread);
- thread_create(&user_thread, &user_main, NULL);
+ thrd_create(&user_thread, &user_main, NULL);
/* Wait for all threads to complete */
thread_wait_finish();
model->print_trace();
/* Wait for all threads to complete */
thread_wait_finish();
model->print_trace();
DEBUG("Exiting\n");
return 0;
DEBUG("Exiting\n");
return 0;
#ifndef __LIBTHREADS_H__
#define __LIBTHREADS_H__
#ifndef __LIBTHREADS_H__
#define __LIBTHREADS_H__
-#include <ucontext.h>
-
-typedef enum thread_state {
- THREAD_CREATED,
- THREAD_RUNNING,
- THREAD_READY,
- THREAD_COMPLETED
-} thread_state;
-
+typedef void (*thrd_start_t)();
-struct thread {
- void (*start_routine)();
- void *arg;
- ucontext_t context;
- void *stack;
- thread_id_t id;
- thread_state state;
-};
+typedef thread_id_t thrd_t;
-int thread_create(struct thread *t, void (*start_routine)(), void *arg);
-int thread_join(struct thread *t);
-int thread_yield(void);
-struct thread *thread_current(void);
+int thrd_create(thrd_t *t, thrd_start_t start_routine, void *arg);
+int thrd_join(thrd_t);
+int thrd_yield(void);
+thrd_t thrd_current(void);
extern void user_main(void);
extern void user_main(void);
delete this->scheduler;
}
delete this->scheduler;
}
-void ModelChecker::assign_id(struct thread *t)
+void ModelChecker::assign_id(Thread *t)
- t->id = ++this->used_thread_id;
+ t->set_id(++used_thread_id);
-void ModelChecker::add_system_thread(struct thread *t)
+void ModelChecker::add_system_thread(Thread *t)
{
this->system_thread = t;
}
{
this->system_thread = t;
}
+int ModelChecker::add_thread(Thread *t)
+{
+ thread_map[t->get_id()] = t;
+ return 0;
+}
+
ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int value)
{
ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int value)
{
- struct thread *t = thread_current();
+ Thread *t = thread_current();
ModelAction *act = this;
act->type = type;
act->order = order;
act->location = loc;
ModelAction *act = this;
act->type = type;
act->order = order;
act->location = loc;
+ act->tid = t->get_id();
#define __MODEL_H__
#include <list>
#define __MODEL_H__
#include <list>
#include "schedule.h"
#include "libthreads.h"
#include "libatomic.h"
#include "schedule.h"
#include "libthreads.h"
#include "libatomic.h"
+#include "threads_internal.h"
ModelChecker();
~ModelChecker();
class Scheduler *scheduler;
ModelChecker();
~ModelChecker();
class Scheduler *scheduler;
- struct thread *system_thread;
- void add_system_thread(struct thread *t);
- void assign_id(struct thread *t);
+ void add_system_thread(Thread *t);
void set_current_action(ModelAction *act) { current_action = act; }
void check_current_action(void);
void print_trace(void);
void set_current_action(ModelAction *act) { current_action = act; }
void check_current_action(void);
void print_trace(void);
+ int add_thread(Thread *t);
+ Thread *get_thread(thread_id_t tid) { return thread_map[tid]; }
+
+ void assign_id(Thread *t);
private:
int used_thread_id;
class ModelAction *current_action;
std::list<class ModelAction *> action_trace;
private:
int used_thread_id;
class ModelAction *current_action;
std::list<class ModelAction *> action_trace;
+ std::map<thread_id_t, class Thread *> thread_map;
};
extern ModelChecker *model;
};
extern ModelChecker *model;
+int thread_switch_to_master(ModelAction *act);
+
+#include "threads_internal.h"
#include "schedule.h"
#include "common.h"
#include "model.h"
#include "schedule.h"
#include "common.h"
#include "model.h"
-void Scheduler::add_thread(struct thread *t)
+void Scheduler::add_thread(Thread *t)
- DEBUG("thread %d\n", t->id);
+ DEBUG("thread %d\n", t->get_id());
-struct thread *Scheduler::next_thread(void)
+Thread *Scheduler::next_thread(void)
{
if (queue.empty())
return NULL;
{
if (queue.empty())
return NULL;
-struct thread *Scheduler::get_current_thread(void)
+Thread *Scheduler::get_current_thread(void)
+#include "threads_internal.h"
#include "model.h"
class Scheduler {
public:
#include "model.h"
class Scheduler {
public:
- void add_thread(struct thread *t);
- struct thread * next_thread(void);
- struct thread * get_current_thread(void);
+ void add_thread(Thread *t);
+ Thread * next_thread(void);
+ Thread * get_current_thread(void);
- std::queue<struct thread *> queue;
- struct thread *current;
+ std::queue<Thread *> queue;
+ Thread *current;
};
#endif /* __SCHEDULE_H__ */
};
#endif /* __SCHEDULE_H__ */
#ifndef __THREADS_INTERNAL_H__
#define __THREADS_INTERNAL_H__
#ifndef __THREADS_INTERNAL_H__
#define __THREADS_INTERNAL_H__
-int thread_switch_to_master(ModelAction *act);
+typedef enum thread_state {
+ THREAD_CREATED,
+ THREAD_RUNNING,
+ THREAD_READY,
+ THREAD_COMPLETED
+} thread_state;
+
+class ModelAction;
+
+class Thread {
+public:
+ Thread(thrd_t *t, void (*func)(), void *a);
+ Thread(thrd_t *t);
+ int swap(Thread *t);
+ void dispose();
+ int switch_to_master(ModelAction *act);
+
+ thread_state get_state() { return state; }
+ void set_state(thread_state s) { state = s; }
+ thread_id_t get_id();
+ void set_id(thread_id_t i) { *user_thread = i; }
+ thrd_t get_thrd_t() { return *user_thread; }
+private:
+ int create_context();
+
+ void (*start_routine)();
+ void *arg;
+ ucontext_t context;
+ void *stack;
+ thrd_t *user_thread;
+ thread_state state;
+};
+
+Thread *thread_current();
#endif /* __THREADS_INTERNAL_H__ */
#endif /* __THREADS_INTERNAL_H__ */
int i;
for (i = 0; i < 10; i++) {
int i;
for (i = 0; i < 10; i++) {
- printf("Thread %d, loop %d\n", thread_current()->id, i);
+ printf("Thread %d, loop %d\n", thrd_current(), i);
switch (i % 4) {
case 1:
atomic_load(obj);
switch (i % 4) {
case 1:
atomic_load(obj);
- printf("Thread %d creating 2 threads\n", thread_current()->id);
- thread_create(&t1, (void (*)())&a, &obj);
- thread_create(&t2, (void (*)())&a, &obj);
+ printf("Creating 2 threads\n");
+ thrd_create(&t1, (void (*)())&a, &obj);
+ thrd_create(&t2, (void (*)())&a, &obj);
- thread_join(&t1);
- thread_join(&t2);
- printf("Thread %d is finished\n", thread_current()->id);
+ thrd_join(t1);
+ thrd_join(t2);
+ printf("Thread is finished\n");