Скачать или смотреть [OOPSLA24] Automated Verification of Parametric Channel-Based Process Communication

Automated Verification of Parametric Channel-Based Process Communication (Video, OOPSLA 2024)
Georgian-Vlad Saioc, Julien Lange, and Anders Møller
(Aarhus University, Denmark; Royal Holloway University of London, United Kingdom; Aarhus University, Denmark)

Abstract: A challenge of writing concurrent message passing programs is ensuring the absence of partial deadlocks, which can cause severe memory leaks in long running systems. Several static analysis techniques have been proposed for automatically detecting partial deadlocks in Go programs. For a large enterprise code base, we found these tools too imprecise to reason about process communication that is parametric, i.e., where the number of channel communication operations or the channel capacities are determined at runtime.
We present a novel approach to automatically verify the absence of partial deadlocks in Go program fragments with such parametric process communication. The key idea is to translate Go fragments to a core language that is sufficiently expressive to represent real-world parametric communication patterns and can be encoded into Dafny programs annotated with postconditions enforcing partial deadlock freedom. In situations where a fragment is partial deadlock free only when the concurrency parameters satisfy certain conditions, a suitable precondition can often be inferred.
Experimental results on a real-world code base containing 583 program fragments that are beyond the reach of existing techniques have shown that the approach can verify the absence of partial deadlocks in 145 cases. For an additional 228 cases, a nontrivial precondition is inferred that the surrounding code must satisfy to ensure partial deadlock freedom.

Article: https://doi.org/10.1145/3689784

Supplementary archive: https://doi.org/10.5281/zenodo.13825844 (Badges: Artifacts Available, Artifacts Evaluated — Reusable)

ORCID: https://orcid.org/0009-0000-1714-3866, https://orcid.org/0000-0001-9697-1378, https://orcid.org/0000-0003-1333-2314

Video Tags: Go, message passing concurrency, partial deadlocks, static analysis, automated verification, invariant discovery, oopslab24main-p731-p, doi:10.1145/3689784, doi:10.5281/zenodo.13825844, orcid:0009-0000-1714-3866, orcid:0000-0001-9697-1378, orcid:0000-0003-1333-2314, Artifacts Available, Artifacts Evaluated — Reusable

Presentation at the OOPSLA 2024 conference, October 20–25, 2024, https://2024.splashcon.org/track/spla...
Sponsored by ACM SIGPLAN,