Lin-Check: Testing concurrent data structures in Java

Writing concurrent programs is hard. However, testing them is not easy as well. In this talk, Nikita presents Lin-Check, a tool for testing concurrent data structures in JVM-based languages. Essentially, it takes some declarations of the data structure operations, generates random scenarios, runs them a lot of times, and verifies the corresponding results. During the talk, Nikita mostly focuses on the verification phase.

At first, he explains how LTS (Labeled Transition System) formalism can help us with implementing the verifier efficiently. After that, he extends LTS to support dual data structures; this formalism is useful for data structures with partial methods (synchronous queues, blocking queues, channels, semaphores, ...). However, such an extension is not sufficient, and some small tricks should be added, which restrict the model a bit but make it possible to use it in practice.