Searcharxiv⌕ Search

arXiv subjects

Bas van den Heuvel

Publications and source records attributed to Bas van den Heuvel.

At least 19 recordsLinked to original sources

Partial Orders for Precise and Efficient Dynamic Deadlock Prediction

Deadlocks are a major source of bugs in concurrent programs. They are hard to predict, because they may only occur under specific scheduling conditions. Dynamic analysis attempts to identify potential deadlocks by examining a single execution trace of the program. A standard approach involves monitoring sequences of lock acquisitions in each thread, with the goal of identifying deadlock patterns. A deadlock pattern is characterized by a cyclic chain of lock acquisitions, where each lock is held by one thread while being requested by the next. However, it is well known that not all deadlock patterns identified in this way correspond to true deadlocks, as they may be impossible to manifest under any schedule. We tackle this deficiency by proposing a new method based on partial orders to eliminate false positives: lock acquisitions must be unordered under a given partial order, and not preceded by other deadlock patterns. We prove soundness (no falsely predicted deadlocks) for the novel TRW partial order, and completeness (no deadlocks missed) for a slightly weakened variant of TRW. Both partial orders can be computed efficiently and report the same deadlocks for an extensive benchmark suite.

cs.PL↗

A Gentle Overview of Asynchronous Session-based Concurrency: Deadlock Freedom by Typing

While formal models of concurrency tend to focus on synchronous communication, asynchronous communication is relevant in practice. In this paper, we will discuss asynchronous communication in the context of session-based concurrency, the model of computation in which session types specify the structure of the two-party protocols implemented by the channels of a communicating process. We overview recent work on addressing the challenge of ensuring the deadlock-freedom property for message-passing processes that communicate asynchronously in cyclic process networks governed by session types. We offer a gradual presentation of three typed process frameworks and outline how they may be used to guarantee deadlock freedom for a concurrent functional language with sessions.

cs.PL↗

Typed Non-determinism in Concurrent Calculi: The Eager Way

We consider the problem of designing typed concurrent calculi with non-deterministic choice in which types leverage linearity for controlling resources, thereby ensuring strong correctness properties for processes. This problem is constrained by the delicate tension between non-determinism and linearity. Prior work developed a session-typed π-calculus with standard non-deterministic choice; well-typed processes enjoy type preservation and deadlock-freedom. Central to this typed calculus is a lazy semantics that gradually discards branches in choices. This lazy semantics, however, is complex: various technical elements are needed to describe the non-deterministic behavior of typed processes. This paper develops an entirely new approach, based on an eager semantics, which more directly represents choices and commitment. We present a π-calculus in which non-deterministic choices are governed by this eager semantics and session types. We establish its key correctness properties, including deadlock-freedom, and demonstrate its expressivity by correctly translating a typed resource λ-calculus.

cs.LO↗

Asynchronous Session-Based Concurrency: Deadlock-freedom in Cyclic Process Networks

We tackle the challenge of ensuring the deadlock-freedom property for message-passing processes that communicate asynchronously in cyclic process networks. Our contributions are twofold. First, we present Asynchronous Priority-based Classical Processes (APCP), a session-typed process framework that supports asynchronous communication, delegation, and recursion in cyclic process networks. Building upon the Curry-Howard correspondences between linear logic and session types, we establish essential meta-theoretical results for APCP, most notably deadlock freedom. Second, we present a new concurrent $λ$-calculus with asynchronous session types, dubbed LASTn. We illustrate LASTn by example and establish its meta-theoretical results; in particular, we show how to soundly transfer the deadlock-freedom guarantee from APCP. To this end, we develop a translation of terms in LASTn into processes in APCP that satisfies a strong formulation of operational correspondence.

cs.LO↗

Comparing Session Type Systems derived from Linear Logic

Session types are a typed approach to message-passing concurrency, where types describe sequences of intended exchanges over channels. Session type systems have been given strong logical foundations via Curry-Howard correspondences with linear logic, a resource-aware logic that naturally captures structured interactions. These logical foundations provide an elegant framework to specify and (statically) verify message-passing processes. In this paper, we rigorously compare different type systems for concurrency derived from the Curry-Howard correspondence between linear logic and session types. We address the main divide between these type systems: the classical and intuitionistic presentations of linear logic. Over the years, these presentations have given rise to separate research strands on logical foundations for concurrency; the differences between their derived type systems have only been addressed informally. To formally assess these differences, we develop $π\mathsf{ULL}$, a session type system that encompasses type systems derived from classical and intuitionistic interpretations of linear logic. Based on a fragment of Girard's Logic of Unity, $π\mathsf{ULL}$ provides a basic reference framework: we compare existing session type systems by characterizing fragments of $π\mathsf{ULL}$ that coincide with classical and intuitionistic formulations. We analyze the significance of our characterizations by considering the locality principle (enforced by intuitionistic interpretations but not by classical ones) and forms of process composition induced by the interpretations.

