projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
fixup whitespace
[model-checker.git]
/
threads.cc
diff --git
a/threads.cc
b/threads.cc
index 6a9391f0302467097b415bf4b129eb1b90fffaa5..f24010697d60f306de512ab40fecdece88875cdd 100644
(file)
--- a/
threads.cc
+++ b/
threads.cc
@@
-1,3
+1,7
@@
+/** @file threads.cc
+ * @brief Thread functions.
+ */
+
#include "libthreads.h"
#include "common.h"
#include "threads.h"
#include "libthreads.h"
#include "common.h"
#include "threads.h"
@@
-5,18
+9,20
@@
/* global "model" object */
#include "model.h"
/* global "model" object */
#include "model.h"
-#define STACK_SIZE (1024 * 1024)
-
+/** Allocate a stack for a new thread. */
static void * stack_allocate(size_t size)
{
return malloc(size);
}
static void * stack_allocate(size_t size)
{
return malloc(size);
}
+/** Free a stack for a terminated thread. */
static void stack_free(void *stack)
{
free(stack);
}
static void stack_free(void *stack)
{
free(stack);
}
+/** Return the currently executing thread. */
+
Thread * thread_current(void)
{
ASSERT(model);
Thread * thread_current(void)
{
ASSERT(model);
@@
-27,17
+33,25
@@
Thread * thread_current(void)
* Provides a startup wrapper for each thread, allowing some initial
* model-checking data to be recorded. This method also gets around makecontext
* not being 64-bit clean
* Provides a startup wrapper for each thread, allowing some initial
* model-checking data to be recorded. This method also gets around makecontext
* not being 64-bit clean
+ * @todo We should make the START event always immediately follow the
+ * CREATE event, so we don't get redundant traces...
*/
*/
+
void thread_startup() {
Thread * curr_thread = thread_current();
/* Add dummy "start" action, just to create a first clock vector */
void thread_startup() {
Thread * curr_thread = thread_current();
/* Add dummy "start" action, just to create a first clock vector */
- model->switch_to_master(new ModelAction(THREAD_START, memory_order_seq_cst, curr_thread));
+ model->switch_to_master(new ModelAction(THREAD_START,
std::
memory_order_seq_cst, curr_thread));
/* Call the actual thread function */
curr_thread->start_routine(curr_thread->arg);
}
/* Call the actual thread function */
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.
+ */
+
int Thread::create_context()
{
int ret;
int Thread::create_context()
{
int ret;
@@
-67,6
+81,9
@@
int Thread::swap(ucontext_t *ctxt, Thread *t)
return swapcontext(ctxt, &t->context);
}
return swapcontext(ctxt, &t->context);
}
+
+/** Terminate a thread and free its stack. */
+
void Thread::complete()
{
if (state != THREAD_COMPLETED) {
void Thread::complete()
{
if (state != THREAD_COMPLETED) {
@@
-77,6
+94,12
@@
void Thread::complete()
}
}
}
}
+/** 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. */
+
Thread::Thread(thrd_t *t, void (*func)(void *), void *a) :
start_routine(func),
arg(a),
Thread::Thread(thrd_t *t, void (*func)(void *), void *a) :
start_routine(func),
arg(a),
@@
-102,6
+125,8
@@
Thread::~Thread()
model->remove_thread(this);
}
model->remove_thread(this);
}
+/** Return the thread_id_t corresponding to this Thread object. */
+
thread_id_t Thread::get_id()
{
return id;
thread_id_t Thread::get_id()
{
return id;