A type and effect system for determinism in multithreaded programs

Lu, Yi, Potter, John, Zhang, Chenyi and Xue, Jingling (2012). A type and effect system for determinism in multithreaded programs. In: Helmut Seidl, Programming languages and systems: 21st European Symposium on Programming, ESOP 2012, Proceedings. European Symposium on Programming (ESOP), Tallinn, Estonia, (518-538). 24 March - 1 April 2012. doi:10.1007/978-3-642-28869-2_26


Author Lu, Yi
Potter, John
Zhang, Chenyi
Xue, Jingling
Title of paper A type and effect system for determinism in multithreaded programs
Conference name European Symposium on Programming (ESOP)
Conference location Tallinn, Estonia
Conference dates 24 March - 1 April 2012
Proceedings title Programming languages and systems: 21st European Symposium on Programming, ESOP 2012, Proceedings   Check publisher's open access policy
Journal name Lecture Notes in Computer Science   Check publisher's open access policy
Series Lecture Notes in Computer Science
Place of Publication Heidelberg, Germany
Publisher Springer
Publication Year 2012
Sub-type Fully published paper
DOI 10.1007/978-3-642-28869-2_26
ISBN 9783642288685
9783642288692
ISSN 0302-9743
1611-3349
Editor Helmut Seidl
Volume 7211
Start page 518
End page 538
Total pages 21
Collection year 2013
Language eng
Formatted Abstract/Summary
There has been much recent interest in supporting deterministic parallelism in imperative programs. Structured parallel programming models have used type systems or static analysis to enforce determinism by constraining potential interference of lexically scoped tasks. But similar support for multithreaded programming, where threads may be ubiquitously spawned with arbitrary lifetimes, especially to achieve a modular and manageable combination of determinism and nondeterminism in multithreaded programs, remains an open problem.
This paper proposes a simple and intuitive approach for tracking thread interference and capturing both determinism and nondeterminism as computational effects. This allows us to present a type and effect system for statically reasoning about determinism in multithreaded programs. Our general framework may be used in multithreaded languages for supporting determinism, or in structured parallel models for supporting threads. Even more sophisticated concurrency models, such as actors, are often implemented on top of an underlying threading model, thus the underlying ideas presented here should be of value in reasoning about the correctness of such implementations.
Q-Index Code E1
Q-Index Status Confirmed Code
Institutional Status UQ
Additional Notes Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012

 
Versions
Version Filter Type
Citation counts: Scopus Citation Count Cited 1 times in Scopus Article | Citations
Google Scholar Search Google Scholar
Created: Fri, 21 Sep 2012, 09:08:36 EST by Ms Imogen Ferrier on behalf of School of Information Technol and Elec Engineering