return model->get_execution_number();
}
-static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 2> * hash, void * ptr)
+static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> * hash, void * ptr)
{
- action_list_t *tmp = hash->get(ptr);
+ SnapVector<action_list_t> *tmp = hash->get(ptr);
if (tmp == NULL) {
- tmp = new action_list_t();
+ tmp = new SnapVector<action_list_t>();
hash->put(ptr, tmp);
}
return tmp;
}
-static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> * hash, void * ptr)
+static simple_action_list_t * get_safe_ptr_action(HashTable<const void *, simple_action_list_t *, uintptr_t, 2> * hash, void * ptr)
{
- SnapVector<action_list_t> *tmp = hash->get(ptr);
+ simple_action_list_t *tmp = hash->get(ptr);
if (tmp == NULL) {
- tmp = new SnapVector<action_list_t>();
+ tmp = new simple_action_list_t();
+ hash->put(ptr, tmp);
+ }
+ return tmp;
+}
+
+static SnapVector<simple_action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<simple_action_list_t> *, uintptr_t, 2> * hash, void * ptr)
+{
+ SnapVector<simple_action_list_t> *tmp = hash->get(ptr);
+ if (tmp == NULL) {
+ tmp = new SnapVector<simple_action_list_t>();
hash->put(ptr, tmp);
}
return tmp;
//TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
//if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
// assert_bug("Lock access before initialization");
+
+ // TODO: lock count for recursive mutexes
state->locked = get_thread(curr);
ModelAction *unlock = get_last_unlock(curr);
//synchronize with the previous unlock statement
/* unlock the lock - after checking who was waiting on it */
state->locked = NULL;
- /* disable this thread */
- get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->addAction(curr);
+ /* remove old wait action and disable this thread */
+ simple_action_list_t * waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
+ for (sllnode<ModelAction *> * it = waiters->begin(); it != NULL; it = it->getNext()) {
+ ModelAction * wait = it->getVal();
+ if (wait->get_tid() == curr->get_tid()) {
+ waiters->erase(it);
+ break;
+ }
+ }
+
+ waiters->push_back(curr);
scheduler->sleep(get_thread(curr));
}
//FAILS AND IN THE CASE IT DOESN'T... TIMED WAITS
//MUST EVENMTUALLY RELEASE...
+ // TODO: lock count for recursive mutexes
/* wake up the other threads */
for (unsigned int i = 0;i < get_num_threads();i++) {
Thread *t = get_thread(int_to_id(i));
break;
}
case ATOMIC_NOTIFY_ALL: {
- action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
+ simple_action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
//activate all the waiting threads
for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
scheduler->wake(get_thread(rit->getVal()));
break;
}
case ATOMIC_NOTIFY_ONE: {
- action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
+ simple_action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
if (waiters->size() != 0) {
Thread * thread = fuzzer->selectNotify(waiters);
scheduler->wake(thread);
if (curr->is_lock()) {
cdsc::mutex *lock = curr->get_mutex();
struct cdsc::mutex_state *state = lock->get_state();
- if (state->locked)
+ if (state->locked) {
+ Thread *lock_owner = (Thread *)state->locked;
+ Thread *curr_thread = get_thread(curr);
+ if (lock_owner == curr_thread && state->type == PTHREAD_MUTEX_RECURSIVE) {
+ return true;
+ }
+
return false;
+ }
} else if (curr->is_thread_join()) {
Thread *blocking = curr->get_thread_operand();
if (!blocking->is_complete()) {
{
int tid = id_to_int(act->get_tid());
if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
- action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
- list->addAction(act);
+ simple_action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
+ act->setActionRef(list->add_back(act));
}
// Update action trace, a total order of all actions
if (act->is_wait()) {
void *mutex_loc = (void *) act->get_value();
- get_safe_ptr_action(&obj_map, mutex_loc)->addAction(act);
+ act->setActionRef(get_safe_ptr_action(&obj_map, mutex_loc)->add_back(act));
}
}
void ModelExecution::add_write_to_lists(ModelAction *write) {
- SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
+ SnapVector<simple_action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
int tid = id_to_int(write->get_tid());
if (tid >= (int)vec->size()) {
uint oldsize =vec->size();
vec->resize(priv->next_thread_id);
for(uint i=oldsize;i<priv->next_thread_id;i++)
- new (&(*vec)[i]) action_list_t();
-
- fixup_action_list(vec);
+ new (&(*vec)[i]) simple_action_list_t();
}
- (*vec)[tid].addAction(write);
+ write->setActionRef((*vec)[tid].add_back(write));
}
/**
ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
{
/* All fences should have location FENCE_LOCATION */
- action_list_t *list = obj_map.get(FENCE_LOCATION);
+ simple_action_list_t *list = obj_map.get(FENCE_LOCATION);
if (!list)
return NULL;
{
void *location = curr->get_location();
- action_list_t *list = obj_map.get(location);
+ simple_action_list_t *list = obj_map.get(location);
if (list == NULL)
return NULL;
*/
SnapVector<ModelAction *> * ModelExecution::build_may_read_from(ModelAction *curr)
{
- SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
+ SnapVector<simple_action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
unsigned int i;
ASSERT(curr->is_read());
if (thrd_lists != NULL)
for (i = 0;i < thrd_lists->size();i++) {
/* Iterate over actions in thread, starting from most recent */
- action_list_t *list = &(*thrd_lists)[i];
+ simple_action_list_t *list = &(*thrd_lists)[i];
sllnode<ModelAction *> * rit;
for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
ModelAction *act = rit->getVal();
(*vec)[act->get_tid()].removeAction(act);
}
if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
- action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
- list->removeAction(act);
+ sllnode<ModelAction *> * listref = act->getActionRef();
+ if (listref != NULL) {
+ simple_action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
+ list->erase(listref);
+ }
} else if (act->is_wait()) {
- void *mutex_loc = (void *) act->get_value();
- get_safe_ptr_action(&obj_map, mutex_loc)->removeAction(act);
+ sllnode<ModelAction *> * listref = act->getActionRef();
+ if (listref != NULL) {
+ void *mutex_loc = (void *) act->get_value();
+ get_safe_ptr_action(&obj_map, mutex_loc)->erase(listref);
+ }
} else if (act->is_free()) {
- SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
- (*vec)[act->get_tid()].removeAction(act);
+ sllnode<ModelAction *> * listref = act->getActionRef();
+ if (listref != NULL) {
+ SnapVector<simple_action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
+ (*vec)[act->get_tid()].erase(listref);
+ }
//Clear it from last_sc_map
if (obj_last_sc_map.get(act->get_location()) == act) {