11th Workshop on Programming Language Approaches to Concurrency- & Communication-cEntric SoftwarePLACES 2019

We present a system of session types based on adjoint logic which generalize standard binary session types. Our system allows us to uniformly capture several new behaviors in the space of asynchronous message-passing communication, including multicast, where a process sends a single message to multiple clients, replicable services, which have multiple clients and replicate themselves on-demand to handle requests from those clients, and cancellation, where a process discards a channel without communicating along it. We provide session fidelity and deadlock-freedom results for this system, from which we then derive a logically justified form of garbage collection.

Klaas Pruiksma

Carnegie Mellon University

Frank Pfenning

Carnegie Mellon University, USA

We describe a generative approach that enables concurrent typestate-oriented programming in Java and other mainstream languages. The approach allows programmers to implement objects exposing a state-sensitive interface using a high-level synchronization abstraction that synchronizes methods with the states of the receiver object in which those methods have an effect. An external tool takes care of generating all the boilerplate code that implements the synchronization logic. Behavioral types are used to specify object protocols. The tool integrates protocol conformance verification with the synchronization logic so that protocol violations are promptly detected at runtime

Rosita Gerbo

Università di Torino

Luca Padovani

University of Turin

Italy

FreeST is an experimental concurrent programming language. Based on a core functional programming language, it features primitives to fork new threads, and for channel creation and communication. A powerful type system of context-free session types governs the interaction on channels. This abstract provides a gentle introduction to the language and discusses the compilation process and runtime system.

Bernardo Almeida

Universidade de Lisboa

Andreia Mordido

Lasige / Faculty of Sciences, Universidade de Lisboa

Vasco T. Vasconcelos

University of Lisbon, Portugal

Modern web applications can now offer desktop-like experiences from within the browser, thanks to technologies such as WebSockets, which enable low-latency duplex communication between the browser and the server. While these advances are great for the user experience, they represent a new responsibility for web developers who now need to manage and verify the correctness of the now more complex now and potentially stateful interactions in their application.

In this paper, we present a technique for developing interactive web applications that are statically guaranteed to communicate following a given protocol. First, the global interaction protocol is described in the Scribble protocol language – based on multiparty session types. Scribble protocols are checked for well-formedness, and then each role is projected to a Finite State Machine representing the structure of communication from the perspective of the role. We use source code generation and a novel type-level encoding of FSMs using multi-parameter type classes to leverage the type system of the target language to guarantee type-safe programs conform to the communication protocol.

Our work targets PureScript – a functional language that compiles to JavaScript – which crucially has an expressive enough type system to provide static linearity guarantees. We demonstrate the effectiveness of our approach through a web-based Battleship game where communication is performed through WebSocket connections.

Jonathan King

Habito and Imperial College London

Nicholas Ng

Imperial College London

United Kingdom

Nobuko Yoshida

Imperial College London

This paper addresses a problem found in the construction of Service Oriented Architecture: the adaptation of service protocols with respect to functional redundancy and heterogeneity of global communication patterns. We intend to utilise the theory of Multiparty Session Types (MPST). Our approach is based upon a notion of a multiparty session type isomorphism that provides a constructive realisation of service adapter code when 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 Multiparty Session type isomorphisms. The main motivation for this line of work is to define the type isomorphism that would allow to assess whether two components/services are substitutable modulo adaptation code, given component specification is considered to be a session type.

Assel Altayeva

Imperial College London

United Kingdom

Nobuko Yoshida

Imperial College London

Session Types offer a typing discipline that allows protocol specifications to be used during type-checking, ensuring that implementations adhere to a given specification. When looking to realise global session types in a dependently typed language care must be taken that values introduced in the description are used by roles that know about the value.

