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

Concurrency is used in modern software systems as a means of addressing performance, availability, and reliability requirements. Using current technologies developers are faced with a tension between correct synchronization and performance. Unfortunately, simple approaches can result in significant run-time overhead. Implementing more sophisticated 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. The paper describes an approach to automatically synthesizing complex synchronization implementations from formal high-level specifications. Moreover, the generated code 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.