Why is my test with loom failing

1

hi, I am trying to test a lock with loom but the test fails with:
Error: Model exceeded maximum number of branches. This is often caused by an algorithm requiring the processor to make progress, e.g. spin locks.

#[test]
#[cfg(feature = "loom")]
fn test_lock() {
    loom::model(|| {
        let lock: &'static _ = Box::leak(Box::new(Lock::new(0)));
        let mut handles = Vec::<JoinHandle<_>>::new();

        let handle = spawn(|| {
            let _read = lock.read();
        });
        handles.push(handle);

        let handle = spawn(|| {
            let mut write = lock.write();
            *write += 1;
        });
        handles.push(handle);

        for handle in handles {
            handle.join().unwrap();
        }

        assert_eq!(*lock.read(), 1);
    });
}

I have to give both of the threads some time to run so I joined them at the very end...
at first I was trying to spawn many threads but the test failed with cannot spawn too many threads....
what's a good way to test this...?

2

loom is a model checker, not a fuzzer.

you only need enough concurrency to cover the value space of all possible race conditions (not data races). how many is enough? it depends on what you are implementing, but you rarely need more than 2 threads.

for example, for a mutual exclusive lock (a.k.a. mutex), 2 threads is usually enough. for rw-lock, you may want to test read/read, read/write, write/write contentions, but you don't have to check them in a single run, you can use smaller test cases for each case, so 2 threads for each should be enough.

3

oh, I see. I think I understand it now after you have explained it. Could you please elaborate the error a bit which I've got. Thanks!
what branches are we talking about here?

4

the model checker works like this (over-simplfied description):

  • you replace (guarded via conditional compilation flags) the synchronization primitives by the loom mockups
  • when you run the model, the mock types are essentially "hooks" of the runtime (the model checker)
  • the checker first records a (serialized) trace of events during the run using these hooks, then it systematically permutate the events to explore alternative execution paths
  • the model is run again with a different interleaving of previous traces
  • this process is repeated until all possible permutations are explored, or a maximum limit of iterations is reached
  • for example, suppose in one run, an atomic read in thread 1 is followed by an atomic write in thread 2, and these two events is not ordered by other constraints, so it will store some scheduling information in the mockup atomic, and in the next run, when the mocked AtomicI32::load() is executed, the events will happen in the determined order. essentially, this scheudling/instrumentation information is a "branch".

due to the nature of dynamic model checker, it cannot cull the state space as efficiently as a static analyzer, the state space can explode drastically, even if the model just grows slightly bigger. so it's best to keep your loom test cases lean and simple.

5

Mentioning just in case you didn't see (hard to tell from the snippet provided): loom tests require using the loom synchronization types

6

yeah, I am using loom types. Thank you!

7

I see. thank you for explaining this! Is there any resource for it that explains this stuff in depth?

also, all of my tests cases for read/write, read/read and write/write passed after I added hint::spin_loop in my read and write functions. Did loom expected me to add this from the very beginning? In the docs it is also mentioned that the loom model checker isn't fair by design, so probably calling spin_loop adds some fairness, am I right?

8

this is the paper that loom's readme file linked:

http://plrg.eecs.uci.edu/publications/toplas16.pdf

there are plenty of resources on model checkers on the internet, you can search yourself, but I happen to know this page as well:

yes.

no. the spin loop hint is not for fairness, but it is required to ensure forward progress.

loom does not run your code on real threads, you can think of the checker like some kind of emulator, but it is not preemptive, it only has the chance to make a decision (this is the "branch" you asked before) when the model "yields" control to the checker (by calling any of the mock synchronization api). this is implemented using stackful coroutines, a.k.a. fibers, a.k.a. green threads, if you are curious about the details, check out the generator crate, which is what loom checker is based on.

because the checker performs no static code analysis, if has no idea whether an operation is part of a (spin-)loop. without the hint, the execution traces will explode unbounded, or in simple word, the model can stuck in a retry loop without making forward progress, until the checker limit is reached and an error is reported.