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
Abstract
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).
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.
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.
Organisations
- Queen Mary University of London (Lead Research Organisation)
- University of Nantes (Collaboration)
- UNIVERSITY OF BIRMINGHAM (Collaboration)
- Trinity College Dublin (Collaboration)
- Aarhus University (Project Partner)
- Microsoft Research (United Kingdom) (Project Partner)
- Facebook UK (Project Partner)
- Yale University (Project Partner)
People |
ORCID iD |
Nikos Tzevelekos (Principal Investigator) |
Publications
Birkedal L
(2021)
Theorems for free from separation logic specifications
in Proceedings of the ACM on Programming Languages
Jaber G
(2018)
A Trace Semantics for System F Parametric Polymorphism
Lin Y-Y
(2020)
Symbolic Execution Game Semantics
Lin Y.-Y.
(2020)
Symbolic execution game semantics
in Leibniz International Proceedings in Informatics, LIPIcs
Murawski A
(2019)
Higher-order linearisability
in Journal of Logical and Algebraic Methods in Programming
Murawski A
(2020)
Game Semantics for Interface Middleweight Java
in Journal of the ACM
Murawski A
(2017)
Algorithmic games for full ground references
in Formal Methods in System Design
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) |
URL | https://www.mokapot.xyz/ |
Description | The mokapot technology can have a profound impact in application modernisation for legacy Java applications. |
First Year Of Impact | 2020 |
Sector | Digital/Communication/Information Technologies (including Software) |
Impact Types | Economic |
Description | Innovation to Commercialisation of University Research (ICURe) |
Amount | £44,502 (GBP) |
Organisation | Innovate UK |
Sector | Public |
Country | United Kingdom |
Start | 04/2019 |
End | 10/2019 |
Description | University PhD Scholarship |
Amount | £60,600 (GBP) |
Organisation | Queen Mary University of London |
Sector | Academic/University |
Country | United Kingdom |
Start | 08/2016 |
End | 09/2019 |
Title | Symbolic Execution Game Semantics |
Description | We present a framework for symbolically executing and model checking higher-order programs with external (open) methods. We focus on the client-library paradigm and in particular we aim to check libraries with respect to any definable client. We combine traditional symbolic execution techniques with operational game semantics to build a symbolic execution semantics that captures arbitrary external behaviour. We prove the symbolic semantics to be sound and complete. This yields a bounded technique by imposing bounds on the depth of recursion and callbacks. We provide an implementation of our technique in the framework and showcase its performance on a custom benchmark based on higher-order coding errors such as reentrancy bugs. |
Type Of Material | Improvements to research infrastructure |
Year Produced | 2020 |
Provided To Others? | Yes |
Impact | Technique further developed to be applied to program equivalence checking. |
Description | Birmingham |
Organisation | University of Birmingham |
Country | United Kingdom |
Sector | Academic/University |
PI Contribution | Joint research project on mokapot/millr technology for automating and optimising application modernisation for the cloud. Focus on millr refactoring and certification tool. |
Collaborator Contribution | Joint research project on mokapot/millr technology for automating and optimising application modernisation for the cloud. Focus on mokapot runtime library. |
Impact | Mokapot/millr technology for automating and optimising application modernisation for the cloud. |
Start Year | 2016 |
Description | Nantes |
Organisation | University of Nantes |
Country | France |
Sector | Academic/University |
PI Contribution | Emanating from the project, the collaboration with Dr Jaber is still ongoing and we are currently collaborating on an adjacent research direction. |
Collaborator Contribution | Emanating from the project, the collaboration with Dr Jaber is still ongoing and we are currently collaborating on an adjacent research direction. |
Impact | None yet. |
Start Year | 2018 |
Description | Trinity |
Organisation | Trinity College Dublin |
Country | Ireland |
Sector | Academic/University |
PI Contribution | Research on program equivalence and regression testing of programs. |
Collaborator Contribution | Research on program equivalence and regression testing of programs, including a tool implementation. |
Impact | No published outputs yet. |
Start Year | 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. |
URL | http://www.mokapot.xyz |
Company Name | Acygn Ltd |
Description | |
Year Established | 2019 |
Impact | N/A |