Time-sensitive protocol design and implementation

Lead Research Organisation: University of Kent
Department Name: Sch of Computing

Abstract

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.

Planned 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.

Publications

10 25 50

publication icon
Massimo Bartoletti (2018) Progress-Preserving Refinements of CTA

publication icon
Murgia M (2019) Input urgent semantics for asynchronous timed session types in Journal of Logical and Algebraic Methods in Programming

 
Description *** Key finding 1 *** We developed a theory of asynchronous timed refinement. Despite the existence of powerful theories and tools - eg., based on timed automata (TA) and its distributed communicating version (CTA) - to verify real-time models, there is little or no support to derive `correct' implementation from `correct' models. In particular, for CTA, there is no suitable notion of refinement to describe the relationship between models at different levels of abstractions and, ultimately, between models and implementations. In this first year we obtained several negative (but useful) results: if a developer implements a CTA in a naive way (following the same interaction structure of the model) and only refining the timing of its send and receive actions (to mimic the practice of implementing CTA using common communication primitives of mainstream programming languages) then there is no guarantee, in general, that the implementation preserves the behaviour or progress properties of the original model. This is quite concerning. We have, therefore, developed a notion of refinement for CTA, and decidable conditions, that ensure behaviour and progress preservation. We built a tool that check for our refinement/conditions. The tool has been useful in two ways: (1) to demonstrate the practicality of our theory on a portfolio of case studies (for each use case we could find at least one correct implementation) and (2) as a first step for automated-support for models implementation. We have explored (2) targeting implementations with the popular Go programming language.

***Key finding 2*** We developed two simple and expressive formal languages to describe time-sensitive protocols and their implementations. The language for protocols allows to define protocols that are correct by construction. The language for implementations is extremely simple and yet it can represent the wide spectrum of communication primitives used in common programming languages, and allow the programmer to set flexible schedules for the timings of actions. These two languages connected via (behavioural) typing. Behavioural typing ensures punctuality of a program with respect to time constraints expressed in a protocol. The typing system allows for higher order messages (a program can send open sessions as messages to another program, hence delegating an ongoing communication session to the receiving party) and relies on a notion of subtyping that improves precision (behavioural typing is notoriously not complete, hence precision is a very desirable feature).

*** Key finding 3 *** We have studied the relationship between asynchronous urgent receive semantics and synchronous semantics. While being developed as a basis for key finding 2 (see above) this study is useful on its own sake.

