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 | |||
16:00 20mTalk | Consistency Types for Safe and Efficient Distributed Programming FTfJP | ||
16:20 35mTalk | Correctness of Partial Escape Analysis for Multithreading Optimization FTfJP Dustin Rhodes , Cormac Flanagan University of California, Santa Cruz, Stephen N. Freund Williams College | ||
16:55 35mTalk | Parametric trace expressions for runtime verification of Java-like programs FTfJP Davide Ancona University of Genova, Angelo Ferrando , Luca Franceschini DIBRIS, University of Genova, Italy, Viviana Mascardi DIBRIS, University of Genova, Italy |