Invariant-based specification, synthesis, and verification of synchronization in concurrent programs

Abstract

Concurrency is used in modern software systems as a means of addressing performance, availability, and reliability requirements. The collaboration of multiple independently executing components is fundamental to meeting such requirements and such collaboration is realized by synchronizing component execution.Using current technologies developers are faced with a tension between correct synchronization and performance. Developers can be confident when simple forms of synchronization are used, for example, locking all accesses to shared data. Unfortunately, such simple approaches can result in significant run-time overhead, and, in fact, there are many cases in which such simple approaches cannot implement required synchronization policies. Implementing more sophisticated (and less constraining) synchronization policies may improve run-time performance and satisfy synchronization requirements, but fundamental difficulties in reasoning about concurrency make it difficult to assess their correctness.This paper describes an approach to automatically synthesizing complex synchronization implementations from formal high-level specifications. Moreover, the generated coded is designed to be processed easily by software model-checking tools such as Bandera. This enables the generated synchronization solutions to be verified for important system correctness properties. We believe this is an effective approach because the tool-support provided makes it simple to use, it has a solid semantic foundation, it is language independent, and we have demonstrated that it is powerful enough to solve numerous challenging synchronization problems.