Article

A capability calculus for concurrency and determinism

Authors:

Tachio Terauchi,

Alex AikenAuthors Info & Claims

CONCUR'06: Proceedings of the 17th international conference on Concurrency Theory

Pages 218 - 232

https://doi.org/10.1007/11817949_15

Published: 27 August 2006 Publication History

Publisher Site

Abstract

We present a capability calculus for checking partial confluence of channel-communicating concurrent processes. Our approach automatically detects more programs to be partially confluent than previous approaches and is able to handle a mix of different kinds of communication channels, including shared reference cells.

References

[1]

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

Digital Library

Google Scholar

[2]

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

Digital Library

Google Scholar

[3]

J. Boyland. Checking interference with fractional permissions. In R. Cousot, editor, Static Analysis, Tenth International Symposium, volume 2694 of Lecture Notes in Computer Science, pages 55-72, San Diego, CA, June 2003. Springer-Verlag.

Digital Library

Google Scholar

[4]

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

Digital Library

Google Scholar

[5]

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

Digital Library

Google Scholar

[6]

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

Digital Library

Google Scholar

[7]

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

Google Scholar

[8]

N. Kobayashi, B. C. Pierce, and D. N. Turner. Linearity and the pi-calculus. ACM Transactions on Programming Languages and Systems, 21(5):914-947, Sept. 1999.

Digital Library

Google Scholar

[9]

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

Digital Library

Google Scholar

[10]

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

Google Scholar

[11]

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

Digital Library

Google Scholar

[12]

T. Terauchi and A. Aiken. A capability calculus for concurrency and determinism. Technical Report UCB/EECS-2006-84, University of California, Berkeley, 2006.

Digital Library

Google Scholar

[13]

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

Digital Library

Google Scholar

Cited By

View all

Chaudhuri SGulwani SLublinerman R(2010)Continuity analysis of programsACM SIGPLAN Notices10.1145/1707801.170630845:1(57-70)Online publication date: 17-Jan-2010
https://dl.acm.org/doi/10.1145/1707801.1706308
Chaudhuri SGulwani SLublinerman RHermenegildo MPalsberg J(2010)Continuity analysis of programsProceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/1706299.1706308(57-70)Online publication date: 17-Jan-2010
https://dl.acm.org/doi/10.1145/1706299.1706308
Terauchi TMegacz A(2008)Inferring channel buffer bounds via linear programmingProceedings of the Theory and practice of software, 17th European conference on Programming languages and systems10.5555/1792878.1792907(284-298)Online publication date: 29-Mar-2008
https://dl.acm.org/doi/10.5555/1792878.1792907
Show More Cited By

A capability calculus for concurrency and determinism
1. Theory of computation

Recommendations

A capability calculus for concurrency and determinism

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 ...
Semantics-based concurrency control: beyond commutativity

The concurrency of transactions executing on atomic data types can be enhanced through the use of semantic information about operations defined on these types. Hitherto, commutativity of operations has been exploited to provide enchanced concurrency ...
Concurrency Theory of cyclic and acyclic processes

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

CONCUR'06: Proceedings of the 17th international conference on Concurrency Theory

August 2006

524 pages

ISBN:3540373764

Editors:
Christel Baier
Institute for Theoretical Computer Science, Technical University Dresden, Germany
,
Holger Hermanns
Institute for Theoretical Computer Science, INRIA, VASY, Grenoble Rhône-Alpes, France

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 27 August 2006

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 30 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Chaudhuri SGulwani SLublinerman R(2010)Continuity analysis of programsACM SIGPLAN Notices10.1145/1707801.170630845:1(57-70)Online publication date: 17-Jan-2010
https://dl.acm.org/doi/10.1145/1707801.1706308
Chaudhuri SGulwani SLublinerman RHermenegildo MPalsberg J(2010)Continuity analysis of programsProceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/1706299.1706308(57-70)Online publication date: 17-Jan-2010
https://dl.acm.org/doi/10.1145/1706299.1706308
Terauchi TMegacz A(2008)Inferring channel buffer bounds via linear programmingProceedings of the Theory and practice of software, 17th European conference on Programming languages and systems10.5555/1792878.1792907(284-298)Online publication date: 29-Mar-2008
https://dl.acm.org/doi/10.5555/1792878.1792907
Terauchi TAiken A(2008)A capability calculus for concurrency and determinismACM Transactions on Programming Languages and Systems10.1145/1387673.138767630:5(1-30)Online publication date: 4-Sep-2008
https://dl.acm.org/doi/10.1145/1387673.1387676
Terauchi T(2008)Checking race freedom via linear programmingACM SIGPLAN Notices10.1145/1379022.137558343:6(1-10)Online publication date: 7-Jun-2008
https://dl.acm.org/doi/10.1145/1379022.1375583
Terauchi TGupta RAmarasinghe S(2008)Checking race freedom via linear programmingProceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/1375581.1375583(1-10)Online publication date: 7-Jun-2008
https://dl.acm.org/doi/10.1145/1375581.1375583
Terauchi TAiken A(2008)Witnessing side effectsACM Transactions on Programming Languages and Systems (TOPLAS)10.1145/1353445.135344930:3(1-42)Online publication date: 21-May-2008
https://dl.acm.org/doi/10.1145/1353445.1353449
Kobayashi NSangiorgi D(2008)A Hybrid Type System for Lock-Freedom of Mobile ProcessesProceedings of the 20th international conference on Computer Aided Verification10.1007/978-3-540-70545-1_10(80-93)Online publication date: 7-Jul-2008
https://dl.acm.org/doi/10.1007/978-3-540-70545-1_10
Kikuchi DKobayashi N(2007)Type-based verification of correspondence assertions for communication protocolsProceedings of the 5th Asian conference on Programming languages and systems10.5555/1784774.1784793(191-205)Online publication date: 29-Nov-2007
https://dl.acm.org/doi/10.5555/1784774.1784793

Abstract

References

Cited By

Recommendations