My research interests are mainly in the field of programming languages and parallel architectures such as FPGAs, manycore processors and GPGPUs.
Current research activities
Low Carbon and Sustainable Computing
• The current emissions from computing are about 2% of the world total but are projected to rise steeply over the next two decades. By 2040 emissions from computing alone will be close to half the emissions level acceptable to keep global warming below 2°C. This growth in computing emissions is unsustainable: it would make it virtually impossible to meet the emissions warming limit.
• The emissions from production of computing devices far exceed the emissions from operating them, so even if devices are more energy efficient producing more of them will make the emissions problem worse. Therefore we must extend the useful life of our computing devices.
• As a society we need to start treating computational resources as finite and precious, to be utilised only when necessary, and as effectively as possible. We need frugal computing: achieving the same results for less energy.
• Imagine we can extend the useful life of our devices and even increase their capabilities without any increase in energy consumption.
• Meanwhile, we will develop the technologies for the next generation of devices, designed for energy efficiency as well as long life.
• Every subsequent cycle will last longer, until finally the world will have computing resources that last forever and hardly use any energy.
AppControl: Enforcing Application Behaviour through Type-Based Constraints
Collaborators: Dr J de Muijnck-Hughes (University of Glasgow); Dr J Cano Reyes (University of Glasgow); Professor N Yoshida (Imperial College London); Professor K McDonald-Maier (University of Essex); Dr X Zhai (University of Essex)
Partners: NASA; UltraSoC Technologies Ltd
Funding: £1.5m EPSRC funding
Funding period: 01 September 2020 - 30 June 2024
Summary: The AppControl project enhances Digital Security By Design for mission-critical Systems-on-Chip. It uses the capabilities provided by the CHERI architecture to enable Design-by-Specification: the Systems-on-Chip has a formal, executable specification (typically created by the system architect), and every software component of the SoC is forced to adhere to this specification. Programs with incompatible specifications cannot run; unspecified run-time behaviour will raise an exception. The practical realisation is through the extension of programming languages to supports expressive specifications and a toolchain which ensures that the specifications are enforced at run time on Capability hardware.
Background: The Problem
With the current state of the art, it is possible to limit the access privileges of a third-party program running on a computer system. The addition of architectural capabilities such as provided by CHERI enable unprecedented fine-grained memory protection and isolation. These mechanisms are however not sufficient to control the behaviour of a program so that it follows the intended specification. For example, if a program performs network access, it is not possible to ensure that the network location accessed is intended by the developer, or the result of a backdoor in the system. In general, this is the case for any system call performed by the program. As a result, malicious programs can e.g. participate in DDoS attacks, or send information about the system to a Command and Control server, etc. It is also the case for library calls, which could perform unspecified actions within the memory space of a process.
The aim of this project is to enhance the provision of Digital Security By Design for mission-critical Systems-on-Chip through Capability hardware-enabled Design-by-Specification. What this means is that the Systems-on-Chip has a formal, executable specification (typically created by the system architect), and every software component of the SoC is forced to adhere to this specification. Programs with incompatible specifications cannot run; unspecified run-time behaviour will raise an exception. For the above example, the specification could govern the network access and also the access to system information. The practical realisation of this aim is through the extension of programming languages to supports expressive specifications and a toolchain which ensures that the specifications are enforced at run time on Capability hardware.
Key Ideas in a Nutshell
Our vision of how to achieve this goal is through the use of behavioural type systems, i.e. the specification of the SoC and each of its individual components are expressed as a type, which effectively and formally describes the allowed interfaces and interactions of each component. This type-based specification will be an integral component of the program executable, and be validated against an overall system specification by the operating system. This proposal focuses on software components, and will build on the capability hardware for enforcement of the type-based specifications. The type-based Design-by-Specification of hardware components is the topic of the EPSRC Border Patrol project (EP/N028201/1), which will run until 2023 and therefore present great potential for synergies with the current proposal.
In our current EPSRC project Border Patrol (EP/N028201/1) we investigate digital security by design for the design of hardware IP-core based SoCs. The key mechanism is the use of type-driven design-by-specification. A design’s specification is encoded in the type system, so that the implementation must follow the specification. Adherence to the spec can be enforced at design time for trusted modules, and at run time for untrusted modules by patrolling the untrusted module’s borders with FSM-based run-time type checkers.
AppControl publications: Google scholar
Border Patrol: Improving Smart Device Security through Type-Aware Systems Design
Collaborators: Dr J de Muijnck-Hughes (University of Glasgow); Professor S Scholz (Heriot-Watt University); Dr R Stewart (Heriot-Watt University); Professor N Yoshida (Imperial College London); Dr C Fensch (ARM Ltd)
Partners: ABB Power Grids UK Limited; EDF Energy; Xilinx
Funding: £1.75m EPSRC funding
Funding period: 01 February 2017 - 31 July 2023
Summary: Border Patrol addresses the increasing concerns about the safety and security of critical infrastructure such as nuclear power plants, the electricity grid and other utilities in the face of possible cyber attacks. Smart devices based on Field-Programmable Gate Arrays (FPGAs) and embedded microprocessors carry the very real risk of malicious functionality hidden in the silicon or in software binaries, dormant and waiting to be activated. Border Patrol closely connects the system design specification with the actual implementation through the use of a formal design methodology based on type systems with static and dynamic type checking. The type system is used as a formal language to encode the design specification so that the actual implementation will automatically be checked against the specification.
Background: The Problem
There are increasing concerns about the safety and security of critical infrastructure such as nuclear power plants, the electricity grid and other utilities in the face of possible cyber attacks. As ageing controllers are replaced by smart devices based on Field-Programmable Gate Arrays (FPGAs) and embedded microprocessors, the safety of such devices raises many concerns. In particular, there is the very real risk of malicious functionality hidden in the silicon or in software binaries, dormant and waiting to be activated. Current hardware and software systems are of such complexity that it is impossible to discover such malicious code through testing.
We aim to address this problem by closely connecting the system design specification with the actual implementation through the use of a formal design methodology based on type systems with static and dynamic type checking. The type system will be used as a formal language to encode the design specification so that the actual implementation will automatically be checked against the specification.
Key Ideas in a Nutshell
Static type checking of data types and multiparty session types can ensure the correctness of the interaction between the components. However, as static checking assume full access to the design source code it cannot be used to protect against potential threads issuing from third-party functional blocks (know as ‘Intellectual Property Cores’ or IP cores) that are commonly used in hardware design. The provider of the IP core can claim adherence to the types and protocols, so that the IP core will meet the compile-time requirements, but the run-time the behaviour cannot be controlled using static techniques. The same applies to third-party compiled software libraries. Therefore we use run-time checking of data types as well as session types at the boundaries of untrusted modules (“Border Patrol”), so that any intentional or unintentional breach of the specification are safely intercepted. ➤ For more info visit the project web site and publications.
Acceleration of Weather and Climate Modelling
Collaborators: Professor Tetsuya Takemi (Kyoto University, Japan); Professor Saji Hameed (University of Aizu, Japan)
Funding: Two EPSRC travel grants and funding from Kyoto University
The aim of this collaborative research is acceleration of weather and climate simulations on GPUs, FPGAs and supercomputers. My focus is on developing source-to-source compilers to automatically convert sequential legacy scientific code in Fortran to parallel code for these platforms. I am particularly interested in the use of novel type annotations to provide hints to the compiler.
As part of the project we have create GPU versions and MPI versions of Prof Takemi’s Large Eddy Simulator for Urban Flows as well as a GPU version of the FLEXPART-WRF model, a Lagrangian Particle Dispersion Model which is used to model e.g. dispersion of particles from the Icelandic volancoes.
Past research projects
TyTra: Exploiting Parallelism through Type Transformations for Hybrid Manycore Systems
Collaborators: Professor SJ Gay (University of Glasgow); Professor N Yoshida (Imperial College London); Professor S Scholz (Heriot-Watt University); Professor W Luk (Imperial College London)
Partners: Codeplay Software Ltd; EPCC Ltd; Maxeler Technologies Ltd; University of Florida
Funding: £1.5m EPSRC funding
Funding period: 06 January 2014 - 05 January 2020
Summary: This collaborative 5-year EPSRC project focused on building compilers for heterogeneous platforms, including FPGAs, using multi-party session types for compiler-based program transformations. The main outcomes were a toolchain consisting of a refactoring compiler for legacy scientific code, an auto-parallelising GPU compiler and an FPGA backend.
Tytra publications on Google scholar
A Novel Service-Based SoC Architecture Using On-Chip Networks with Smart Packets and Dynamically Reconfigurable Logic
Funding: £270k EPSRC Advanced Fellowship
Funding period: 01 October 2004 - 30 September 2009
Summary: This research aimed to create a novel way to design Systems-on-Chip using Networks-on-Chip and reconfigurable logic. It resulted in the Gannet architecture, a concurrent hardware virtual machine implementing a reduction machine, targeted at ASICs and FPGAs. This architecture was then adapted for manycore architectures as the Glasgow Parallel Reduction Machine (GPRM), which we showed to outperform competing task-based parallel programming solutions.
Advanced Fellowship publications on Google scholar