scholarly journals Fair Refinement for Asynchronous Session Types

2021 ◽  
pp. 144-163
Author(s):  
Mario Bravetti ◽  
Julien Lange ◽  
Gianluigi Zavattaro
Keyword(s):  
Message Passing ◽  
Contract Theory ◽  
Communication Protocols ◽  
General Notion ◽  
Service Contract ◽  
Session Types ◽  
Novel Variant

AbstractSession types are widely used as abstractions of asynchronous message passing systems. Refinement for such abstractions is crucial as it allows improvements of a given component without compromising its compatibility with the rest of the system. In the context of session types, the most general notion of refinement is the asynchronous session subtyping, which allows to anticipate message emissions but only under certain conditions. In particular, asynchronous session subtyping rules out candidates subtypes that occur naturally in communication protocols where, e.g., two parties simultaneously send each other a finite but unspecified amount of messages before removing them from their respective buffers. To address this shortcoming, we study fair compliance over asynchronous session types and fair refinement as the relation that preserves it. This allows us to propose a novel variant of session subtyping that leverages the notion of controllability from service contract theory and that is a sound characterisation of fair refinement. In addition, we show that both fair refinement and our novel subtyping are undecidable. We also present a sound algorithm, and its implementation, which deals with examples that feature potentially unbounded buffering.

scholarly journals Nested Session Types

2021 ◽  
pp. 178-206
Author(s):  
Ankush Das ◽  
Henry DeYoung ◽  
Andreia Mordido ◽  
Frank Pfenning
Keyword(s):  
Programming Language ◽  
Message Passing ◽  
Communication Protocols ◽  
Type System ◽  
First Order ◽  
Session Types ◽  
Parametric Polymorphism ◽  
Trace Equivalence

AbstractSession types statically describe communication protocols between concurrent message-passing processes. Unfortunately, parametric polymorphism even in its restricted prenex form is not fully understood in the context of session types. In this paper, we present the metatheory of session types extended with prenex polymorphism and, as a result, nested recursive datatypes. Remarkably, we prove that type equality is decidable by exhibiting a reduction to trace equivalence of deterministic first-order grammars. Recognizing the high theoretical complexity of the latter, we also propose a novel type equality algorithm and prove its soundness. We observe that the algorithm is surprisingly efficient and, despite its incompleteness, sufficient for all our examples. We have implemented our ideas by extending the Rast programming language with nested session types. We conclude with several examples illustrating the expressivity of our enhanced type system.

A Concept for Mobile Ad-Hoc Messaging Networks (AMNet)

2010 ◽  
pp. 1569-1580
Author(s):  
Stefan Stieglitz ◽  
Christoph Fuchß ◽  
Sascha Stöckel ◽  
Christoph Lattemann
Keyword(s):  
Message Passing ◽  
Ad Hoc ◽  
Communication Protocols ◽  
Innovative Approach ◽  
Mobile Nodes ◽  
Simulation Results ◽  
Mobile Ad Hoc ◽  
Store And Forward ◽  
Application Specific

This article shows an innovative approach for an ad-hoc messaging network (AMNET) which uses simple store-and-forward message passing to spread data asynchronously. This approach primarily focuses on application specific needs that can be covered by simple message passing mechanisms. In this paper we will describe a powerful network by using simple devices and communication protocols on the basis of AMNETs. Simulation results of our AMNET approach provide insights into speeding up the network setup process and enable the use of AMNETs even with few participants by introducing a hybrid infrastructure and mobile nodes.

scholarly journals Session Coalgebras: A Coalgebraic View on Session Types and Communication Protocols

2021 ◽  
pp. 375-403
Author(s):  
Alex C. Keizer ◽  
Henning Basold ◽  
Jorge A. Pérez
Keyword(s):  
Communication Protocols ◽  
Type System ◽  
Type Systems ◽  
Software Systems ◽  
Compositional Techniques ◽  
Behavioural Type ◽  
Session Types ◽  
Session Type ◽  
Coalgebra Structure ◽  
Large Systems

