sleeps.o history.o funcnode.o funcinst.o printf.o
CPPFLAGS += -Iinclude -I.
-LDFLAGS := -ldl -lrt -rdynamic
+LDFLAGS := -ldl -lrt -rdynamic -lpthread
SHARED := -shared
# Mac OSX options
SNAPSHOTALLOC
};
-
-#ifdef TLS
-#include <dlfcn.h>
-
-//Code taken from LLVM and licensed under the University of Illinois Open Source
-//License.
-static uintptr_t thread_descriptor_size;
-#if __LP64__ || defined(_WIN64)
-# define SANITIZER_WORDSIZE 64
-#else
-# define SANITIZER_WORDSIZE 32
-#endif
-
-#if SANITIZER_WORDSIZE == 64
-# define FIRST_32_SECOND_64(a, b) (b)
-#else
-# define FIRST_32_SECOND_64(a, b) (a)
-#endif
-
-#if defined(__x86_64__) && !defined(_LP64)
-# define SANITIZER_X32 1
-#else
-# define SANITIZER_X32 0
-#endif
-
-#if defined(__arm__)
-# define SANITIZER_ARM 1
-#else
-# define SANITIZER_ARM 0
-#endif
-
-uintptr_t ThreadDescriptorSize() {
- uintptr_t val = thread_descriptor_size;
- if (val)
- return val;
-#if defined(__x86_64__) || defined(__i386__) || defined(__arm__)
-#ifdef _CS_GNU_LIBC_VERSION
- char buf[64];
- uintptr_t len = confstr(_CS_GNU_LIBC_VERSION, buf, sizeof(buf));
- if (len < sizeof(buf) && strncmp(buf, "glibc 2.", 8) == 0) {
- char *end;
- int minor = strtoll(buf + 8, &end, 10);
- if (end != buf + 8 && (*end == '\0' || *end == '.' || *end == '-')) {
- int patch = 0;
- if (*end == '.')
- // strtoll will return 0 if no valid conversion could be performed
- patch = strtoll(end + 1, nullptr, 10);
-
- /* sizeof(struct pthread) values from various glibc versions. */
- if (SANITIZER_X32)
- val = 1728;// Assume only one particular version for x32.
- // For ARM sizeof(struct pthread) changed in Glibc 2.23.
- else if (SANITIZER_ARM)
- val = minor <= 22 ? 1120 : 1216;
- else if (minor <= 3)
- val = FIRST_32_SECOND_64(1104, 1696);
- else if (minor == 4)
- val = FIRST_32_SECOND_64(1120, 1728);
- else if (minor == 5)
- val = FIRST_32_SECOND_64(1136, 1728);
- else if (minor <= 9)
- val = FIRST_32_SECOND_64(1136, 1712);
- else if (minor == 10)
- val = FIRST_32_SECOND_64(1168, 1776);
- else if (minor == 11 || (minor == 12 && patch == 1))
- val = FIRST_32_SECOND_64(1168, 2288);
- else if (minor <= 13)
- val = FIRST_32_SECOND_64(1168, 2304);
- else
- val = FIRST_32_SECOND_64(1216, 2304);
- }
- }
-#endif
-#elif defined(__mips__)
- // TODO(sagarthakur): add more values as per different glibc versions.
- val = FIRST_32_SECOND_64(1152, 1776);
-#elif defined(__aarch64__)
- // The sizeof (struct pthread) is the same from GLIBC 2.17 to 2.22.
- val = 1776;
-#elif defined(__powerpc64__)
- val = 1776; // from glibc.ppc64le 2.20-8.fc21
-#elif defined(__s390__)
- val = FIRST_32_SECOND_64(1152, 1776); // valid for glibc 2.22
-#endif
- if (val)
- thread_descriptor_size = val;
- return val;
-}
-
-#ifdef __i386__
-# define DL_INTERNAL_FUNCTION __attribute__((regparm(3), stdcall))
-#else
-# define DL_INTERNAL_FUNCTION
-#endif
-
-intptr_t RoundUpTo(uintptr_t size, uintptr_t boundary) {
- return (size + boundary - 1) & ~(boundary - 1);
-}
-
-uintptr_t getTlsSize() {
- // all current supported platforms have 16 bytes stack alignment
- const size_t kStackAlign = 16;
- typedef void (*get_tls_func)(size_t*, size_t*) DL_INTERNAL_FUNCTION;
- get_tls_func get_tls;
- void *get_tls_static_info_ptr = dlsym(RTLD_NEXT, "_dl_get_tls_static_info");
- memcpy(&get_tls, &get_tls_static_info_ptr, sizeof(get_tls_static_info_ptr));
- ASSERT(get_tls != 0);
- size_t tls_size = 0;
- size_t tls_align = 0;
- get_tls(&tls_size, &tls_align);
- if (tls_align < kStackAlign)
- tls_align = kStackAlign;
- return RoundUpTo(tls_size, tls_align);
-}
-
-#endif
-
/** @brief Constructor */
ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
model(m),
fuzzer(new Fuzzer()),
thrd_func_list(),
thrd_func_inst_lists()
-#ifdef TLS
- ,tls_base(NULL),
- tls_addr(0),
- tls_size(0),
- thd_desc_size(0)
-#endif
{
/* Initialize a model-checker thread, for special ModelActions */
model_thread = new Thread(get_next_id());
scheduler->register_engine(this);
}
-#ifdef TLS
-void ModelExecution::initTLS() {
- tls_addr = get_tls_addr();
- tls_size = getTlsSize();
- tls_addr -= tls_size;
- thd_desc_size = ThreadDescriptorSize();
- tls_addr += thd_desc_size;
- tls_base = (char *) snapshot_calloc(tls_size,1);
- memcpy(tls_base, reinterpret_cast<const char *>(tls_addr), tls_size);
-}
-#endif
-
/** @brief Destructor */
ModelExecution::~ModelExecution()
{
* This data structure is handled by ModelHistory
*/
SnapVector< SnapList< func_inst_list_t *> *> thrd_func_inst_lists;
-
-#ifdef TLS
-public:
- char * getTLSBase() {return tls_base;}
- uintptr_t getTLSAddr() {return tls_addr;}
- uintptr_t getTLSSize() {if (!tls_base) initTLS();return tls_size;}
- uintptr_t getThdDescSize() {return thd_desc_size;}
-private:
- void initTLS();
- char * tls_base;
- uintptr_t tls_addr;
- uintptr_t tls_size;
- uintptr_t thd_desc_size;
-#endif
};
#endif /* __EXECUTION_H__ */
void ModelHistory::enter_function(const uint32_t func_id, thread_id_t tid)
{
- /* //model_print("thread %d entering func %d\n", tid, func_id);
- uint32_t id = id_to_int(tid);
- SnapVector<func_id_list_t *> * thrd_func_list = model->get_execution()->get_thrd_func_list();
- SnapVector< SnapList<func_inst_list_t *> *> *
- thrd_func_inst_lists = model->get_execution()->get_thrd_func_inst_lists();
+ //model_print("thread %d entering func %d\n", tid, func_id);
+ uint32_t id = id_to_int(tid);
+ SnapVector<func_id_list_t *> * thrd_func_list = model->get_execution()->get_thrd_func_list();
+ SnapVector< SnapList<func_inst_list_t *> *> *
+ thrd_func_inst_lists = model->get_execution()->get_thrd_func_inst_lists();
- if ( thrd_func_list->size() <= id ) {
- thrd_func_list->resize( id + 1 );
- thrd_func_inst_lists->resize( id + 1 );
- }
+ if ( thrd_func_list->size() <= id ) {
+ thrd_func_list->resize( id + 1 );
+ thrd_func_inst_lists->resize( id + 1 );
+ }
- func_id_list_t * func_list = thrd_func_list->at(id);
- SnapList<func_inst_list_t *> * func_inst_lists = thrd_func_inst_lists->at(id);
+ func_id_list_t * func_list = thrd_func_list->at(id);
+ SnapList<func_inst_list_t *> * func_inst_lists = thrd_func_inst_lists->at(id);
- if (func_list == NULL) {
- func_list = new func_id_list_t();
- thrd_func_list->at(id) = func_list;
- }
+ if (func_list == NULL) {
+ func_list = new func_id_list_t();
+ thrd_func_list->at(id) = func_list;
+ }
- if (func_inst_lists == NULL) {
- func_inst_lists = new SnapList< func_inst_list_t *>();
- thrd_func_inst_lists->at(id) = func_inst_lists;
- }
+ if (func_inst_lists == NULL) {
+ func_inst_lists = new SnapList< func_inst_list_t *>();
+ thrd_func_inst_lists->at(id) = func_inst_lists;
+ }
- func_list->push_back(func_id);
- func_inst_lists->push_back( new func_inst_list_t() );
+ func_list->push_back(func_id);
+ func_inst_lists->push_back( new func_inst_list_t() );
- if ( func_nodes.size() <= func_id )
- resize_func_nodes( func_id + 1 );
- */}
+ if ( func_nodes.size() <= func_id )
+ resize_func_nodes( func_id + 1 );
+}
/* @param func_id a non-zero value */
void ModelHistory::exit_function(const uint32_t func_id, thread_id_t tid)
{
- /* uint32_t id = id_to_int(tid);
- SnapVector<func_id_list_t *> * thrd_func_list = model->get_execution()->get_thrd_func_list();
- SnapVector< SnapList<func_inst_list_t *> *> *
- thrd_func_inst_lists = model->get_execution()->get_thrd_func_inst_lists();
-
- func_id_list_t * func_list = thrd_func_list->at(id);
- SnapList<func_inst_list_t *> * func_inst_lists = thrd_func_inst_lists->at(id);
-
- uint32_t last_func_id = func_list->back();
-
- if (last_func_id == func_id) {
- FuncNode * func_node = func_nodes[func_id];
- func_node->clear_read_map(tid);
-
- func_inst_list_t * curr_inst_list = func_inst_lists->back();
- func_node->link_insts(curr_inst_list);
-
- func_list->pop_back();
- func_inst_lists->pop_back();
- } else {
- model_print("trying to exit with a wrong function id\n");
- model_print("--- last_func: %d, func_id: %d\n", last_func_id, func_id);
- }
- //model_print("thread %d exiting func %d\n", tid, func_id);*/
+ uint32_t id = id_to_int(tid);
+ SnapVector<func_id_list_t *> * thrd_func_list = model->get_execution()->get_thrd_func_list();
+ SnapVector< SnapList<func_inst_list_t *> *> *
+ thrd_func_inst_lists = model->get_execution()->get_thrd_func_inst_lists();
+
+ func_id_list_t * func_list = thrd_func_list->at(id);
+ SnapList<func_inst_list_t *> * func_inst_lists = thrd_func_inst_lists->at(id);
+
+ uint32_t last_func_id = func_list->back();
+
+ if (last_func_id == func_id) {
+ FuncNode * func_node = func_nodes[func_id];
+ func_node->clear_read_map(tid);
+
+ func_inst_list_t * curr_inst_list = func_inst_lists->back();
+ func_node->link_insts(curr_inst_list);
+
+ func_list->pop_back();
+ func_inst_lists->pop_back();
+ } else {
+ model_print("trying to exit with a wrong function id\n");
+ model_print("--- last_func: %d, func_id: %d\n", last_func_id, func_id);
+ }
+ //model_print("thread %d exiting func %d\n", tid, func_id);
}
void ModelHistory::resize_func_nodes(uint32_t new_size)
/** Wrapper to run the user's main function, with appropriate arguments */
void user_main_wrapper(void *)
{
-#ifdef TLS
- model->get_execution()->getTLSSize();
-#endif
user_main(model->params.argc, model->params.argv);
}
void ModelChecker::startMainThread() {
init_thread->set_state(THREAD_RUNNING);
scheduler->set_current_thread(init_thread);
- thread_startup();
+ main_thread_startup();
}
static bool is_nonsc_write(const ModelAction *act) {
#include "stl-model.h"
#include "context.h"
#include "classlist.h"
+#include "pthread.h"
struct thread_params {
thrd_start_t func;
bool is_model_thread() const { return model_thread; }
friend void thread_startup();
+#ifdef TLS
+ friend void setup_context();
+ friend void * helper_thread(void *);
+ friend void finalize_helper_thread();
+#endif
/**
* Intentionally NOT allocated with MODELALLOC or SNAPSHOTALLOC.
ucontext_t context;
void *stack;
#ifdef TLS
+public:
char *tls;
+ ucontext_t helpercontext;
+ pthread_mutex_t mutex;
+ pthread_mutex_t mutex2;
+ pthread_t thread;
+private:
#endif
thrd_t *user_thread;
thread_id_t id;
Thread * thread_current();
void thread_startup();
+void main_thread_startup();
static inline thread_id_t thrd_to_id(thrd_t t)
{
#include "execution.h"
#ifdef TLS
+#include <dlfcn.h>
uintptr_t get_tls_addr() {
uintptr_t addr;
asm ("mov %%fs:0, %0" : "=r" (addr));
return model->get_current_thread();
}
+void main_thread_startup() {
+#ifdef TLS
+ Thread * curr_thread = thread_current();
+ /* Add dummy "start" action, just to create a first clock vector */
+ model->switch_to_master(new ModelAction(THREAD_START, std::memory_order_seq_cst, curr_thread));
+#endif
+ thread_startup();
+}
+
/**
* Provides a startup wrapper for each thread, allowing some initial
* model-checking data to be recorded. This method also gets around makecontext
void thread_startup()
{
Thread * curr_thread = thread_current();
-
+#ifndef TLS
/* Add dummy "start" action, just to create a first clock vector */
model->switch_to_master(new ModelAction(THREAD_START, std::memory_order_seq_cst, curr_thread));
-
-#ifdef TLS
- if (curr_thread->tls == NULL) {
- uintptr_t tlssize = model->get_execution()->getTLSSize();
- uintptr_t thddesc = model->get_execution()->getThdDescSize();
- curr_thread->tls = (char*) Thread_malloc(tlssize);
- memcpy(curr_thread->tls, model->get_execution()->getTLSBase(), tlssize);
- curr_thread->tls += tlssize - thddesc;
- set_tls_addr((uintptr_t)curr_thread->tls);
- }
#endif
/* Call the actual thread function */
model->switch_to_master(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, curr_thread));
}
+#ifdef TLS
+int real_pthread_mutex_init(pthread_mutex_t *__mutex, const pthread_mutexattr_t *__mutexattr) {
+ static int (*pthread_mutex_init_p) (pthread_mutex_t *__mutex, const pthread_mutexattr_t *__mutexattr) = NULL;
+ char * error;
+ if (!pthread_mutex_init_p) {
+ pthread_mutex_init_p = (int (*)(pthread_mutex_t *__mutex, const pthread_mutexattr_t *__mutexattr))dlsym(RTLD_NEXT, "pthread_mutex_init");
+ if ((error = dlerror()) != NULL) {
+ fputs(error, stderr);
+ exit(EXIT_FAILURE);
+ }
+ }
+ return pthread_mutex_init_p(__mutex, __mutexattr);
+}
+
+int real_pthread_mutex_lock (pthread_mutex_t *__mutex) {
+ static int (*pthread_mutex_lock_p) (pthread_mutex_t *__mutex) = NULL;
+ char * error;
+ if (!pthread_mutex_lock_p) {
+ pthread_mutex_lock_p = (int (*)(pthread_mutex_t *__mutex))dlsym(RTLD_NEXT, "pthread_mutex_lock");
+ if ((error = dlerror()) != NULL) {
+ fputs(error, stderr);
+ exit(EXIT_FAILURE);
+ }
+ }
+ return pthread_mutex_lock_p(__mutex);
+}
+
+int real_pthread_mutex_unlock (pthread_mutex_t *__mutex) {
+ static int (*pthread_mutex_unlock_p) (pthread_mutex_t *__mutex) = NULL;
+ char * error;
+ if (!pthread_mutex_unlock_p) {
+ pthread_mutex_unlock_p = (int (*)(pthread_mutex_t *__mutex))dlsym(RTLD_NEXT, "pthread_mutex_unlock");
+ if ((error = dlerror()) != NULL) {
+ fputs(error, stderr);
+ exit(EXIT_FAILURE);
+ }
+ }
+ return pthread_mutex_unlock_p(__mutex);
+}
+
+int real_pthread_create (pthread_t *__restrict __newthread, const pthread_attr_t *__restrict __attr, void *(*__start_routine)(void *), void *__restrict __arg) {
+ static int (*pthread_create_p) (pthread_t *__restrict, const pthread_attr_t *__restrict, void *(*)(void *), void * __restrict) = NULL;
+ char * error;
+ if (!pthread_create_p) {
+ pthread_create_p = (int (*)(pthread_t *__restrict, const pthread_attr_t *__restrict, void *(*)(void *), void *__restrict))dlsym(RTLD_NEXT, "pthread_create");
+ if ((error = dlerror()) != NULL) {
+ fputs(error, stderr);
+ exit(EXIT_FAILURE);
+ }
+ }
+ return pthread_create_p(__newthread, __attr, __start_routine, __arg);
+}
+
+int real_pthread_join (pthread_t __th, void ** __thread_return) {
+ static int (*pthread_join_p) (pthread_t __th, void ** __thread_return) = NULL;
+ char * error;
+ if (!pthread_join_p) {
+ pthread_join_p = (int (*)(pthread_t __th, void ** __thread_return))dlsym(RTLD_NEXT, "pthread_join");
+ if ((error = dlerror()) != NULL) {
+ fputs(error, stderr);
+ exit(EXIT_FAILURE);
+ }
+ }
+ return pthread_join_p(__th, __thread_return);
+}
+
+void finalize_helper_thread() {
+ Thread * curr_thread = thread_current();
+ model_print("finalize_helper_thread\n");
+ real_pthread_mutex_lock(&curr_thread->mutex);
+ curr_thread->tls = (char *) get_tls_addr();
+ real_pthread_mutex_unlock(&curr_thread->mutex);
+ //Wait in the kernel until it is time for us to finish
+ real_pthread_mutex_lock(&curr_thread->mutex2);
+ real_pthread_mutex_unlock(&curr_thread->mutex2);
+ //return to helper thread function
+ setcontext(&curr_thread->context);
+}
+
+void * helper_thread(void * ptr) {
+ Thread * curr_thread = thread_current();
+ model_print("helper_thread\n");
+
+ //build a context for this real thread so we can take it's context
+ int ret = getcontext(&curr_thread->helpercontext);
+ ASSERT(!ret);
+
+ /* Initialize new managed context */
+ void *helperstack = stack_allocate(STACK_SIZE);
+ curr_thread->helpercontext.uc_stack.ss_sp = helperstack;
+ curr_thread->helpercontext.uc_stack.ss_size = STACK_SIZE;
+ curr_thread->helpercontext.uc_stack.ss_flags = 0;
+ curr_thread->helpercontext.uc_link = model->get_system_context();
+ makecontext(&curr_thread->helpercontext, finalize_helper_thread, 0);
+
+ model_swapcontext(&curr_thread->context, &curr_thread->helpercontext);
+
+ //start the real thread
+ thread_startup();
+
+ //now the real thread has control again
+ stack_free(helperstack);
+
+ return NULL;
+}
+
+void setup_context() {
+ Thread * curr_thread = thread_current();
+ model_print("setup_context\n");
+
+ /* Add dummy "start" action, just to create a first clock vector */
+ model->switch_to_master(new ModelAction(THREAD_START, std::memory_order_seq_cst, curr_thread));
+
+ /* Initialize our lock */
+ real_pthread_mutex_init(&curr_thread->mutex, NULL);
+ real_pthread_mutex_init(&curr_thread->mutex2, NULL);
+ real_pthread_mutex_lock(&curr_thread->mutex2);
+
+ /* Create the real thread */
+ real_pthread_create(&curr_thread->thread, NULL, helper_thread, NULL);
+ model_print("thread_created\n");
+ bool notdone = true;
+ while(notdone) {
+ real_pthread_mutex_lock(&curr_thread->mutex);
+ if (curr_thread->tls != NULL)
+ notdone = false;
+ real_pthread_mutex_unlock(&curr_thread->mutex);
+ }
+
+ set_tls_addr((uintptr_t)curr_thread->tls);
+ model_print("tls taken\n");
+ setcontext(&curr_thread->context);
+}
+#endif
+
/**
* Create a thread context for a new thread so we can use
* setcontext/getcontext/swapcontext to swap it out.
context.uc_stack.ss_size = STACK_SIZE;
context.uc_stack.ss_flags = 0;
context.uc_link = model->get_system_context();
+#ifdef TLS
+ if (model != NULL)
+ makecontext(&context, setup_context, 0);
+ else
+ makecontext(&context, thread_startup, 0);
+#else
makecontext(&context, thread_startup, 0);
+#endif
return 0;
}
if (stack)
stack_free(stack);
#ifdef TLS
- if (tls && get_id() != 1)
- tls += model->get_execution()->getTLSSize() - model->get_execution()->getThdDescSize();
- Thread_free(tls);
+ if (this != model->getInitThread()) {
+ real_pthread_mutex_unlock(&mutex2);
+ real_pthread_join(thread, NULL);
+ }
#endif
}