The three findings have been published (or accepted/to appear) in three different venues. Key findings 1 and 2 have appeared or will appear in top-class international conferences on concurrency and programming languages (CONCUR'18 and ESOP'19). Key finding 3 has been presented in an international workshop (ICE'18) as a singled authored publication by the RA of this project, hence contributing to establishing his independence as a researcher.
Exploitation Route ***Key finding 1*** By being based on automata, the theory of refinement is general and can be used in different contexts (eg., session types). For example, we are using the theory of refinement as a basis for a notion of subtyping for timed session types (in the ongoing thread of this project). The theory of refinement, by itself, sets a series of guidelines on how to implement a timed models that are immediately useful to developers. Moreover, it can be exploited to develop tools supporting code development, or even for semi-automated code generation. The tool associated with the theory can support code development (we outlined a simple method towards developing implementations in Go), but other tools could be developed, targeting other languages or catering for more structured development processes.

***Key finding 2*** Our typing theory is targeted at being applied to programming languages. First, the calculus has been designed to reflect common communication and time-sensitive primitives. While minimal, the calculus features (1) receive actions that are blocking or non-blocking, with or without timeout, and (2) delays of arbitrary (yet bounded) delays that can well represent time-consuming actions in general. Moreover, the calculus has a (realistic) urgent receive semantics. The calculus and work was well received by academics and practitioners (when presented at venues such as S-REPLS 11 at Facebook, EPSRC ABCD project meeting). This work can be brought forward in three way: (1) extend an existing compiler to allow behavioural typing of concrete programs (initially planned), (2) use the theory towards API generation (producing skeletons of programs that are correct by construction), and/or (3) run-time verification by using the typing system to inject run-time instrumentation (that can easily be derived by the protocols) into programs.

***Key finding 3*** Could influence (i.e., simplify) development of theories of asynchronous communication in the future.
Sectors Digital/Communication/Information Technologies (including Software),Energy,Environment,Financial Services, and Management Consultancy,Healthcare,Transport

URL https://www.cs.kent.ac.uk/people/staff/lb514/fg.html
 
Description In the early stages, the main impact of the project was that of bringing forward a perspective of integration between formal methods and programming practices. The work done in the first months has put light on existing gaps between verification theories/tools and common programming primitives/practices, in the context of time-sensitive asynchronous communications: while we can rely on powerful tools to analyze real-time models, little support exists to guide implementation and ensure that implementations will behave as good as their models. As concrete output towards impact, we have developed a theory of asynchronous timed refinement (backed by a tool) to determine when a concrete model (or implementation) has the same behaviour and progress properties of an abstract model. This theory allows to make concrete use of the already existing powerful tools for verification of time-sensitive models: it sets conditions that ensure, against the general case, that time-sensitive programs preserve the desirable properties of their time-sensitive models. To facilitate practical utilisation of these results by developers, we have outlined a simple method for deriving implementations out of models (with the guarantee that implementations preserve behaviour and progress properties of their model). The method is centred on our tool. The tool has potential to give concrete support a smooth transition from correct models to correct code and it is currently being extended to make it user-friendly for wider use. The problem itself, the shift of perspective, and our theory of refinement, was a basis for enriching exchanges and discussions with academics and students on the role and practical relevance of formal methods. Two talks, given by the PI, were particularly precious in feeding this discussion: - a seminar/lecture at the University of Leicester involving academics and postgraduate students (both PhD and MSc), - a talk at the 2017 meeting of project EPSRC (EP/K034413/1 -- From Data Types to Session Types---A Basis for Concurrency and Distribution ABCD) involving attendants from both academy and industry. In the second year of the project we have developed a concrete behavioural framework theory for a realistic calculus (i.e., featuring realistic time-sensitive primitives that one finds in mainstream programming languages). This theory has potential for being used as a basis for tools for API generation and static/dynamic verification of time-sensitive programs. In the aforementioned work, we have also introduced a more realistic semantics (i.e., urgent receive semantics) for time-sensitive programs that lays somewhere in between synchronous and (common but harder to verify) asynchronous communications. This semantics will affect (i.e., simplify) future development of theories of concurrent communication in the timed and untimed scenario. The PI has presents the aforementioned framework in two talks to audiences that included students and/or industry, attracting encouraging interest, and enriching feedback: - a talk at the 2018 meeting of project EPSRC (EP/K034413/1 -- From Data Types to Session Types---A Basis for Concurrency and Distribution ABCD) involving attendants from both academy and industry, - a talk to S-REPLS 11 hosted by Facebook, also involving attendants from both academy and industry. On a different line, the project is having impact on developing the networking (other than technical) skills of the RA hired on this project. The RA has been engaging in dissemination, and networking activities: he gave two one-hour seminars (one locally at Kent and one at Imperial College London, in occasion of a one-day visit funded by the project) presenting our work together, and received encouraging feedback. The RA also published and presented a single authored paper at an international workshop (ICE'18, Madrid). The RA has been successful in securing himself another RA position (University of Cagliari) after the contract funded by this project had terminated. The RA has now also two co-authored publications in top-class conferences (CONCUR'18 and ESOP'19).
First Year Of Impact 2018
Sector Digital/Communication/Information Technologies (including Software)
Impact Types Cultural

 
Description Collaboration with Dr Massimo Bartoletti, University of Cagliari 
Organisation University of Cagliari
Country Italy 
Sector Academic/University 
PI Contribution Contribution to a `theory of asynchronous timed refinement' being developed in the project. The theory establishes conditions by which developers can derive correct programs from correct models. In fact, the theory establishes a first link between existing powerful theories for verification of timed automata and the developer's practice of implementing safe models.
Collaborator Contribution The theory has been developed in collaboration. The collaboration also includes co-authoring a paper that is currently under review at a top international conference.
Impact Theory of asynchronous timed refinement including : a notion of refinement and a sound conditions for `correct implementation' of a model, a sound decidable approximation of the condition, a supporting tool to check for the conditions, evaluation of the practicality of theory via case studies.
Start Year 2017
 
Description Collaboration with Prof. Nobuko Yoshida, Imperial College London 
Organisation Imperial College London
Department Department of Computing
Country United Kingdom 
Sector Academic/University 
PI Contribution A (timed) behavioural typing theory for a practical and representative calculus.
Collaborator Contribution Advise on directions and decisions, and feedback.
Impact A draft for a research paper on preparation. Two research seminars.
Start Year 2017
 
Description Collaboration with Vasco Vasconcelos, University of Lisbon 
Organisation University of Lisbon
Country Portugal 
Sector Academic/University 
PI Contribution Generation rules for asynchronous timed session types (to guarantee progress and strong non-zenoness), semantics for a realistic calculus modelling time-sensitive programs.
Collaborator Contribution Prof. Vasco Vasconcelos hosted me for a visit (May 24rd - June 1st) at the University of Lisbon. We worked together in setting up the foundations of the project's work (see aforementioned contributions). He introduced me to local colleagues working on cost analysis -- annotation of code with actions' duration. This orthogonal topic could be paramount towards the project's impact at a later stage.
Impact Ongoing research paper and two research presentations/seminars.
Start Year 2017
 
Title Tool: checking for asynchronous timed refinement 
Description Prototype tool implementing the theory of timed asynchronous refinement developed in this project. The tool checks if a model is a correct refinement of another and can be used by developers to support implementation of models (expressed at Communicating Timed Automata). The tool at the moment was used to support evaluation of the theory. It is being extended to allow use from general public and semi-automated code generation. 
Type Of Technology Software 
Year Produced 2018 
Impact The practicality of a theory of asynchronous timed refinement was assessed on the basis of the tool. The outcome illustrated: the practicality of the theory, how to use it to facilitate development. Aforementioned future extensions will allow the tool to concretely impact models implementation by developers. 
 
Description Participation and talk given at project meeting of EP/K034413/1 (From Data Types to Session Types---A Basis for Concurrency and Distribution). 
Form Of Engagement Activity A formal working group, expert panel or dialogue
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Presentation given on the project and its latest results. The audience was engaged and expressed interest in the presentation and project's topics. I was asked for further information or material by several participants, both from academia and industry. Fruitful communications followed with both types of participants (mostly centring on case studies).
Year(s) Of Engagement Activity 2017
URL http://groups.inf.ed.ac.uk/abcd/meeting-december2017/index.html
 
Description Participation and talk given at project meeting of EP/K034413/1 (From Data Types to Session Types---A Basis for Concurrency and Distribution). 
Form Of Engagement Activity A formal working group, expert panel or dialogue
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Dissemination (talk on the latest results and outcomes of the project), attendance of talks on results and outcomes of EP/K034413/1, discussions on ongoing and future collaborations with one member of EP/K034413/1 (Nobuko Yoshida) and a member of the advisor board (Vasco Thudichum Vasconcelos), discussion (feedback and directions towards integration) with other attending partners of EP/K034413/1.
Year(s) Of Engagement Activity 2018
URL http://groups.inf.ed.ac.uk/abcd/meeting-december2018/index.html
 
Description Seminar at the University of Leicester 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Postgraduate students
Results and Impact Seminar on the project and its latest outcomes. The presentation was targeted at MSc students (some of which possibly pondering on doing doctoral studies) and academics. I made an announcement about my availability to supervise PhD projects on the topics presented. Many attendants met me after the talk and engaged is discussion on the topic. I received a request for future collaboration from an academic at Leicester.
Year(s) Of Engagement Activity 2018
URL http://www.cs.le.ac.uk/seminars/Programme.html
 
Description Talk at S-REPLS 11 event, at Facebook, London 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Industry/Business
Results and Impact Talk with title "Time-sensitive protocols design and implementation" on the latest outcomes of the project. Attendance of all workshop and discussion/networking with attendants.
Year(s) Of Engagement Activity 2019
URL https://splashthat.com/sites/view/sreplsevent2019.splashthat.com?fbclid=IwAR0J4PZlB81zhDCXYPA7VPUlXZ...
 
Description University of Lisbon - Faculty of Science - visit and seminar 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Talk to present background (state of the art), open problem, motivation, and first plan of the project. The talk also had the aim of gathering feedback. Precious feedback was received from experts in formal verification and cost-analysis. With the latter, we envisaged future collaboration.
Year(s) Of Engagement Activity 2017