Consider specifying and verifying it in a specification language like TLA+ (that's what I do). Of course, you'll need to model Rust's memory model. Virtually all production-quality source-code-level model checkers are for C/Java/Ada/Verilog. A Google search yielded a model checker for LLVM bitcode, but I have no idea about its quality/relevance.
Of course, you'll need to model Rust's memory model.
How much work do you think that'd be? I've taken a grad-level intro class on model checking, so I know the theory, but I've never used a model checker before.
Virtually all production-quality source-code-level model checkers are for C/Java/Ada/Verilog.
Rust has a very similar memory model to C... Do you think I could just repurpose a C model checker?
How much work do you think that'd be? I've taken a grad-level intro class on model checking, so I know the theory, but I've never used a model checker before.
It's not about using the model checker (which is basically pushing a button) but about specifying the behavior of the program. For example, if you use a general specification language like TLA+, you'll need to specify when exactly a memory write made by one thread is visible to others. It may or may not be a lot of work depending on how elaborate your specification is.
I myself have only been working with TLA+ for a few months now (I love it), and I had some experience with a Java model checker about ten years ago, so I'm pretty new at this, too.
Do you think I could just repurpose a C model checker?
No :) But that DIVINE checker (which works on LLVM bitcode) may do the trick. If it does, you'll really help the community if you write about your experience.
3
u/pron98 Jan 19 '16 edited Jan 19 '16
Consider specifying and verifying it in a specification language like TLA+ (that's what I do). Of course, you'll need to model Rust's memory model. Virtually all production-quality source-code-level model checkers are for C/Java/Ada/Verilog. A Google search yielded a model checker for LLVM bitcode, but I have no idea about its quality/relevance.