/** Initializes a CycleGraph object. */
CycleGraph::CycleGraph() :
+ discovered(new HashTable<CycleNode *, CycleNode *, uintptr_t, 4, model_malloc, model_calloc, model_free>(16)),
hasCycles(false),
oldCycles(false),
hasRMWViolation(false),
*/
bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) {
std::vector<CycleNode *, ModelAlloc<CycleNode *> > queue;
- HashTable<CycleNode *, CycleNode *, uintptr_t, 4, model_malloc, model_calloc, model_free> discovered(64);
+ discovered->reset();
queue.push_back(from);
- discovered.put(from, from);
+ discovered->put(from, from);
while(!queue.empty()) {
CycleNode * node=queue.back();
queue.pop_back();
for(unsigned int i=0;i<node->getEdges()->size();i++) {
CycleNode *next=(*node->getEdges())[i];
- if (!discovered.contains(next)) {
- discovered.put(next,next);
+ if (!discovered->contains(next)) {
+ discovered->put(next,next);
queue.push_back(next);
}
}
bool CycleGraph::checkPromise(const ModelAction *fromact, Promise *promise) {
std::vector<CycleNode *, ModelAlloc<CycleNode *> > queue;
- HashTable<CycleNode *, CycleNode *, uintptr_t, 4, model_malloc, model_calloc, model_free> discovered(64);
+ discovered->reset();
CycleNode *from = actionToNode.get(fromact);
queue.push_back(from);
- discovered.put(from, from);
+ discovered->put(from, from);
while(!queue.empty()) {
CycleNode * node=queue.back();
queue.pop_back();
for(unsigned int i=0;i<node->getEdges()->size();i++) {
CycleNode *next=(*node->getEdges())[i];
- if (!discovered.contains(next)) {
- discovered.put(next,next);
+ if (!discovered->contains(next)) {
+ discovered->put(next,next);
queue.push_back(next);
}
}
SNAPSHOTALLOC
private:
CycleNode * getNode(const ModelAction *);
+ HashTable<CycleNode *, CycleNode *, uintptr_t, 4, model_malloc, model_calloc, model_free> * discovered;
/** @brief A table for mapping ModelActions to CycleNodes */
HashTable<const ModelAction *, CycleNode *, uintptr_t, 4> actionToNode;
* @tparam _free Provide your own 'free' for the table, or default to
* snapshotting.
*/
-template<typename _Key, typename _Val, void * (* _malloc)(size_t), void * (* _calloc)(size_t, size_t), void (*_free)(void *)>
+template<typename _Key, typename _Val>
+
struct hashlistnode {
_Key key;
_Val val;
- struct hashlistnode<_Key,_Val, _malloc, _calloc, _free> *next;
-
- void * operator new(size_t size) {
- return _malloc(size);
- }
-
- void operator delete(void *p, size_t size) {
- _free(p);
- }
-
- void * operator new[](size_t size) {
- return _malloc(size);
- }
-
- void operator delete[](void *p, size_t size) {
- _free(p);
- }
};
/**
*/
HashTable(unsigned int initialcapacity=1024, double factor=0.5) {
// Allocate space for the hash table
- table = (struct hashlistnode<_Key,_Val, _malloc, _calloc,_free> **) _calloc(initialcapacity, sizeof(struct hashlistnode<_Key,_Val, _malloc, _calloc, _free> *));
+ table = (struct hashlistnode<_Key,_Val> *) _calloc(initialcapacity, sizeof(struct hashlistnode<_Key,_Val>));
loadfactor = factor;
capacity = initialcapacity;
+ capacitymask = initialcapacity - 1;
+
threshold = (unsigned int) (initialcapacity*loadfactor);
- mask = (capacity << _Shift)-1;
size = 0; // Initial number of elements in the hash
}
/** Destructor */
~HashTable() {
- for(unsigned int i=0;i<capacity;i++) {
- struct hashlistnode<_Key,_Val, _malloc, _calloc, _free> * bin = table[i];
- while(bin!=NULL) {
- struct hashlistnode<_Key,_Val, _malloc, _calloc, _free> * next=bin->next;
- delete bin;
- bin=next;
- }
- }
_free(table);
}
/** Reset the table to its initial state. */
void reset() {
- for(unsigned int i=0;i<capacity;i++) {
- struct hashlistnode<_Key,_Val, _malloc, _calloc, _free> * bin = table[i];
- while(bin!=NULL) {
- struct hashlistnode<_Key,_Val, _malloc, _calloc, _free> * next=bin->next;
- delete bin;
- bin=next;
- }
- }
- memset(table, 0, capacity*sizeof(struct hashlistnode<_Key, _Val, _malloc, _calloc, _free> *));
+ memset(table, 0, capacity*sizeof(struct hashlistnode<_Key, _Val>));
size=0;
}
if (size > threshold)
resize(capacity << 1);
- struct hashlistnode<_Key,_Val, _malloc, _calloc, _free> *ptr = table[(((_KeyInt)key) & mask)>>_Shift];
- struct hashlistnode<_Key,_Val, _malloc, _calloc, _free> *search = ptr;
+ struct hashlistnode<_Key,_Val> *search;
- while(search!=NULL) {
+ unsigned int index=((_KeyInt)key)>>_Shift;
+ do {
+ index=index&capacitymask;
+ search = &table[index];
if (search->key==key) {
search->val=val;
return;
}
- search=search->next;
- }
-
- struct hashlistnode<_Key,_Val, _malloc, _calloc, _free> *newptr=(struct hashlistnode<_Key,_Val,_malloc,_calloc,_free> *)new struct hashlistnode<_Key,_Val, _malloc, _calloc, _free>;
- newptr->key=key;
- newptr->val=val;
- newptr->next=ptr;
- table[(((_KeyInt)key)&mask)>>_Shift]=newptr;
+ index++;
+ } while(search->key);
+
+ search->key=key;
+ search->val=val;
size++;
}
- /**
- * @brief Get a valid pointer to a value corresponding to a given key
- *
- * Ensure that key is present in the hash table, then return a pointer
- * to its value bin. This may require either creating a new bin for
- * this key (with a default-constructed value) or simply locating and
- * returning a pointer to an existing value.
- * @param key The key to check
- * @return A pointer to the value in the table
- */
- _Val * get_safe_ptr(_Key key) {
- if (size > threshold)
- resize(capacity << 1);
-
- struct hashlistnode<_Key,_Val, _malloc, _calloc, _free> *ptr = table[(((_KeyInt)key) & mask)>>_Shift];
- struct hashlistnode<_Key,_Val, _malloc, _calloc, _free> *search = ptr;
-
- while(search!=NULL) {
- if (search->key==key) {
- return &search->val;
- }
- search=search->next;
- }
-
- struct hashlistnode<_Key,_Val, _malloc, _calloc, _free> *newptr=(struct hashlistnode<_Key,_Val, _malloc, _calloc, _free> *)new struct hashlistnode<_Key,_Val, _malloc, _calloc, _free>;
- newptr->key=key;
- newptr->next=ptr;
- table[(((_KeyInt)key)&mask)>>_Shift]=newptr;
- size++;
- return &newptr->val;
- }
-
/** Lookup the corresponding value for the given key. */
_Val get(_Key key) {
- struct hashlistnode<_Key,_Val, _malloc, _calloc, _free> *search = table[(((_KeyInt)key) & mask)>>_Shift];
+ struct hashlistnode<_Key,_Val> *search;
- while(search!=NULL) {
+ unsigned int index=((_KeyInt)key)>>_Shift;
+ do {
+ index=index&capacitymask;
+ search = &table[index];
if (search->key==key) {
return search->val;
}
- search=search->next;
- }
- return (_Val)0;
- }
-
- /** Lookup the corresponding value for the given key. */
- _Val * getptr(_Key key) {
- struct hashlistnode<_Key,_Val, _malloc, _calloc, _free> *search = table[(((_KeyInt)key) & mask)>>_Shift];
-
- while(search!=NULL) {
- if (search->key==key) {
- return & search->val;
- }
- search=search->next;
- }
- return (_Val *) NULL;
+ index++;
+ } while(search->key);
+ return (_Val) 0;
}
/** Check whether the table contains a value for the given key. */
bool contains(_Key key) {
- struct hashlistnode<_Key,_Val, _malloc, _calloc, _free> *search = table[(((_KeyInt)key) & mask)>>_Shift];
+ struct hashlistnode<_Key,_Val> *search;
- while(search!=NULL) {
+ unsigned int index=((_KeyInt)key)>>_Shift;
+ do {
+ index=index&capacitymask;
+ search = &table[index];
if (search->key==key) {
return true;
}
- search=search->next;
- }
+ index++;
+ } while(search->key);
return false;
}
/** Resize the table. */
void resize(unsigned int newsize) {
- struct hashlistnode<_Key,_Val, _malloc, _calloc, _free> ** oldtable = table;
- struct hashlistnode<_Key,_Val, _malloc, _calloc, _free> ** newtable;
+ struct hashlistnode<_Key,_Val> * oldtable = table;
+ struct hashlistnode<_Key,_Val> * newtable;
unsigned int oldcapacity = capacity;
- if((newtable = (struct hashlistnode<_Key,_Val, _malloc, _calloc, _free> **) _calloc(newsize, sizeof(struct hashlistnode<_Key,_Val, _malloc, _calloc, _free> *))) == NULL) {
+ 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;
+ capacitymask = newsize - 1;
- for(unsigned int i = 0; i < oldcapacity; i++) {
- struct hashlistnode<_Key, _Val, _malloc, _calloc, _free> * bin = oldtable[i];
-
- while(bin!=NULL) {
- _Key key=bin->key;
- struct hashlistnode<_Key, _Val, _malloc, _calloc, _free> * next=bin->next;
+ threshold = (unsigned int) (newsize * loadfactor);
- unsigned int index = (((_KeyInt)key) & mask) >>_Shift;
- struct hashlistnode<_Key, _Val, _malloc, _calloc, _free> * tmp=newtable[index];
- bin->next=tmp;
- newtable[index]=bin;
- bin = next;
- }
+ struct hashlistnode<_Key, _Val> * bin = &oldtable[0];
+ struct hashlistnode<_Key, _Val> * lastbin = &oldtable[oldcapacity];
+ for(; bin < lastbin; bin++) {
+ _Key key=bin->key;
+
+ struct hashlistnode<_Key,_Val> *search;
+
+ unsigned int index=((_KeyInt)key)>>_Shift;
+ do {
+ index=index&capacitymask;
+ search = &table[index];
+ index++;
+ } while(search->key);
+
+ search->key=key;
+ search->val=bin->val;
}
_free(oldtable); //Free the memory of the old hash table
}
private:
- struct hashlistnode<_Key,_Val, _malloc, _calloc, _free> **table;
+ struct hashlistnode<_Key,_Val> *table;
unsigned int capacity;
- _KeyInt mask;
unsigned int size;
+ unsigned int capacitymask;
unsigned int threshold;
double loadfactor;
};
earliest_diverge(NULL),
action_trace(new action_list_t()),
thread_map(new HashTable<int, Thread *, int>()),
- obj_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
- lock_waiters_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
- condvar_waiters_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
- obj_thrd_map(new HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 >()),
+ obj_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
+ lock_waiters_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
+ condvar_waiters_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
+ obj_thrd_map(new HashTable<void *, std::vector<action_list_t> *, uintptr_t, 4 >()),
promises(new std::vector< Promise *, SnapshotAlloc<Promise *> >()),
futurevalues(new std::vector< struct PendingFutureValue, SnapshotAlloc<struct PendingFutureValue> >()),
pending_rel_seqs(new std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >()),
delete mo_graph;
}
+static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr) {
+ action_list_t * tmp=hash->get(ptr);
+ if (tmp==NULL) {
+ tmp=new action_list_t();
+ hash->put(ptr, tmp);
+ }
+ return tmp;
+}
+
+static std::vector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, std::vector<action_list_t> *, uintptr_t, 4> * hash, void * ptr) {
+ std::vector<action_list_t> * tmp=hash->get(ptr);
+ if (tmp==NULL) {
+ tmp=new std::vector<action_list_t>();
+ hash->put(ptr, tmp);
+ }
+ return tmp;
+}
+
/**
* Restores user program to initial state and resets all model-checker data
* structures.
case ATOMIC_WRITE:
case ATOMIC_RMW: {
/* linear search: from most recent to oldest */
- action_list_t *list = obj_map->get_safe_ptr(act->get_location());
+ action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
case ATOMIC_LOCK:
case ATOMIC_TRYLOCK: {
/* linear search: from most recent to oldest */
- action_list_t *list = obj_map->get_safe_ptr(act->get_location());
+ action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
}
case ATOMIC_UNLOCK: {
/* linear search: from most recent to oldest */
- action_list_t *list = obj_map->get_safe_ptr(act->get_location());
+ action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
}
case ATOMIC_WAIT: {
/* linear search: from most recent to oldest */
- action_list_t *list = obj_map->get_safe_ptr(act->get_location());
+ action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
case ATOMIC_NOTIFY_ALL:
case ATOMIC_NOTIFY_ONE: {
/* linear search: from most recent to oldest */
- action_list_t *list = obj_map->get_safe_ptr(act->get_location());
+ action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
//unlock the lock
state->islocked = false;
//wake up the other threads
- action_list_t *waiters = lock_waiters_map->get_safe_ptr(curr->get_location());
+ action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, curr->get_location());
//activate all the waiting threads
for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
scheduler->wake(get_thread(*rit));
//unlock the lock
state->islocked = false;
//wake up the other threads
- action_list_t *waiters = lock_waiters_map->get_safe_ptr((void *) curr->get_value());
+ action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, (void *) curr->get_value());
//activate all the waiting threads
for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
scheduler->wake(get_thread(*rit));
waiters->clear();
//check whether we should go to sleep or not...simulate spurious failures
if (curr->get_node()->get_misc()==0) {
- condvar_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr);
+ get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr);
//disable us
scheduler->sleep(get_current_thread());
}
break;
}
case ATOMIC_NOTIFY_ALL: {
- action_list_t *waiters = condvar_waiters_map->get_safe_ptr(curr->get_location());
+ action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
//activate all the waiting threads
for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
scheduler->wake(get_thread(*rit));
break;
}
case ATOMIC_NOTIFY_ONE: {
- action_list_t *waiters = condvar_waiters_map->get_safe_ptr(curr->get_location());
+ action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
int wakeupthread=curr->get_node()->get_misc();
action_list_t::iterator it = waiters->begin();
advance(it, wakeupthread);
else if (newcurr->is_wait())
newcurr->get_node()->set_misc_max(2);
else if (newcurr->is_notify_one()) {
- newcurr->get_node()->set_misc_max(condvar_waiters_map->get_safe_ptr(newcurr->get_location())->size());
+ newcurr->get_node()->set_misc_max(get_safe_ptr_action(condvar_waiters_map, newcurr->get_location())->size());
}
return true; /* This was a new ModelAction */
}
struct std::mutex_state * state = lock->get_state();
if (state->islocked) {
//Stick the action in the appropriate waiting queue
- lock_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr);
+ get_safe_ptr_action(lock_waiters_map, curr->get_location())->push_back(curr);
return false;
}
} else if (curr->get_type() == THREAD_JOIN) {
//accidentally clear by rolling back
if (!isfeasible())
return;
- std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
+ std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
int tid = id_to_int(curr->get_tid());
/* Skip checks */
*/
bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf)
{
- std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
+ std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
unsigned int i;
bool added = false;
ASSERT(curr->is_read());
*/
void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf)
{
- std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
+ std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
unsigned int i;
ASSERT(curr->is_read());
*/
bool ModelChecker::w_modification_order(ModelAction *curr)
{
- std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
+ std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
unsigned int i;
bool added = false;
ASSERT(curr->is_write());
*/
bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
{
- std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location());
+ std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, reader->get_location());
unsigned int i;
/* Iterate over all threads */
for (i = 0; i < thrd_lists->size(); i++) {
/* else relaxed write; check modification order for contiguous subsequence
* -> rf must be same thread as release */
int tid = id_to_int(rf->get_tid());
- std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(rf->get_location());
+ std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, rf->get_location());
action_list_t *list = &(*thrd_lists)[tid];
action_list_t::const_reverse_iterator rit;
int tid = id_to_int(act->get_tid());
action_trace->push_back(act);
- obj_map->get_safe_ptr(act->get_location())->push_back(act);
+ get_safe_ptr_action(obj_map, act->get_location())->push_back(act);
- std::vector<action_list_t> *vec = obj_thrd_map->get_safe_ptr(act->get_location());
+ std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, act->get_location());
if (tid >= (int)vec->size())
vec->resize(priv->next_thread_id);
(*vec)[tid].push_back(act);
if (act->is_wait()) {
void *mutex_loc=(void *) act->get_value();
- obj_map->get_safe_ptr(mutex_loc)->push_back(act);
+ get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
- std::vector<action_list_t> *vec = obj_thrd_map->get_safe_ptr(mutex_loc);
+ std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, mutex_loc);
if (tid >= (int)vec->size())
vec->resize(priv->next_thread_id);
(*vec)[tid].push_back(act);
ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) const
{
void *location = curr->get_location();
- action_list_t *list = obj_map->get_safe_ptr(location);
+ action_list_t *list = get_safe_ptr_action(obj_map, 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++)
ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const
{
void *location = curr->get_location();
- action_list_t *list = obj_map->get_safe_ptr(location);
+ action_list_t *list = get_safe_ptr_action(obj_map, location);
/* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++)
*/
void ModelChecker::build_reads_from_past(ModelAction *curr)
{
- std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
+ std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
unsigned int i;
ASSERT(curr->is_read());
/** Per-object list of actions. Maps an object (i.e., memory location)
* to a trace of all actions performed on the object. */
- HashTable<const void *, action_list_t, uintptr_t, 4> *obj_map;
+ HashTable<const void *, action_list_t *, uintptr_t, 4> *obj_map;
/** Per-object list of actions. Maps an object (i.e., memory location)
* to a trace of all actions performed on the object. */
- HashTable<const void *, action_list_t, uintptr_t, 4> *lock_waiters_map;
+ HashTable<const void *, action_list_t *, uintptr_t, 4> *lock_waiters_map;
/** Per-object list of actions. Maps an object (i.e., memory location)
* to a trace of all actions performed on the object. */
- HashTable<const void *, action_list_t, uintptr_t, 4> *condvar_waiters_map;
+ HashTable<const void *, action_list_t *, uintptr_t, 4> *condvar_waiters_map;
- HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 > *obj_thrd_map;
+ HashTable<void *, std::vector<action_list_t> *, uintptr_t, 4 > *obj_thrd_map;
std::vector< Promise *, SnapshotAlloc<Promise *> > *promises;
std::vector< struct PendingFutureValue, SnapshotAlloc<struct PendingFutureValue> > *futurevalues;
projects / model-checker.git / commitdiff