Write a Blog >>
Tue 20 Jun 2017 16:20 - 16:55 at Vertex WS217 - D Chair(s): Radu Grigore

Compilers often use escape analysis to elide locking operations on thread-local data. Similarly, dynamic race detectors may use escape analysis to elide race checks on thread-local data. In this paper, we study the correctness of these two related optimizations when using a partial escape analysis, which identifies objects that are currently thread-local but that may later become thread-shared.

We show that lock elision based on partial escape analysis is unsound for the Java memory model. We also show that race check elision based on a partial escape analysis weakens the precision of dynamic race detectors. Finally, we prove that race check elision based on a partial escape analysis is sound with respect to this weakened, but still useful, notion of precision.

Tue 20 Jun

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 18:00
DFTfJP at Vertex WS217
Chair(s): Radu Grigore University of Kent
Consistency Types for Safe and Efficient Distributed Programming
Alessandro Margara Politecnico di Milano, Guido Salvaneschi TU Darmstadt
Correctness of Partial Escape Analysis for Multithreading Optimization
Dustin Rhodes , Cormac Flanagan University of California, Santa Cruz, Stephen N. Freund Williams College
Parametric trace expressions for runtime verification of Java-like programs
Davide Ancona University of Genova, Angelo Ferrando , Luca Franceschini DIBRIS, University of Genova, Italy, Viviana Mascardi DIBRIS, University of Genova, Italy