Papers, Talks and Patents

My Google Scholar and DBLP pages.


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


Specifications: The Next Verification Bottleneck

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.

Trusting Large Specifications: The Virtuous Cycle

First talk emphasizing the importance of having multiple users of a single specification.

Trustworthy Specifications of ARM System Level Architecture

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]


US 14/606,510 Exponent Monitoring
Guy Larri, Lee Douglas Smith, David Raymond Lutz, Alastair David Reid, US Patent Application, November 2014
US 14/461,664 Data processing apparatus and method for controlling performance of speculative vector operations
Alastair David Reid, Daniel Kershaw, US Patent Application, October 2013
US 9,696,994 Apparatus and method for comparing a first vector of data elements and a second vector of data elements
Alastair David Reid, US Patent, December 2011
US 9,557,995 Data processing apparatus and method for performing segmented operations
Mbou Eyole-monono, Alastair David Reid, Matthias Lothar Böttcher, Giacomo Gabrielli, US Patent, February 2014
US 9,483,438 Apparatus and method for controlling the number of vector elements written to a data store while performing speculative vector write operations
Alastair David Reid, Daniel Kershaw, US Patent, October 2013
US 9,176,737 Controlling the execution of adjacent instructions that are dependent upon a same data condition
Alastair David Reid, US Patent, February 2011
US 9,098,265 Controlling an order for processing data elements during vector processing
Alastair David Reid, US Patent, July 2011
US 9,081,564 Converting scalar operation to specific type of vector operation using modifier instruction
Alastair David Reid, US Patent, April 2011
US 9,021,233 Interleaving data accesses issued in response to vector access instructions
Alastair David Reid, US Patent, September 2011
US 8,887,001 Trace data priority selection
John Michael Horley, Michael John Williams, Katherine Elizabeth Kneebone, Alastair David Reid, US Patent, February 2010
US 8,359,588 Reducing inter-task latency in a multiprocessor system
Alastair David Reid, US Patent, November 2009
US 8,250,549 Variable coherency support when mapping a computer program to a data processing apparatus
Alastair David Reid, Edmund Grimley-Evans, Simon Andrew Ford, US Patent, October 2006
US 8,200,948 Apparatus and method for performing re-arrangement operations on data
Daniel Kershaw, Dominic Hugo Symes, Alastair David Reid, US Patent, December 2006
US 8,190,807 Mapping a computer program to an asymmetric multiprocessing apparatus
Alastair David Reid, Edmund Grimley-Evans, Simon Andrew Ford, US Patent, October 2006
US 8,185,724 Monitoring values of signals within an integrated circuit
Simon Andrew Ford, Alastair David Reid, US Patent, March 2006
US 8,020,039 Recovering from errors in streaming DSP applications
Alastair David Reid, Daryl Wayne Bradley, US Patent, December 2007
US 7,809,989 Performing diagnostic operations upon an asymmetric multiprocessor apparatus
Simon Andrew Ford, Alastair David Reid, Katherine Elizabeth Kneebone, Edmund Grimley-Evans, US Patent, October 2006
US 7,805,595 Data processing apparatus and method for updating prediction data based on an operation's priority level
Emre Özer, Alastair David Reid, Stuart David Biles, US Patent, April 2007
US 7,574,314 Spurious signal detection
Simon Andrew Ford, David Michael Bull, Alastair David Reid, US Patent, October 2006