TruSt Implementation in Lincheck

This project was initiated as a research internship at the Max Planck Institute for Software Systems (MPI-SWS) in the summer of 2023, in collaboration with Ava Mirmohammadmahdi and under the supervision of Prof. Rupak Majumdar.

Purpose

This project involved the partial implementation of the TruSt algorithm within the Lincheck framework, a model-checking tool for concurrent data structures in JVM-based languages, developed by JetBrains. TruSt is a stateless dynamic partial order reduction (DPOR) algorithm designed to minimize the number of explored interleavings in concurrent programs using execution graphs.

Implementation

The implementation was carried out in Kotlin and the repository for the implementation can be found here.

Challenges

We encountered several challenges, primarily due to the high-level characteristics of Java. The algorithm required identifying each shared object uniquely, which was challenging because of the garbage collection and the lack of a unique identifier for each object in Java. The details of these challenges and some possible solutions are further elaborated in the accompanying report.

Outcome

Unfortunately, the implementation was not completed due to time constraints. However, the work done so far has been documented in the repository and the accompanying report. The implementation can be further extended and integrated into the Lincheck framework to enhance its capabilities.