action: add NULL dereference assertion

In user programs, we might find a NULL atomic object being dereferenced,
causing strange model-checker behavior which will track memory address 0
as an atomic object. This may result in apparently-uninitialized
variables, for instance.

So, just nip these in the bud with an assertion. Perhaps these things
can transformed into some more informative type of warning in the
future, where user-visible bugs might print helpful messages.

diff --git a/action.cc b/action.cc
index 1a819eaf5584f1e97e88fca439104392c07b7f1b..ca1285612b00c75fd7294bee5af80d3aa52a3468 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -36,6 +36,9 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
        cv(NULL),
        sleep_flag(false)
 {
+       /* References to NULL atomic variables can end up here */
+       ASSERT(loc || type == MODEL_FIXUP_RELSEQ);
+
        Thread *t = thread ? thread : thread_current();
        this->tid = t->get_id();
 }