VLDB 2026 Research / reviewers in the wild / expert
Matthew Naylor 0002
dblp:80/2682-2
· DBLP profile ↗
13ranked-venue papers
10as first author
5since 2021 · last 2026
0000-0001-9827-8497ORCID · verified
Domains — the database's venue-derived domains; a paper can count in several
Systems, architecture and hardware · 8 · 7 first-author · 3 since 2021Software engineering, systems software and programming languages · 4 · 3 first-author · 2 since 2021Security and privacy · 2 · 1 since 2021Theory of computation · 2 · 2 first-author
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2026 | CHERI-SIMT: Implementing Capability Memory Protection in GPUsabstractGovernments are increasingly advising software manufacturers to employ memory-safe languages and technologies to combat adversarial attacks on modern computing infrastructure. This introduces pressures across the entire computing industry, including GPU vendors who provide implementations of unsafe C/C++-based languages, such as CUDA and OpenCL, for programming the devices they produce. One of the memory-safety technologies being recommended is Capability Hardware Enhanced RISC Instructions (CHERI). CHERI builds strong and efficient memory safety into underlying instruction-set architectures allowing continued, but memory-safe, use of C/C++-based languages on top. Matthew Naylor 0002, Alexandre Joannou, A. Theodore Markettos, Paul Metzger, Simon W. Moore, Timothy M. Jones 0001 |
ASPLOS (1) | 1 |
| 2025 | Deprivileging Low-Level GPU Drivers Efficiently with User-Space Processes and CHERI CompartmentsabstractDevice drivers are a prominent source of operating system bugs and vulnerabilities, due to market pressures on hardware vendors and access to privileged system resources. OSes increasingly deprivilege drivers by moving them out of the kernel into user space, but this is widely understood to come with significant overhead. The perfect storm concerns GPU drivers, which are very large, complex and yet highly performance-sensitive. For performance reasons, large parts of these drivers run with full kernel privileges on major OSes. Paul Metzger, A. Theodore Markettos, Edward Napierala, Matthew Naylor 0002, Robert N. M. Watson, Timothy M. Jones 0001 |
CCS | 4 |
| 2025 | Adaptive CHERI Compartmentalization for Heterogeneous AcceleratorsabstractHardware accelerators offer high performance and energy efficiency for specific tasks compared to general-purpose processors.However, current hardware accelerator designs focus primarily on performance, overlooking security.This poses significant security risks due to potential memory safety violations that can affect the entire hardware system.Existing methods either rely on Input-Output Memory Management Units (IOMMUs) for memory isolation between memory pages, leading to vulnerabilities in intra-page memory accesses, or modify an accelerator architecture for specialized memory protection, which requires significant effort and cannot scale across multiple diverse applications.In this paper, we propose a general method for fine-grained memory protection in heterogeneous systems without modifying accelerator architectures.We extend the Capability Hardware Enhanced RISC Instructions (CHERI) from CPUs to an adaptive hardware interface named CapChecker.The CapChecker imports capabilities from the CPU and guards memory accesses at the pointer level from CHERI-unaware accelerators as if they were CHERI-aware natively.Over a set of benchmarks on hardware accelerators in a heterogeneous system, our approach achieves fine-grained memory protection, with a 1.4% performance overhead compared to CHERI-unaware accelerators on average. Jianyi Cheng, A. Theodore Markettos, Alexandre Joannou, Paul Metzger, Matthew Naylor 0002, Peter Rugg, Timothy M. Jones 0001 |
ISCA | 5 |
| 2024 | Advanced Dynamic Scalarisation for RISC-V GPGPUsabstractRecently, researchers have proposed the use of the open RISC-V standard as a basis for GPGPU instruction sets, enabling development of unencumbered GPGPU hardware while reusing extensive general-purpose instruction-set, compiler, and software infrastructure where appropriate. In this paper, we identify and overcome a major deficiency in existing SIMT-style RISC-V GPGPUs: the inability to exploit value regularity whereby threads executing in lockstep often compute the same or similar intermediate values. As a solution, we propose advanced dynamic scalarisation, a set of new microarchitectural features to exploit value regularity without requiring any extensions to the instruction set or compiler. These features include register-file compression to reduce on-chip storage requirements in heavily-threaded designs and parallel scalar and vector pipelines to increase instruction throughput, and are fully implemented and evaluated in a new, open-source, synthesisable RISC-V GPGPU called Simtight. Our results show a reduction in register-file storage requirements of 68%, saving 178KB of fast on-chip memory per 2048-thread streaming multiprocessor, and an increase in run-time performance of 20% at low hardware cost. Matthew Naylor 0002, Alexandre Joannou, A. Theodore Markettos, Paul Metzger, Simon W. Moore, Timothy M. Jones 0001 |
ICCD | 1 |
| 2021 | General hardware multicasting for fine-grained message-passing architecturesabstractManycore architectures are increasingly favouring message-passing or partitioned global address spaces (PGAS) over cache coherency for reasons of power efficiency and scalability. However, in the absence of cache coherency, there can be a lack of hardware support for one-to-many communication patterns, which are prevalent in some application domains. To address this, we present new hardware primitives for multicast communication in rack-scale manycore systems. These primitives guarantee delivery to both colocated and distributed destinations, and can capture large unstructured communication patterns precisely. As a result, reliable multicast transfers among any number of software tasks, connected in any topology, can be fully offloaded to hardware. We implement the new primitives in a research platform consisting of 50K RISC-V threads distributed over 48 FPGAs, and demonstrate significant performance benefits on a range of applications expressed using a high-level vertex-centric programming model. Matthew Naylor 0002, Simon W. Moore, David B. Thomas, Jonathan Beaumont, Shane T. Fleming, Mark Vousden, A. Theodore Markettos, Thomas Bytheway, Andrew D. Brown |
PDP | 1 |
| 2020 | Termination detection for fine-grained message-passing architecturesabstractBarrier primitives provided by standard parallel programming APIs are the primary means by which applications implement global synchronisation. Typically these primitives are fully-committed to synchronisation in the sense that, once a barrier is entered, synchronisation is the only way out. For message-passing applications, this raises the question of what happens when a message arrives at a thread that already resides in a barrier. Without a satisfactory answer, barriers do not interact with message-passing in any useful way.In this paper, we propose a new refutable barrier primitive that combines with message-passing to form a simple, expressive, efficient, well-defined API. It has a clear semantics based on termination detection, and supports the development of both globally-synchronous and asynchronous parallel applications.To evaluate the new primitive, we implement it in a prototype large-scale message-passing machine with 49,152 RISC-V threads distributed over 48 FPGAs. We show that hardware support for the primitive leads to a highly-efficient implementation, capable of synchronisation rates that are an order-of-magnitude higher than what is achievable in software. Using the primitive, we implement synchronous and asynchronous versions of a range of applications, observing that each version can have significant advantages over the other, depending on the application. Therefore, a barrier primitive supporting both styles can greatly assist the development of parallel programs. Matthew Naylor 0002, Simon W. Moore, Andrey Mokhov, David B. Thomas, Jonathan Beaumont, Shane T. Fleming, A. Theodore Markettos, Thomas Bytheway, Andrew D. Brown |
ASAP | 1 |
| 2020 | Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation processabstractThe root causes of many security vulnerabilities include a pernicious combination of two problems, often regarded as inescapable aspects of computing. First, the protection mechanisms provided by the mainstream processor architecture and C/C++ language abstractions, dating back to the 1970s and before, provide only coarse-grain virtual-memory-based protection. Second, mainstream system engineering relies almost exclusively on test-and-debug methods, with (at best) prose specifications. These methods have historically sufficed commercially for much of the computer industry, but they fail to prevent large numbers of exploitable bugs, and the security problems that this causes are becoming ever more acute.In this paper we show how more rigorous engineering methods can be applied to the development of a new security-enhanced processor architecture, with its accompanying hardware implementation and software stack. We use formal models of the complete instruction-set architecture (ISA) at the heart of the design and engineering process, both in lightweight ways that support and improve normal engineering practice - as documentation, in emulators used as a test oracle for hardware and for running software, and for test generation - and for formal verification. We formalise key intended security properties of the design, and establish that these hold with mechanised proof. This is for the same complete ISA models (complete enough to boot operating systems), without idealisation.We do this for CHERI, an architecture with hardware capabilities that supports fine-grained memory protection and scalable secure compartmentalisation, while offering a smooth adoption path for existing software. CHERI is a maturing research architecture, developed since 2010, with work now underway on an Arm industrial prototype to explore its possible adoption in mass-market commercial processors. The rigorous engineering work described here has been an integral part of its development to date, enabling more rapid and confident experimentation, and boosting confidence in the design. Kyndylan Nienhuis, Alexandre Joannou, Thomas Bauereiß, Anthony C. J. Fox, Michael Roe, Brian Campbell 0001, Matthew Naylor 0002, Robert M. Norton, Simon W. Moore, Peter G. Neumann, Ian Stark, Robert N. M. Watson, Peter Sewell |
SP | 7 |
| 2019 | Tinsel: A Manythread Overlay for FPGA ClustersabstractCommodity FPGA boards with advanced networking facilities have great potential in the construction of high-performance compute clusters that scale. However, low-level design tools and long synthesis times are major barriers to productivity for application developers. In this paper, we explore the potential of a distributed soft-processor overlay, programmed in software at a high-level of abstraction, to deliver a useful level of performance for FPGA clusters. In particular, we demonstrate the use of hardware multhreading to achieve a fast, space-efficient, high-throughput overlay, and compare a 12-FPGA instance of it (12,288 RISC-V threads) against a conventional Xeon cluster on the problem of distributed graph processing. Matthew Naylor 0002, Simon W. Moore, David B. Thomas |
FPL | 1 |
| 2016 | A consistency checker for memory subsystem tracesabstractVerifying the memory subsystem in a modern shared-memory multiprocessor is a big challenge. Optimized implementations are highly sophisticated, yet must provide subtle consistency and liveness guarantees for the correct execution of concurrent programs. We present a tool that supports efficient specification-based testing of the memory subsystem against a range of formally specified consistency models. Our tool operates directly on the memory subsystem interface, promoting a compositional approach to system-on-chip verification, and can be used to search for simple failure cases - assisting rapid debug. It has recently been incorporated into the development flows of two open-source implementations - Berkeley's Rocket Chip(RISC-V) and Cambridge's BERI (MIPS) - where it has uncovered a number of serious bugs. Matthew Naylor 0002, Simon W. Moore, Alan Mujumdar |
FMCAD | 1 |
| 2015 | A generic synthesisable test benchabstractWriting test benches is one of the most frequently-performed tasks in the hardware development process. The ability to reuse common test bench features is therefore key to productivity. In this paper, we present a generic test bench, parameterised by a specification of correctness, which can be used to test any design. Our test bench provides several important features, including automatic test-sequence generation and shrinking of counter-examples, and is fully synthesisable, allowing rigorous testing on FPGA as well as in simulation. The approach is easy to use, cheap to implement, and encourages the formal specification of hardware components through the reward of automatic testing and simple failure cases. Matthew Naylor 0002, Simon W. Moore |
MEMOCODE | 1 |
| 2014 | Rapid codesign of a soft vector processor and its compilerabstractDespite a decade of activity in the development of soft vector processors for FPGAs, high-level language support remains thin. We attribute this problem to a design method in which the high-level vector programming interface is only really considered once the processor architecture has been perfected, by which point the designer may be committed to the time-consuming development of a complicated compiler. In this paper, we present the codesign of a soft vector processor and a lightweight compiler, which together lift the level of abstraction for the programmer while allowing a rapid compiler implementation phase.We demonstrate the effectiveness of our approach on a range of applications from digital signal processing, neuroscience, and machine learning. Matthew Naylor 0002, Simon W. Moore |
FPL | 1 |
| 2013 | A spiking neural network on a portable FPGA tabletabstractWe will demonstrate a portable FPGA tablet running a spiking neural network for handwriting recognition. The user draws digits on the tablet's touch-screen, and the neural network performs digit recognition. Matthew Naylor 0002, Paul James Fox, A. Theodore Markettos, Simon W. Moore |
FPL | 1 |
| 2013 | Managing the FPGA memory wall: Custom computing or vector processing?abstractManaging the memory wall is critical for massively parallel FPGA applications where data-sets are large and external memory must be used. We demonstrate that a soft vector processor can efficiently stream data from external memory whilst running computation in parallel. A non-trivial neural computation case study illustrates that multi-core vector processing coupled with careful layout of data structures performs similarly to an elaborate full-custom memory controller and execution pipeline. The vector processing version was far simpler to code so we encourage others to consider vector machines before contemplating a full-custom architecture on FPGA. Matthew Naylor 0002, Paul James Fox, A. Theodore Markettos, Simon W. Moore |
FPL | 1 |