TY - GEN
T1 - Safe nondeterminism in a deterministic-by-default parallel language
AU - Bocchino, Robert L.
AU - Heumann, Stephen
AU - Honarmand, Nima
AU - Adve, Sarita V.
AU - Adve, Vikram S.
AU - Welc, Adam
AU - Shpeisman, Tatiana
PY - 2010
Y1 - 2010
N2 - A number of deterministic parallel programming models with strong safety guarantees are emerging, but similar support for nondeterministic algorithms, such as branch and bound search, remains an open question. We present a language together with a type and effect system that supports nondeterministic computations with a deterministic-by-default guarantee: nondeterminism must be explicitly requested via special parallel constructs (marked nd), and any deterministic construct that does not execute any nd construct has deterministic input-output behavior. Moreover, deterministic parallel constructs are always equivalent to a sequential composition of their constituent tasks, even if they enclose, or are enclosed by, nd constructs. Finally, in the execution of nd constructs, interference may occur only between pairs of accesses guarded by atomic statements, so there are no data races, either between atomic statements and unguarded accesses (strong isolation) or between pairs of unguarded accesses (stronger than strong isolation alone). We enforce the guarantees at compile time with modular checking using novel extensions to a previously described effect system. Our effect system extensions also enable the compiler to remove unnecessary transactional synchronization. We provide a static semantics, dynamic semantics, and a complete proof of soundness for the language, both with and without the barrier removal feature. An experimental evaluation shows that our language can achieve good scalability for realistic parallel algorithms, and that the barrier removal techniques provide significant performance gains.
AB - A number of deterministic parallel programming models with strong safety guarantees are emerging, but similar support for nondeterministic algorithms, such as branch and bound search, remains an open question. We present a language together with a type and effect system that supports nondeterministic computations with a deterministic-by-default guarantee: nondeterminism must be explicitly requested via special parallel constructs (marked nd), and any deterministic construct that does not execute any nd construct has deterministic input-output behavior. Moreover, deterministic parallel constructs are always equivalent to a sequential composition of their constituent tasks, even if they enclose, or are enclosed by, nd constructs. Finally, in the execution of nd constructs, interference may occur only between pairs of accesses guarded by atomic statements, so there are no data races, either between atomic statements and unguarded accesses (strong isolation) or between pairs of unguarded accesses (stronger than strong isolation alone). We enforce the guarantees at compile time with modular checking using novel extensions to a previously described effect system. Our effect system extensions also enable the compiler to remove unnecessary transactional synchronization. We provide a static semantics, dynamic semantics, and a complete proof of soundness for the language, both with and without the barrier removal feature. An experimental evaluation shows that our language can achieve good scalability for realistic parallel algorithms, and that the barrier removal techniques provide significant performance gains.
KW - Languages
KW - Performance
KW - Verification
UR - http://www.scopus.com/inward/record.url?scp=79952031302&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=79952031302&partnerID=8YFLogxK
U2 - 10.1145/1926385.1926447
DO - 10.1145/1926385.1926447
M3 - Conference contribution
AN - SCOPUS:79952031302
SN - 9781450304900
T3 - Conference Record of the Annual ACM Symposium on Principles of Programming Languages
SP - 535
EP - 548
BT - POPL'11 - Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
T2 - 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'11
Y2 - 26 January 2011 through 28 January 2011
ER -