CASA: An Approach for Exposing and Documenting Concurrency-Related Software Properties

Finding concurrency bugs is hard because of two reasons. Reconstruction of concurrency-specific software properties from source code or binary is an NP-hard problem, and some information might not be present in the software implementation at all (e.g., intentions of synchronisation). Existing approaches for finding concurrency bugs use over-approximating analyses and testing, but these respectively often lead to potential false warnings or fail to report some concurrency bugs. Without knowledge of concurrency properties (memory locations shared between threads and used synchronisation mechanisms), it is hard to complement existing analyses and make their output more precise. Furthermore, choosing a testing tool without knowledge of concurrency-specific software properties is also a challenge and can result in big overhead. Therefore, in this paper we present a light-weight approach that forces developers to plan and document decisions about used synchronisation mechanisms during development. The approach is implemented as part of Agile SCRUM framework. Documented concurrency-related decisions are used to choose adequate testing tools and improve their precision.