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

This program is tentative and subject to change.

Fri 20 Jun 2025 10:50 - 11:10 at Grand Ball Room 1 - Compilers 2

It is a long-standing open problem to support verified compilation of multi-threaded programs compositionally when sharing of stack data between threads is allowed. Although certain solutions exist on paper, none of them is completely formalized because of the difficulty in simultaneously enabling sharing and forbidding modification of stack memory in presence of arbitrary memory operations (e.g., pointer arithmetic). We present a compiler verification framework that solves this open problem in the setting of cooperative multi-threading. To address the challenges of sharing stack data, we introduce threaded Kripke memory relations (TKMR) to support both protection and sharing of stacks in a multi-stack memory model. We further introduce threaded forward simulations parameterized by TKMR to capture semantics preservation for compiling program modules in multi-threaded contexts. We show that threaded forward simulations are both horizontally composable— thereby enabling the compositional verification of open threads and heterogeneous modules—and vertically composable—thereby enabling composition of compiler correctness for multiple compiler passes. Furthermore, threaded forward simulations can be converted into backward simulations. We apply this framework to 18 passes of CompCert to get CompCertOC, the first optimizing verified compiler that supports compositional verification of cooperative multi-threaded programs with shared stacks.

This program is tentative and subject to change.

Fri 20 Jun

Displayed time zone: Seoul change

10:30 - 12:10
10:30
20m
Talk
Robustifying Debug Information Updates in LLVM via Control-Flow Conformance Analysis
PLDI Research Papers
Shan Huang East China Normal University, Jingjing Liang East China Normal University, Ting Su East China Normal University, Qirun Zhang Georgia Institute of Technology
DOI
10:50
20m
Talk
CompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared Stacks
PLDI Research Papers
Ling Zhang Shanghai Jiao Tong University, Yuting Wang Shanghai Jiao Tong University, Yalun Liang Shanghai Jiao Tong University, Zhong Shao Yale University
DOI
11:10
20m
Talk
Link-Time Optimization of Dynamic Casts in C++ Programs
PLDI Research Papers
Xufan Lu INESC-ID / Instituto Superior Técnico, University of Lisbon, Nuno P. Lopes INESC-ID; Instituto Superior Técnico - University of Lisbon
Link to publication DOI
11:30
20m
Talk
Divergence-Aware Testing of Graphics Shader Compiler Back-Ends
PLDI Research Papers
Dongwei Xiao Hong Kong University of Science and Technology, Shuai Wang Hong Kong University of Science and Technology, Zhibo Liu Hong Kong University of Science and Technology, Yiteng Peng Hong Kong University of Science and Technology, Daoyuan Wu Hong Kong University of Science and Technology, Zhendong Su ETH Zurich
DOI
11:50
20m
Talk
Optimization-Directed Compiler Fuzzing for Continuous Translation Validation
PLDI Research Papers
DOI Pre-print