promise: add max_available_thread_idx() interface

[model-checker.git] / execution.cc

diff --git a/execution.cc b/execution.cc
index 74fa43ef90f26861455a196d53fec6c3b4b6bf14..66418a4abb630a5b234b035342f4179435c52363 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -64,9 +64,9 @@ ModelExecution::ModelExecution(ModelChecker *m,
        model(m),
        params(params),
        scheduler(scheduler),
-       action_trace(new action_list_t()),
-       thread_map(),
-       obj_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
+       action_trace(),
+       thread_map(2), /* We'll always need at least 2 threads */
+       obj_map(),
        condvar_waiters_map(),
        obj_thrd_map(),
        promises(),
@@ -80,7 +80,7 @@ ModelExecution::ModelExecution(ModelChecker *m,
 {
        /* Initialize a model-checker thread, for special ModelActions */
        model_thread = new Thread(get_next_id());
-       thread_map.put(id_to_int(model_thread->get_id()), model_thread);
+       add_thread(model_thread);
        scheduler->register_engine(this);
 }
 
@@ -88,10 +88,7 @@ ModelExecution::ModelExecution(ModelChecker *m,
 ModelExecution::~ModelExecution()
 {
        for (unsigned int i = 0; i < get_num_threads(); i++)
-               delete thread_map.get(i);
-
-       delete obj_map;
-       delete action_trace;
+               delete get_thread(int_to_id(i));
 
        for (unsigned int i = 0; i < promises.size(); i++)
                delete promises[i];
@@ -309,7 +306,7 @@ ModelAction * ModelExecution::get_last_fence_conflict(ModelAction *act) const
                return NULL;
 
        /* Skip past the release */
-       const action_list_t *list = action_trace;
+       const action_list_t *list = &action_trace;
        action_list_t::const_reverse_iterator rit;
        for (rit = list->rbegin(); rit != list->rend(); rit++)
                if (*rit == last_release)
@@ -375,7 +372,7 @@ ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
                ModelAction *ret = NULL;
 
                /* linear search: from most recent to oldest */
-               action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
+               action_list_t *list = obj_map.get(act->get_location());
                action_list_t::reverse_iterator rit;
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        ModelAction *prev = *rit;
@@ -397,7 +394,7 @@ ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
        case ATOMIC_LOCK:
        case ATOMIC_TRYLOCK: {
                /* linear search: from most recent to oldest */
-               action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
+               action_list_t *list = obj_map.get(act->get_location());
                action_list_t::reverse_iterator rit;
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        ModelAction *prev = *rit;
@@ -408,7 +405,7 @@ ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
        }
        case ATOMIC_UNLOCK: {
                /* linear search: from most recent to oldest */
-               action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
+               action_list_t *list = obj_map.get(act->get_location());
                action_list_t::reverse_iterator rit;
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        ModelAction *prev = *rit;
@@ -419,7 +416,7 @@ ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
        }
        case ATOMIC_WAIT: {
                /* linear search: from most recent to oldest */
-               action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
+               action_list_t *list = obj_map.get(act->get_location());
                action_list_t::reverse_iterator rit;
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        ModelAction *prev = *rit;
@@ -434,7 +431,7 @@ ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
        case ATOMIC_NOTIFY_ALL:
        case ATOMIC_NOTIFY_ONE: {
                /* linear search: from most recent to oldest */
-               action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
+               action_list_t *list = obj_map.get(act->get_location());
                action_list_t::reverse_iterator rit;
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
                        ModelAction *prev = *rit;
@@ -856,7 +853,7 @@ bool ModelExecution::process_fence(ModelAction *curr)
         */
        bool updated = false;
        if (curr->is_acquire()) {
-               action_list_t *list = action_trace;
+               action_list_t *list = &action_trace;
                action_list_t::reverse_iterator rit;
                /* Find X : is_read(X) && X --sb-> curr */
                for (rit = list->rbegin(); rit != list->rend(); rit++) {
@@ -1004,7 +1001,7 @@ void ModelExecution::process_relseq_fixup(ModelAction *curr, work_queue_t *work_
                work_queue->push_back(MOEdgeWorkEntry(acquire));
 
                /* propagate synchronization to later actions */
-               action_list_t::reverse_iterator rit = action_trace->rbegin();
+               action_list_t::reverse_iterator rit = action_trace.rbegin();
                for (; (*rit) != acquire; rit++) {
                        ModelAction *propagate = *rit;
                        if (acquire->happens_before(propagate)) {
@@ -2077,7 +2074,7 @@ bool ModelExecution::resolve_release_sequences(void *location, work_queue_t *wor
                                work_queue->push_back(MOEdgeWorkEntry(acquire));
 
                        /* propagate synchronization to later actions */
-                       action_list_t::reverse_iterator rit = action_trace->rbegin();
+                       action_list_t::reverse_iterator rit = action_trace.rbegin();
                        for (; (*rit) != acquire; rit++) {
                                ModelAction *propagate = *rit;
                                if (acquire->happens_before(propagate)) {
@@ -2113,7 +2110,7 @@ void ModelExecution::add_action_to_lists(ModelAction *act)
        int tid = id_to_int(act->get_tid());
        ModelAction *uninit = NULL;
        int uninit_id = -1;
-       action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
+       action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
        if (list->empty() && act->is_atomic_var()) {
                uninit = get_uninitialized_action(act);
                uninit_id = id_to_int(uninit->get_tid());
@@ -2121,9 +2118,9 @@ void ModelExecution::add_action_to_lists(ModelAction *act)
        }
        list->push_back(act);
 
-       action_trace->push_back(act);
+       action_trace.push_back(act);
        if (uninit)
-               action_trace->push_front(uninit);
+               action_trace.push_front(uninit);
 
        SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
        if (tid >= (int)vec->size())
@@ -2146,7 +2143,7 @@ void ModelExecution::add_action_to_lists(ModelAction *act)
 
        if (act->is_wait()) {
                void *mutex_loc = (void *) act->get_value();
-               get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
+               get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
 
                SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
                if (tid >= (int)vec->size())
@@ -2194,7 +2191,7 @@ ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
 {
        void *location = curr->get_location();
-       action_list_t *list = get_safe_ptr_action(obj_map, location);
+       action_list_t *list = obj_map.get(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) != curr; rit++)
@@ -2216,8 +2213,12 @@ ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
  */
 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
 {
-       /* All fences should have NULL location */
-       action_list_t *list = get_safe_ptr_action(obj_map, NULL);
+       /* All fences should have location FENCE_LOCATION */
+       action_list_t *list = obj_map.get(FENCE_LOCATION);
+
+       if (!list)
+               return NULL;
+
        action_list_t::reverse_iterator rit = list->rbegin();
 
        if (before_fence) {
@@ -2246,7 +2247,7 @@ ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const Mode
 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
 {
        void *location = curr->get_location();
-       action_list_t *list = get_safe_ptr_action(obj_map, location);
+       action_list_t *list = obj_map.get(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++)
@@ -2609,7 +2610,7 @@ void ModelExecution::dumpGraph(char *filename) const
        mo_graph->dumpNodes(file);
        ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
 
-       for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
+       for (action_list_t::iterator it = action_trace.begin(); it != action_trace.end(); it++) {
                ModelAction *act = *it;
                if (act->is_read()) {
                        mo_graph->dot_print_node(file, act);
@@ -2657,7 +2658,7 @@ void ModelExecution::print_summary() const
                model_print("\n");
        } else
                print_infeasibility(" INFEASIBLE");
-       print_list(action_trace);
+       print_list(&action_trace);
        model_print("\n");
        if (!promises.empty()) {
                model_print("Pending promises:\n");
@@ -2676,7 +2677,10 @@ void ModelExecution::print_summary() const
  */
 void ModelExecution::add_thread(Thread *t)
 {
-       thread_map.put(id_to_int(t->get_id()), t);
+       unsigned int i = id_to_int(t->get_id());
+       if (i >= thread_map.size())
+               thread_map.resize(i + 1);
+       thread_map[i] = t;
        if (!t->is_model_thread())
                scheduler->add_thread(t);
 }
@@ -2688,7 +2692,10 @@ void ModelExecution::add_thread(Thread *t)
  */
 Thread * ModelExecution::get_thread(thread_id_t tid) const
 {
-       return thread_map.get(id_to_int(tid));
+       unsigned int i = id_to_int(tid);
+       if (i < thread_map.size())
+               return thread_map[i];
+       return NULL;
 }
 
 /**