From: Brian Norris Date: Sat, 9 Mar 2013 20:51:36 +0000 (-0800) Subject: mymemory, threads: add allocator specifically for Thread X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=db2c4ca161b4cba9e453431517af86798c0e9bdb mymemory, threads: add allocator specifically for Thread clas Thread is a special exception, where user-space allocations should happend from the model-checker context. So provide a special set of functions to specifically differentiate these allocations. --- diff --git a/mymemory.cc b/mymemory.cc index 44985fa3..ea8670d6 100644 --- a/mymemory.cc +++ b/mymemory.cc @@ -155,14 +155,30 @@ static bool DontFree(void *ptr) return (ptr >= (&bootstrapmemory[0]) && ptr < (&bootstrapmemory[BOOTSTRAPBYTES])); } -/** @brief Snapshotting malloc implementation for user programs */ +/** + * @brief The allocator function for "user" allocation + * + * Should only be used for allocations which will not disturb the allocation + * patterns of a user thread. + */ +static void * user_malloc(size_t size) +{ + void *tmp = mspace_malloc(user_snapshot_space, size); + ASSERT(tmp); + return tmp; +} + +/** + * @brief Snapshotting malloc implementation for user programs + * + * Do NOT call this function from a model-checker context. Doing so may disrupt + * the allocation patterns of a user thread. + */ void *malloc(size_t size) { - if (user_snapshot_space) { - void *tmp = mspace_malloc(user_snapshot_space, size); - ASSERT(tmp); - return tmp; - } else + if (user_snapshot_space) + return user_malloc(size); + else return HandleEarlyAllocationRequest(size); } @@ -195,6 +211,18 @@ void * calloc(size_t num, size_t size) } } +/** @brief Snapshotting allocation function for use by the Thread class only */ +void * Thread_malloc(size_t size) +{ + return user_malloc(size); +} + +/** @brief Snapshotting free function for use by the Thread class only */ +void Thread_free(void *ptr) +{ + free(ptr); +} + /** @brief Snapshotting new operator for user programs */ void * operator new(size_t size) throw(std::bad_alloc) { diff --git a/mymemory.h b/mymemory.h index f2a31865..a62ab83b 100644 --- a/mymemory.h +++ b/mymemory.h @@ -56,6 +56,9 @@ void * snapshot_calloc(size_t count, size_t size); void * snapshot_realloc(void *ptr, size_t size); void snapshot_free(void *ptr); +void * Thread_malloc(size_t size); +void Thread_free(void *ptr); + /** @brief Provides a non-snapshotting allocator for use in STL classes. * * The code was adapted from a code example from the book The C++ diff --git a/threads-model.h b/threads-model.h index e77e80cc..eb0fd438 100644 --- a/threads-model.h +++ b/threads-model.h @@ -126,6 +126,18 @@ public: * to allow their allocation/deallocation to follow the same pattern as * the rest of the backtracked/replayed program. */ + void * operator new(size_t size) { + return Thread_malloc(size); + } + void operator delete(void *p, size_t size) { + Thread_free(p); + } + void * operator new[](size_t size) { + return Thread_malloc(size); + } + void operator delete[](void *p, size_t size) { + Thread_free(p); + } private: int create_context();