Runtime Checking of Expressive Heap Assertions
Motivated by the unreliability of large software systems due to concurrency bugs and limitations of static analysis, the goal is to enable runtime analysis of deep semantic properties with low overhead. This involves checking expressive heap assertions at runtime with minimal impact on performance, reusing components of parallel GC and enabling reasoning about various path properties. A motivating example illustrates the importance of ensuring that every connection is reachable from at most one thread.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Runtime checking of expressive heap assertions Greta Yorsh, Martin Vechev, Eran Yahav, Bard Bloom
Motivation Reliability of large software systems illusive concurrency bugs, misuse of interfaces static analysis are inherently limited Vision: runtime analysis of deep semantic properties with low overhead testing, debugging, and production real applications leverage available system cores 2
Our goal Checking expressive heap assertions at runtime with low overhead reuse components of parallel GC Enable reasoning about path properties sharing reachability through/avoiding disjointness domination object ownership (encapsulation) thread ownership (concurrency) stack ownership (escape analysis) 3
Motivating Example: JdbF public class ConnectionSource { private Connection conn; private boolean used; public Connection getConnection() throws SQLEx { if (!used) { used = true; return conn; } throw new SQLEx(...); } public class Database { private ConnectionManager cm; public int insert(...) throws MappingEx { Connection c = cm.getConnection(...); ... } ... } public class ConnectionManager { private Map conns = Collections.synchronizedMap(new HashMap()); public Connection getConnection(String s) throws MappingException { try { ConnectionSource c = conns.get(s); if (c != null) return c.getConnection(); throw new MappingException(...); } catch (SQLEx e) { ... } } ... }
Root current thread Running Running Static Thread Database Thread Stack Connection Manager Stack HashMap Connection Source Connection Source Connection Source Connection Connection Connection every connection is reachable from at most one thread
Root current thread Running Running Static Thread Database Thread Stack Connection Manager Stack HashMap Connection Source Connection Source Connection Source Connection Connection Connection every connection is reachable from at most one thread
Motivating Example: JdbF public class ConnectionSource { private Connection conn; private boolean used; public Connection getConnection() throws SQLEx { if (!used) { used = true; return conn; } throw new SQLEx(...); } public class Database { private ConnectionManager cm; public int insert(...) throws MappingEx { Connection c = cm.getConnection(...); assert Phalanx.getThreadReach(c,cm) == 1 ... } ... } reachable from one thread (avoiding connection manager) every connection is only public class ConnectionManager { private Map conns = Collections.synchronizedMap(new HashMap()); public Connection getConnection(String s) throws MappingException { try { ConnectionSource c = conns.get(s); if (c != null) return c.getConnection(); throw new MappingException(...); } catch (SQLEx e) { ... } } ... }
Common Heap Queries Query Description Heap pred(o).size() > 0 Is o pointed to by a heap object? Sharing pred(o).size() > 1 Is o pointed to by two or more heap objects? Reachability reach(src).has(dst) Is dst reachable from src? Disjointnesss !(exists Object v; reach(o1).has(v); reach(o2).has(v)) Is there an object reachable from both o1 and o2? Ownership !(exists Object v ; reach(o).has(v) ; !dom(o,v)) Does o dominate all objects reachable from it? Reachability through !reach(o1,cut).has(o2) Does every path from o1 to o2 go through an object in cut Thread ownership dom(Thread.currentThread(), o) Does the current thread dominate o? ...
Subtle Semantics dom(x,y) = ? Root Running Thread Stack y x 9
Tool: Phalanx JML extended with additional primitives reach(Object o, Object[] avoiding) pred(Object o) dom(Object o1,Object o2) Modified JML compiler maps common queries to efficient implementation in Phalanx runtime
Experimental evaluation Implementation on top of QVM platform IBM J9 production virtual machine can leverage QVM adaptive overhead manager new parallel algorithms for common queries Implementation based on JVMTI less efficient, no parallel algorithms portable
Heap Assertions in Real Applications Application LOC Probes Violations AOI TVLA Azureus Freemind Frostwire JEdit jrisk rssowl tvbrowser 111,333 57,594 425,367 70,483 245,959 93,790 20,807 74,280 105,471 10 10 0 0 334 16 184 66 45 95 40 16 2 2 0 12 3 1
Disposal of Shared SWT Resources replace code of the form: exp.dispose(); with code of the form if (Phalanx.isShared(exp)) Phalanx.warning( disposal of \ shared resource +exp) ; exp.dispose();
Redundant Synchronization replace code of the form: synchronized(exp) { ... } with code of the form synchronized(exp) { if(Phalanx.dom(Thread.currentThread(),exp)) Phalanx.warning( synchronization on \ an owned object +exp) ; ... }
Summary common heap queries and usage scenarios new JML primitives modified JML compiler subtle semantics implementation parallel implementation in J9 production jvm portable implementation in JVMTI experimental evaluation real-world applications performance benchmarks 15
