Annotations for Race-freedom
Univ. of Illinois at Urbana-Champaign, U.S.A.
The advent of multicore has renewed interest in parallel programming. Unfortunately, current parallel programming languages for shared-memory programming suffer from a fundamental problem in handling programs with data-races. An execution of a concurrent program has a data-race if there are two concurrent accesses to the same memory location where one of them is a write. Attempts to give semantics for programs with data-races in the presence of compiler optimizations has essentially failed to deliver a simple memory model (for Java and C++), and it's common belief that programs with data-races are best avoided for at least the common programmer. The new semantics for C++ does not even provide semantics for programs with data-races.
This leaves us in the unusual situation of not being able to give a syntactic check for well-formed programs! Checking for data-races is hard (undecidable).
In this work, we explore proof mechanisms using which a programmer can prove race-freedom of a parallel program. We provide a robust mechanism for only restricted fork-join parallelism using foreach loop constructs that essentially exploit data-parallelism by working on separable parts of multi-dimensional arrays. Our framework allows the programmer to specify annotations that imply race-freedom. Checking race-freedom then decomposes into two well-known problems--- a constraint satisfaction problem and a sequential verification problem. Using a variety of examples we illustrate our framework of proving race-freedom using automatic theorem provers (SMT solvers; Z3) and Floyd-Hoare verification mechanisms (Boogie).