×

A concurrent lambda calculus with futures. (English) Zbl 1110.68023

Summary: We introduce a new lambda calculus with futures, \(\lambda (\text{fut})\), that models the operational semantics of concurrent statically typed functional programming languages with mixed eager and lazy threads such as Alice ML, a concurrent extension of Standard ML. \(\lambda (\text{fut})\) is a minimalist extension of the call-by-value \(\lambda\)-calculus that is sufficiently expressive to define and combine a variety of standard concurrency abstractions, such as channels, semaphores, and ports. Despite its minimality, the basic machinery of \(\lambda (\text{fut})\) is sufficiently powerful to support explicit recursion and call-by-need evaluation.
We present a static type system for \(\lambda (\text{fut})\) and distinguish a fragment of \(\lambda (\text{fut})\) that we prove to be uniformly confluent. This result confirms our intuition that reference cells are the sole source of indeterminism. This fragment assumes the absence of so called handle errors that violate the single assignment assumption of \(\lambda (\text{fut})\)’s handled future-construct.
Finally, we present a linear type system for \(\lambda (\text{fut})\) by which to prove the absence of handle errors. Our system is rich enough to type definitions of the above mentioned concurrency abstractions. Consequently, these cannot be corrupted in any (not necessarily linearly) well-typed context.

MSC:

68N18 Functional programming and lambda calculus
68Q55 Semantics in the theory of computing

Software:

