In the simply-typed lambda-calculus we can recover the full range of expressiveness of the untyped lambda-calculus solely by adding a single recursive type U = U -> U. In contrast, in the session-typed pi-calculus, recursion alone is insufficient to recover the untyped pi-calculus, primarily due to linearity: each channel just has two unique endpoints. In this paper, we show that shared channels with a corresponding sharing semantics (based on the language SILL_S developed in prior work) are enough to embed the untyped asynchronous pi-calculus via a universal shared session type U_S. We show that our encoding of the asynchronous pi-calculus satisfies operational correspondence and preserves observable actions (i.e., processes are weakly bisimilar to their encoding). Moreover, we clarify the expressiveness of SILL_S by developing an operationally correct encoding of SILL_S in the asynchronous pi-calculus.
more »
« less
Manifest Deadlock-Freedom for Shared Session Types
Shared session types generalize the Curry-Howard correspondence between intuitionistic linear logic and the session-typed pi-calculus with adjoint modalities that mediate between linear and shared session types, giving rise to a programming model where shared channels must be used according to a locking discipline of acquire-release. While this generalization greatly increases the range of programs that can be written, the gain in expressiveness comes at the cost of deadlock-freedom, a property which holds for many linear session type systems. In this paper, we develop a type system for logically-shared sessions in which types capture not only the interactive behavior of processes but also constrain the order of resources (i.e., shared processes) they may acquire. This type-level information is then used to rule out cyclic dependencies among acquires and synchronization points, resulting in a system that ensures deadlock-free communication for well-typed processes in the presence of shared sessions, higher-order channel passing, and recursive processes. We illustrate our approach on a series of examples, showing that it rules out deadlocks in circular networks of both shared and linear recursive processes, while still being permissive enough to type concurrent implementations of shared imperative data structures as processes.
more »
« less
- Award ID(s):
- 1718267
- PAR ID:
- 10099208
- Date Published:
- Journal Name:
- 28th European Symposium on Programming (ESOP) 2019
- Volume:
- 11423
- Page Range / eLocation ID:
- 611-639
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
null (Ed.)Programming digital contracts comes with unique challenges, which include (i) expressing and enforcing protocols of interaction, (ii) controlling resource usage, and (iii) preventing the duplication or deletion of a contract's assets. This article presents the design and type-theoretic foundation of Nomos, a programming language for digital contracts that addresses these challenges. To express and enforce protocols, Nomos is based on shared binary session types. To control resource usage, Nomos employs automatic amortized resource analysis. To prevent the duplication or deletion of assets, Nomos uses a linear type system. A monad integrates the effectful session-typed language with a general-purpose functional language. Nomos' prototype implementation features linear-time type checking and efficient type reconstruction that includes automatic inference of resource bounds via off-the-shelf linear optimization. The effectiveness of the language is evaluated with case studies on implementing common smart contracts such as auctions, elections, and currencies. Nomos is completely formalized, including the type system, a cost semantics, and a transactional semantics to deploy Nomos contracts on a blockchain. The type soundness proof ensures that protocols are followed at run-time and that types establish sound upper bounds on the resource consumption, ruling out re-entrancy and out-of-gas vulnerabilities.more » « less
-
This paper presents a formulation of multiparty session types (MPSTs) for practical fault-tolerant distributed programming. We tackle the challenges faced by session types in the context of distributed systems involving asynchronous and concurrent partial failures – such as supporting dynamic replacement of failed parties and retrying failed protocol segments in an ongoing multiparty session – in the presence of unreliable failure detection. Key to our approach is that we develop a novel model of event-driven concurrency for multiparty sessions. Inspired by real-world practices, it enables us to unify the session-typed handling of regular I/O events with failure handling and the combination of features needed to express practical fault-tolerant protocols. Moreover, the characteristics of our model allow us to prove a global progress property for well-typed processes engaged in multiple concurrent sessions, which does not hold in traditional MPST systems. To demonstrate its practicality, we implement our framework as a toolchain and runtime for Scala, and use it to specify and implement a session-typed version of the cluster management system of the industrial-strength Apache Spark data analytics framework. Our session-typed cluster manager composes with other vanilla Spark components to give a functioning Spark runtime; e.g., it can execute existing third-party Spark applications without code modification. A performance evaluation using the TPC-H benchmark shows our prototype implementation incurs an average overhead below 10%.more » « less
-
Morales, J.F. ; Orchard, D. (Ed.)In this paper, we describe our experience incorporating gradual types in a statically typed functional language with Hindley-Milner style type inference. Where most gradually typed systems aim to improve static checking in a dynamically typed language, we approach it from the opposite perspective and promote dynamic checking in a statically typed language. Our approach provides a glimpse into how languages like SML and OCaml might handle gradual typing. We discuss our implementation and challenges faced—specifically how gradual typing rules apply to our representation of composite and recursive types. We review the various implementations that add dynamic typing to a statically typed language in order to highlight the different ways of mixing static and dynamic typing and examine possible inspirations while maintaining the gradual nature of our type system. This paper also discusses our motivation for adding gradual types to our language, and the practical benefits of doing so in our industrial setting.more » « less
-
Mixed-typed languages enable programmers to link typed and untyped components in various ways. Some offer rich type systems to facilitate the smooth migration of untyped code to the typed world; others merely provide a convenient form of type Dynamic together with a conventional structural type system. Orthogonal to this dimension, Natural systems ensure the integrity of types with a sophisticated contract system, while Transient systems insert simple first-order checks at strategic places within typed code. Furthermore, each method of ensuring type integrity comes with its own blame-assignment strategy. Typed Racket has a rich migratory type system and enforces the types with a Natural semantics. Reticulated Python has a simple structural type system extended with Dynamic and enforces types with a Transient semantics. While Typed Racket satisfies the most stringent gradual-type soundness properties at a significant performance cost, Reticulated Python seems to limit the performance penalty to a tolerable degree and is nevertheless type sound. This comparison raises the question of whether Transient checking is applicable to and beneficial for a rich migratory type system. This paper reports on the surprising difficulties of adapting the Transient semantics of Reticulated Python to the rich migratory type system of Typed Racket. The resulting implementation, Shallow Typed Racket, is faster than the standard Deep Typed Racket but only when the Transient blame assignment strategy is disabled. For language designers, this report provides valuable hints on how to equip an existing compiler to support a Transient semantics. For theoreticians, the negative experience with Transient blame calls for a thorough investigation of this strategy.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/10.1007/978-3-030-17184-1_22
