A capability calculus for concurrency and determinism

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: Alexander Aiken , David Gay, Barrier inference, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.342-354, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268974]
• 2: Stefan Blom , Jaco van de Pol, State Space Reduction by Proving Confluence, Proceedings of the 14th International Conference on Computer Aided Verification, p.596-609, July 27-31, 2002
• 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.
• 5: William S. Coates , Jon K. Lexau , Ian W. Jones , Scott M. Fairbanks , Ivan E. Sutherland, FLEETzero: An Asynchronous Switching Experiment, Proceedings of the 7th International Symposium on Asynchronous Circuits and Systems, p.173, March 11-14, 2001
• 6: Karl Crary , David Walker , Greg Morrisett, Typed memory management in a calculus of capabilities, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.262-275, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292564]
• 7: Robert DeLine , Manuel Fähndrich, Enforcing high-level protocols in low-level software, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.59-69, June 2001, Snowbird, Utah, United States
• 8: Stephen A. Edwards , Olivier Tardieu, SHIM: a deterministic model for heterogeneous embedded systems, Proceedings of the 5th ACM international conference on Embedded software, September 18-22, 2005, Jersey City, NJ, USA [doi>10.1145/1086228.1086277]
• 9: Jeffrey S. Foster , Tachio Terauchi , Alex Aiken, Flow-sensitive type qualifiers, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 10: Gordon, A. D. and Jeffrey, A. 2001. Typing correspondence assertions for communication protocols. Theor. Comput. Sci. 45.
• 11: Gordon, A. D. and Jeffrey, A. 2002. Types and Effects for Asymmetric Cryptographic Protocols. IEEE Computer Society.
• 12: Jan Friso Groote , Jaco van de Pol, State Space Reduction Using Partial tau-Confluence, Proceedings of the 25th International Symposium on Mathematical Foundations of Computer Science, p.383-393, September 01, 2000
• 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.
• 14: Kohei Honda , Mario Tokoro, On Asynchronous Communication Semantics, Proceedings of the Workshop on Object-Based Concurrent Computing, p.21-51, July 15-16, 1991
• 15: Atsushi Igarashi , Naoki Kobayashi, A generic type system for the Pi-calculus, Theoretical Computer Science, v.311 n.1-3, p.121-163, 23 January 2004 [doi>10.1016/S0304-3975(03)00325-6]
• 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: Naoki Kobayashi , Motoki Nakade , Akinori Yonezawa, Static Analysis of Communication for Asynchronous Concurrent Programming Languages, Proceedings of the Second International Symposium on Static Analysis, p.225-242, September 25-27, 1995
• 19: Naoki Kobayashi , Benjamin C. Pierce , David N. Turner, Linearity and the pi-calculus, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.5, p.914-947, Sept. 1999 [doi>10.1145/330249.330251]
• 20: Barbara König, Analysing Input/Output-Capabilities of Mobile Processes with a Generic Type System, Proceedings of the 27th International Colloquium on Automata, Languages and Programming, p.403-414, July 09-15, 2000
• 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: Frederick Smith , David Walker , J. Gregory Morrisett, Alias Types, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.366-381, April 02, 2000
• 25: Herb Sutter , James Larus, Software and the concurrency revolution, Queue, v.3 n.7, September 2005 [doi>10.1145/1095408.1095421]
• 26: Tachio Terauchi , Alex Aiken, Witnessing side-effects, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 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.
• 28: David Walker , J. Gregory Morrisett, Alias Types for Recursive Data Structures, Selected papers from the Third International Workshop on Types in Compilation, p.177-206, September 21, 2000
• 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: Nobuko Yoshida , Martin Berger , Kohei Honda, Strong normalisation in the π-calculus, Information and Computation, v.191 n.2, p.145-202, 15 June 2004 [doi>10.1016/j.ic.2003.08.004]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Concurrent programming structures

Keywords:
Determinism, capabilities, type systems