projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
action / threads: add THREAD_START action at start of each thread
[model-checker.git]
/
threads.cc
diff --git
a/threads.cc
b/threads.cc
index ba7b54730781369fd6c17ec9f4bc492d660b3843..6a9391f0302467097b415bf4b129eb1b90fffaa5 100644
(file)
--- a/
threads.cc
+++ b/
threads.cc
@@
-23,10
+23,18
@@
Thread * thread_current(void)
return model->scheduler->get_current_thread();
}
return model->scheduler->get_current_thread();
}
-/* This method just 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
+ */
void thread_startup() {
Thread * curr_thread = thread_current();
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));
+
+ /* Call the actual thread function */
curr_thread->start_routine(curr_thread->arg);
}
curr_thread->start_routine(curr_thread->arg);
}