execution: convert HashTable to SnapVector

We don't actually need a hash table for threads, since we allocate their
indeces contiguously, at least for now. Also, HashTable is really
designed for pointer-based keys and may not accept a 0-valued key. To
avoid these problems, just switch to a snapshotted vector.

diff --git a/execution.cc b/execution.cc
index 17ea954a65570160ffccd1a42f247c95956b8fa2..3c6d0d7588dc2ff33984a94577b34de37bfdac2f 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -65,7 +65,7 @@ ModelExecution::ModelExecution(ModelChecker *m,
        params(params),
        scheduler(scheduler),
        action_trace(),
-       thread_map(),
+       thread_map(2), /* We'll always need at least 2 threads */
        obj_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
        condvar_waiters_map(),
        obj_thrd_map(),
@@ -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,7 +88,7 @@ ModelExecution::ModelExecution(ModelChecker *m,
 ModelExecution::~ModelExecution()
 {
        for (unsigned int i = 0; i < get_num_threads(); i++)
-               delete thread_map.get(i);
+               delete get_thread(int_to_id(i));
 
        delete obj_map;
 
@@ -2675,7 +2675,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);
 }
@@ -2687,7 +2690,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;
 }
 
 /**

diff --git a/execution.h b/execution.h
index 6e4fd2ab900988df3d40e1b06be6c8f38d8df3f7..41a1bc1479ceb8f9d12a2ebb81fb6bacf925d6a6 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -186,7 +186,7 @@ private:
        ModelAction * get_uninitialized_action(const ModelAction *curr) const;
 
        action_list_t action_trace;
-       HashTable<int, Thread *, int> thread_map;
+       SnapVector<Thread *> thread_map;
 
        /** Per-object list of actions. Maps an object (i.e., memory location)
         * to a trace of all actions performed on the object. */