Model Checking Under JAM21
M. Rączkiewicz (TU Delft - Electrical Engineering, Mathematics and Computer Science)
S.S. Chakraborty – Mentor (TU Delft - Programming Languages)
A. van Deursen – Graduation committee member (TU Delft - Software Engineering)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
This thesis presents the first known implementation of a model checker for the Java memory model JAM21 within the GenMC framework - a tool for stateless model checking using custom memory models. In addition to the baseline GenMC implementation, we introduce a more efficient model checking algorithm based on vector clocks, which significantly outperforms the initial version. We provide a formal proof of equivalence between the new vector clock algorithm and the original implementation to ensure correctness. Our approach is evaluated using the standard suite of litmus tests included with GenMC. The results confirm that both algorithms correctly enforce the guarantees of JAM21. Furthermore, we successfully replicate prior findings by disallowing erroneous behaviors that went undetected under JAM19.