Legato: An At-Most-Once Analysis with Applications to Dynamic Configuration Updates
Modern software increasingly relies on external resources whose location or content can change during program execution. Examples of such resources include remote network hosts, database entries, dynamically updated configuration options, etc. Long running, adaptable programs must handle these changes gracefully and correctly. Dealing with all possible resource update scenarios is difficult to get right, especially if, as is common, external resources can be modified without prior warning by code and/or users outside of the application’s direct control. If a resource unexpectedly changes during a computation, an application may observe multiple, inconsistent states of the resource, leading to incorrect program behavior.
This paper presents a sound and precise static analysis, Legato, that verifies consistent access patterns for external resources. Our analysis ensures that every value computed by an application reflects a single, consistent version of every external resource’s state. Although consistent computation in the presence of concurrent resource updates is fundamentally a concurrency issue, our analysis relies on the novel at-most-once condition to avoid explicitly reasoning about concurrency. The at-most-once condition requires that all values depend on at most one access of each resource. Our analysis is flow-, field-, and context-sensitive. It scales to real-world Java programs while producing a moderate number of false positives. We applied Legato to 10 applications with dynamically updated configurations, and found several non-trivial consistency bugs.
Sat 21 JulDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
11:00 - 12:40 | |||
11:00 25mResearch paper | Defensive Points-To Analysis: Effective Soundness via Laziness ECOOP Research Papers DOI | ||
11:25 25mResearch paper | Legato: An At-Most-Once Analysis with Applications to Dynamic Configuration Updates ECOOP Research Papers DOI Pre-print | ||
11:50 25mResearch paper | Definite Reference Mutability ECOOP Research Papers Ana Milanova Rensselaer Polytechnic Institute DOI | ||
12:15 25mResearch paper | Efficient Reflection String Analysis via Graph Coloring ECOOP Research Papers Neville Grech University of Athens, George Kastrinis University of Athens, Yannis Smaragdakis University of Athens DOI |