From db2c4ca161b4cba9e453431517af86798c0e9bdb Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Sat, 9 Mar 2013 12:51:36 -0800 Subject: [PATCH] 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. --- mymemory.cc | 40 ++++++++++++++++++++++++++++++++++------ mymemory.h | 3 +++ threads-model.h | 12 ++++++++++++ 3 files changed, 49 insertions(+), 6 deletions(-) diff --git a/mymemory.cc b/mymemory.cc index 44985fa..ea8670d 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 f2a3186..a62ab83 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 e77e80c..eb0fd43 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(); -- 2.34.1