cs.LO↗

Information Flow Control in Cyclic Process Networks

Protection of confidential data is an important security consideration of today's applications. Of particular concern is to guard against unintentional leakage to a (malicious) observer, who may interact with the program and draw inference from made observations. Information flow control (IFC) type systems address this concern by statically ruling out such leakage. This paper contributes an IFC type system for message-passing concurrent programs, the computational model of choice for many of today's applications such as cloud computing and IoT applications. Such applications typically either implicitly or explicitly codify protocols according to which message exchange must happen, and to statically ensure protocol safety, behavioral type systems such as session types can be used. This paper marries IFC with session typing and contributes over prior work in the following regards: (1) support of realistic cyclic process networks as opposed to the restriction to tree-shaped networks, (2) more permissive, yet entirely secure, IFC control, exploiting cyclic process networks, and (3) considering deadlocks as another form of side channel, and asserting deadlock-sensitive noninterference (DSNI) for well-typed programs. To prove DSNI, the paper develops a novel logical relation that accounts for cyclic process networks. The logical relation is rooted in linear logic, but drops the tree-topology restriction imposed by prior work.

cs.LO↗

Correctly Communicating Software: Distributed, Asynchronous, and Beyond (extended version)

Much of the software we use in everyday life consists of distributed components (running on separate cores or even computers) that collaborate through communication (by exchanging messages). It is crucial to develop robust methods that can give reliable guarantees about the behavior of such message-passing software. With a focus on session types as communication protocols and their foundations in logic, this thesis revolves around the following question: How can we push the boundaries of the logical foundations of session types (binary and multiparty), extending their expressiveness and applicability, while preserving fundamental correctness properties? In this context, this thesis studies several intertwined aspects of message-passing.

cs.LO↗

Monitoring Blackbox Implementations of Multiparty Session Protocols

We present a framework for the distributed monitoring of networks of components that coordinate by message-passing, following multiparty session protocols specified as global types. We improve over prior works by (i) supporting components whose exact specification is unknown ("blackboxes") and (ii) covering protocols that cannot be analyzed by existing techniques. We first give a procedure for synthesizing monitors for blackboxes from global types, and precisely define when a blackbox correctly satisfies its global type. Then, we prove that monitored blackboxes are sound (they correctly follow the protocol) and transparent (blackboxes with and without monitors are behaviorally equivalent).

cs.PL↗

Typed Non-determinism in Functional and Concurrent Calculi

We study functional and concurrent calculi with non-determinism, along with type systems to control resources based on linearity. The interplay between non-determinism and linearity is delicate: careless handling of branches can discard resources meant to be used exactly once. Here we go beyond prior work by considering non-determinism in its standard sense: once a branch is selected, the rest are discarded. Our technical contributions are three-fold. First, we introduce a $π$-calculus with non-deterministic choice, governed by session types. Second, we introduce a resource $λ$-calculus, governed by intersection types, in which non-determinism concerns fetching of resources from bags. Finally, we connect our two typed non-deterministic calculi via a correct translation.

cs.LO↗

Asynchronous Functional Sessions: Cyclic and Concurrent (Extended Version)

We present Concurrent GV (CGV), a functional calculus with message-passing concurrency governed by session types. With respect to prior calculi, CGV has increased support for concurrent evaluation and for cyclic network topologies. The design of CGV draws on APCP, a session-typed asynchronous pi-calculus developed in prior work. Technical contributions are (i) the syntax, semantics, and type system of CGV; (ii) a correct translation of CGV into APCP; (iii) a technique for establishing deadlock-free CGV programs, by resorting to APCP's priority-based type system.

cs.LO↗

A Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in Channel-Based Concurrency

