// 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())
/** 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;
/** 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
return false;
}
-/**
+/**
* Gets the clock corresponding to a given thread id from the clock
* vector. */
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. */
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;
_Val get(_Key key) {
struct hashlistnode<_Key,_Val> *search = table[(((_KeyInt)key) & mask)>>_Shift];
-
+
while(search!=NULL) {
if (search->key==key) {
return search->val;
bool contains(_Key key) {
struct hashlistnode<_Key,_Val> *search = table[(((_KeyInt)key) & mask)>>_Shift];
-
+
while(search!=NULL) {
if (search->key==key) {
return true;
}
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;
bin = next;
}
}
-
+
free(oldtable); //Free the memory of the old hash table
}
-
+
private:
struct hashlistnode<_Key,_Val> **table;
unsigned int capacity;
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();
/** @file model.h
- * @brief Core model checker.
+ * @brief Core model checker.
*/
#ifndef __MODEL_H__
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");
exit(EXIT_FAILURE);
}
}
- ptr = mallocp(size);
+ ptr = mallocp(size);
return ptr;
#else
if( !sTheRecord ){
//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))) {
/** 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) {
int backTrackBeforeStep(int seq_index);
void snapshotStep(int seq_index);
- private:
+ private:
struct stackEntry * stack;
};
#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
}
/** 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));
#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
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 ){
projects / c11tester.git / commitdiff