Automated Verification of Parametric Channel-Based Process Communication
This program is tentative and subject to change.
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 codebase, 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 codebase containing 585 program fragments that are beyond the reach of existing techniques have shown that the approach can verify the absence of partial deadlocks in 140 cases. For an additional 234 cases, a nontrivial precondition is inferred that the surrounding code must satisfy to ensure partial deadlock freedom.
This program is tentative and subject to change.
Thu 24 OctDisplayed time zone: Pacific Time (US & Canada) change
16:00 - 17:40 | |||
16:00 20mTalk | Concurrent Data Structures Made Easy OOPSLA 2024 Callista Le Yale-NUS College, Kiran Gopinathan National University of Singapore, Lee Koon Wen Ahrefs, Seth Gilbert National University of Singapore, Ilya Sergey National University of Singapore | ||
16:20 20mTalk | Automated Verification of Parametric Channel-Based Process Communication OOPSLA 2024 Georgian-Vlad Saioc Aarhus University, Julien Lange Royal Holloway, University of London, Anders Møller Aarhus University | ||
16:40 20mTalk | Automated Robustness Verification of Concurrent Data Structure Libraries Against Relaxed Memory Models OOPSLA 2024 Kartik Nagar IIT Madras, Anmol Sahoo Purdue University, Romit Roy Chowdhury Chennai Mathematical Institute, Suresh Jagannathan Purdue University | ||
17:00 20mTalk | Scenario-based Proofs for Concurrent Objects OOPSLA 2024 | ||
17:20 20mTalk | Verified Lock-Free Session Channels with Linking OOPSLA 2024 |