update TODO's

diff --git a/model.cc b/model.cc
index 9fc15cd894fc48062c74ac131884fbebc530a5e2..c86a6f676718d3fab6122282483786dd85589cb0 100644 (file)
--- 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 6a9391f0302467097b415bf4b129eb1b90fffaa5..e3aed76d2e756f564411796fef2e3e3e5cc990cc 100644 (file)
--- 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));