Systematic testing of our concurrency primitives

[bblum]

@brson and I were talking about different strategies for verifying our concurrency primitives (task spawn/scheduling, pipes, arcs), specifically wondering if the technique I work on during my "day job" (i.e. grad student) could be applied.

In short, systematic testing means exploring the state space of possible test executions that can result from different thread interleavings. This depends on a notion of decision points, which are code locations where the testing framework "should try" to force threads to interleave in different ways. The set of decision points defines an execution tree which represents the state space (size = {number of threads}^{number of decision points}). If there is a bug in some branches of the tree, but not others, that bug is a race condition.

Though my research focuses on kernel-level testing, a colleague of mine at CMU has developed a tool for doing the same thing on userspace programs, called dBug (http://www.cs.cmu.edu/~jsimsa/dbug/). It uses LD_PRELOAD to interpose on library calls, such as pthread operations and file I/O.

There are two points which need consideration before introducing dBug and Rust to each other:

• Threads vs tasks. dBug doesn't have a notion of userspace thread scheduling, and I think it would be quite difficult to model that and have any userspace systematic tester be able to force a single "rust_sched_loop" thread to switch to an arbitrary task. (This is essentially the problem that my research on doing it in kernel-space, is for!) But, lacking this functionality in the meantime, we could still configure rust to spawn each new task on a new scheduler of its own. This would sacrifice the ability to test the thread-rescheduling code within schedulers, but make it easier to test stuff at higher levels, such as pipes.
• One of the final things Jiri (dBug's developer) is working on for his thesis is a domain-specific modelling language for expressing how concurrency primitives behave, so that dBug can understand their semantics (e.g., cond_wait puts a thread to sleep until a cond_signal on the same cvar). We might be able to use this to model pipes themselves, enabling coarser-grained testing of stuff that's implemented on top of pipes (e.g. linked task failure, RWARCs).

[emberian]

Visiting for triage; nothing to add except this would be super cool

[flaper87]

Triage bump, nothing to add.

[alexcrichton]

Quite a bit of time has passed since this was opened, and I think that our need for such a testing infrastructure has lessened quite a bit over time. All of green scheduling has been removed along with many of the based-on-channels implementations of primitives like mutexes and condition variables.

I think it'd still be great to have a suite of concurrency-testing primitives, but for now I think this isn't particularly actionable as-is (and has probably just been getting stale for some time now). As a result I'm going to close this, but we can certainly try to pursue strategies such as this in the future!