Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Thu 21 Jan 2021 19:20 - 19:30 at POPL-A - Complexity

Many program analyses need to reason about pairs of matching actions, such as call/return, lock/unlock, or set-field/get-field. The family of Dyck languages {Dk}, where Dk has k kinds of parenthesis pairs, can be used to model matching actions as balanced parentheses. Consequently, many program-analysis problems can be formulated as Dyck-reachability problems on edge-labeled digraphs. Interleaved Dyck-reachability (InterDyck-reachability), denoted by Dk ⊙ Dk-reachability, is a natural extension of Dyck-reachability that allows one to formulate program-analysis problems that involve multiple kinds of matching-action pairs. Unfortunately, the general InterDyck-reachability problem is undecidable.

In this paper, we study variants of InterDyck-reachability on bidirected graphs, where for each edge ⟨p, q⟩ labeled by an open parenthesis “(a”, there is an edge ⟨q, p⟩ labeled by the corresponding close parenthesis “)a”, and vice versa. Language-reachability on a bidirected graph has proven to be useful both (1) in its own right, as a way to formalize many program-analysis problems, such as pointer analysis, and (2) as a relaxation method that uses a fast algorithm to over-approximate language-reachability on a directed graph. However, unlike its directed counterpart, the complexity of bidirected InterDyck-reachability still remains open.

We establish the first decidable variant (i.e., D1 ⊙ D1-reachability) of bidirected InterDyck-reachability. In D1 ⊙ D1-reachability, each of the two Dyck languages is restricted to have only a single kind of parenthesis pair. In particular, we show that the bidirected D1 ⊙ D1 problem is in PTIME. We also show that when one extends each Dyck language to involve k different kinds of parentheses (i.e., Dk ⊙ Dk-reachability), the problem is NP-hard (and therefore much harder).

We have implemented the polynomial-time algorithm for bidirected D1 ⊙ D1-reachability. Dk ⊙ Dk-reachability provides a new over-approximation method for bidirected Dk ⊙ Dk-reachability in the sense that Dk ⊙ Dk-reachability can first be relaxed to bidirected D1 ⊙ D1-reachability, and then the resulting bidirected D1 ⊙ D1-reachability problem is solved precisely. We compare this approach to over-approximating bidirected Dk ⊙ Dk-reachability against another known over-approximation algorithm for the problem. Surprisingly, we found that the over-approximation approach based on bidirected D1 ⊙ D1-reachability computes more precise solutions, even though the D1 ⊙ D1 formalism is inherently less expressive than the Dk ⊙ Dk formalism.

Thu 21 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:30 - 19:30
ComplexityPOPL at POPL-A
18:30
10m
Talk
Learning the Boundary of Inductive Invariants
POPL
Yotam M. Y. Feldman Tel Aviv University, Mooly Sagiv Tel Aviv University, Sharon Shoham Tel Aviv University, James R. Wilcox University of Washington
Link to publication DOI
18:40
10m
Talk
The Fine-Grained and Parallel Complexity of Andersen's Pointer Analysis
POPL
Andreas Pavlogiannis Aarhus University, Anders Alnor Mathiasen Aarhus University
Link to publication DOI
18:50
10m
Talk
Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory ProgramsDistinguished Paper
POPL
Pascal Baumann Max Planck Institute for Software Systems (MPI-SWS), Rupak Majumdar MPI-SWS, Ramanathan S. Thinniyam Max Planck Institute for Software Systems (MPI-SWS), Georg Zetzsche Max Planck Institute for Software Systems (MPI-SWS)
Link to publication DOI
19:00
10m
Talk
Deciding ω-Regular Properties on Linear Recurrence Sequences
POPL
Shaull Almagor Technion, Toghrul Karimov Max Planck Institute for Software Systems, Edon Kelmendi University of Oxford, Joël Ouaknine Max Planck Institute for Software Systems and University of Oxford, James Worrell University of Oxford
Link to publication DOI
19:10
10m
Talk
Deciding Reachability under Persistent x86-TSO
POPL
Parosh Aziz Abdulla Uppsala University, Sweden, Mohamed Faouzi Atig Uppsala University, Sweden, Ahmed Bouajjani IRIF, Université Paris Diderot, K Narayan Kumar Chennai Mathematical Institute, Prakash Saivasan The Institute of Mathematical Sciences, India
Link to publication DOI
19:20
10m
Talk
On the Complexity of Bidirected Interleaved Dyck-Reachability
POPL
Yuanbo Li Georgia Institute of Technology, USA, Qirun Zhang Georgia Institute of Technology, USA, Thomas Reps University of Wisconsin--Madison
Link to publication DOI