The Virtual Recency Abstraction (Strong Updates for Abstract Interpreters with Shared State)
This program is tentative and subject to change.
Abstract interpreters enable sound static analysis, but are hard to develop. In recent years, researchers have proposed a component-based approach to developing abstract interpreters, where different parts of the abstract domain (e.g., numeric, call frame, heap) are handled by isolated components. This works well as long as components do not share or expose their internal state: Any state update that is locally sound is also globally sound. However, some abstract domains require shared state, most prominently relational abstract domains, which use symbolic expressions such as $2x+5$ to represent abstract values. As the relational component performs a strong update of $x$, the abstract value $2x+5$ can change non-monotonically, which breaks soundness. We propose a novel solution to this problem: A virtual recency abstractions that decouples the relational component, supports strong updates, and allows recursion. We prove that the virtual recency abstraction restores soundness: Any shared state wrapped in our virtual recency abstraction may be locally updated non-monotonically, while global soundness persists. We applied our approach to develop the first relational WebAssembly analysis, reusing many components from an existing inter-procedural abstract interpreter. Furthermore, we evaluate the recall, precision, and scalibility of this analysis to demonstrate the practicality of the virtual recency abstraction.
This program is tentative and subject to change.
Thu 2 JulDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
14:00 - 15:30 | Compilers, Interpreters & Runtime SystemsTechnical Papers at I.2.03 Chair(s): Christian Hammer University of Passau | ||
14:00 22mTalk | Eliminate Branches by Melding IR Instructions Technical Papers Yuze Li Virginia Tech, Srinivasan Ramachandra Sharma Virginia Tech, Charitha Saumya Intel, Ali R. Butt Virginia Tech, Kirshanthan Sundararajah Virginia Tech | ||
14:22 22mTalk | Characterizing Type Feedback in Just-in-Time Compilation Technical Papers Sebastián Krynski Czech Technical University in Prague, Filip Riha Czech Technical University, Filip Křikava Czech Technical University in Prague, Jan Vitek Northeastern University | ||
14:45 22mTalk | Optimizing Record/Replay through Relaxed Total Ordering and Multi-Version eXecution Technical Papers | ||
15:07 22mTalk | The Virtual Recency Abstraction (Strong Updates for Abstract Interpreters with Shared State) Technical Papers Sven Keidel Fraunhofer SIT | ATHENE, Raphaël Monat Inria and University of Lille, Sebastian Erdweg KIT Pre-print | ||