From: Brian Demsky Date: Fri, 20 Jul 2012 21:39:23 +0000 (-0700) Subject: switch everything over to our own hashtable X-Git-Tag: pldi2013~314 X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=b7153285e24941be76175eeb163d25f6f604f96f switch everything over to our own hashtable give us a calloc to use from our code --- diff --git a/hashtable.h b/hashtable.h index e59a995..c877d9f 100644 --- a/hashtable.h +++ b/hashtable.h @@ -18,7 +18,7 @@ template /** Hashtable class. By default it is snapshotting, but you can pass in your own allocation functions. */ -template +template class HashTable { public: HashTable(unsigned int initialcapacity=1024, double factor=0.5) { @@ -100,6 +100,32 @@ template>_Shift]=newptr; } + /** Put a key entry into the table. */ + _Val * ensureptr(_Key key) { + if(size > threshold) { + //Resize + unsigned int newsize = capacity << 1; + resize(newsize); + } + + struct hashlistnode<_Key,_Val> *ptr = table[(((_KeyInt)key) & mask)>>_Shift]; + size++; + struct hashlistnode<_Key,_Val> *search = ptr; + + while(search!=NULL) { + if (search->key==key) { + return &search->val; + } + search=search->next; + } + + struct hashlistnode<_Key,_Val> *newptr=(struct hashlistnode<_Key,_Val> *)new struct hashlistnode<_Key,_Val>; + newptr->key=key; + newptr->next=ptr; + table[(((_KeyInt)key)&mask)>>_Shift]=newptr; + return &newptr->val; + } + /** Lookup the corresponding value for the given key. */ _Val get(_Key key) { struct hashlistnode<_Key,_Val> *search = table[(((_KeyInt)key) & mask)>>_Shift]; @@ -113,6 +139,19 @@ template *search = table[(((_KeyInt)key) & mask)>>_Shift]; + + while(search!=NULL) { + if (search->key==key) { + return & search->val; + } + search=search->next; + } + return (_Val *) NULL; + } + /** Check whether the table contains a value for the given key. */ bool contains(_Key key) { struct hashlistnode<_Key,_Val> *search = table[(((_KeyInt)key) & mask)>>_Shift]; diff --git a/model.cc b/model.cc index e18fda1..de8f10c 100644 --- a/model.cc +++ b/model.cc @@ -27,9 +27,9 @@ ModelChecker::ModelChecker() diverge(NULL), nextThread(THREAD_ID_T_NONE), action_trace(new action_list_t()), - thread_map(new std::map), - obj_map(new std::map()), - obj_thrd_map(new std::map >()), + thread_map(new HashTable()), + obj_map(new HashTable()), + obj_thrd_map(new HashTable, uintptr_t, 4 >()), thrd_last_action(new std::vector(1)), node_stack(new NodeStack()), next_backtrack(NULL), @@ -40,9 +40,9 @@ ModelChecker::ModelChecker() /** @brief Destructor */ ModelChecker::~ModelChecker() { - std::map::iterator it; + /* std::map::iterator it; for (it = thread_map->begin(); it != thread_map->end(); it++) - delete (*it).second; + delete (*it).second;*/ delete thread_map; delete obj_thrd_map; @@ -102,7 +102,7 @@ Thread * ModelChecker::schedule_next_thread() Thread *t; if (nextThread == THREAD_ID_T_NONE) return NULL; - t = (*thread_map)[id_to_int(nextThread)]; + t = thread_map->get(id_to_int(nextThread)); ASSERT(t != NULL); @@ -190,7 +190,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) return NULL; } /* linear search: from most recent to oldest */ - action_list_t *list = &(*obj_map)[act->get_location()]; + action_list_t *list = obj_map->ensureptr(act->get_location()); action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; @@ -349,7 +349,7 @@ ModelAction * ModelChecker::process_rmw(ModelAction * act) { * @param rf The action that curr reads from. Must be a write. */ void ModelChecker::r_modification_order(ModelAction * curr, const ModelAction *rf) { - std::vector *thrd_lists = &(*obj_thrd_map)[curr->get_location()]; + std::vector *thrd_lists = obj_thrd_map->ensureptr(curr->get_location()); unsigned int i; ASSERT(curr->is_read()); @@ -381,7 +381,7 @@ void ModelChecker::r_modification_order(ModelAction * curr, const ModelAction *r * @param curr The current action. Must be a write. */ void ModelChecker::w_modification_order(ModelAction * curr) { - std::vector *thrd_lists = &(*obj_thrd_map)[curr->get_location()]; + std::vector *thrd_lists = obj_thrd_map->ensureptr(curr->get_location()); unsigned int i; ASSERT(curr->is_write()); @@ -425,9 +425,9 @@ void ModelChecker::add_action_to_lists(ModelAction *act) int tid = id_to_int(act->get_tid()); action_trace->push_back(act); - (*obj_map)[act->get_location()].push_back(act); + obj_map->ensureptr(act->get_location())->push_back(act); - std::vector *vec = &(*obj_thrd_map)[act->get_location()]; + std::vector *vec = obj_thrd_map->ensureptr(act->get_location()); if (tid >= (int)vec->size()) vec->resize(next_thread_id); (*vec)[tid].push_back(act); @@ -453,7 +453,7 @@ ModelAction * ModelChecker::get_last_action(thread_id_t tid) */ ModelAction * ModelChecker::get_last_seq_cst(const void *location) { - action_list_t *list = &(*obj_map)[location]; + action_list_t *list = obj_map->ensureptr(location); /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */ action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) @@ -488,7 +488,7 @@ ClockVector * ModelChecker::get_cv(thread_id_t tid) { */ void ModelChecker::build_reads_from_past(ModelAction *curr) { - std::vector *thrd_lists = &(*obj_thrd_map)[curr->get_location()]; + std::vector *thrd_lists = obj_thrd_map->ensureptr(curr->get_location()); unsigned int i; ASSERT(curr->is_read()); @@ -580,7 +580,7 @@ void ModelChecker::print_summary(void) int ModelChecker::add_thread(Thread *t) { - (*thread_map)[id_to_int(t->get_id())] = t; + thread_map->put(id_to_int(t->get_id()), t); scheduler->add_thread(t); return 0; } diff --git a/model.h b/model.h index 8593b98..b6099c6 100644 --- a/model.h +++ b/model.h @@ -6,7 +6,6 @@ #define __MODEL_H__ #include -#include #include #include #include @@ -46,7 +45,7 @@ public: int add_thread(Thread *t); void remove_thread(Thread *t); - Thread * get_thread(thread_id_t tid) { return (*thread_map)[id_to_int(tid)]; } + Thread * get_thread(thread_id_t tid) { return thread_map->get(id_to_int(tid)); } thread_id_t get_next_id(); int get_num_threads(); @@ -93,13 +92,13 @@ private: ucontext_t *system_context; action_list_t *action_trace; - std::map *thread_map; + HashTable *thread_map; /** Per-object list of actions. Maps an object (i.e., memory location) * to a trace of all actions performed on the object. */ - std::map *obj_map; + HashTable *obj_map; - std::map > *obj_thrd_map; + HashTable, uintptr_t, 4 > *obj_thrd_map; std::vector *thrd_last_action; NodeStack *node_stack; ModelAction *next_backtrack; diff --git a/mymemory.cc b/mymemory.cc index e851818..a365bb4 100644 --- a/mymemory.cc +++ b/mymemory.cc @@ -13,10 +13,37 @@ int howManyFreed = 0; static mspace sStaticSpace = NULL; #endif +/** Non-snapshotting calloc for our use. */ +void *MYCALLOC(size_t count, size_t size) { +#if USE_MPROTECT_SNAPSHOT + static void *(*callocp)(size_t count, size_t size)=NULL; + char *error; + void *ptr; + + /* get address of libc malloc */ + if (!callocp) { + callocp = ( void * ( * )( size_t, size_t ) )dlsym(RTLD_NEXT, "calloc"); + if ((error = dlerror()) != NULL) { + fputs(error, stderr); + exit(EXIT_FAILURE); + } + } + ptr = callocp(count, size); + return ptr; +#else + if( !snapshotrecord) { + createSharedMemory(); + } + if( NULL == sStaticSpace ) + sStaticSpace = create_mspace_with_base( ( void * )( snapshotrecord->mSharedMemoryBase ), SHARED_MEMORY_DEFAULT -sizeof( struct SnapShot ), 1 ); + return mspace_calloc( sStaticSpace, count, size ); +#endif +} + /** Non-snapshotting malloc for our use. */ void *MYMALLOC(size_t size) { #if USE_MPROTECT_SNAPSHOT - static void *(*mallocp)(size_t size); + static void *(*mallocp)(size_t size)=NULL; char *error; void *ptr; diff --git a/mymemory.h b/mymemory.h index fb6df12..4c44f5b 100644 --- a/mymemory.h +++ b/mymemory.h @@ -28,6 +28,7 @@ #define SNAPSHOTALLOC void *MYMALLOC(size_t size); +void *MYCALLOC(size_t count, size_t size); void MYFREE(void *ptr); void system_free( void * ptr ); diff --git a/snapshot.cc b/snapshot.cc index 9020bb7..95a6593 100644 --- a/snapshot.cc +++ b/snapshot.cc @@ -3,7 +3,7 @@ #include #include #include -#include +#include "hashtable.h" #include #include #include "snapshot.h" @@ -281,7 +281,7 @@ snapshot_id takeSnapshot( ){ */ void rollBack( snapshot_id theID ){ #if USE_MPROTECT_SNAPSHOT - std::map< void *, bool, std::less< void * >, MyAlloc< std::pair< const void *, bool > > > duplicateMap; + HashTable< void *, bool, uintptr_t, 4, MYMALLOC, MYCALLOC, MYFREE> duplicateMap; for(unsigned int region=0; regionlastRegion;region++) { if( mprotect(snapshotrecord->regionsToSnapShot[region].basePtr, snapshotrecord->regionsToSnapShot[region].sizeInPages*sizeof(struct SnapShotPage), PROT_READ | PROT_WRITE ) == -1 ){ perror("mprotect"); @@ -290,14 +290,8 @@ void rollBack( snapshot_id theID ){ } } for(unsigned int page=snapshotrecord->snapShots[theID].firstBackingPage; pagelastBackingPage; page++) { - bool oldVal = false; - if( duplicateMap.find( snapshotrecord->backingRecords[page].basePtrOfPage ) != duplicateMap.end() ){ - oldVal = true; - } - else{ - duplicateMap[ snapshotrecord->backingRecords[page].basePtrOfPage ] = true; - } - if( !oldVal ){ + if( !duplicateMap.contains(snapshotrecord->backingRecords[page].basePtrOfPage )) { + duplicateMap.put(snapshotrecord->backingRecords[page].basePtrOfPage, true); memcpy(snapshotrecord->backingRecords[page].basePtrOfPage, &snapshotrecord->backingStore[page], sizeof(struct SnapShotPage)); } }