Correctness of Partial Escape Analysis for Multithreading Optimization
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 JunDisplayed 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