PLDI 2025
Mon 16 - Fri 20 June 2025 Seoul, South Korea

This program is tentative and subject to change.

Fri 20 Jun 2025 14:20 - 14:40 at Cosmos, Violet & Tulip - Concurrency Chair(s): Jeehoon Kang

This paper revisits the fundamental problem of monitoring the linearizability of concurrent stacks, queues, sets, and multisets.

Given a history of a library implementing one of these abstract data types, the monitoring problem is to answer whether the given history is linearizable.

For stacks, queues, and (multi)sets, we present monitoring algorithms with complexities $\bigo(n^2)$, $\bigo(n~\log~n)$, and $\bigo(n)$, respectively, where $n$ is the number of operations in the input history.

For stacks and queues, our results hold under the standard assumption of {\it data-independence}, i.e., the behavior of the library is not sensitive to the actual values stored in the data structure.

Past works to solve the same problems have cubic time complexity and (more seriously) have correctness issues: they either (i) lack correctness proofs or (ii) have unsound correctness proofs (we present counter-examples of the correctness proofs), or (iii) have unsound algorithms.

Our improved complexity results rely on substantially different algorithms for which we provide detailed proofs of correctness.

We have implemented our stack and queue algorithms in LiMo (Linearizability Monitor). We evaluate LiMo and compare it with the state-of-the-art tool Violin – whose correctness proofs we have found errors in – which checks for linearizability violations. Our experimental evaluation confirms that LiMo outperforms Violin regarding both efficiency and scalability.

This program is tentative and subject to change.

Fri 20 Jun

Displayed time zone: Seoul change

14:00 - 15:20
14:00
20m
Talk
Efficient Timestamping for Sampling-Based Race Detection
PLDI Research Papers
Minjian Zhang University of Illinois at Urbana-Champaign, Daniel Wee Soong Lim National University of Singapore, Mosaad Al Thokair Saudi Aramco, Umang Mathur National University of Singapore, Mahesh Viswanathan University of Illinois at Urbana-Champaign
DOI Pre-print
14:20
20m
Talk
Efficient Linearizability Monitoring
PLDI Research Papers
Parosh Aziz Abdulla Uppsala University; Mälardalen University, Samuel Grahn Uppsala University, Bengt Jonsson Uppsala University, Shankaranarayanan Krishna IIT Bombay, Om Swostik Mishra IIT Bombay
DOI
14:40
20m
Talk
[TOPLAS] Sound Static Data Race Verification for C: Is the Race Lost?
PLDI Research Papers
Karoliine Holter University of Tartu, Estonia, Simmo Saan University of Tartu, Estonia, Patrick Lam University of Waterloo, Vesal Vojdani University of Tartu
DOI Pre-print
15:00
20m
Talk
Nola: Later-Free Ghost State for Verifying Termination in Iris
PLDI Research Papers
Yusuke Matsushita Kyoto University, Takeshi Tsukada Chiba University
Link to publication DOI