Lock and Immutability Checkers for Concurrent Programs

@immutability_related_issues and @entailLocking_related_issues NEWS:

This page contains our research on identifying concurrency-related issues in real-world programs.

Concurrent Programs are hard to analyze or debug due to the complex program logic and unpredictable execution environment. According to Lu et al. [1], wrong assumptions on synchronization/ordering intentions are usually responsible for many concurrency bugs. However, we observe that even when programmers have correct intentions of synchronization, they may still write programs with concurrency issues due to the lack of understanding to certain concurrency-related API. Thus our work aims at enforcing correct usage of concurrency related APIs. We adopt natural language processing techniques to analyze Java API specifications to extract annotations related to common concurrency-related issues. Then we systematically detect misuse of those APIs with the extracted annotations.

We adopt the Stanford Parser for the purpose of natural language parsing, specifically dependency parsing. Then we extract annotations from the dependency trees, which are the parse result of the Stanford Parser. We are especially interested in five kinds of annotations, i.e., @threadsafe, @!threadsafe, @immutable, @!reentrant and @!entailLocking. We processed the Java SE 8 API specification and the full list of annotations extracted can be found here.

To show how we can detect potential concurrency related issues with the extracted annotations, we crawled the top 1k most popular projects from GitHub. We then detected potential concurrency issues related to @immutable and @!entailLocking type annotations since they are under-supported. We report the list of potential issues (@immutability_related_issues and @entailLocking_related_issues) that are found by our method. We’ve reported the found issues to the corresponding developers and received responses from 12 projects, among which 8 confirm that the found issues are real bugs in their projects. We pick some responses (including both confirmations and false positives) from the developers here:

The Checkers:

We developed a locker-checker based on the Checker Framework for the purpose of detecting @entailLocking related issues. For the purpose of detecting @immutability issues, we extended the Javari Checker, which is a build in checker in the Checker Framework. The jar files of the checkers are downloadable here (including checker.jar, checker_qual.jar). Replace the corresponding files of the Checker Framework (downloadable here) in path checker-framework/checker/dist with them and run the Checker Framework following the steps described here.

An example failure reported by the locker-checker looks like this:

[ERROR] /Users/ls/Research/concurrency/git_source/mrniko/redisson/src/main/java/org/redisson/RedissonLock.java:[80,29] error: [redundancy.locking] There is redundancy lock: the concurrent collection guarantees thread-safety for read/write on single entries.
[ERROR] /Users/ls/Research/concurrency/git_source/mrniko/redisson/src/main/java/org/redisson/RedissonLock.java:[59,88] error: [assignment.type.incompatible] incompatible types in assignment.
[ERROR] -> [Help 1]
org.apache.maven.lifecycle.LifecycleExecutionException: Failed to execute goal org.apache.maven.plugins:maven-compiler-plugin:3.3:compile (default-compile) on project redisson: Compilation failure

We will keep this website updated if we find more bugs or received confirmations from the programmers. Please contact shuang_liu@sutd.edu.sg if there are any questions.

 

[1] S. Lu, S. Park, E. Seo, and Y. Zhou. Learning from mistakes: A comprehensive study on real world concurrency bug characteristics. In Proceedings of the 13th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS XIII, pages 329–339, New York, USA, 2008. ACM.