From: Brian Norris <banorris@uci.edu>
Date: Wed, 1 Aug 2012 00:13:30 +0000 (-0700)
Subject: update TODO's
X-Git-Tag: pldi2013~331
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=a02d0bed3bc5ab757c3ed30a9589c53b05919688;p=model-checker.git

update TODO's
---

diff --git a/model.cc b/model.cc
index 9fc15cd..c86a6f6 100644
--- a/model.cc
+++ b/model.cc
@@ -304,8 +304,6 @@ void ModelChecker::check_current_action(void)
 	set_backtracking(curr);
 
 	/* Assign reads_from values */
-	/* TODO: perform release/acquire synchronization here; include
-	 * reads_from as ModelAction member? */
 	Thread *th = get_thread(curr->get_tid());
 	uint64_t value = VALUE_NONE;
 	if (curr->is_read()) {
diff --git a/threads.cc b/threads.cc
index 6a9391f..e3aed76 100644
--- a/threads.cc
+++ b/threads.cc
@@ -31,6 +31,9 @@ Thread * thread_current(void)
 void thread_startup() {
 	Thread * curr_thread = thread_current();
 
+	/* TODO -- we should make this event always immediately follow the
+		 CREATE event, so we don't get redundant traces...  */
+
 	/* Add dummy "start" action, just to create a first clock vector */
 	model->switch_to_master(new ModelAction(THREAD_START, memory_order_seq_cst, curr_thread));