Time-sensitive protocol design and implementation

In the last decade, the web infrastructure has evolved to support on-the-fly access of services provided by different vendors. Potentially, this enables collaborations that are cross-boundary and obey precise non-trivial patterns of conversation. However, today services are still used separately, with little integration and guarantees of safety and quality of service.

To enable the digital economy to concretely benefit from service integration and open collaborations among several parties, it is critical to ensure safety guarantees (e.g., deadlock freedom) that encompass whole systems, and not just single services. Moreover, as services are developed separately and composed on-the-fly, verification should be modular. Modularity is supported by existing frameworks based on multiparty session types (MPST), which allow effective static (behavioural) local type-checking of programs against global protocol specifications involving several parties.

Unfortunately, the state of the art on session types does not sufficiently address non-functional aspects of program correctness. A quality-aware approach to process engineering is particularly critical, as quality properties may affect the functional behaviour of the overall system. For example, the response time of a remote database may affect the deadlock freedom of complex interactions with several clients. This project will focus on time, which is at the basis of many critical safety and quality properties, as many non-trivial collaborations rely on some notion of deadline or timeout (e.g., the Twitter Streaming API requires clients to "...reconnect no more than twice every four minutes").

The aim of the project is to provide a framework for engineering time-sensitive distributed protocols. Protocols are intended here as ad-hoc, application level, abstract specifications of the interaction patterns that actual distributed implementations should follow. Some examples of protocol are the Post Office Protocol (POP2) or Map-Reduce.

The framework we propose will be practical, formally grounded, and support: specification of time-sensitive protocols, their modular implementation as executable programs, and modular automated verification of programs against protocols via type-checking. We will provide two languages, one for the specification and one for the implementation of time-sensitive protocols, and establish their relationship in terms of a verification (i.e., behavioural type-checking) framework based on MPST.

Modularity and formality will derive from using MPST. Three open challenges will be addressed, which are critical for the practical applicability of MPST to timed session programming: expressiveness, tractability, and embedding into concrete languages and tools.

By expressiveness we mean the ability of the programming primitives to set flexible schedules for the timing of actions and support run-time adjustments (e.g., depending on the actual timing in which actions are executed, or on the run-time system load). This will yield robustness of the overall approach by enabling programs to adapt to unpredicted run-time delays.

When verifying programs with such flexible time schedules, tractability will be ensured by combining static and dynamic verification (i.e., via hybrid typing). Hybrid typing of timed interactions is still an unexplored direction, but a promising one in terms of efficiency of verification and robustness.

Finally, the programming primitives for timed session programming will be embedded into a mainstream programming language that can be directly used by practitioners. Concretely, we will provide a Java API for time-aware session programming and a hybrid type-checking tool for programs written with this API. This will enable timely assessment of the theory, wide access to the project's results from academics and practitioners, and support impact.

One of the main motivations of this project is to enable theories for the verification of distributed programs, which have been already explored in simplified scenarios, to have concrete impact in the practice of timed session programming. This will be done by addressing expressiveness, robustness and tractability, and via embedding into concrete languages and tools.

We have identified, as main point of economic and societal impact, the possibility of composing and integrating applications offered by different organisations to enhance collaborations while promoting freedom of vendor choice, thanks to the increased guarantees of safety and robustness in time-sensitive scenarios that this project will offer. Three of the areas EPSRC identified for growth would gain particular benefit from this project: (1) programming languages and compilers (the calculus primitives, Java API and tool), (2) verification and correctness (static and dynamic), (3) software engineering (design, and modular cross-boundary implementation of choreographic protocols, short-timescale development). The project will affect another area of national importance, that is supporting the digital economy, by contributing towards a tool for users and vendors to decide whether they can accept/commit to a specific level of quality without compromising their program's correctness. Correctness includes conformance to timed protocols, which can capture most common scenarios e.g., communication with web servers.

The importance of making concurrent software more reliable and easier to construct by structuring communications using session types is recognised. This is, for instance, the main goal of the project EP/K034413/1 'From Data Types to Session Types-A Basis for Concurrency and Distribution' (ABCD). We will contribute with a complementary perspective based on quality, in particular time. We will extend the usual notion of type-safety ensured by (untimed) session types with punctuality, that is predictability of the timing of interactions with respect to the time-constraints set by protocols. This will ultimately contribute to the control and reduction of energy consumption. In fact, predictability is not only an intrinsic feature of some protocols or a user's commodity, but can have an impact in resource management and load balance, allowing to limit cost inefficiency and energy consumption, which is often caused by busy wait.

Considering time will open the way to precise quantification and verification of properties like eventual consistency when using weak memory models over the cloud (e.g., "the database will reach consistency in at most 5 minutes from the last write"). The long-term purpose is to enable open participation of independent small- to large-sized vendors to collaborations/opportunities, and freedom of choice of vendors, platforms and programming languages.

Being intrinsically platform-agnostic, our framework would contribute towards a common middleware for interoperation between multiple (IAAS) cloud infrastructures.

The main beneficiaries are: (1) the designers of application-level distributed protocols, (2) the programmers of distributed applications (in particular over the Web and Cloud) and (3) industries. We will ensure highest impact: towards (1) via interaction with projects focused on protocol design (e.g., Savara and Scribble); towards (2) by maintaining a project's web site with tools and information targeted at practitioners (note that the use of Java as a reference language offers the advantage of being widely used, hence likely to attract interest and feedback from developers); towards (3) via live demos and direct interaction, e.g., with ABCD's industry partners. Continuous extension of our contacts portfolio will be guaranteed via networking (e.g., at venues, in the web site's discussion forum, on social media such as Twitter) and via a user tracking functionality provided by the project's web site.