model: temporary fix for uninitialized loads
authorBrian Norris <banorris@uci.edu>
Fri, 16 Nov 2012 01:51:43 +0000 (17:51 -0800)
committerBrian Norris <banorris@uci.edu>
Fri, 16 Nov 2012 01:51:43 +0000 (17:51 -0800)
This patch does two things:

(1) Convert 'set_assert()' to 'assert_bug()' to provide:
    - More unified bug printing
    - Only printing the bug for a feasible prefix
(2) Avoids the work_queue loop if a bug was asserted

Part (1) mostly provides some cosmetic fixes.
Part (2) prevents an ASSERT() from being thrown in future values, since
we don't abort the trace early enough when there's nothing to read from.

This all needs better treatment of uninitialized loads, as there are
some loose ends.

model.cc

index 417252c..3b83b56 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1037,7 +1037,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
 
        /* Initialize work_queue with the "current action" work */
        work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
-       while (!work_queue.empty()) {
+       while (!work_queue.empty() && !has_asserted()) {
                WorkQueueEntry work = work_queue.front();
                work_queue.pop_front();
 
@@ -2179,11 +2179,8 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                }
        }
 
-       if (!initialized) {
-               /** @todo Need a more informative way of reporting errors. */
-               printf("ERROR: may read from uninitialized atomic\n");
-               set_assert();
-       }
+       if (!initialized)
+               assert_bug("May read from uninitialized atomic");
 
        if (DBG_ENABLED() || !initialized) {
                printf("Reached read action:\n");