Alastair F. Donaldson

News

Offloading Threading Building Blocks (August 2010) George Russell from Codeplay just presented joint work with me, others at Codeplay, and Paul Keir at Glasgow, on using the Offload C++ system to get a subset of Intel's TBB running across the SPE cores of the Cell processor. Check it out.

HiPEAC Collaboration Grant (June 2010) Albert Cohen, Sean Halle (INRIA) and I have been awarded a HiPEAC collaboration grant to work on Scalable Verification of Side Effects for Portable Parallelism.

Intel SCC Research Project (June 2010) Intel have accepted a proposal on Programming Tools for the Intel Single-chip Cloud Computer, which I put together with Paul Kelly at Imperial College London, and colleagues at Codeplay Software Ltd. The result is that Intel will grant us access to their 48-core research platform, to investigate formal verification and performance optimization techniques. Watch this space!

Symmetry Survey (April 2010) Thomas Wahl and I have published an up-to-date survey of symmetry reduction techniques for model checking. Check it out here. This survey complements and extends a previous ACM Computing Surveys article on the topic, which I published with Alice Miller and Muffy Calder.

Short Bio

• 2010-: Research Fellow, Wolfson College Oxford
• 2009-: EPSRC Postdoctoral Research Fellow, University of Oxford
• 2007-2009: Research Engineer at Codeplay Software Ltd.
• 2005: Summer intern, Graham Technology
• 2003-2007: PhD in Computing Science, University of Glasgow, supervised by Alice Miller
• 2002: Summer intern, Reuters Plc.
• 1999-2003: BSc in Computing Science and Mathematics (combined), University of Glasgow

Tools

• SCRATCH - automatic DMA race analysis for the Cell BE processor
• Offload C++ - a framework for offloading portions of C++ applications to run across the SPE cores of the Cell BE processor. Designed and developed by Codeplay Software Ltd. (my former employer)
• TopSPIN - an automatic symmetry reduction package for the SPIN model checker
• Etch - an enhanced type checker for Promela. Etch can statically detect type errors in Promela specifications that are missed by the SPIN tool
• GRIP - a symmetry reduction tool for the PRISM model checker

Research Outline

I am interested in automated techniques for helping developers to write reliable software that runs efficiently on modern hardware.

Formal verification techniques for multicore software. I am especially interested in lightweight, automatic formal verification techniques, capable of operating directly on source code, that can be implemented as efficient tools to be used in day-to-day software development. My current research in this area is on static data-race analysis for multicore programs, based on:

• symbolic model checking
• k-induction
• abstract interpretation
• Craig interpolation
• separation logic

Other verification-related interests include predicate abstraction for concurrent programs, and symmetry reduction techniques for model checking.

Software performance optimization for multicore processors. To take advantage of modern multicore processors, we need suitable abstractions to allow programmers to write high-level, portable programs, from which efficient parallel code can be generated. I got interested in this area while working as a Research Engingeer at Codeplay Software Ltd., and continue to collaborate with Codeplay on this topic, as well as with the group of Prof. Paul Kelly at Imperial College London.

Selected Papers

List of all my papers.

• Automatic Analysis of Scratch-pad Memory Code for Heterogeneous Multicore Processors (TACAS'10)
• Offload - Automating Code Migration to Heterogeneous Multicore Systems (HiPEAC'10)
• On the Constructive Orbit Problem (Annals of Mathematics and Artificial Intelligence)
  This is an extended version of a paper at FM'06
• Language-level Symmetry Reduction for Probabilistic Model Checking (QEST'10)
• Deriving Efficient Data Movement From Decoupled Access/Execute Specifications (HiPEAC'09)
• Automatic Symmetry Detection for Promela (Journal of Automated Reasoning)
  This is an extended version of a paper at FM'05
• Compile-time and Run-time Issues in an Auto-parallelisation System for the Cell BE Processor (HPPC'08)
• Symmetry in Temporal Logic Model Checking (ACM Computing Surveys)

Teaching

SICSA International Summer School on Advances in Programming Languages, Heriot-Watt University, Edinburgh, August 2009:

• Gave lecture entitled Multicore Compilation: an Industrial Approach, and designed practical session based on Codeplay's Offload C++.

At Oxford:

• Software Verification (Hilary Term 2010). Designed and oversaw practicals on Bounded Model Checking and Counter Example Guided Abstraction Refinement.
• Compilers (Hilary Term 2010). Gave guest lectures on Type Checking and Runtime Environments. Also took classes and helped with practicals.
• Object-Oriented Programming (Michaelmas Term 2009). Gave guest lectures on Object Identity and Memory Management. Took students from Merton College and Corpus-Christi College for tutorial sessions.

Guest lectures while at Codeplay Software Ltd:

• Advances in Programming Languages course at University of Edinburgh (2008 and 2009). Gave guest lectures: The Cell Processor: a Compiler Challenge (2008) and Method Duplication: Automating Code Migration to Multicore (2009).
• Compilers course at University of Glasgow (2008 and 2009). Gave same guest lectures as for the Edinburgh course above.

At Glasgow:

• Data Structures and Algorithms (Autumn 2006). Gave guest lectures on Abstract Data Types and Binary Trees.
• CS1P Introductory Programming (2002-2006). Tutored groups of 1st year undergraduates.
• CS1Q Introduction to HCI, Databases and Systems (2002-2006), Tutored groups of 1st year undergraduates.

Service

• I am serving/have served on the PC of:
  • HPCC 2010
  • 3PGCIC 2010
  • HIPS 2010
  • MuCoCoS 2010
  • International Symmetry Conference 2007
• Co-chair: 6th International Workshop on Symmetry and Constraint Satisfaction Problems, Nantes, France, 2006
• Organizer: 27th Scottish Theorem Proving Seminar, Glasgow, UK, 2006
• Co-organizer: SymNet Workshop on "Almost Symmetry" in Search, New Lanark, UK, 2005 (funded by the SymNet EPSRC Network of Excellence)

Acknowledgement

The design of this website has been borrowed, with permission, from Daniel Kroening.