assert bugs through common interface
authorBrian Norris <banorris@uci.edu>
Thu, 15 Nov 2012 21:50:40 +0000 (13:50 -0800)
committerBrian Norris <banorris@uci.edu>
Fri, 16 Nov 2012 01:38:55 +0000 (17:38 -0800)
- User-provied assertions (MODEL_ASSERT())
- Data races
- Deadlocks
- Unlock before lock

Notably, I have not yet converted the "uninitialized load" bug, because
it actually isn't correct yet. It needs to handle future values and lazy
synchronization better.

common.cc
datarace.cc
model.cc

index f4aa7ec..8b5c997 100644 (file)
--- a/common.cc
+++ b/common.cc
@@ -46,9 +46,9 @@ void assert_hook(void)
 void model_assert(bool expr, const char *file, int line)
 {
        if (!expr) {
-               printf("  [BUG] Program has hit assertion in file %s at line %d\n",
+               char msg[100];
+               sprintf(msg, "Program has hit assertion in file %s at line %d\n",
                                file, line);
-               model->set_assert();
-               model->switch_to_master(NULL);
+               model->assert_bug(msg, true);
        }
 }
index ac364d7..c292133 100644 (file)
@@ -102,10 +102,8 @@ static void reportDataRace(thread_id_t oldthread, modelclock_t oldclock, bool is
        unrealizedraces.push_back(race);
 
        /* If the race is realized, bail out now. */
-       if (checkDataRaces()) {
-               model->set_assert();
-               model->switch_to_master(NULL);
-       }
+       if (checkDataRaces())
+               model->assert_bug("Datarace", true);
 }
 
 /** This function goes through the list of unrealized data races,
index a2a0a6d..417252c 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -417,7 +417,7 @@ bool ModelChecker::next_execution()
                num_feasible_executions++;
 
                if (is_deadlocked())
-                       assert_bug("Deadlock detected", false);
+                       assert_bug("Deadlock detected");
 
                print_bugs();
                checkDataRaces();
@@ -677,10 +677,8 @@ bool ModelChecker::process_mutex(ModelAction *curr) {
        }
                //otherwise fall into the lock case
        case ATOMIC_LOCK: {
-               if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock) {
-                       printf("Lock access before initialization\n");
-                       set_assert();
-               }
+               if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
+                       assert_bug("Lock access before initialization");
                state->islocked = true;
                ModelAction *unlock = get_last_unlock(curr);
                //synchronize with the previous unlock statement
@@ -890,7 +888,7 @@ void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_qu
 
        /* See if we have realized a data race */
        if (checkDataRaces())
-               set_assert();
+               assert_bug("Datarace");
 }
 
 /**
@@ -1821,9 +1819,8 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
        }
 
        // If we resolved promises or data races, see if we have realized a data race.
-       if (checkDataRaces()) {
-               set_assert();
-       }
+       if (checkDataRaces())
+               assert_bug("Datarace");
 
        return updated;
 }