+ - Add an intricated way to verify the access to non-reentrant data structures
+ It requires code annotation, as shown in examples/sthread/stdobject/stdobject.cpp
+
+Model checking:
+ - Synchronize the MBI tests with upstream.
+ - Show the full actor bactraces when replaying a MC trace (with model-check/replay)
+ and the status of all actors on deadlocks in MC mode.