Скачать или смотреть [VMCAI'25] Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts

Correctness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts (Video, VMCAI)
Julian Erhard, Manuel Bentele, Matthias Heizmann, Dominik Klumpp, Simmo Saan, Frank Schüssele, Michael Schwarz, Helmut Seidl, Sarah Tilscher, and Vesal Vojdani
(LMU Munich; TU Munich; University of Freiburg; University of Freiburg, Germany; University of Freiburg; University of Tartu, Estonia; University of Freiburg; TU Munich; TU Munich; Technical University of Munich, Garching, Germany; University of Tartu)

Abstract: Static analyzers are typically complex tools and thus prone to contain bugs themselves. To increase the trust in the verdict of such tools, witnesses encode key reasoning steps underlying the verdict in an exchangeable format, enabling independent validation of the reasoning by other tools. For the correctness of concurrent programs, no agreed-upon witness format exists – in no small part due to the divide between the semantics considered by analyzers, ranging from interleaving to thread-modular approaches, making it challenging to exchange information. We propose a format that leverages the well-known notion of ghosts to embed the claims a tool makes about a program into a modified program with ghosts, such that the validity of a witness can be decided by analyzing this program. Thus, the validity of witnesses with respect to the interleaving and the thread-modular semantics coincides. Further, thread-modular invariants computed by an abstract interpreter can naturally be expressed in the new format using ghost statements. We evaluate the approach by generating such ghost witnesses for a subset of concurrent programs from the SV-COMP benchmark suite, and pass them to a model checker. It can confirm 75 % of these witnesses – indicating that ghost witnesses can bridge the semantic divide between interleaving and thread-modular approaches.


Presentation at the VMCAI conference, January 20-21, 2025, https://popl25.sigplan.org/home/vmcai...
Sponsored by ACM SIGPLAN