The emergence of propositions-as-sessions, a Curry-Howard correspondence between propositions of Linear Logic and session types for concurrent processes, has settled the logical foundations of message-passing concurrency. Central to this approach is the resource consumption paradigm heralded by Linear Logic. In this paper, we investigate a new point in the design space of session type systems for message-passing concurrent programs. We identify O'Hearn and Pym's Logic of Bunched Implications (BI) as a fruitful basis for an interpretation of the logic as a concurrent programming language. This leads to a treatment of non-linear resources that is radically different from existing approaches based on Linear Logic. We introduce a new $π$-calculus with sessions, called $π$BI; its most salient feature is a construct called spawn, which expresses new forms of sharing that are induced by structural principles in BI. We illustrate the expressiveness of $π$BI and lay out its fundamental theory: type preservation, deadlock-freedom, and weak normalization results for well-typed processes; an operationally sound and complete typed encoding of an affine $λ$-calculus; and a non-interference result for access of resources.

cs.LO↗

Asynchronous Functional Sessions: Cyclic and Concurrent

We present Concurrent GV (CGV), a functional calculus with message-passing concurrency governed by session types. With respect to prior calculi, CGV has increased support for concurrent evaluation and for cyclic network topologies. The design of CGV draws on APCP, a session-typed asynchronous pi-calculus developed in prior work. Technical contributions are (i) the syntax, semantics, and type system of CGV; (ii) a correct translation of CGV into APCP; (iii) a technique for establishing deadlock-free CGV programs, by resorting to APCP's priority-based type system.

cs.LO↗

A Decentralized Analysis of Multiparty Protocols

Protocols provide the unifying glue in concurrent and distributed software today; verifying that message-passing programs conform to such governing protocols is important but difficult. Static approaches based on multiparty session types (MPST) use protocols as types to avoid protocol violations and deadlocks in programs. An elusive problem for MPST is to ensure both protocol conformance and deadlock freedom for implementations with interleaved and delegated protocols. We propose a decentralized analysis of multiparty protocols, specified as global types and implemented as interacting processes in an asynchronous $π$-calculus. Our solution rests upon two novel notions: router processes and relative types. While router processes use the global type to enable the composition of participant implementations in arbitrary process networks, relative types extract from the global type the intended interactions and dependencies between pairs of participants. In our analysis, processes are typed using APCP, a type system that ensures protocol conformance and deadlock freedom with respect to binary protocols, developed in prior work. Our decentralized, router-based analysis enables the sound and complete transference of protocol conformance and deadlock freedom from APCP to multiparty protocols.

cs.PL↗

Deadlock Freedom for Asynchronous and Cyclic Process Networks

This paper considers the challenging problem of establishing deadlock freedom for message-passing processes using behavioral type systems. In particular, we consider the case of processes that implement session types by communicating asynchronously in cyclic process networks. We present APCP, a typed process framework for deadlock freedom which supports asynchronous communication, delegation, recursion, and a general form of process composition that enables specifying cyclic process networks. We discuss the main decisions involved in the design of APCP and illustrate its expressiveness and flexibility using several examples.

cs.LO↗

Session Type Systems based on Linear Logic: Classical versus Intuitionistic

Session type systems have been given logical foundations via Curry-Howard correspondences based on both intuitionistic and classical linear logic. The type systems derived from the two logics enforce communication correctness on the same class of pi-calculus processes, but they are significantly different. Caires, Pfenning and Toninho informally observed that, unlike the classical type system, the intuitionistic type system enforces locality for shared channels, i.e. received channels cannot be used for replicated input. In this paper, we revisit this observation from a formal standpoint. We develop United Linear Logic (ULL), a logic encompassing both classical and intuitionistic linear logic. Then, following the Curry-Howard correspondences for session types, we define piULL, a session type system for the pi-calculus based on ULL. Using piULL we can formally assess the difference between the intuitionistic and classical type systems, and justify the role of locality and symmetry therein.

cs.LO↗

Glueballs on the three-sphere

We study the non-perturbative effects of the global features of the configuration space for SU(2) gauge theory on the three-sphere. The strategy is to reduce the full problem to an effective theory for the dynamics of the low-energy modes. By explicitly integrating out the high-energy modes, the one-loop correction to the effective hamiltonian is obtained. Imposing the $θ$ dependence through boundary conditions in configuration space incorporates the non-perturbative effects of the non-contractable loops in the full configuration space. After this we obtain the glueball spectrum of the effective theory with a variational method.

hep-lat↗

Glueballs on S^3

For SU(2) gauge theory on the three-sphere we study the dynamics of the low-energy modes. By explicitely integrating out the high-energy modes, the one-loop correction to the hamiltonian for this problem is obtained. After imposing the $θ$-dependence through boundary conditions in configuration space, we obtain the glueball spectrum of the effective theory with a variational method.

hep-lat↗