No Arabic abstract
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.
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.
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.
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.
With the increase of complexity of modern software, social collaborative coding and reuse of open source software packages become more and more popular, which thus greatly enhances the development efficiency and software quality. However, the explosive growth of open source software packages exposes developers to the challenge of information overload. While this can be addressed by conventional recommender systems, they usually do not consider particular constraints of social coding such as social influence among developers and dependency relations among software packages. In this paper, we aim to model the dynamic interests of developers with both social influence and dependency constraints, and propose the Session-based Social and Dependency-aware software Recommendation (SSDRec) model. This model integrates recurrent neural network (RNN) and graph attention network (GAT) into a unified framework. A RNN is employed to model the short-term dynamic interests of developers in each session and two GATs are utilized to capture social influence from friends and dependency constraints from dependent software packages, respectively. Extensive experiments are conducted on real-world datasets and the results demonstrate that our model significantly outperforms the competitive baselines.
This technical report documents the poster session of SSS 2005, the Symposium on Self-Stabilizing Systems published by Springer as LNCS volume 3764. The poster session included five presentations. Two of these presentations are summarized in brief abstracts contained in this technical report.