Loom - A concurrency checker used by Tokio

[carllerche]

Loom is a model checker for concurrent Rust code and is used to test Tokio's
concurrency primitives. It explores the behaviors of code under the C11 memory
model, which Rust inherits. It attempts to avoid combinatorial explosion by
pruning the state space. Currently, loom checks can take a long time as it does
an exhaustive search of all possible executions.

The goal of the project is to make it possible to use loom to check concurrent
code in 10 seconds or less. This requires:

1. Making the loom runtime faster
2. Implement bounded exploration.

Expected outcomes

Tokio's loom based tests complete in 10 seconds or less on a modern personal computer.

Stretch goals

• Add atomic fence support.
• Increase C11 memory model coverage.

Skills

• Rust
• Concurrency

Difficulty level

Hard

[ibabushkin]

Alright, since I expect I'll be writing a proposal for this project idea, given that I'm very much intrgued by the fuzzing-approach as it is applied to concurrency testing, I'll just dump some of my thoughts and a few questions here. Hope that's alright.

So to begin with the core goals -- I have yet to profile loom on the workloads relevant to tokio, so I can't provide any insight regarding the proposed optimizations of the allocation behaviour, but to take a stab in the dark I'll just assume retrofitting one of the arena allocators available (such as typed_arena) and using an arena per type of allocated object and permutation would be a viable first step. Maybe we could even get away with using an arena capable of allocating heterogenous objects. That would be slower, but require even less changes to the code.

Implementing bounded partial order reduction is certainly more challenging, but essentially amounts to implementing the algorithms in the second paper to determine an extended set of backtracking points for the search, and retrofitting a preemption counter to the search as well (which should be relatively easy to do). Right now, I need to do more research in this area before coming up with a detailed implementation strategy (and that's obviously the core contribution here, so I'll focus on that).

Some thoughts on the stretch goals:

Implementing fence support should be relatively straightforward given that a number of other primitives that behave the same way with regards to memory order semantics are already implemented (and loom's code structure, from what I have observed, allows for rather simple extension in this area, as the APIs of std primitives are just mirrored). Additionally, the paper already describes most of the language lawyery involved, which can be used as an additional source (though probably with caveats, as the fine details of the semantics could differ). Maybe I am missing something here? Please correct me if I am wrong.

Finally, extending the support for the memory model seems to be a tricky one. I initially assumed that loom, much like the tool CDSchecker described in the original paper, does not yet provide support for release/consume memory ordering semantics, but since Rust does not expose those (neither does LLVM), I could not yet spot what other aspects of the memory model are missing (but my familiarity with loom's codebase is rather basic at this point). Further reading led to the assumption that loom might not have full support for relaxed memory models. Is that correct?

If anyone wants to talk to me directly/discuss the points above, I am available in the gsoc-related gitter channel :)

[carllerche]

@ibabushkin

Your summary is good. You are correct that an arena would significantly improve the situation.

An easier, but not trivial, first step may be to add random exploration (tracked here). This would not attempt a complete exploration but would provide a reproducible way to test permutations.

[ibabushkin]

Alright, I have a proposal draft uploaded:

http://twki.de/proposal/proposal.html

If anyone wants to leave feedback I'd greatly appreciate it.

[carllerche]

@ibabushkin nice proposal. I would look at https://github.com/fitzgen/bumpalo for the allocation (new crate since gsoc proposals started).

Besides that, I would submit the proposal via the UI.

[ibabushkin]

That's good news then! I'm still ironing out some minor kinks people noticed, and will submit via the gsoc website shortly. I'll look into bumpalo as well, maybe that can provide some insight too.