research-article

Open access

A capability calculus for concurrency and determinism

Authors:

Tachio Terauchi,

Alex AikenAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 30, Issue 5

Article No.: 27, Pages 1 - 30

https://doi.org/10.1145/1387673.1387676

Published: 04 September 2008 Publication History

Abstract

This article presents a static system for checking determinism (technically, partial confluence) of communicating concurrent processes. Our approach automatically detects partial confluence in programs communicating via a mix of different kinds of communication methods: rendezvous channels, buffered channels, broadcast channels, and reference cells. Our system reduces the partial confluence checking problem in polynomial time (in the size of the program) to the problem of solving a system of rational linear inequalities, and is thus efficient.

References

[1]

Aiken, A. and Gay, D. 1998. Barrier inference. In Proceedings of the 25th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 342--354.

Digital Library

[2]

Blom, S. and van de Pol, J. 2002. State space reduction by proving confluence. In Proceedings of the 14th International Conference on Computer Aided Verification. 596--609.

Digital Library

[3]

Boudol, G. 1992. Asynchrony and the pi-calculus. Tech. rep. 1702, INRIA Sophia Antipolis.

[4]

Boyland, J. 2003. Checking interference with fractional permissions. In Proceedings of the 10th International Symposium on Static Ananysis. 55--72.

Digital Library

[5]

