Formal Methods and Tools to Check Correctness
Principal Investigators: Madhu Parthasarathy
The disciplined programming methodologies we propose will go a long way in managing the complexity of writing a concurrent program and arguing its correctness. However, multicore programs will still be prone to errors due to concurrency, both in the new components written for our disciplined models and in components that continue to use current models.
There are two serious problems related to correctness that we wish to address through a combination of formal methods and correctness checking tools. First, there is a pressing problem in the engineering of tools that assure correctness of concurrent code. Second, even as we transition to disciplined languages, programs will likely have components that adhere to different levels of this discipline; e.g., deterministic components, non-deterministic but data-race-free components with locks, and even low-level shared memory legacy components. A rational composition of such modules into a single program that can be analyzed for correctness will be crucial in furthering the applicability and adoption of the disciplined programming languages we propose.
We advocate addressing the above problems by first building an understanding of the high-level synchronization intentions that help programmers co-ordinate the parallelism and simplify reasoning about the correctness of their code. We believe that this understanding, inferred by detailed bug and code analysis, will prove useful in addressing both the testing and the composition problems described above. In testing a concurrent program, we plan to use the high-level synchronization intentions to effectively prune the space of interleavings, concentrating only on those that violate these intentions as they are more likely to have errors. The high-level synchronization intentions will also help build a language to summarize the high-level synchronizations for the less disciplined code so that we can encapsulate them, verify them, and compose them with newly written disciplined code, while assuring correctness of the entire program.
