Lincheck: A Practical Framework for Testing Concurrent Data Structures on JVM

Abstract

Abstract This paper presents , a new practical and user-friendly framework for testing concurrent algorithms on the Java Virtual Machine (JVM). provides a simple and declarative way to write concurrent tests: instead of describing how to perform the test, users specify what to test by declaring all the operations to examine; the framework automatically handles the rest. As a result, tests written with are concise and easy to understand. The framework automatically generates a set of concurrent scenarios, examines them using stress-testing or bounded model checking, and verifies that the results of each invocation are correct. Notably, if an error is detected via model checking, provides an easy-to-follow trace to reproduce it, significantly simplifying the bug investigation. To the best of our knowledge, is the first production-ready tool on the JVM that offers such a simple way of writing concurrent tests, without requiring special skills or expertise. We successfully integrated in the development process of several large projects, such as Kotlin Coroutines, and identified new bugs in popular concurrency libraries, such as a race in Java’s standard and a liveliness bug in Java’s framework, which is used in most of the synchronization primitives. We believe that can significantly improve the quality and productivity of concurrent algorithms research and development and become the state-of-the-art tool for checking their correctness.