Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userCommunication-Safe Web Programming in TypeScript with Routed Multiparty Session Types
155
0
0.0
(
0
)
Added by
Fangyi Zhou
Publication date
2021
fields
Informatics Engineering
and research's language is
English
Authors
Anson Miu
Ask ChatGPT about the research
No Arabic abstract
Modern web programming involves coordinating interactions between browser clients and a server. Typically, the interactions in web-based distributed systems are informally described, making it hard to ensure correctness, especially communication safety, i.e. all endpoints progress without type errors or deadlocks, conforming to a specified protocol. We present STScript, a toolchain that generates TypeScript APIs for communication-safe web development over WebSockets, and RouST, a new session type theory that supports multiparty communications with routing mechanisms. STScript provides developers with TypeScript APIs generated from a communication protocol specification based on RouST. The generated APIs build upon TypeScript concurrency practices, complement the event-driven style of programming in full-stack web development, and are compatible with the Node.js runtime for server-side endpoints and the React.js framework for browser-side endpoints. RouST can express multiparty interactions routed via an intermediate participant. It supports peer-to-peer communication between browser-side endpoints by routing communication via the server in a way that avoids excessive serialisation. RouST guarantees communication safety for endpoint web applications written using STScript APIs. We evaluate the expressiveness of STScript for modern web programming using several production-ready case studies deployed as web applications.
rate research
Read More
Multiparty Session Types (MPST) are a well-established typing discipline for message-passing processes interacting on sessions involving two or more participants. Session typing can ensure desirable properties: absence of communication errors and deadlocks, and protocol conformance. However, existing MPST works provide a subject reduction result that is arguably (and sometimes, surprisingly) restrictive: it only holds for typing contexts with strong duality constraints on the interactions between pairs of participants. Consequently, many intuitively correct examples cannot be typed and/or cannot be proved type-safe. We illustrate some of these examples, and discuss the reason for these limitations. Then, we outline a novel MPST typing system that removes these restrictions.
Actor coordination armoured with a suitable protocol description language has been a pressing problem in the actors community. We study the applicability of multiparty session type (MPST) protocols for verification of actor programs. We incorporate sessions to actors by introducing minimum additions to the model such as the notion of actor roles and protocol mailbox. The framework uses Scribble, which is a protocol description language based on multiparty session types. Our programming model supports actor-like syntax and runtime verification mechanism guaranteeing type-safety and progress of the communicating entities. An actor can implement multiple roles in a similar way as an object can implement multiple interfaces. Multiple roles allow for inter-concurrency in a single actor still preserving its progress property. We demonstrate our framework by designing and implementing a session actor library in Python and its runtime verification mechanism.
Advancements in mobile device computing power have made interactive web applications possible, allowing the web browser to render contents dynamically and support low-latency communication with the server. This comes at a cost to the developer, who now needs to reason more about correctness of communication patterns in their application as web applications support more complex communication patterns. Multiparty session types (MPST) provide a framework for verifying conformance of implementations to their prescribed communication protocol. Existing proposals for applying the MPST framework in application developments either neglect the event-driven nature of web applications, or lack compatibility with industry tools and practices, which discourages mainstream adoption by web developers. In this paper, we present an implementation of the MPST framework for developing interactive web applications using familiar industry tools using TypeScript and the React.js framework. The developer can use the Scribble protocol language to specify the protocol and use the Scribble toolchain to validate and obtain the local protocol for each role. The local protocol describes the interactions of the global communication protocol observed by the role. We encode the local protocol into TypeScript types, catering for server-side and client-side targets separately. We show that our encoding guarantees that only implementations which conform to the protocol can type-check. We demonstrate the effectiveness of our approach through a web-based implementation of the classic Noughts and Crosses game from an MPST formalism of the game logic.
Session types are a rich type discipline, based on linear types, that lifts the sort of safety claims that come with type systems to communications. However, web-based applications and microservices are often written in a mix of languages, with type disciplines in a spectrum between static and dynamic typing. Gradual session types address this mixed setting by providing a framework which grants seamless transition between statically typed handling of sessions and any required degree of dynamic typing. We propose Gradual GV as a gradually typed extension of the functional session type system GV. Following a standard framework of gradual typing, Gradual GV consists of an external language, which relaxes the type system of GV using dynamic types, and an internal language with casts, for which operational semantics is given, and a cast-insertion translation from the former to the latter. We demonstrate type and communication safety as well as blame safety, thus extending previous results to functional languages with session-based communication. The interplay of linearity and dynamic types requires a novel approach to specifying the dynamics of the language.
This paper addresses a problem found within the construction of Service Oriented Architecture: the adaptation of service protocols with respect to functional redundancy and heterogeneity of global communication patterns. We utilise the theory of Multiparty Session Types (MPST). Our approach is based upon the notion of a multiparty session type isomorphism, utilising a novel constructive realisation of service adapter code to establishing equivalence. We achieve this by employing trace semantics over a collection of local types and introducing meta abstractions over the syntax of global types. We develop a corresponding equational theory for MPST isomorphisms. The main motivation for this line of work is to define a type isomorphism that affords the assessment of whether two components/services are substitutables, modulo adaptation code given software components formalised as session types.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
