From: Brian Norris <banorris@uci.edu>
Date: Tue, 16 Apr 2013 16:30:17 +0000 (-0700)
Subject: execution: convert HashTable to SnapVector
X-Git-Tag: oopsla2013~54
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=dd34ddf490dd97c2c202092c8fa44064a07f8c4f

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 17ea954..3c6d0d7 100644
--- 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 6e4fd2a..41a1bc1 100644
--- 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. */