SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Thu 19 Nov 2020 09:20 - 09:40 at SPLASH-V - Session 3

Systems of transformations arise in many programming systems, such as in type graphs of implicit type conversion functions. It is important to ensure that these diagrams commute: that any composing path of transformations from the same source to the same destination yields the same result. However, a straightforward approach to verifying commutativity must contend with cycles, and even so it runs in exponential time. Previous work has shown how to verify commutativity in the special case of acyclic diagrams in O(|V|^4|E|^2) time, but this is a batch algorithm: the entire diagram must be known ahead of time. We present an online algorithm that efficiently verifies that a commutative diagram remains commutative when adding a new edge. The new incremental algorithm runs in O(|V|^2(|E|+|V|)) time. For the case when checking the equality of paths is expensive, we also present an optimization that runs in O(|V|^4) time but reduces to the minimum possible number of equality checks.We implement the algorithms and compare them to batch baselines, and we demonstrate their practical application in the compiler of a domain-specific language for geometry types. To study the algorithms’ scalability to large diagrams, we apply them to discover discrepancies in currency conversion graphs.

Thu 19 Nov

Displayed time zone: Central Time (US & Canada) change

09:00 - 10:20
Session 3TAPAS at SPLASH-V
09:00
20m
Short-paper
API Analytics for Curating Static Analysis Rules
TAPAS
09:20
20m
Paper
Online Verification of Commutativity
TAPAS
Aditi Kabra Carnegie Mellon University, Dietrich Geisler Cornell University, Adrian Sampson Cornell University
Pre-print
09:40
20m
Short-paper
Towards Checkpoint Placement for Dynamic Memory Allocation in Intermittent Computing
TAPAS
Nicholas Shoemaker , Ruzica Piskac Yale University, USA, Mark Santolucito Barnard College, Columbia University, USA