$(CXX) $(SHARED) -o $(LIB_SO) $(OBJECTS) $(LDFLAGS)
malloc.o: malloc.c
- $(CC) -fPIC -c malloc.c -DMSPACES -DONLY_MSPACES -DHAVE_MMAP=0 $(CPPFLAGS)
+ $(CC) -fPIC -c malloc.c -DMSPACES -DONLY_MSPACES -DHAVE_MMAP=0 $(CPPFLAGS) -Wno-unused-variable
%.o: %.cc
$(CXX) -fPIC -c $< $(CPPFLAGS)
this->tid = t->get_id();
}
+/** @brief ModelAction destructor */
ModelAction::~ModelAction()
{
- /** We can't free the clock vector:
- * The reason is as follows:
- * Clock vectors are snapshotting state... when we delete model actions
- * they are at the end of the node list and have invalid old clock vectors...
- * They are already free at that point...
+ /**
+ * We can't free the clock vector:
+ * Clock vectors are snapshotting state. When we delete model actions,
+ * they are at the end of the node list and have invalid old clock
+ * vectors which have already been rolled back to an unallocated state.
*/
-
- /* if (cv)
- delete cv;*/
+
+ /*
+ if (cv)
+ delete cv; */
}
void ModelAction::copy_from_new(ModelAction *newaction)
#ifdef CONFIG_DEBUG
#define DEBUG(fmt, ...) do { printf("*** %25s(): line %-4d *** " fmt, __func__, __LINE__, ##__VA_ARGS__); } while (0)
-#define DBG() DEBUG("\n");
+#define DBG() DEBUG("\n")
#define DBG_ENABLED() (1)
#else
#define DEBUG(fmt, ...)
assert_hook(); \
exit(EXIT_FAILURE); \
} \
-} while (0);
+} while (0)
#define error_msg(...) fprintf(stderr, "Error: " __VA_ARGS__)
* @return True, @a from can reach @a to; otherwise, false
*/
bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) {
- std::vector<CycleNode *, MyAlloc<CycleNode *> > queue;
+ std::vector<CycleNode *, ModelAlloc<CycleNode *> > queue;
HashTable<CycleNode *, CycleNode *, uintptr_t, 4, model_malloc, model_calloc, model_free> discovered;
queue.push_back(from);
#include "threads.h"
#include <stdio.h>
#include <cstring>
+#include "mymemory.h"
struct ShadowTable *root;
std::vector<struct DataRace *> unrealizedraces;
/** This function initialized the data race detector. */
void initRaceDetector() {
- root=(struct ShadowTable *) calloc(sizeof(struct ShadowTable),1);
+ root = (struct ShadowTable *)snapshot_calloc(sizeof(struct ShadowTable), 1);
}
/** This function looks up the entry in the shadow table corresponding to a
#if BIT48
currtable=(struct ShadowTable *) currtable->array[(((uintptr_t)address)>>32)&MASK16BIT];
if (currtable==NULL) {
- currtable=(struct ShadowTable *) (root->array[(((uintptr_t)address)>>32)&MASK16BIT]=calloc(sizeof(struct ShadowTable),1));
+ currtable = (struct ShadowTable *)(root->array[(((uintptr_t)address)>>32)&MASK16BIT] = snapshot_calloc(sizeof(struct ShadowTable), 1));
}
#endif
struct ShadowBaseTable * basetable=(struct ShadowBaseTable *) currtable->array[(((uintptr_t)address)>>16)&MASK16BIT];
if (basetable==NULL) {
- basetable=(struct ShadowBaseTable *) (currtable->array[(((uintptr_t)address)>>16)&MASK16BIT]=calloc(sizeof(struct ShadowBaseTable),1));
+ basetable = (struct ShadowBaseTable *)(currtable->array[(((uintptr_t)address)>>16)&MASK16BIT] = snapshot_calloc(sizeof(struct ShadowBaseTable), 1));
}
return &basetable->array[((uintptr_t)address)&MASK16BIT];
}
modelclock_t writeClock = WRITEVECTOR(shadowval);
thread_id_t writeThread = int_to_id(WRTHREADID(shadowval));
- struct RaceRecord * record=(struct RaceRecord *)calloc(1,sizeof(struct RaceRecord));
+ struct RaceRecord *record = (struct RaceRecord *)snapshot_calloc(1, sizeof(struct RaceRecord));
record->writeThread=writeThread;
record->writeClock=writeClock;
if (readClock!=0) {
record->capacity=INITCAPACITY;
- record->thread=(thread_id_t *) malloc(sizeof(thread_id_t)*record->capacity);
- record->readClock=(modelclock_t *) malloc(sizeof(modelclock_t)*record->capacity);
+ record->thread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t)*record->capacity);
+ record->readClock = (modelclock_t *)snapshot_malloc(sizeof(modelclock_t)*record->capacity);
record->numReads=1;
record->thread[0]=readThread;
record->readClock[0]=readClock;
/** This function is called when we detect a data race.*/
static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool isoldwrite, ModelAction *newaction, bool isnewwrite, void *address) {
- struct DataRace * race=(struct DataRace *)malloc(sizeof(struct DataRace));
+ struct DataRace *race = (struct DataRace *)snapshot_malloc(sizeof(struct DataRace));
race->oldthread=oldthread;
race->oldclock=oldclock;
race->isoldwrite=isoldwrite;
if (copytoindex>=record->capacity) {
int newCapacity=record->capacity*2;
- thread_id_t *newthread=(thread_id_t *) malloc(sizeof(thread_id_t)*newCapacity);
- modelclock_t * newreadClock=(modelclock_t *) malloc(sizeof(modelclock_t)*newCapacity);
+ thread_id_t *newthread = (thread_id_t *)snapshot_malloc(sizeof(thread_id_t)*newCapacity);
+ modelclock_t *newreadClock =( modelclock_t *)snapshot_malloc(sizeof(modelclock_t)*newCapacity);
std::memcpy(newthread, record->thread, record->capacity*sizeof(thread_id_t));
std::memcpy(newreadClock, record->readClock, record->capacity*sizeof(modelclock_t));
- free(record->readClock);
- free(record->thread);
+ snapshot_free(record->readClock);
+ snapshot_free(record->thread);
record->readClock=newreadClock;
record->thread=newthread;
record->capacity=newCapacity;
#include <stdlib.h>
#include <stdio.h>
+#include "mymemory.h"
/**
* Hashtable linked node class, for chained storage of hash table conflicts. By
* @tparam _free Provide your own 'free' for the table, or default to
* snapshotting.
*/
-template<typename _Key, typename _Val, typename _KeyInt, int _Shift=0, void * (* _malloc)(size_t)=malloc, void * (* _calloc)(size_t, size_t)=calloc, void (*_free)(void *)=free>
+template<typename _Key, typename _Val, typename _KeyInt, int _Shift=0, void * (* _malloc)(size_t)=snapshot_malloc, void * (* _calloc)(size_t, size_t)=snapshot_calloc, void (*_free)(void *)=snapshot_free>
class HashTable {
public:
/**
main_argv = argv;
/* Let's jump in quickly and start running stuff */
- initSnapShotLibrary(10000, 1024, 1024, 4000, &real_main);
+ initSnapshotLibrary(10000, 1024, 1024, 4000, &real_main);
}
class Promise;
/** @brief Shorthand for a list of release sequence heads */
-typedef std::vector< const ModelAction *, MyAlloc<const ModelAction *> > rel_heads_list_t;
+typedef std::vector< const ModelAction *, ModelAlloc<const ModelAction *> > rel_heads_list_t;
/**
* Model checker parameter structure. Holds run-time configuration options for
#endif
}
+/** @brief Snapshotting malloc, for use by model-checker (not user progs) */
+void * snapshot_malloc(size_t size)
+{
+ return malloc(size);
+}
+
+/** @brief Snapshotting calloc, for use by model-checker (not user progs) */
+void * snapshot_calloc(size_t count, size_t size)
+{
+ return calloc(count, size);
+}
+
+/** @brief Snapshotting free, for use by model-checker (not user progs) */
+void snapshot_free(void *ptr)
+{
+ free(ptr);
+}
+
void *system_malloc( size_t size ){
static void *(*mallocp)(size_t size);
char *error;
}
-/** This global references the mspace for the snapshotting heap */
+/** @brief Global mspace reference for the snapshotting heap */
mspace mySpace = NULL;
-/** This global references the unaligned memory address that was malloced for the snapshotting heap */
-void * basemySpace = NULL;
+/** @brief Global reference to the unaligned memory address that was malloc'd
+ * for the snapshotting heap */
+void *basemySpace = NULL;
/** Bootstrap allocation. Problem is that the dynamic linker calls
* require calloc to work and calloc requires the dynamic linker to
return (ptr>=(&bootstrapmemory[0])&&ptr<(&bootstrapmemory[BOOTSTRAPBYTES]));
}
-/** Snapshotting malloc implementation for user programs. */
-void *malloc( size_t size ) {
+/** @brief Snapshotting malloc implementation for user programs */
+void *malloc( size_t size )
+{
if (mySpace) {
void *tmp=mspace_malloc( mySpace, size );
ASSERT(tmp);
return tmp;
- } else
+ } else
return HandleEarlyAllocationRequest( size );
}
-/** Snapshotting free implementation for user programs. */
+/** @brief Snapshotting free implementation for user programs */
void free( void * ptr ){
- if( DontFree( ptr ) ) return;
- mspace_free( mySpace, ptr );
+ if (!DontFree(ptr))
+ mspace_free(mySpace, ptr);
}
-/** Snapshotting realloc implementation for user programs. */
-void *realloc( void *ptr, size_t size ){
- void *tmp=mspace_realloc( mySpace, ptr, size );
+/** @brief Snapshotting realloc implementation for user programs */
+void *realloc( void *ptr, size_t size )
+{
+ void *tmp = mspace_realloc(mySpace, ptr, size);
ASSERT(tmp);
return tmp;
}
-/** Snapshotting calloc implementation for user programs. */
-void * calloc( size_t num, size_t size ){
+/** @brief Snapshotting calloc implementation for user programs */
+void * calloc( size_t num, size_t size )
+{
if (mySpace) {
- void *tmp=mspace_calloc( mySpace, num, size );
+ void *tmp = mspace_calloc(mySpace, num, size);
ASSERT(tmp);
return tmp;
} else {
}
}
-/** Snapshotting new operator for user programs. */
-void * operator new(size_t size) throw(std::bad_alloc) {
+/** @brief Snapshotting new operator for user programs */
+void * operator new(size_t size) throw(std::bad_alloc)
+{
return malloc(size);
}
-/** Snapshotting delete operator for user programs. */
-void operator delete(void *p) throw() {
+/** @brief Snapshotting delete operator for user programs */
+void operator delete(void *p) throw()
+{
free(p);
}
-/** Snapshotting new[] operator for user programs. */
-void * operator new[](size_t size) throw(std::bad_alloc) {
+/** @brief Snapshotting new[] operator for user programs */
+void * operator new[](size_t size) throw(std::bad_alloc)
+{
return malloc(size);
}
-/** Snapshotting delete[] operator for user programs. */
-void operator delete[](void *p, size_t size) {
+/** @brief Snapshotting delete[] operator for user programs */
+void operator delete[](void *p, size_t size)
+{
free(p);
}
* memory in the non-snapshotting heap. */
#define MEMALLOC \
void * operator new(size_t size) { \
- return model_malloc(size);\
- }\
+ return model_malloc(size); \
+ } \
void operator delete(void *p, size_t size) { \
- model_free( p ); \
- }\
+ model_free(p); \
+ } \
void * operator new[](size_t size) { \
- return model_malloc(size);\
- }\
- void operator delete[](void *p, size_t size) {\
- model_free(p);\
+ return model_malloc(size); \
+ } \
+ void operator delete[](void *p, size_t size) { \
+ model_free(p); \
}
/** SNAPSHOTALLOC declares the allocators for a class to allocate
* memory in the snapshotting heap. */
-#define SNAPSHOTALLOC
+#define SNAPSHOTALLOC \
+ void * operator new(size_t size) { \
+ return snapshot_malloc(size); \
+ } \
+ void operator delete(void *p, size_t size) { \
+ snapshot_free(p); \
+ } \
+ void * operator new[](size_t size) { \
+ return snapshot_malloc(size); \
+ } \
+ void operator delete[](void *p, size_t size) { \
+ snapshot_free(p); \
+ }
void *model_malloc(size_t size);
void *model_calloc(size_t count, size_t size);
void model_free(void *ptr);
-static inline void * snapshot_malloc(size_t size) {
- return malloc(size);
-}
-static inline void * snapshot_calloc(size_t count, size_t size) {
- return calloc(count, size);
-}
-static inline void snapshot_free(void *ptr) {
- free(ptr);
-}
+void * snapshot_malloc(size_t size);
+void * snapshot_calloc(size_t count, size_t size);
+void snapshot_free(void *ptr);
void system_free( void * ptr );
void *system_malloc( size_t size );
* warranty, and with no claim as to its suitability for any purpose.
*/
template <class T>
- class MyAlloc {
- public:
- // type definitions
- typedef T value_type;
- typedef T* pointer;
- typedef const T* const_pointer;
- typedef T& reference;
- typedef const T& const_reference;
- typedef size_t size_type;
- typedef size_t difference_type;
-
- // rebind allocator to type U
- template <class U>
- struct rebind {
- typedef MyAlloc<U> other;
- };
-
- // return address of values
- pointer address (reference value) const {
- return &value;
- }
- const_pointer address (const_reference value) const {
- return &value;
- }
-
- /* constructors and destructor
- * - nothing to do because the allocator has no state
- */
- MyAlloc() throw() {
- }
- MyAlloc(const MyAlloc&) throw() {
- }
- template <class U>
- MyAlloc (const MyAlloc<U>&) throw() {
- }
- ~MyAlloc() throw() {
- }
-
- // return maximum number of elements that can be allocated
- size_type max_size () const throw() {
- return std::numeric_limits<size_t>::max() / sizeof(T);
- }
-
- // allocate but don't initialize num elements of type T
- pointer allocate (size_type num, const void* = 0) {
- pointer p = ( pointer )model_malloc( num * sizeof( T ) );
- return p;
- }
-
- // initialize elements of allocated storage p with value value
- void construct (pointer p, const T& value) {
- // initialize memory with placement new
- new((void*)p)T(value);
- }
-
- // destroy elements of initialized storage p
- void destroy (pointer p) {
- // destroy objects by calling their destructor
- p->~T();
- }
-
- // deallocate storage p of deleted elements
- void deallocate (pointer p, size_type num) {
- model_free((void*)p);
- }
- };
+class ModelAlloc {
+ public:
+ // type definitions
+ typedef T value_type;
+ typedef T* pointer;
+ typedef const T* const_pointer;
+ typedef T& reference;
+ typedef const T& const_reference;
+ typedef size_t size_type;
+ typedef size_t difference_type;
+
+ // rebind allocator to type U
+ template <class U>
+ struct rebind {
+ typedef ModelAlloc<U> other;
+ };
+
+ // return address of values
+ pointer address(reference value) const {
+ return &value;
+ }
+ const_pointer address(const_reference value) const {
+ return &value;
+ }
+
+ /* constructors and destructor
+ * - nothing to do because the allocator has no state
+ */
+ ModelAlloc() throw() {
+ }
+ ModelAlloc(const ModelAlloc&) throw() {
+ }
+ template <class U>
+ ModelAlloc(const ModelAlloc<U>&) throw() {
+ }
+ ~ModelAlloc() throw() {
+ }
+
+ // return maximum number of elements that can be allocated
+ size_type max_size() const throw() {
+ return std::numeric_limits<size_t>::max() / sizeof(T);
+ }
+
+ // allocate but don't initialize num elements of type T
+ pointer allocate(size_type num, const void * = 0) {
+ pointer p = (pointer)model_malloc(num * sizeof(T));
+ return p;
+ }
+
+ // initialize elements of allocated storage p with value value
+ void construct(pointer p, const T& value) {
+ // initialize memory with placement new
+ new((void*)p)T(value);
+ }
+
+ // destroy elements of initialized storage p
+ void destroy(pointer p) {
+ // destroy objects by calling their destructor
+ p->~T();
+ }
+
+ // deallocate storage p of deleted elements
+ void deallocate(pointer p, size_type num) {
+ model_free((void*)p);
+ }
+};
/** Return that all specializations of this allocator are interchangeable. */
- template <class T1, class T2>
- bool operator== (const MyAlloc<T1>&,
- const MyAlloc<T2>&) throw() {
- return true;
- }
+template <class T1, class T2>
+bool operator== (const ModelAlloc<T1>&,
+ const ModelAlloc<T2>&) throw() {
+ return true;
+}
/** Return that all specializations of this allocator are interchangeable. */
- template <class T1, class T2>
- bool operator!= (const MyAlloc<T1>&,
- const MyAlloc<T2>&) throw() {
- return false;
- }
+template <class T1, class T2>
+bool operator!= (const ModelAlloc<T1>&,
+ const ModelAlloc<T2>&) throw() {
+ return false;
+}
#ifdef __cplusplus
extern "C" {
ModelAction *action;
Node *parent;
int num_threads;
- std::vector< bool, MyAlloc<bool> > explored_children;
- std::vector< bool, MyAlloc<bool> > backtrack;
- std::vector< struct fairness_info, MyAlloc< struct fairness_info> > fairness;
+ std::vector< bool, ModelAlloc<bool> > explored_children;
+ std::vector< bool, ModelAlloc<bool> > backtrack;
+ std::vector< struct fairness_info, ModelAlloc< struct fairness_info> > fairness;
int numBacktracks;
bool *enabled_array;
/** The set of ModelActions that this the action at this Node may read
* from. Only meaningful if this Node represents a 'read' action. */
- std::vector< const ModelAction *, MyAlloc< const ModelAction * > > may_read_from;
+ std::vector< const ModelAction *, ModelAlloc< const ModelAction * > > may_read_from;
unsigned int read_from_index;
- std::vector< struct future_value, MyAlloc<struct future_value> > future_values;
- std::vector< promise_t, M
yAlloc<promise_t> > promises;
+ std::vector< struct future_value, ModelAlloc<struct future_value> > future_values;
+ std::vector< promise_t, M
odelAlloc<promise_t> > promises;
int future_index;
};
-typedef std::vector< Node *, MyAlloc< Node * > > node_list_t;
+typedef std::vector< Node *, ModelAlloc< Node * > > node_list_t;
/**
* @brief A stack of nodes
void Scheduler::set_enabled(Thread *t, bool enabled_status) {
int threadid=id_to_int(t->get_id());
if (threadid>=enabled_len) {
- bool * new_enabled=(bool *)malloc(sizeof(bool)*(threadid+1));
+ bool *new_enabled = (bool *)snapshot_malloc(sizeof(bool) * (threadid + 1));
memset(&new_enabled[enabled_len], 0, (threadid+1-enabled_len)*sizeof(bool));
if (is_enabled != NULL) {
memcpy(new_enabled, is_enabled, enabled_len*sizeof(bool));
- free(is_enabled);
+ snapshot_free(is_enabled);
}
is_enabled=new_enabled;
enabled_len=threadid+1;
typedef unsigned int snapshot_id;
typedef void (*VoidFuncPtr)();
-void initSnapShotLibrary(unsigned int numbackingpages,
+void initSnapshotLibrary(unsigned int numbackingpages,
unsigned int numsnapshots, unsigned int nummemoryregions,
unsigned int numheappages, VoidFuncPtr entryPoint);
#endif
-/** The initSnapShotLibrary function initializes the Snapshot library.
+/** The initSnapshotLibrary function initializes the snapshot library.
* @param entryPoint the function that should run the program.
*/
#if USE_MPROTECT_SNAPSHOT
-void initSnapShotLibrary(unsigned int numbackingpages,
+void initSnapshotLibrary(unsigned int numbackingpages,
unsigned int numsnapshots, unsigned int nummemoryregions,
unsigned int numheappages, VoidFuncPtr entryPoint) {
/* Setup a stack for our signal handler.... */
entryPoint();
}
#else
-void initSnapShotLibrary(unsigned int numbackingpages,
+void initSnapshotLibrary(unsigned int numbackingpages,
unsigned int numsnapshots, unsigned int nummemoryregions,
unsigned int numheappages, VoidFuncPtr entryPoint) {
basemySpace=system_malloc((numheappages+1)*PAGESIZE);
/** Allocate a stack for a new thread. */
static void * stack_allocate(size_t size)
{
- return malloc(size);
+ return snapshot_malloc(size);
}
/** Free a stack for a terminated thread. */
static void stack_free(void *stack)
{
- free(stack);
+ snapshot_free(stack);
}
/** Return the currently executing thread. */
};
/** @brief typedef for the work queue type */
-typedef std::list< WorkQueueEntry, MyAlloc<WorkQueueEntry> > work_queue_t;
+typedef std::list< WorkQueueEntry, ModelAlloc<WorkQueueEntry> > work_queue_t;
#endif /* __WORKQUEUE_H__ */
projects / model-checker.git / commitdiff