assert bugs through common interface

- 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.

diff --git a/common.cc b/common.cc
index f4aa7ecefa023417c7eec4680e38e1c25a5cc13b..8b5c99717137d1d3f6a95b423fb6c8bf6fc2b08f 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);
        }
 }

diff --git a/datarace.cc b/datarace.cc
index ac364d79f83976196fb3ac14695bffbcb0c79433..c29213308cf2713ba3c1dd2d39c5c751bce31a2b 100644 (file)
--- a/datarace.cc
+++ b/datarace.cc
@@ -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,

diff --git a/model.cc b/model.cc
index a2a0a6d4d39f5c2eaf99caa7e9b743e0acda4ffb..417252c3f92ceb3a4bb7948612ca3592f1be49de 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;
 }