TY - GEN
T1 - Isolating determinism in multi-threaded programs
AU - Ziarek, Lukasz
AU - Tiwary, Siddharth
AU - Jagannathan, Suresh
PY - 2012
Y1 - 2012
N2 - Futures are a program abstraction that express a simple form of fork-join parallelism. The expression future (e) declares that e can be evaluated concurrently with the future's continuation. Safe-futures provide additional deterministic guarantees, ensuring that all data dependencies found in the original (non-future annotated) version are respected. In this paper, we present a dynamic analysis for enforcing determinism of safe-futures in an ML-like language with dynamic thread creation and first-class references. Our analysis tracks the interaction between futures (and their continuations) with other explicitly defined threads of control, and enforces an isolation property that prevents the effects of a continuation from being witnessed by its future, indirectly through their interactions with other threads. Our analysis is defined via a lightweight capability-based dependence tracking mechanism that serves as a compact representation of an effect history. Implementation results support our premise that futures and threads can extract additional parallelism compared to traditional approaches for safe-futures.
AB - Futures are a program abstraction that express a simple form of fork-join parallelism. The expression future (e) declares that e can be evaluated concurrently with the future's continuation. Safe-futures provide additional deterministic guarantees, ensuring that all data dependencies found in the original (non-future annotated) version are respected. In this paper, we present a dynamic analysis for enforcing determinism of safe-futures in an ML-like language with dynamic thread creation and first-class references. Our analysis tracks the interaction between futures (and their continuations) with other explicitly defined threads of control, and enforces an isolation property that prevents the effects of a continuation from being witnessed by its future, indirectly through their interactions with other threads. Our analysis is defined via a lightweight capability-based dependence tracking mechanism that serves as a compact representation of an effect history. Implementation results support our premise that futures and threads can extract additional parallelism compared to traditional approaches for safe-futures.
UR - https://www.scopus.com/pages/publications/84861216345
U2 - 10.1007/978-3-642-29860-8_6
DO - 10.1007/978-3-642-29860-8_6
M3 - Conference contribution
AN - SCOPUS:84861216345
SN - 9783642298592
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 63
EP - 77
BT - Runtime Verification - Second International Conference, RV 2011, Revised Selected Papers
T2 - 2nd International Conference on Runtime Verification, RV 2011
Y2 - 27 September 2011 through 30 September 2011
ER -