|PhD 19||Defining interfaces between hardware and software: Quality and performance|
|POPL 19||ISA Semantics for ARMv8-A, RISC-V, and CHERI-MIPS|
|ARW 18||Detailed Models of Instruction Set Architectures: From Pseudocode to Formal Semantics|
|OOPSLA 17||Who guards the guards? Formal Validation of the ARM v8-M Architecture Specification|
|IEEE Micro||The ARM Scalable Vector Extension|
|FMCAD 16||Trustworthy Specifications of ARM v8-A and v8-M System Level Architecture|
|CAV 16||End-to-End Verification of ARM Processors with ISA-Formal|
|DATE 14||Advanced SIMD: Extending the reach of contemporary SIMD architectures|
|CASES 08||SoC-C: efficient programming abstractions for heterogeneous multicore systems on chip|
|MICRO 08||From SODA to scotch: The evolution of a wireless baseband processor|
|SBAC-PAD 07||Low-cost Techniques for Reducing Branch Context Pollution in a Soft Realtime Embedded Multithreaded Processor|
|SiPS 06||Design and Implementation of Turbo Decoders for Software Defined Radio|
|SDR 06||SPEX: A programming language for software defined radio|
|TECS 05||Eliminating stack overflow by abstract interpretation|
|ASPLOS 04||HOIST: a system for automatically deriving static analyzers for embedded systems|
|ACP4IS 03||Lock inference for systems software|
|EMSOFT 03||Eliminating Stack Overflow by Abstract Interpretation|
|RTSS 03||Evolving real-time systems using hierarchical scheduling and concurrency analysis|
|Haskell FFI||The Haskell 98 Foreign Function Interface 1.0: An Addendum to the Haskell 98 Report|
|ICSE 02||Static and dynamic structure in design patterns|
|ASPSE 01||Aspect Weaving as Component Knitting: Separating Concerns with Knit|
|PADL 01||FVision: A Declarative Language for Visual Tracking|
|GLib 01||The Hugs Graphics Library (Version 2.0)|
|OSDI 00||Knit: Component Composition for Systems Software|
|ICSE 99||Prototyping Real-Time Vision Systems: An Experiment in DSL Design|
|PLDI 99||A Semantics for Imprecise Exceptions|
|Haskell Report||Haskell 98: A non-strict, purely functional language|
|Haskell Lib||Standard Libraries for the Haskell 98 Programming Language|
|IFL 98||Putting the Spine Back in the Spineless Tagless G-Machine: An Implementation of Resumable Black-Holes|
|Exceptions||Handling Exceptions in Haskell|
|StdLib 98||Designing the Standard Haskell Libraries|
|Haskell 97||Green Card: a foreign-language interface for Haskell|
|Haskell 95a||Adding Records to Haskell|
|Haskell 95b||A Proposal for the Standard Haskell Libraries|
|GFPW 94||Malloc Pointers and Stable Pointers: Improving Haskell's Foreign Language Interface|
|GFPW 93||Implementing Fudgets with Standard Widget Sets|
|MSc 93||A Precise Semantics for Ultraloose Specifications|
|GFPW 89||Designing Data Structures|
The Hardware-Software Interface: Quality and Performance
One of the most important interfaces in a computer system is the interface between hardware and software. This talk examines two critical aspects of defining the hardware-software interface: quality and performance.
The first aspect concerns the “radical” idea of creating a single, high-quality, formal specification of microprocessors that everybody can use. This idea does not seem “radical” until you realize that standard practice is for every group to create their own version of a specification in their preferred toolchain. I will describe the challenges that lead to this behavior and how to overcome the challenges. This project lead to the creation of Arm’s official formal specification of their microprocessors and to the formal validation of Arm’s processors against that specification.
The second aspect concerns the tradeoff between portability and performance in the context of high performance, energy efficient, parallel systems. I will describe the challenges in balancing portability and performance and how I overcame them by defining the hardware-software interface in terms of extensions of the C language. This project played a key part in creation of a software-defined radio system capable of implementing the 4G cellphone protocol.
The Arm architecture is the largest computer architecture by volume in the world; it behooves us to ensure that the interface it describes is appropriately defined.
- Computer Science Department, Glasgow, UK. 21 February, 2019 [pdf]
Engineering and Using Large Formal Specifications
We have great tools and technique to formally verify hardware and software but, if we are apply these to real world systems, we need high quality specifications of real world artifacts such as processors, OSes, libraries, programming languages and internet protocols. This talk is about how we are going to avoid a specification bottleneck - it uses my experience in formalising the ARM processor architecture to suggest an approach that we can use on other large, complex hardware and software to create the specifications we need.
What makes processors fail - and how to prevent it
A more accessible presentation of the ideas in the ISA-Formal paper for the Electromagnetic Field maker festival.
Modern processors are amazing devices: small, fast, low power and getting better with every generation. But the most amazing things about modern microprocessors is that they work so incredibly reliably despite all their incredible complexity.
This talk is about the battle between complexity and correctness and about how new formal verification tools can be used to help you design higher performance processors that actually work. I will describe the common optimisations, the bugs that these often introduce and how open source tools such as SAT solvers and bounded model checkers can be used to find these bugs.
Creating Formal Specifications of the Arm Processor Architecture
A talk about why creating formal specifications for real world systems is hard and what we can do about it. Some of the key problems are the semantic gap between the architects’ intention and the written specification; challenges persuading different groups to adopt a common specification; the number and diversity of existing implementations; and the practical impossibility of formally verifying all implementations against the specification. I discuss lessons learned when creating a formal specification of the Arm Processor Architecture and using that specification to formally validate processors against the specification. And I discuss how those lessons can be applied in other contexts. This includes use of traditional testing, formal validation, social engineering and building a virtuous cycle to drive up the quality of the specification.
Agence National de la sécurité des systèmes d’information (ANSSI)
Invited talk, Paris, France. 24 October, 2018. [pdf]
Specifications: The Next Verification Bottleneck
A talk about the importance and difficulty of creating trustworthy specifications of all the software and protocols we will need to verify software and about the techniques I used to create a trustworthy specification of the ARM processor architecture.
- ENTROPY 2018: ENabling TRust through Os Proofs…and beYond
Invited talk, Villeneuve d’Ascq, France, 25-26 January, 2018. [pdf]
How can you trust formally verified software?
A talk about practical things you can do with ARM’s executable formal specification with an emphasis on security research. Despite having the same title, this is a completely different talk from the next one. TUWAT!
How can you trust formally verified software?
A gradually evolving series of talks about my work on creating correct formal specifications (when there are multiple implementations already in existence). Reinforces the idea of having multiple users of a single specification and includes a short version of the FMCAD16, CAV16 and OOPSLA17 talks.
High Performance Embedded and Distributed Systems (HiPEDS) seminar series
Invited talk, Imperial College London, UK, 6th November, 2017. [pdf]
Formal Aspects of Computing Science (British Computer Society)
Invited talk, London, UK, 29th September, 2017. [pdf]
Reliable, Secure and Scalable Software Systems (RS4) Workshop
Invited talk, Glasgow, UK, 1st September, 2017. [pdf]
(Completely rewritten from May version.)
Invited talk, Cambridge, UK, 22nd May, 2017.
Queen Mary University
Invited talk, London, UK, 30th November, 2016. [pdf]
Trusting Large Specifications: The Virtuous Cycle
First talk emphasizing the importance of having multiple users of a single specification.
- The 4th South of England Regional Programming Language Seminar (S-REPLS 4)
Imperial College London, UK, 27th September, 2016. [pdf]
Trustworthy Specifications of ARM System Level Architecture
- First Deepspec Workshop, Princeton, NJ, USA, 7th June, 2016.
Backwards compatible formalization of the ARM Architecture
First public talk about creating formal specifications of ARM processors.
- Cambridge University Computer Laboratory
Cambridge, UK, February, 2012. [pdf]