MR
M. Rączkiewicz
info
Please Note
<p>This page displays the records of the person named above and is not linked to a unique person identifier. This record may need to be merged to a profile.</p>
1 records found
1
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.
...
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.