(lib/model) fix: exit step early before initialisation

Check `is_initialised` early, before trying to acquire any locks.
This means that if we take casemate steps before pgtables are enabled,
we keep going and do not try perform any atomic operations later on
(namely the Casemate internal locks).

Author: bensimner

src/lib/include/casemate-impl/sync.h

@@ -5,4 +5,10 @@ void init_sm_lock(void);
 void lock_sm(void);
 void unlock_sm(void);
 
+#define LOAD_RLX(L) \
+  *((volatile typeof(L)*)&L)
+
+#define STORE_RLX(L, V) \
+  *((volatile typeof(L)*)(&L)) = V
+
 #endif /* CASEMATE_SYNC_H */

src/lib/src/model.c

@@ -1711,9 +1711,6 @@ void step(struct casemate_model_step trans)
 	touched_watchpoint = false;
 	traced_current_trans = false;
 
-	if (!is_initialised)
-		goto out;
-
 	if (!opts()->enable_checking)
 		goto out;
 
@@ -1757,6 +1754,9 @@ void step(struct casemate_model_step trans)
 
 void casemate_model_step(struct casemate_model_step trans)
 {
+	if (!LOAD_RLX(is_initialised))
+		return;
+
 	lock_sm();
 	step(trans);
 	unlock_sm();

src/lib/src/utilities/blobs.c

@@ -12,7 +12,7 @@ void initialise_ghost_ptes_memory(phys_addr_t phys, u64 size) {
 		the_ghost_state->memory.blobs_backing[i].valid = false;
 		the_ghost_state->memory.ordered_blob_list[i] = 0xDEADDEADDEADDEAD;
 	}
-	is_initialised = true;
+	STORE_RLX(is_initialised, true);
 	GHOST_LOG_CONTEXT_EXIT();
 }