We present Sessions, a Resource Dependent Embedded Domain Specific Language (EDSL) for describing global session descriptions in the dependently typed language Idris. As we construct session descriptions the values parameterising the EDSLs’ type keeps track of roles and messages they have encountered. We can use this knowledge to ensure that message values are only used by those who know the value. Sessions supports protocol descriptions that are computable, composable, higher-order, and value-dependent. We demonstrate Sessions expressiveness by describing the TCP Handshake, a multi-modal server providing echo and basic arithmetic operations, and a Higher-Order protocol that supports an authentication interaction step.

Jan de Muijnck-Hughes

University of Glasgow

United Kingdom

Edwin Brady

University of St. Andrews, UK

United Kingdom

Wim Vanderbauwhede

University of Glasgow

With increasing levels of parallelism in all computers since the end of Dennard Scaling in 2005, all software is now becoming parallel or concurrent by default. It is increasingly important to examine the foundations of parallelism underlying current software from the verification perspective. In many cases, this foundation is based on “unstructured parallelism”, as exemplified by the use of threads and locks.

In this talk, we summarize experiences gained in the Habanero Extreme Scale Software Research Laboratory (first at Rice University, and now at Georgia Tech) in developing a foundation for parallel and concurrent software based on a collection of structured parallel execution model primitives that enable enhanced verification relative to unstructured parallelism. We show how this execution model can enable verification of entire classes of programs that use well defined subsets of parallel primitives (e.g., deadlock freedom, determinism), verification of specific programs that use less constrained primitives (e.g., permissions, determinism), and verification of program-input pairs with even fewer constraints (e.g., datarace freedom, determinism, deadlock avoidance).

Vivek Sarkar

Rice University, USA

United States

Vivek Sarkar is Professor of Computer Science and the E.D. Butcher Chair in Engineering at Rice University. He conducts research in multiple aspects of parallel software including programming languages, program analysis, compiler optimizations and runtimes systems for diverse parallel platforms. He currently leads the Habanero Extreme Scale Software Research Laboratory at Rice University, and is PI of the DARPA-funded Pliny project on “big code” analytics. Prior to joining Rice in July 2007, Vivek was Senior Manager of Programming Technologies at IBM Research. His responsibilities at IBM included leading IBM’s research efforts in programming model, tools, and productivity in the PERCS project during 2002- 2007 as part of the DARPA High Productivity Computing System program. His prior research projects include the X10 programming language, the Jikes Research Virtual Machine for the Java language, the ASTI optimizer used in IBM’s XL Fortran product compilers, the PTRAN automatic parallelization system, and profile-directed partitioning and scheduling of Sisal programs. In 1997, he was on sabbatical as a visiting associate professor at MIT, where he was a founding member of the MIT Raw multicore project. Vivek became a member of the IBM Academy of Technology in 1995, and was inducted as an ACM Fellow in 2008. He holds a B.Tech. degree from the Indian Institute of Technology, Kanpur, an M.S. degree from University of Wisconsin-Madison, and a Ph.D. from Stanford University. Vivek has been serving as a member of the US Department of Energy’s Advanced Scientific Computing Advisory Committee (ASCAC) since 2009, and on CRA’s Board of Directors since 2015.

We present an end-to-end solution for verified distributed programming. Building upon the foundation of Multiparty Session Types with refinements, we propose a programming language with refinement types and discuss an API generation strategy to allow type checking to statically validate the refinements from the specification of the protocol to the implementation of each of its clients.

Fangyi Zhou

Imperial College London

Francisco Ferreira

Imperial College London

Rumyana Neykova

Brunel University London

United Kingdom

Nobuko Yoshida

Imperial College London

Sharing confidential information in distributed systems is a necessity in many applications, however, it opens the problem of controlling information sharing even among trusted parties. In this paper, we present a formal model in which dissemination of information is disabled at the level of the syntax in a direct way. We introduce a subcalculi of the p-calculus in which channels are considered as confidential information. The only difference with respect to the pi-calculus is that channels once received cannot be forwarded later on. Another contribution of the model is that some privacy notions already studied in the past, such as group creation and name hiding, are directly representable without any additional language constructs. We also present an encoding of the pi-calculus in our calculus.

Ivan Prokić

University of Novi Sad