AbstractCompositional methods are central to the development and verification of software systems. They allow breaking down large systems into smaller components, while enabling reasoning about the behaviour of the composed system. For concurrent and communicating systems, compositional techniques based on behavioural type systems have received much attention. By abstracting communication protocols as types, these type systems can statically check that programs interact with channels according to a certain protocol, whether the intended messages are exchanged in a certain order. In this paper, we put on our coalgebraic spectacles to investigate session types, a widely studied class of behavioural type systems. We provide a syntax-free description of session-based concurrency as states of coalgebras. As a result, we rediscover type equivalence, duality, and subtyping relations in terms of canonical coinductive presentations. In turn, this coinductive presentation makes it possible to elegantly derive a decidable type system with subtyping for $$\pi $$ π -calculus processes, in which the states of a coalgebra will serve as channel protocols. Going full circle, we exhibit a coalgebra structure on an existing session type system, and show that the relations and type system resulting from our coalgebraic perspective agree with the existing ones.

scholarly journals Mixed Sessions

2020 ◽  
pp. 715-742
Author(s):  
Vasco T. Vasconcelos ◽  
Filipe Casal ◽  
Bernardo Almeida ◽  
Andreia Mordido
Keyword(s):  
Program Development ◽  
Message Passing ◽  
Type System ◽  
The Other ◽  
Runtime System ◽  
Type Checking ◽  
Session Types ◽  
Patterns Of Interaction

AbstractSession types describe patterns of interaction on communicating channels. Traditional session types include a form of choice whereby servers offer a collection of options, of which each client picks exactly one. This sort of choice constitutes a particular case of separated choice: offering on one side, selecting on the other. We introduce mixed choices in the context of session types and argue that they increase the flexibility of program development at the same time that they reduce the number of synchronisation primitives to exactly one. We present a type system incorporating subtyping and prove preservation and absence of runtime errors for well-typed processes. We further show that classical (conventional) sessions can be faithfully and tightly embedded in mixed choices. Finally, we discuss algorithmic type checking and a runtime system built on top of a conventional (choice-less) message-passing architecture.

On asynchronous eventful session semantics

2014 ◽  
Vol 26 (2) ◽  
pp. 303-364 ◽  
Author(s):  
DIMITRIOS KOUZAPAS ◽  
NOBUKO YOSHIDA ◽  
RAYMOND HU ◽  
KOHEI HONDA
Keyword(s):  
Programming Languages ◽  
Message Passing ◽  
Control Flow ◽  
Central Component ◽  
Behavioural Theory ◽  
Session Types ◽  
Event Driven ◽  
Π Calculus ◽  
And Performance ◽  
The Cost

Event-driven programming is one of the major paradigms in concurrent and communication-based programming, where events are typically detected as the arrival of messages on asynchronous channels. Unfortunately, the flexibility and performance of traditional event-driven programming come at the cost of more complex programs: low-level APIs and the obfuscation of event-driven control flow make programs difficult to read, write and verify.This paper introduces a π-calculus with session types that modelsevent-driven session programming(called ESP) and studies its behavioural theory. The main characteristics of the ESP model are asynchronous, order-preserving message passing, non-blocking detection of event/message arrivals and dynamic inspection of session types. Session types offer formal safety guarantees, such as communication and event handling safety, and programmatic benefits that overcome problems with existing event-driven programming languages and techniques. The new typed bisimulation theory developed for the ESP model is distinct from standard synchronous or asynchronous bisimulation, capturing the semantic nature of eventful session-based processes. The bisimilarity coincides with reduction-closed barbed congruence.We demonstrate the features and benefits of ESP and the behavioural theory through two key use cases. First, we examine an encoding and the semantic behaviour of the event selector, a central component of general event-driven systems, providing core results for verifying type-safe event-driven applications. Second, we examine the Lauer–Needham duality, building on the selector encoding and bisimulation theory to prove that a systematic transformation from multithreaded to event-driven session processes is type- and semantics-preserving.

scholarly journals An Evaluation of Communication Protocol Languages for Engineering Multiagent Systems

2020 ◽  
Vol 69 ◽  
pp. 1351-1393
Author(s):  
Amit K Chopra ◽  
Samuel H Christie V ◽  
Munindar P. Singh
Keyword(s):  
Multiagent Systems ◽  
Comparative Evaluation ◽  
Communication Protocol ◽  
Communication Protocols ◽  
Future Research ◽  
State Machines ◽  
Session Types ◽  
Information Causality ◽  
Architecture Style ◽  
Hierarchical State Machines

