Programming Languages
The School of Computing Science has a long history and tradition of outstanding programming language research. Across its research sections the School hosts a unique combination of world-leading researchers in programming languages research, broadly construed, ranging from foundational research into type systems, to the implementation of parallel runtime systems, to research into how people learn programming languages, naming but a few. Programming Languages researchers at Glasgow typically span theory and practice, with a strong emphasis on the development of practical tools.
Our Programming Languages Research Theme allows researchers from all research Sections, at present including FATA, GLASS, and EAP, with the aim of fostering cross-discipline collaborations. FATA hosts experts in the foundations of programming languages, with a particular focus on session types for concurrent and distributed systems. GLASS hosts experts in compilation, parallel and distributed computing. EAP brings together experts on software engineering and Computing Science education research.
Project Highlights
Uni-pi: Safety, Adaptability, Resilience --- by Construction
The pervasive adoption of distributed software systems in our society is drastically changing the landscape of the global digital infrastructure and economy. To avoid catastrophe, it is imperative that these systems behave as intended, even under constantly changing environmental conditions, software upgrades, or unplanned events, such as failures or service degradation. This project aims to develop Uni-pi, the first unified formal model based on the pi-calculus and linear/session types for the verification of safety, adaptability and resilience properties, whilst maintaining a realistic view of distributed software ecosystems in the presence of failures, message inconsistencies or service degradation.
Uni-pi: Safety, Adaptability, Resilience --- by Construction
M4Secure: Making Memory Management More Secure
Memory management is an essential feature of computing software. During execution time, a program will frequently call a memory allocator library to request space on the computer memory to store data. Unfortunately, memory management systems are vulnerable. According to recent studies from Microsoft and Google, memory bugs account for 70% of critical software vulnerabilities, which can crash our important IT infrastructures and leak confidential and personal data. Such problems are frequently caused by (mis)management of dynamically allocated memory. At the same time, memory allocation is also significant for performance. A large proportion of program execution time is devoted to memory management routines.
This project will develop an entirely new way to build memory allocators. It aims to massively reduce human involvement in developing and optimising memory management libraries to target a diverse range of hardware architectures. Our approach involves specifying the required memory management attributes and then synthesising performant memory management code to satisfy these specifications. Our approach ensures such code is correct by construction by using model-checking techniques to verify the generated code match the expected behaviour and enhanced security requirements. Further, we will support a range of processor backends featuring recently proposed novel secure extensions for hardware architectures.
STARDUST: Session Types for Reliable Distributed Systems
Distributed software systems are an essential part of the infrastructure of modern society. Such systems typically comprise diverse software components deployed across networks of hosts. Ensuring their reliability is challenging, as software components must correctly communicate and synchronise with each other, and any of the hardware or software components may fail. Failure and service "outage" is extremely costly, with worldwide financial losses due to software failures in 2017 estimated at US$1.7tn, up from US$1.1tn in 2016.
Failures can occur at all levels of the system stack: hardware, operating systems, networks, software, and users. Here we focus on using advanced programming language technologies to enable the software level to handle failures that arise from any level of the stack. Our aim is to provide software-level reliability for distributed systems by combining fault prevention with fault tolerance. The key objective is to combine the communication-structuring mechanism of session types with the scalability and fault-tolerance of actor-based software architectures.
The result will be a well-founded theory of reliable actor programming, supported by a collection of libraries and tools, and validated on a range of case studies. Key aims are to deliver tools that provide lightweight support for developers – e.g. warning of potential issues – and to allow developers to continue to use established idioms. By doing so we aim to deliver a step change in the engineering of reliable distributed software systems.