System-Level Game Semantics: A unifying framework for composing systems

Lead Research Organisation: Queen Mary, University of London
Department Name: Sch of Electronic Eng & Computer Science


The recent work on System-Level Games provides a semantic framework for modelling low-level code interactions involving resources shared between a program and its environment.
This project will apply the framework for deriving compositional analysis techniques for software compilation and verification. Semantically, the project will produce a paradigmatic model for programs made of combinations of arbitrary low- and high-level code fragments.
By directly examining the interaction traces of code, as produced by our model, we will extract trace-based analyses based on co-induction, as well as behavioural types governing game plays. By trace analysis we will also produce syntax-independent compilation analyses on tamper-resistance and code linking.
These techniques will be applied on the prototype language Verity and will deliver significant improvements to its existing GOS compiler, which is particularly suitable a test-bench because of its high degree of heterogeneity both in terms of languages (functional vs. hardware) and platforms (CPU-based vs. FPGA).

Planned Impact

Cloud computing and heterogeneous computing are widely acknowledged to dominate the software landscape in the foreseeable future.
Our work will contribute directly to making such software sufficiently accessible for non-systems programmers, a line of work acknowledged as a priority direction of development.
Rationalising the burgeoning and chaotic world of APIs has been declared "the future of coding''.
Since computing is becoming the main infrastructure of the economy and of much scientific research, we argue that the impact of this line of work, as generally construed, will be extremely broad.
These considerations apply equally to the international research and economic landscape.
Description This work has looked into distributing computation onto several machines. In particular, we focussed into distributing components of Java programs to different Java Virtual Machines, either statically or dynamically via code migration, in a way that is transparent, requiring minimal programmer effort, and preserving the program semantics. We implemented this into a framework, called Mokapot. As part of a secondment funded by Innovate UK, we looked into industrial applications of the Mokapot framework and identified a market for the tool in legacy Java code modernisation, and more specifically modernisation for the cloud.
Exploitation Route Users and enterprises using the Mokapo framework will be able to modernise their Java codebases for the cloud with a fragment of the effort, and programmer cost, that is required today.
Sectors Digital/Communication/Information Technologies (including Software)

Description University PhD Scholarship
Amount £60,600 (GBP)
Organisation Queen Mary University of London 
Sector Academic/University
Country United Kingdom
Start 09/2016 
End 09/2019
Title Mokapot 
Description Mokapot makes JVM-languages software development for cloud, mobile, and IoT development as easy as conventional single-device programming. An application is developed as if for a single-device, with additional devices being drawn in automatically and seamlessly. We call this "elastic co-processing". With it, the distribution of computation is abstracted away from the code, making it transparent from the developer's perspective. 
Type Of Technology Software 
Year Produced 2019 
Impact Mokapot technology has evolved from deep research in the semantics of programming languages. It innovates by making distribution of code on different nodes seamless. Unlike with state-of-the-art technologies that require heavy re-engineering, this disruptive development allows mokapot to automatically partition a legacy application into smaller components, thus making it fully able to take advantage of the greater resilience and scalability offered by the cloud. It hence results in a dramatic increase in programmer productivity during this process, called application modernisation for the cloud. This innovation furthermore enables a wealth of satellite applications, some of them having already been developed alongside it.