From: Brian Norris Date: Wed, 11 Jul 2012 04:31:24 +0000 (-0700) Subject: remove EOL spaces, fix indentation X-Git-Tag: pldi2013~363^2~4 X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=2db2ef3b8bdabacc7784fd5a4e7e7520f1cd2298 remove EOL spaces, fix indentation --- diff --git a/action.cc b/action.cc index f41b0eb..44d3f8f 100644 --- a/action.cc +++ b/action.cc @@ -101,7 +101,7 @@ bool ModelAction::is_synchronizing(const ModelAction *act) const // Different locations commute if (!same_var(act)) return false; - + // Explore interleavings of seqcst writes to guarantee total order // of seq_cst operations that don't commute if (is_write() && is_seqcst() && act->is_write() && act->is_seqcst()) diff --git a/action.h b/action.h index 111ac31..00bb5c2 100644 --- a/action.h +++ b/action.h @@ -90,7 +90,7 @@ private: /** The thread id that performed this action. */ thread_id_t tid; - + /** The value read or written (if RMW, then the value written). This * should probably be something longer. */ int value; @@ -98,7 +98,7 @@ private: /** A back reference to a Node in NodeStack, if this ModelAction is * saved on the NodeStack. */ Node *node; - + modelclock_t seq_number; /** The clock vector stored with this action; only needed if this diff --git a/clockvector.cc b/clockvector.cc index cfd99c6..162a7c2 100644 --- a/clockvector.cc +++ b/clockvector.cc @@ -84,7 +84,7 @@ bool ClockVector::synchronized_since(const ModelAction *act) const return false; } -/** +/** * Gets the clock corresponding to a given thread id from the clock * vector. */ diff --git a/datarace.cc b/datarace.cc index 29ace0a..5a23d82 100644 --- a/datarace.cc +++ b/datarace.cc @@ -45,7 +45,7 @@ static bool clock_may_race(ClockVector *clock1, thread_id_t tid1, return tid1 != tid2 && clock2 != 0 && clock1->getClock(tid2) <= clock2; } -/** +/** * Expands a record from the compact form to the full form. This is * necessary for multiple readers or for very large thread ids or time * stamps. */ diff --git a/hashtable.h b/hashtable.h index b544988..b1cd327 100644 --- a/hashtable.h +++ b/hashtable.h @@ -48,14 +48,14 @@ template memset(table, 0, capacity*sizeof(struct hashlistnode<_Key, _Val> *)); size=0; } - + void put(_Key key, _Val val) { 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; @@ -77,7 +77,7 @@ template _Val get(_Key key) { struct hashlistnode<_Key,_Val> *search = table[(((_KeyInt)key) & mask)>>_Shift]; - + while(search!=NULL) { if (search->key==key) { return search->val; @@ -89,7 +89,7 @@ template bool contains(_Key key) { struct hashlistnode<_Key,_Val> *search = table[(((_KeyInt)key) & mask)>>_Shift]; - + while(search!=NULL) { if (search->key==key) { return true; @@ -98,29 +98,29 @@ template } return false; } - + void resize(unsigned int newsize) { struct hashlistnode<_Key,_Val> ** oldtable = table; struct hashlistnode<_Key,_Val> ** newtable; unsigned int oldcapacity = capacity; - + if((newtable = (struct hashlistnode<_Key,_Val> **) calloc(newsize, sizeof(struct hashlistnode<_Key,_Val> *))) == NULL) { printf("Calloc error %s %d\n", __FILE__, __LINE__); exit(-1); } - + table = newtable; //Update the global hashtable upon resize() capacity = newsize; threshold = (unsigned int) (newsize * loadfactor); mask = (newsize << _Shift)-1; - + for(unsigned int i = 0; i < oldcapacity; i++) { struct hashlistnode<_Key, _Val> * bin = oldtable[i]; - + while(bin!=NULL) { _Key key=bin->key; struct hashlistnode<_Key, _Val> * next=bin->next; - + unsigned int index = (((_KeyInt)key) & mask) >>_Shift; struct hashlistnode<_Key, _Val> * tmp=newtable[index]; bin->next=tmp; @@ -128,10 +128,10 @@ template bin = next; } } - + free(oldtable); //Free the memory of the old hash table } - + private: struct hashlistnode<_Key,_Val> **table; unsigned int capacity; diff --git a/main.cc b/main.cc index a400fe3..19f12f1 100644 --- a/main.cc +++ b/main.cc @@ -56,8 +56,9 @@ static void thread_wait_finish(void) { void real_main() { thrd_t user_thread; ucontext_t main_context; - //Initialize race detector - initRaceDetector(); + + //Initialize race detector + initRaceDetector(); //Create the singleton SnapshotStack object snapshotObject = new SnapshotStack(); diff --git a/model.h b/model.h index 97e9849..941601b 100644 --- a/model.h +++ b/model.h @@ -1,5 +1,5 @@ /** @file model.h - * @brief Core model checker. + * @brief Core model checker. */ #ifndef __MODEL_H__ diff --git a/mymemory.cc b/mymemory.cc index 88018e2..f3464fc 100644 --- a/mymemory.cc +++ b/mymemory.cc @@ -20,7 +20,7 @@ void *MYMALLOC(size_t size) { static void *(*mallocp)(size_t size); char *error; void *ptr; - + /* get address of libc malloc */ if (!mallocp) { mallocp = ( void * ( * )( size_t ) )dlsym(RTLD_NEXT, "malloc"); @@ -29,7 +29,7 @@ void *MYMALLOC(size_t size) { exit(EXIT_FAILURE); } } - ptr = mallocp(size); + ptr = mallocp(size); return ptr; #else if( !sTheRecord ){ diff --git a/snapshot-interface.cc b/snapshot-interface.cc index baedf47..fbbc677 100644 --- a/snapshot-interface.cc +++ b/snapshot-interface.cc @@ -56,7 +56,7 @@ static void SnapshotGlobalSegments(){ //Skip out at the end of the section if (buf[0]=='\n') break; - + sscanf(buf, "%22s %p-%p [%5dK] %c%c%c/%c%c%c SM=%3s %200s\n", &type, &begin, &end, &size, &r, &w, &x, &mr, &mw, &mx, smstr, regionname); if (w == 'w' && (strstr(regionname, MYBINARYNAME) || strstr(regionname, MYLIBRARYNAME))) { @@ -113,11 +113,11 @@ SnapshotStack::~SnapshotStack(){ /** This method returns to the last snapshot before the inputted * sequence number. This function must be called from the model - * checking thread and not from a snapshotted stack. - * @param seqindex is the sequence number to rollback before. + * checking thread and not from a snapshotted stack. + * @param seqindex is the sequence number to rollback before. * @return is the sequence number we actually rolled back to. */ - + int SnapshotStack::backTrackBeforeStep(int seqindex) { while(true) { if (stack->index<=seqindex) { diff --git a/snapshot-interface.h b/snapshot-interface.h index 5f54edb..9912a1b 100644 --- a/snapshot-interface.h +++ b/snapshot-interface.h @@ -28,7 +28,7 @@ class SnapshotStack { int backTrackBeforeStep(int seq_index); void snapshotStep(int seq_index); - private: + private: struct stackEntry * stack; }; diff --git a/snapshot.cc b/snapshot.cc index 1e7d80b..b6e20fd 100644 --- a/snapshot.cc +++ b/snapshot.cc @@ -34,7 +34,7 @@ struct Snapshot * sTheRecord = NULL; #if !USE_MPROTECT_SNAPSHOT /** @statics -* These variables are necessary because the stack is shared region and +* These variables are necessary because the stack is shared region and * there exists a race between all processes executing the same function. * To avoid the problem above, we require variables allocated in 'safe' regions. * The bug was actually observed with the forkID, these variables below are @@ -66,7 +66,7 @@ static void * ReturnPageAlignedAddress(void * addr) { } /** The initSnapShotRecord method initialized the snapshotting data - * structures for the mprotect based snapshot. + * structures for the mprotect based snapshot. */ static void initSnapShotRecord(unsigned int numbackingpages, unsigned int numsnapshots, unsigned int nummemoryregions) { snapshotrecord=( struct SnapShot * )MYMALLOC(sizeof(struct SnapShot)); @@ -235,7 +235,7 @@ void initSnapShotLibrary(unsigned int numbackingpages, #endif } -/** The addMemoryRegionToSnapShot function assumes that addr is page aligned. +/** The addMemoryRegionToSnapShot function assumes that addr is page aligned. */ void addMemoryRegionToSnapShot( void * addr, unsigned int numPages) { #if USE_MPROTECT_SNAPSHOT @@ -310,7 +310,7 @@ void rollBack( snapshot_id theID ){ getcontext( &sTheRecord->mContextToRollback ); /* * This is used to quit the process on rollback, so that - * the process which needs to rollback can quit allowing the process whose snapshotid matches the rollbackid to switch to + * the process which needs to rollback can quit allowing the process whose snapshotid matches the rollbackid to switch to * this context and continue.... */ if( !sTemp ){