Coates, W. S., Lexau, J. K., Jones, I. W., Fairbanks, S. M., and Sutherland, I. E. 2001. Fleetzero: An asynchronous switching experiment. In Proceedings of the 7th International Symposium on Advanced Research in Asynchronous Circuits and Systems (ASYNC'01). IEEE Computer Society.

Digital Library

[6]

Crary, K., Walker, D., and Morrisett, G. 1999. Typed memory management in a calculus of capabilities. In Proceedings of the 26th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 262--275.

Digital Library

[7]

DeLine, R. and Fähndrich, M. 2001. Enforcing High-Level Protocols in Low-Level Software. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. 1, 59--69.

Digital Library

[8]

Edwards, S. A. and Tardieu, O. 2005. Shim: a deterministic model for heterogeneous embedded systems. In Proceedings of the 5th ACM International Conference On Embedded Software. 264--272.

Digital Library

[9]

Foster, J. S., Terauchi, T., and Aiken, A. 2002. Flow-sensitive type qualifiers. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation.

Digital Library

[10]

Gordon, A. D. and Jeffrey, A. 2001. Typing correspondence assertions for communication protocols. Theor. Comput. Sci. 45.

Digital Library

[11]

Gordon, A. D. and Jeffrey, A. 2002. Types and Effects for Asymmetric Cryptographic Protocols. IEEE Computer Society.

[12]

Groote, J. F. and van de Pol, J. 2000. State space reduction using partial tau-confluence. In Proceedings of 25th International Symposium on the Mathematical Foundations of Computer Science. 383--393.

Digital Library

[13]

Hansen, H. and Valmari, A. 2006. Operational determinism and fast algorithms. In Concurrency Theory, 17th International Conference (CONCUR'06). Vol. 4137. Springer, 188--202.

Digital Library

[14]

Honda, K. and Tokoro, M. 1992. On asynchronous communication semantics. In Proceedings of the European Conference on Object-Oriented Programming Workshop on Object-Based Concurrent Computing. Springer-Verlag, 21--51.

Digital Library

[15]

Igarashi, A. and Kobayashi, N. 2004. A generic type system for the pi-calculus. Theor. Comput. Sci. 311, 1-3, 121--163.

Digital Library

[16]

Kahn, G. 1974. The semantics of a simple language for parallel programming In Information Processing. Stockholm, Sweden, 471--475.

[17]

Kobayashi, N. 2007. Personal communication.

[18]

Kobayashi, N., Nakade, M., and Yonezawa, A. 1995. Static analysis of communication for asynchronous concurrent programming languages. In Proceedings of the 2nd International Symposium on Static Analysis. Glasgow, Scotland, 225--242.

Digital Library

[19]

Kobayashi, N., Pierce, B. C., and Turner, D. N. 1999. Linearity and the pi-calculus. ACM Trans. Program. Lang. Syst. 21, 5, 914--947.

Digital Library

[20]

König, B. 2000. Analysing input/output-capabilities of mobile processes with a generic type system. In Proceedings of the 27th International Colloquium on Automata, Languages and Programming. 403--414.

Digital Library

[21]

Lee, E. A. 2006. The problem with threads. Tech. rep. UCB/EECS-2006-1, EECS Department, University of California, Berkeley.

[22]

Megacz, A. 2006. CCCD implementation. http://research.cs.berkeley.edu/project/cccd-impl/README.

[23]

Nestmann, U. and Steffen, M. 1997. Typing confluence. In Proceedings of FMICS '97. 77--101.

[24]

Smith, F., Walker, D., and Morrisett, G. 2000. Alias Types. In Proceedings of the 9th European Symposium on Programming, G. Smolka, Ed. Lecture Notes in Computer Science, vol. 1782. Springer-Verlag, Berlin, Germany, 366--381.

Digital Library

[25]

Sutter, H. and Larus, J. 2005. Software and the concurrency revolution. Queue 3, 7, 54--62.

Digital Library

[26]

Terauchi, T. and Aiken, A. 2005. Witnessing side-effects. In Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming. ACM, 105--115.

Digital Library

[27]

Terauchi, T. and Aiken, A. 2006. A capability calculus for concurrency and determinism. In Concurrency Theory, 17th International Conference (CONCUR'06). Vol. 4137. Springer, Bonn, Germany, 218--232.

Digital Library

[28]

Walker, D. and Morrisett, G. 2000. Alias types for recursive data structures. In Proceedings of the International Workshop on Types in Compilation. Montreal, Canada.

Digital Library

[29]

Wang, X. and Kwiatkowska, M. 2006. Compositional state space reduction using untangled actions. In Proceedings of the 13th International Workshop on Expressiveness in Concurrency (EXPRESS'06). 16--28.

[30]

Yoshida, N., Berger, M., and Honda, K. 2004. Strong normalisation in the pi-calculus. Inform. Comput. 191, 2, 145--202.

Digital Library

Cited By

Fava DSteffen M(2020)Ready, set, Go!Science of Computer Programming10.1016/j.scico.2020.102473195(102473)Online publication date: Sep-2020
https://doi.org/10.1016/j.scico.2020.102473
Boyland J(2013)Fractional permissionsAliasing in Object-Oriented Programming10.5555/2554511.2554526(270-288)Online publication date: 1-Jan-2013
https://dl.acm.org/doi/10.5555/2554511.2554526
Bocchino R(2013)Alias control for deterministic parallelismAliasing in Object-Oriented Programming10.5555/2554511.2554521(156-195)Online publication date: 1-Jan-2013
https://dl.acm.org/doi/10.5555/2554511.2554521
Show More Cited By

Index Terms

A capability calculus for concurrency and determinism
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Concurrent programming structures
2. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

Recommendations

Static lock capabilities for deadlock freedom
TLDI '12: Proceedings of the 8th ACM SIGPLAN workshop on Types in language design and implementation

We present a technique --- lock capabilities --- for statically verifying that multithreaded programs with locks will not deadlock. Most previous work on deadlock prevention requires a strict total order on all locks held simultaneously by a thread, but ...
Asserting and checking determinism for multithreaded programs
ESEC/FSE '09: Proceedings of the 7th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering

The trend towards processors with more and more parallel cores is increasing the need for software that can take advantage of parallelism. The most widespread method for writing parallel software is to use explicit threads. Writing correct multithreaded ...
Type-based safe resource deallocation for shared-memory concurrency
OOPSLA '12: Proceedings of the ACM international conference on Object oriented programming systems languages and applications

We propose a type system to guarantee safe resource deallocation for shared-memory concurrent programs by extending the previous type system based on fractional ownerships. Here, safe resource deallocation means that memory cells, locks, or threads are ...

Comments

Information & Contributors

Information

Published In

cover image ACM Transactions on Programming Languages and Systems

ACM Transactions on Programming Languages and Systems Volume 30, Issue 5

August 2008

193 pages

ISSN:0164-0925

EISSN:1558-4593

DOI:10.1145/1387673

Issue’s Table of Contents

Copyright © 2008 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 September 2008

Accepted: 01 November 2007

Revised: 01 October 2007

Received: 01 September 2007

Published in TOPLAS Volume 30, Issue 5

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

KAKENHAI

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

24
Total Citations
View Citations
581
Total Downloads

Downloads (Last 12 months)69
Downloads (Last 6 weeks)6

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Fava DSteffen M(2020)Ready, set, Go!Science of Computer Programming10.1016/j.scico.2020.102473195(102473)Online publication date: Sep-2020
https://doi.org/10.1016/j.scico.2020.102473
Boyland J(2013)Fractional permissionsAliasing in Object-Oriented Programming10.5555/2554511.2554526(270-288)Online publication date: 1-Jan-2013
https://dl.acm.org/doi/10.5555/2554511.2554526
Bocchino R(2013)Alias control for deterministic parallelismAliasing in Object-Oriented Programming10.5555/2554511.2554521(156-195)Online publication date: 1-Jan-2013
https://dl.acm.org/doi/10.5555/2554511.2554521
Bocchino R(2013)Alias Control for Deterministic ParallelismAliasing in Object-Oriented Programming. Types, Analysis and Verification10.1007/978-3-642-36946-9_7(156-195)Online publication date: 2013
https://doi.org/10.1007/978-3-642-36946-9_7
Boyland J(2013)Fractional PermissionsAliasing in Object-Oriented Programming. Types, Analysis and Verification10.1007/978-3-642-36946-9_10(270-288)Online publication date: 2013
https://doi.org/10.1007/978-3-642-36946-9_10
Muller SChong S(2012)Towards a practical secure concurrent languageACM SIGPLAN Notices10.1145/2398857.238462147:10(57-74)Online publication date: 19-Oct-2012
https://dl.acm.org/doi/10.1145/2398857.2384621
Muller SChong SLeavens GDwyer M(2012)Towards a practical secure concurrent languageProceedings of the ACM international conference on Object oriented programming systems languages and applications10.1145/2384616.2384621(57-74)Online publication date: 19-Oct-2012
https://dl.acm.org/doi/10.1145/2384616.2384621
Kawaguchi MRondon PBakst AJhala R(2012)Deterministic parallelism via liquid effectsACM SIGPLAN Notices10.1145/2345156.225407147:6(45-54)Online publication date: 11-Jun-2012
https://dl.acm.org/doi/10.1145/2345156.2254071
Kawaguchi MRondon PBakst AJhala RVitek JLin HTip F(2012)Deterministic parallelism via liquid effectsProceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2254064.2254071(45-54)Online publication date: 11-Jun-2012
https://dl.acm.org/doi/10.1145/2254064.2254071
Lu YPotter JZhang CXue J(2012)A type and effect system for determinism in multithreaded programsProceedings of the 21st European conference on Programming Languages and Systems10.1007/978-3-642-28869-2_26(518-538)Online publication date: 24-Mar-2012
https://dl.acm.org/doi/10.1007/978-3-642-28869-2_26
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Figures

Tables

Media

View Issue’s Table of Contents