Best Practices for Verifiably-Correct Concurrent Systems

Concurrent software systems play a vital role in our life. Unfortunately, they are known to be difficult to design, implement, debug, and verify: The tremendous number of potential interactions between concurrently executing threads leads to scenarios which defy human intuition. The growing dependence of modern society on software systems calls for more rigorous techniques for ensuring correctness of concurrent systems.

The goal of the proposed research is to change the current unsatisfactory state of affairs. Specifically, we will provide formal, implementation-independent, definition of best-practices for constructing concurrent systems, and design tools that can either verify that a given concurrent module adheres to the desired best-practice or synthesize a concurrent module which respects an intended correctness condition in a provably correct manner.

Success criteria. We aim to develop our techniques so they can be applied to real-life systems. Thus, we will measure our success by the scale of the systems for which they can be applied. By scale, we do not mean the number of lines of code in the system, but the complexity of its concurrency control mechanism. In particular, the success of this project will be measured by the ability of the tools it will provide to specify/verify/synthesize interesting concurrent modules which cannot be handled by current state-of-the-art formal techniques.

An ideal outcome of our project would be a “cookbook” which a programmer wishing to build a concurrent module satisfying a certain correctness condition, e.g., serializability, using a particular synchronization mechanism, e.g., optimistic locking, could open, and find a formal definition of a policy which she should follow, together with a verification technique that could determine if she implemented the practice correctly, or even a mechanism that would allow her to synthesize a correct implementation out of a sequential module. However, achieving such a result would require far more resources than we can ask for. Thus, we plan to focus our work by selecting a few correctness conditions, e.g., serializability, linearizability, and opacity, and address the three aforementioned challenges with these conditions in mind, but place the particular emphasis on the specification and verification aspects of the project. The selection of the particular conditions will be directed by the practical test cases that we will review at the beginning of the research. We believe that even if we limit ourselves to a few correctness conditions, the techniques and approaches that we will develop will inspire and enable other researchers to follow a similar research program, but targeting different condition. Furthermore, as the conditions that we will handle will be ones the we find in real-life applications, our results would help programmer construct safe and secure practical concurrent systems.