Hunting For Bugs in Libraries for Concurrent Programming

Synchronization bugs in concurrent applications result in errors (deadlocks, race conditions etc.), which are not easily reproducible and it is therefore practically impossible to find them with ordinary testing. Software libraries for concurrency programming are supposed to provide proven solutions for synchronization, in terms of safety (e.g. mutual exclusion, correct ordering of operations) and liveness (e.g. absence of starvation). However, in most cases they lack proper documentation or formal specifications of the semantics of the provided operations. Software model checking is a viable alternative against testing for concurrency verification, but it is only feasible if the API is considered as part of a larger system with a specific functionality. In this work, we present our experience on the software model checking of an open source library using NASA’s JavaPathFinder (JPF) model checker. Our approach was based on the API’s test classes, which were transformed into an analyzable input for the JPF tool. The results can reveal bugs or can simply provide valuable feedback towards the formal specification of the API’s operation semantics.