2020 Imperial MEng Computing Individual Project: Recap

Type-Safe Web Programming Using Routed Multiparty Session Types in TypeScript

Anson Miu

This project was originally submitted in June 2020 in fulfilment of the MEng Computing Final Year Undergraduate Individual Project.

Context

The aim of this project is to integrate multiparty session types (MPST) in modern web development as well-typed endpoint web applications enjoy communication safety guarantees from MPST theory. Existing work [1][2] either lack support for multiparty sessions, or rely on practices that deviate from mainstream web programming (i.e. functional programming).

🔧 Current State

The current implementation features a toolchain for generating TypeScript APIs based on a communication protocol specification. Developers are encouraged to follow a three-step workflow:

Specify the communication aspect of their web application as a Scribble protocol;
Use our toolchain to generate TypeScript APIs for each role (e.g. client, server, ...) involved in the protocol;
Implement the endpoint application (e.g. Node.js server, React.js browser-side application) using the generated APIs;

By generating APIs based on multiparty session types, endpoint applications built via this workflow enjoy communication safety guarantees.

The current implementation succeeds in the following:

Targets Node.js and React.js;
Supports modern concurrency primitives in TypeScript (e.g. Promise, async/await);
Statically guarantees channel linearity and the absence of communication mismatch by construction from the generated APIs;
Provides hooks for error handling within the generated APIs;
Supports client-to-client interactions in multiparty sessions;

💡 Future Work

We expand on the future work discussed in Chapter 11.2 of the thesis

1️⃣ Support Explicit Connection Actions

Currently, all roles involved in the protocol need to connect before the session commences. Using the Travel Agency example, assume that the agency needs to communicate with a client running some hotel systems software to process the accommodation payment. If the traveler does not make an order, then the hotel system client would still have needed to connect to the sesssion under the current implementation.

One can explore supporting explicit connection actions [3] in the toolchain. We give an example of the Travel Agency example using explicit connection actions:

explicit global protocol TravelAgency(role Traveller, role Agency, role HotelClient) {
  connect Traveller to Agency;
  do EnquireTravel(Traveller, Agency, HotelClient);
}

aux global protocol EnquireTravel(role Traveller, role Agency, role HotelClient) {
  Enquiry(destination: string, date: string) from Traveler to Agency;
  choice at Agency {
    Available(rooms: [string, number][]);
    choice at Traveller {
      Pick(roomType: string) from Traveller to Agency;
      do ProcessPayment(Traveller, Agency, HotelClient);
    } or {
      Retry() from Traveller to Agency;
      do EnquireTravel(Traveller, Agency, HotelClient);
    } or {
      Quit() from Traveller to Agency;
    }
  } or {
    Nothing() from Agency to Traveller;
  }
}

aux global protocol ProcessPayment(role Traveller, role Agency, role HotelClient) {
   Payment(details) from Traveller to Agency;
   connect Agency to HotelClient;
   Selection(roomType: string, paymentDetails) from Agency to HotelClient;
   Ack() from HotelClient to Agency;
   Confirmation() from Agency to Traveller;
}

Other use cases include:

OnlineWallet [4] - role S does not need to be involved if login failed, only explicitly connected on the success branch
Ticket - in the original paper [5], the Bank role is always involved. We could give the Seller an extra choice -- NO (maybe if the buyer negotiates too many times), in which case the Bank would not need to be involved (in this branch)

2️⃣ Multiple Node.js Endpoints

Currently, RoutedSessions mandates that there is exactly one router role, which is the server by convention, because only WebSocket servers can accept connections. However, it is possible for Node.js endpoints to implement WebSocket clients, meaning they can, in theory, connect to other WebSocket servers.

One can explore how to support having multiple Node.js endpoints in the same protocol. This will open up more possibilities for use cases such as:

// both 'Bank' and 'CentralBank' are Node.js endpoints
global protocol AskLoan(role Client, role Bank, role CentralBank) {
   Request(details, loanAmount) from Client to Bank;
   GetCreditRating(details) from Bank1 to CentralBank;    // possible to add explicit connection action here
   CreditRating(rating) from CentralBank to Bank;
   choice at Bank {
     Offer(loanDetails) from Bank to Client;
     choice at Client {
        Accept() from Client to Bank;
     } or {
        Reject() from Client to Bank;
     }
   } or {
     Reject(reason) from Bank to Client;
   }
}

3️⃣ Improve Browser-Side Performance

Currently, for browser-side endpoints, each EFSM state must be a separate React component, and the session runtime must re-render on every state change. This incurs a significant performance overhead relative to a baseline implementation, as well as relative to Node endpoints built using the generated APIs.

One can investigate how to better leverage React APIs (e.g. functional components, React hooks, shouldComponentUpdate to avoid unnecessary reconciliation, ...) to minimise the overhead. Alternatively, one can propose a different way of writing browser-side endpoints that equally guarantee communication safety (in particular, statically avoiding channel reuse) in a more performant manner, and produce comparative benchmarks against this work.

4️⃣ Deploy Toolchain

Currently, the toolchain can only be used via the Docker image, albeit it is possible to build it locally via performing the Dockerfile commands directly on your machine. In other words, it is not readily accessible.

One can explore how to deploy this toolchain as a client-facing application (e.g. a web/desktop application?) that allows developers to upload their protocol, specify the roles and obtain the generated APIs. For example, it can directly create the scaffolding on an online playground (e.g. codepen.io) so developers can get started on their web application quickly. A CI/CD pipeline would also be highly beneficial -- i.e. changes made to the repository get deployed into the client-facing application automatically.

5️⃣ Refine Toolchain

Generate the EFSM diagram alongside the APIs, to let developers visualise the state identifiers in the context of their protocol
Extend Scribble to support annotating roles with their endpoints, e.g. global protocol Ring(role A @node, role B @browser, role C @node) { ... }, so we don't need to specify this in the toolchain CLI.