Galois - Building a Concurrency Verifier Using Crucible
Tools
News & Insights
About Us
Get Started
GET IN TOUCH<br>We take pride in personally connecting with all interested partners, collaborators and potential clients. Please email us with a brief description of how you would like to be connected with Galois and we will do our best to respond within one business day.
Email<br>contact@galois.com<br>PHONE<br>503.626.6616
Building a Concurrency Verifier Using Crucible
Alexander Bakst and Mike Dodds<br>June 18, 2021
Many of the verification and static analysis tools we build at Galois are based on the same technology: a symbolic execution engine for a language called Crucible. There are a lot of advantages to doing this. It’s what makes it possible for SAW to reason about C, C++, Rust, and x86 assembly, all through the same interface, just by translating into Crucible. Improvements to Crucible improve all our tools at once, and the systems we’ve verified form a natural test set that helps us avoid bugs and performance regressions.<br>Crucible also makes it much easier to build new tools. For instance, Galois recently announced Crux, a verification tool based on symbolic testing. A user of Crux can write a test harness with symbolic inputs and then check whether assertions in the test case could ever fail. Behind the scenes, Crux translates programs to Crucible.<br>This works great for sequential programs, but it made us wonder whether we could use the same technology to build a simple verifier for multi-threaded Rust programs. It turns out that Crucible makes that pretty easy! Let’s take a look at what we did.<br>Example<br>Let’s examine the following simple program:<br>fn inc(val: u32) -> u32<br>if val == u32::MAX { val } else { val + 1 }
fn dec(val: u32) -> u32<br>if val == 0 { val } else { val - 1 }
fn action(do_inc: bool, value: u32) -> u32<br>if do_inc { inc(value) } else { dec(value) }
We might want to check that if we chain action three times, then the difference between the resulting value and the original value is no more than 3. We can devise the following test in crux-mir (the Rust version of Crux) to check this is the case for an arbitrary starting value and an arbitrary sequence of three actions:<br>#[cfg_attr(crux, crux_test)]<br>fn test() {<br>let v0 = u32::symbolic("value");<br>let mut v = v0;
for i in 0..3 {<br>let do_inc = bool::symbolic("do_inc");<br>v = action(do_inc, v);
crucible_assert!(if v >= v0 { v - v0 } else { v0 - v }<br>Here, the declaration u32::symbolic("value") tells Crux to consider any possible value rather than a single one. Crux-mir verifies that the assertion succeeds, meaning the assertion is true for any choice of v0 and do_inc. Pretty cool!<br>The Crucible language (and, hence, the symbolic execution engine) is itself single-threaded, leaving verifying properties of multithreaded programs out of Crux’s reach. For example, we would like to be able to modify the above program so that each action is performed by a separate thread concurrently:<br>fn inc(val: u32) -> u32<br>if val == u32::MAX { val } else { val + 1 }
fn dec(val: u32) -> u32<br>if val == 0 { val } else { val - 1 }
fn action(do_inc: bool, value: &Arc>)<br>let mut pval = value.lock().unwrap();<br>*pval = if do_inc { inc(*pval) } else { dec(*pval) };
#[cfg_attr(crux, crux_test)]<br>fn main() {<br>let v0 = u32::symbolic("value");<br>let value = Arc::new(Mutex::new(v0));
for i in 0..NUM_THREADS {<br>let do_inc = bool::symbolic("do_inc");<br>let t_value = value.clone();<br>thread::spawn(move || action(do_inc, &t_value));
let mut pval = value.lock().unwrap();<br>let v = *pval;<br>crucible_assert!(if v >= v0 { v - v0 } else { v0 - v }<br>Fortunately, it turns out that we can support threads in Crucible without modifying the engine at all. This means we can benefit from the years of engineering that have been poured into Crucible but would benefit from any future improvements as well. Likewise, leaving threads out of the language supported by Crucible reduces the complexity of maintenance on, and improvements, to the symbolic executor.<br>Adding Concurrency<br>We can model the behavior of the multithreaded program above as a collection of all of the different executions of the program. For example, we might have the following two execution orders:<br>Thread 0: inc → Thread 1: dec → Thread 2: inc<br>Thread 1: dec → Thread 2: inc → Thread 0: inc<br>Each of these executions corresponds to a particular thread interleaving, or ordering of the different atomic statements executed by all of the threads.<br>At a high level, then, we approach the problem by searching for new interleavings and then using Crucible to verify each one. We built out a prototype implementation of this idea as a new library and instantiated it for use in crux-mir.<br>Conceptually, our approach works as follows:<br>A Scheduler steps through a Crucible program (much like how you would use gdb to step through a C program). The scheduler adds threads to a pool of running threads as they are created. The Scheduler picks a thread and its next instruction at each...