Communication protocols are central to engineering decentralized multiagent systems. Modern protocol languages are typically formal and address aspects of decentralization, such as asynchrony. However, modern languages differ in important ways in their basic abstractions and operational assumptions. This diversity makes a comparative evaluation of protocol languages a challenging task. We contribute a rich evaluation of diverse and modern protocol languages. Among the selected languages, Scribble is based on session types; Trace-C and Trace-F on trace expressions; HAPN on hierarchical state machines, and BSPL on information causality. Our contribution is four-fold. One, we contribute important criteria for evaluating protocol languages. Two, for each criterion, we compare the languages on the basis of whether they are able to specify elementary protocols that go to the heart of the criterion. Three, for each language, we map our findings to a canonical architecture style for multiagent systems, highlighting where the languages depart from the architecture. Four, we identify design principles for protocol languages as guidance for future research.

scholarly journals Session-based concurrency, declaratively

2021 ◽  
Author(s):  
Mauricio Cano ◽  
Hugo A. López ◽  
Jorge A. Pérez ◽  
Camilo Rueda
Keyword(s):  
Message Passing ◽  
Partial Information ◽  
Contextual Information ◽  
Communication Patterns ◽  
Session Types ◽  
Information Constraints ◽  
Realistic Communication ◽  
Message Passing Programs

AbstractSession-based concurrency is a type-based approach to the analysis of message-passing programs. These programs may be specified in an operational or declarative style: the former defines how interactions are properly structured; the latter defines governing conditions for correct interactions. In this paper, we study rigorous relationships between operational and declarative models of session-based concurrency. We develop a correct encoding of session $$\pi $$ π -calculus processes into the linear concurrent constraint calculus ($$\texttt {lcc}$$ lcc ), a declarative model of concurrency based on partial information (constraints). We exploit session types to ensure that our encoding satisfies precise correctness properties and that it offers a sound basis on which operational and declarative requirements can be jointly specified and reasoned about. We demonstrate the applicability of our results by using our encoding in the specification of realistic communication patterns with time and contextual information.

Sharing of Worldwide Spread Knowledge Using Hypermedia Facilities & Fast Communication Protocols (Mosaic and World Wide Web): The Example of ExPASy

1995 ◽  
Vol 34 (01/02) ◽  
pp. 75-78 ◽  
Author(s):  
R. D. Appel ◽  
O. Golaz ◽  
Ch. Pasquali ◽  
J.-C. Sanchez ◽  
A. Bairoch ◽  
...  
Keyword(s):  
World Wide Web ◽  
World Wide ◽  
Relevant Literature ◽  
Communication Protocols ◽  
Laboratory Data ◽  
Central Element ◽  
University Hospital ◽  
New Information ◽  
The University ◽  
Link Information

Abstract:The sharing of knowledge worldwide using hypermedia facilities and fast communication protocols (i.e., Mosaic and World Wide Web) provides a growth capacity with tremendous versatility and efficacy. The example of ExPASy, a molecular biology server developed at the University Hospital of Geneva, is striking. ExPASy provides hypermedia facilities to browse through several up-to-date biological and medical databases around the world and to link information from protein maps to genome information and diseases. Its extensive access is open through World Wide Web. Its concept could be extended to patient data including texts, laboratory data, relevant literature findings, sounds, images and movies. A new hypermedia culture is spreading very rapidly where the international fast transmission of documents is the central element. It is part of the emerging new “information society”.

The Economic Theory of the Firm: A Generalization

2012 ◽  
pp. 41-66 ◽  
Author(s):  
M. Storchevoy
Keyword(s):  
Economic Theory ◽  
General Theory ◽  
Contract Theory ◽  
Theory Of The Firm ◽  
Material Structure ◽  
Structural Factors ◽  
Boundaries Of The Firm ◽  
Opportunistic Behaviour ◽  
New Variant

The paper deals with development of a general theory of the firm. It discusses the demand for such a theory, reviews existing approaches to its generalization, and offers a new variant of general theory of the firm based on the contract theory. The theory is based on minimization of opportunistic behaviour determined by the material structure of production (a classification of ten structural factors is offered). This framework is applied to the analysis of three boundaries problems (boundaries of the job, boundaries of the unit, boundaries of the firm) and five integration dilemmas (vertical, horizontal, functional, related, and conglomerate).

Sign in / Sign up

Export Citation Format

Share Document