Pict; Oz; JoCaml; Multilisp
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Abadi, M.; Lamport, L., Conjoining specifications, ACM Trans. Programming Languages and Systems, 17, 3, 507-534 (1995)
[2] Ariola, Z. M.; Felleisen, M., The call-by-need lambda calculus, J. Funct. Programming, 7, 3, 265-301 (1997) · Zbl 0887.68007
[3] Ariola, Z. M.; Klop, J. W., Lambda calculus with explicit recursion, Inform. and Comput., 139, 2, 154-233 (1997) · Zbl 0892.68015
[4] Arvind; Nikhil, R. S.; Pingali, K. K., I-structures: data structures for parallel computing, ACM Trans. Programming Languages and Systems, 11, 4, 598-632 (1989)
[5] Baker, H.; Hewitt, C., The incremental garbage collection of processes, ACM Sigplan Notices, 12, 55-59 (1977)
[6] E. Barendsen, S. Smetsers, Uniqueness type inference, in: Proc. PLILP’95, Lecture Notes in Computer Science, Vol. 982, Springer, 1995, pp. 189-206.; E. Barendsen, S. Smetsers, Uniqueness type inference, in: Proc. PLILP’95, Lecture Notes in Computer Science, Vol. 982, Springer, 1995, pp. 189-206. · Zbl 0910.68096
[7] G. Boudol, The \(\operatorname{\Pi;} \)-calculus in direct style, in: 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1997, pp. 228-241.; G. Boudol, The \(\operatorname{\Pi;} \)-calculus in direct style, in: 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1997, pp. 228-241.
[8] Caromel, D.; Henrio, L., A Theory of Distributed Objects (2005), Springer: Springer Berlin · Zbl 1084.68012
[9] E. Chailloux, P. Manoury, B. Pagano, Developing Applications With Objective Caml, O’Reilly, 2000, available online at \(\langle;\) http://caml.inria.fr/oreilly-book \(\rangle;\).; E. Chailloux, P. Manoury, B. Pagano, Developing Applications With Objective Caml, O’Reilly, 2000, available online at \(\langle;\) http://caml.inria.fr/oreilly-book \(\rangle;\).
[10] S. Conchon, F.L. Fessant, Jocaml: mobile agents for objective-caml, in: First International Symposium on Agent Systems and Applications (ASA’99)/Third International Symposium on Mobile Agents (MA’99), 1999.; S. Conchon, F.L. Fessant, Jocaml: mobile agents for objective-caml, in: First International Symposium on Agent Systems and Applications (ASA’99)/Third International Symposium on Mobile Agents (MA’99), 1999.
[11] Flanagan, C.; Felleisen, M., The semantics of future and an application, J. Funct. Programming, 9, 1, 1-31 (1999) · Zbl 0926.68075
[12] Fournet, C.; Gonthier, G., The reflexive chemical abstract machine and the join-calculus, (Proc. POPL’96 (1996), ACM Press: ACM Press New York), 372-385
[13] C. Fournet, C. Laneve, L. Maranget, D. Rémy, Implicit typing à la ML for the join-calculus, in: Proceedings of the CONCUR’97, Lecture Notes in Computer Science, Vol. 1243, Springer, Berlin, 1997, pp. 196-212.; C. Fournet, C. Laneve, L. Maranget, D. Rémy, Implicit typing à la ML for the join-calculus, in: Proceedings of the CONCUR’97, Lecture Notes in Computer Science, Vol. 1243, Springer, Berlin, 1997, pp. 196-212.
[14] Halstead, R. H., Multilisp: a language for concurrent symbolic computation, ACM Trans. Programming Languages and Systems, 7, 4, 501-538 (1985) · Zbl 0581.68037
[15] Haridi, S.; Van Roy, P.; Brand, P.; Mehl, M.; Scheidhauer, R.; Smolka, G., Efficient logic variables for distributed computing, ACM Trans. Programming Languages and Systems, 21, 3, 569-626 (1999)
[16] Jeffrey, A.; Rathke, J., A fully abstract may testing semantics for concurrent objects, (Proc. Lics 2002, 17th Annual Symposium on Logic in Computer Science (2002)), 101-112
[17] Jones, S. P.; Gordon, A.; Finne, S., Concurrent Haskell, (Proc. POPL’96 (1996), ACM Press: ACM Press New York), 295-308
[18] Kobayashi, N.; Pierce, B. C.; Turner, D. N., Linearity and the pi-calculus, ACM Trans. Programming Languages and Systems, 21, 5, 914-947 (1999)
[19] Landin, P. J., The mechanical evaluation of expressions, Comput. J., 6, 4, 308-320 (1964) · Zbl 0122.36106
[20] Liskov, B.; Shrira, L., Promises: linguistic support for efficient asynchronous procedure calls in distributed systems, SIGPLAN Notices, 23, 7, 260-267 (1988)
[21] Maraist, J.; Odersky, M.; Wadler, P., The call-by-need lambda calculus, J. Funct. Programming, 8, 3, 275-317 (1998) · Zbl 0918.03019
[22] R. Milner, The polyadic \(\operatorname{\Pi;} \)-calculus: a tutorial, in: F.L. Bauer, W. Brauer, H. Schwichtenberg (Eds.), Logic and Algebra of Specification, Proc. Marktoberdorf Summer School, Springer, Berlin, 1993, pp. 203-246.; R. Milner, The polyadic \(\operatorname{\Pi;} \)-calculus: a tutorial, in: F.L. Bauer, W. Brauer, H. Schwichtenberg (Eds.), Logic and Algebra of Specification, Proc. Marktoberdorf Summer School, Springer, Berlin, 1993, pp. 203-246.
[23] Milner, R.; Tofte, M.; Harper, R.; MacQueen, D. B., The Standard ML Programming Language (Revised) (1997), MIT Press: MIT Press Cambridge, MA
[24] Moreau, L., The semantics of scheme with future, (Internat. Conference on Functional Programming (1996), ACM Press: ACM Press New York), 146-156 · Zbl 1345.68066
[25] M. Müller, Set-based failure diagnosis for concurrent constraint programming, Ph.D. Thesis, Saarland University, Saarbrücken, 1998.; M. Müller, Set-based failure diagnosis for concurrent constraint programming, Ph.D. Thesis, Saarland University, Saarbrücken, 1998.
[26] Niehren, J., Uniform confluence in concurrent computation, J. Funct. Programming, 10, 5, 453-499 (2000) · Zbl 0974.68061
[27] J. Niehren, J. Schwinghammer, G. Smolka, A concurrent lambda calculus with futures, in: B. Gramlich (Ed.), Frontiers of Combining Systems, Lecture Notes in Artificial Intelligence, Vol. 3717, Springer, Berlin, 2005, pp. 248-263.; J. Niehren, J. Schwinghammer, G. Smolka, A concurrent lambda calculus with futures, in: B. Gramlich (Ed.), Frontiers of Combining Systems, Lecture Notes in Artificial Intelligence, Vol. 3717, Springer, Berlin, 2005, pp. 248-263. · Zbl 1171.68409
[28] F. Nielson (Ed.), ML with Concurrency: Design, Analysis, Implementation, and Application, Monographs in Computer Science, Springer, Berlin, 1997.; F. Nielson (Ed.), ML with Concurrency: Design, Analysis, Implementation, and Application, Monographs in Computer Science, Springer, Berlin, 1997.
[29] Pierce, B. C.; Turner, D. N., Pict: a programming language based on the pi-calculus, (Plotkin, G.; Stirling, C.; Tofte, M., Proof, Language and Interaction: Essays in Honour of Robin Milner (2000), MIT Press: MIT Press Cambridge, MA)
[30] Reppy, J. H., Concurrent Programming in ML (1999), Cambridge University Press: Cambridge University Press Cambridge · Zbl 1137.68409
[31] A. Rossberg, Generativity and dynamic opacity for abstract types, in: Proc. Fifth Internat. ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP’03), ACM Press, New York, 2003, pp. 241-252.; A. Rossberg, Generativity and dynamic opacity for abstract types, in: Proc. Fifth Internat. ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP’03), ACM Press, New York, 2003, pp. 241-252.
[32] A. Rossberg, The missing link—dynamic components for ML, in: Eleventh International Conference on Fuctional Programming, ACM Press 2006.; A. Rossberg, The missing link—dynamic components for ML, in: Eleventh International Conference on Fuctional Programming, ACM Press 2006.
[33] A. Rossberg, D.L. Botlan, G. Tack, T. Brunklaus, G. Smolka, Alice through the looking glass, Trends in Functional Programming, Vol. 5, Intellect Books, Bristol, UK, Munich, Germany, 2006 pp. 77-96 (Chapter 6) (ISBN 1-84150144-1).; A. Rossberg, D.L. Botlan, G. Tack, T. Brunklaus, G. Smolka, Alice through the looking glass, Trends in Functional Programming, Vol. 5, Intellect Books, Bristol, UK, Munich, Germany, 2006 pp. 77-96 (Chapter 6) (ISBN 1-84150144-1).
[34] Saraswat, V. A.; Rinard, M.; Panangaden, P., Semantic foundations of concurrent constraint programming, (Proc. POPL’91 (1991), ACM Press: ACM Press New York), 333-352
[35] Shapiro, E., The family of concurrent logic programming languages, ACM Comput. Surveys, 21, 3, 413-510 (1989)
[36] G. Smolka, The Oz programming model, in: J. van Leeuwen (Ed.), Computer Science Today, Lecture Notes in Computer Science, Vol. 1000, Springer, Berlin, 1995, pp. 324-343.; G. Smolka, The Oz programming model, in: J. van Leeuwen (Ed.), Computer Science Today, Lecture Notes in Computer Science, Vol. 1000, Springer, Berlin, 1995, pp. 324-343.
[37] G. Tack, L. Kornstaedt, G. Smolka, Generic pickling and minimization, ENTCS 148 (2) (2006) 79-103.; G. Tack, L. Kornstaedt, G. Smolka, Generic pickling and minimization, ENTCS 148 (2) (2006) 79-103.
[38] The Alice Project, web site at the Programming Systems Lab, Saarland University \(\langle;\) http://www.ps.uni-sb.de/alice \(\rangle;\), 2006.; The Alice Project, web site at the Programming Systems Lab, Saarland University \(\langle;\) http://www.ps.uni-sb.de/alice \(\rangle;\), 2006.
[39] Turner, D. N.; Wadler, P.; Mossin, C., Once upon a type, (Proc. Seventh ICFPCA (1995), ACM Press: ACM Press New York), 1-11
[40] P.Wadler, Linear types can change the world!, in: M.Broy, C.B. Jones(Eds.), Programming Concepts and Methods, 1990 North-Holland, Amsterdam, pp.546-566.; P.Wadler, Linear types can change the world!, in: M.Broy, C.B. Jones(Eds.), Programming Concepts and Methods, 1990 North-Holland, Amsterdam, pp.546-566.
[41] Wright, A. K., Simple imperative polymorphism, Lisp and Symbolic Comput., 8, 4, 343-355 (1995)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.