Our paper, Randomised Testing of the Compiler for a Verification-Aware Programming Language, won Best Paper at the Industry track of ICST 2024! This is a collaboration between me and two outstanding MEng students, Dilan Sheth and Alex Usher at Imperial, and Jean-Baptiste Tristan at Amazon, and was supported by an Amazon Research Award.

Our paper, Validating Database System Isolation Level Implementations with Version Certificate Recovery, led by Jack Clark, won a Best Paper award at EuroSys 2024 in Athens!

I am delighted to be selected as one of the recipients of an Amazon Research Award on Validating Compilers for the Dafny Verified Programming Language, following on last year’s Amazon Research Award on DafnyDefender: automated testing for the Dafny ecosystem.

We will be presenting three papers at the upcoming ISSTA conference in Seattle!

GrayC: Greybox Fuzzing of Compilers and Analysers for C is about a new technique and tool for finding (crash) bugs in compilers and analysers for the C programming language, by performing coverage-guided fuzzing using custom mutators tailored specially for C. It is joint with Karine Even-Mendoza (former Imperial postdoc, now faculty at King’s College London), Arindam Sharma (Imperial PhD student) and Cristian Cadar.

RustSmith: Random Differential Compiler Testing for Rust is a tool demonstration paper about the first (to our knowledge) tool aimed at differential testing of Rust compilers. It seems that the official Rust compiler, rustc, is pretty reliable: RustSmith did not find any new bugs, though the tool was able to find a number of (new to us) historical bugs, and provide some coverage improvements. This is based on the excellent MEng thesis work of Mayank Sharma, and is also a collaboration with Imperial PhD student Pingshi Yu.

Grammar Mutation for Testing Input Parsers presents a new technique for grammar-based fuzzing that involve mutating the grammar itself to generate weird - but not too weird - inputs. It is a “registered report”, which means that it sets out a plan for a large experimental campaign (yet to be run) to evaluate the idea. This idea and plan will be presented at the FUZZING workshop. The work is led by Bachir Bendrissou (Imperial PhD student) and is joint with Cristian Cadar.

Delighted that a new paper, Program Reconditioning: Avoiding Undefined Behaviour When Finding and Reducing Compiler Bugs, will appear at PLDI 2023. This is joint work with former masters students Bastien Lecoeur and Hasan Mohsin. I’m very fortunate to get to work with such talented students at Imperial!

The paper focuses on the problem of what to do about programming language undefined behaviour when deploying random differential testing and test case reduction to find compiler bugs.

This paper is close to my heart and has been a bit of a labour of love - rejected from PLDI 2022 and FSE 2022 (but with very useful reviewer feedback). I hope people find it interesting.

Check it out!

Happy New Year everybody! Having not posted any news for a while, here is a summary of some of the exciting things that have been happening since June!

• New PhD students: Bachir Bendrissou and Pingshi Yu joined the group as PhD students (with Bachir being co-supervised by Cristian Cadar)

• New postdoc: Chengsong Tan has joined the group as a postdoc on the IRIS project, working under my and John Wickerson‘s guidance

• Dan Iorga passed his viva: Dan Iorga (co-supervised with John Wickerson) successfully defended his PhD thesis, “Memory Models for Heterogeneous Systems”, in November - congratulations Dan!

• Inaugural Lecture: I gave my Inaugural Lecture, “My Plan B” - check it out on YouTube!

• Most Influential Paper award: Our paper on GPUVerify from 2012 won the Most Influential Paper award at OOPSLA 2022! At time of writing the only evidence for this claim comes from Twitter, but the announcement should make it here in due course.

• Paper at POPL 2023: We have had a paper, “Taking Back Control in an Intermediate Language for GPU Computing”, accepted at POPL 2023 - check it out! The paper is about using formal modelling techniques to improve the SPIR-V programming language - see this tweet summary. Joint work with Vasileios Klimis, Jack Clark and John Wickerson at Imperial, and our collaborators Alan Baker and David Neto at Google.

• Paper at ICST 2023 Industry Track: During 2021 and 2022 I spent time as a Visiting Researcher at Google working on compiler testing techniques for the WebGPU and SPIR-V shading languages. We have had a paper, “Industrial Deployment of Compiler Fuzzing Techniques for Two GPU Shading Languages”, describing this experience accepted at the industry track of the ICST 2023 conference. The work features contributions from two excellent former Imperial undergraduates, Hasan Mohsin and Hana Watson, as well as Vasyl Teliman, an independent contributor based in Ukraine, and Ben Clayton, Ryan Harrison and David Neto at Google. Draft available soon!

• Paper at CC 2023: George Mitenkov, formerly an undergrad at Imperial, did an excellent BEng project jointly with members of the Blue Brain team at EPFL, on generating efficient vector and GPU code from the NMODL domain specific language using LLVM IR. We have just had a paper on this work, entitled “MOD2IR: High-Performance Code Generation for a Biophysically Detailed Neuronal Simulation DSL”, accepted at the CC 2023 conference - this is joint work with George Mitenkov, Ioannis Magkanaris, Omar Awile, Pramod Kumbhar and Felix Schürmann. Draft available soon!

Looking forward to an exciting year ahead!

It’s wonderful to be back at an in-person conference - PLDI’22 in San Diego. Dan Iorga will present last year’s OOPSLA paper on CPU/FPGA memory models. I enjoyed participating in the Student Research Competition as a judge, and am looking forward to the Steering Committee meeting.

Frank Busse, Pritam Gharat, Cristian Cadar and I have had an experience paper accepted at ISSTA 2022 on various attempts to combine static analysis and dynamic symbolic execution.

The paper actually reports a couple of negative results: the static analysers we investigated are not able to find real-world bugs in the kinds of applications we were able to apply the KLEE tool to, and on a large set of synthetic bugs we found that equipping KLEE with information from candidate error traces reported by static analysers did not actually help much in accelerating KLEE’s progress towards the bug. I was pleased that the ISSTA reviewers were receptive to the idea of publishing these negative results, which we hope will provide inspiration for future work.

Check out the paper.

Check out our paper, High-coverage Metamorphic Testing of Concurrency Support in C Compilers, with Matt Windsor and John Wickerson, that just appeared in the STVR journal!

I took a bit of a break from PC service after serving as PC chair for ECOOP 2019 and general chair for PLDI 2020, and while I was only part time in academia. But now, it is my honour to have recently served on, or be due to serve on, some exciting program committees, including ECOOP 2022, CAV 2022, ASE 2022 and POPL 2023.

I’m excited that Matt Windsor will be giving a demonstration today of C4, the C Compiler Concurrency Checker, at ISSTA 2021. Check out our tool demonstartion paper on C4.

We have had two papers conditionally accepted at OOPSLA 2021, which I’m very much hoping to be able to attend in person in October.

“The semantics of shared memory in Intel CPU/FPGA systems” was led by PhD student Dan Iorga, and is a collaboration with John Wickerson, Tyler Sorensen and myself. In this paper we study the memory model of a recent combined CPU/FPGA system from Intel, presenting operational and axoimatic versions of the memory model, and show how formal specification and tools can be used to reason about and generate litmus tests. Check out John’s blog post about the paper!

“Specifying and testing GPU workgroup progress models” was led by Tyler Sorensen, and is a collaboration with former Princeton undergraduates Lucas Salvador and Harmit Raval, Hugues Evrard at Google, myself and John Wickerson at Imperial, and Margaret Martonosi at Princeton. Rather like the CPU/FPGA paper, we also apply formal specification and tooling, but this time to the domain of GPU execution models, allowing a variety of GPU schedulers to be described at a high level of abstraction using process algebra, using model checking to determine whether particular execution model litmus tests are guaranteed to terminate with respect to a given progress model, and using the Alloy tool to synthesise execution model conformance tests.

Drafts available after we make changes requested by the reviewers.

Check out this song, “Pure Implementation”, based on the music of “Pure Imagination” but with new lyrics by John Wickerson, arrangements and production by me, and contributions from many members of the PL community, to help promote the upcoming PLDI 2021 conference:

I’m delighted that Vasileios Klimis has joined us as a Postdoctoral Research Associate, to work with John Wickerson and myself as part of the IRIS Programme Grant. Welcome Vasileios!

I’m really happy that our paper, “Test-Case Reduction and Deduplication Almost for Free with Transformation-Based Compiler Testing”, has been accepted at PLDI 2021! Check out the paper; check out the artifact.

This paper shows that transformation-based compiler testing - a kind of metamorphic testing that involves applying semantics-preserving transformations to an initial program to obtain an equivalent program that should yield the same result when executed - can be designed in a manner that yields a form of test case reduction and a heuristic for bug de-duplication automatically. We devised this take on transformation-based testing when building the spirv-fuzz compiler testing tool, for the SPIR-V programming model, one of the main open source projects I contributed to while at Google.

This is joint work with Paul Thomson at Google (former Multicore group member), and with Vasyl Teliman and André Perez Maselco, who did Google Summer of Code with us during 2020, and Stefano Milizia and Antoni Karpiński, who did internships in our team at Google during 2020.

We were delighted to hear that our paper, “Dreaming Up Metamorphic Relations: Experiences from Three Fuzzer Tools”, was selected as Best Paper at the upcoming MET workshop on Metamorphic Testing. Check out the paper, which is joint work with Andrei Lascu, Matt Windsor, Tobias Grosser, John Wickerson and myself.

I’m delighted that Andrei Lascu, Tobias Grosser, Torsten Hoefler and I have a paper on metamorphic fuzzing of C++ libraries at ICST. Check out the paper!

After a thrilling 2.5 years being mainly an industrialist, with a part time position in academia, I’m excited to have returned full time to my Professor position at Imperial College London!

I really enjoyed being Ashish Darbari‘s guest for his latest Axiomise podcast.

Check it out:

I’m really delighted to have been promoted to Professor of Programming Languages! Thanks to all my wonderful collaborators, colleagues and students, and to the Department and College, for supporting me in my career so far.

Karine Even-Mendoza, Cristian Cadar and I have a paper, Closer to the Edge: Testing Compilers More Thoroughly by Being Less Conservative About Undefined Behaviour, at the New Idea track at the ASE 2020 virtual conference.

The paper proposes investigating how much further we can go with compiler testing if we relax the methods that compiler fuzzers put in place to ensure that programs are free from undefined behaviours. Programs need to be UB-free if they are to be useful for finding bugs, but putting in place overly restrictive methods for avoiding UB can limit the diversity of programs, so that bug finding ability is limited.

The work already led to a couple of previously unknown GCC bugs (1, 2) that regular Csmith could not find, but that our new appraoch (which builds on Csmith) could find, which the GCC developers promptly fixed.

Thanks to everyone who helped to make Virtual PLDI 2020 a big success!

I have written a report on the conference which I hope will be useful to future organizers of virtual conferences.

Dan Iorga, Tyler Sorensen, John Wickerson and I have a paper on multicore interference at RTAS 2020. Check it out: Slow and Steady: Measuring and Tuning Multicore Interference.

As General Chair of PLDI 2020, which I will host in London in June, I encourage you to submit your most exciting workshop and tutorial ideas, and your best papers, to the event! Deadlines are coming up in November - see important dates on the website.

Our paper “One Size Doesn’t Fit All: Quantifying Performance Portability of Graph Applications on GPUs”, by Tyler Sorensen, Sreepathi Pai and myself, received Best Paper Award at the IISWC 2019 conference!

I’m thrilled that a paper that aims to evaluate the impact of fuzzer-found compiler bugs has been accepted at the OOPLSA 2019 conference. The paper, “Compiler Fuzzing: How Much Does It Matter?”, led by Michael Marcozzi and Qiyi Tang, and co-authored by Cristian Cadar and myself, proposes a methodology for assessing the impact of compiler bugs on the reliability of widely-used software applications, and compares the impact of fuzzer-found bugs and user-reported bugs on a large set of Debian packages.

Check out the paper and the associated artifact.

Daniel Liew, Cristian Cadar, J. Ryan Stinnett and I recently had a paper accepted at the ESEC/FSE conference: “Just Fuzz It: Solving Floating-Point Constraints using Coverage-Guided Fuzzing”. Thanks to Dan for delivering the talk at the conference in Tallin!

Tyler Sorensen, Sreepathi Pai and I have had a paper, “One Size Doesn’t Fit All: Quantifying Performance Portability of Graph Applications on GPUs”, accepted at the 2019 IEEE International Symposium on Workload Characterization (IISWC’19).

I’m really excited that we have two papers that will appear at the ECOOP 2020 virtual conference.

Test-Case Reduction via Test-Case Generation: Insights From the Hypothesis Reducer, with David MacIver, is a tool insights paper that focuses on the novel approach to test case reduction taken by the Hypothesis property-based testing tool.

Putting Randomized Compiler Testing into Production, with Hugues Evrard and Paul Thomson, is an experience report describing what we’ve been doing at Google in relation to the GraphicsFuzz project — a research project that we started at Imperial College London.

The ECOOP conference recently took place in London - along with CurryOn and various other events, and I think went really well!

I enjoyed giving a talk about GraphicsFuzz at CurryOn (with my Google hat on).

I served as Program Chair for ECOOP - check out the great papers in the proceedings.

Many congratulations to the General Chair of the whole event, Laurence Tratt, for putting on a great show.

I presented Christopher Lidbury and my paper, “Sparse Record and Replay with Controlled Scheduling” at PLDI 2019 in Phoenix Arizona.

I also gave an invited talk at the Programming Languages Mentoring Workshop, giving advice on how to cope when suffering from lack of novelty in your research. I didn’t share slides for that talk, as it was a bit of an experiment, but am happy to share them individually to folks who are interested.

I am really honoured to have been awarded an Imperial College President’s Medal for Excellence in Innovation and Entrepreneurship in relation to my work on GraphicsFuzz!

I had a great time at the 4th International Workshop on Metamorphic Testing, where I gave the keynote on the applications of metamorphic testing to graphics drivers that we started at Imperial College London and are now taking forward at Google via the GraphicsFuzz project.

Check out the extended abstract associated with my talk.

I am delighted that the extended abstract by Tyler Sorensen, Sreepathi Pai and myself, “Performance Evaluation of OpenCL Standard Support (and Beyond)”, is the recipient of Best Paper Award at the 2019 International Workshop on OpenCL (IWOCL)!

I am honoured to be serving on the Program Committee for the POPL 2020 conference.

Dan Iorga visited Rapita Systems and talked about the approach of our group to evaluating worst-case execution time on multicore systems. Check it out here.

The GraphicsFuzz code base has now been open sourced by Google, where I am continuing to work on it with Hugues Evrard and Paul Thomson. Check out the GitHub repo, and this press coverage from Phoronix.

I’m really excited that my company, GraphicsFuzz, has been acquired by Google, and that I’ll be joining the Android Graphics team whilst maintaining a part-time appointment at Imperial. Check out the announcement.

We are hiring for a 2.5 year postdoc to work on reasoning techniques for many-core systems where performance and reliability are both of prime importance. This is part of the EPSRC-funded IRIS Programme Grant. The post will be co-supervised by John Wickerson.

Closing date is 1 July 2018.

Here is the job advert.

Please get in touch informally if you are interested and have questions!

We are hiring for a 2.5 year postdoc to work on novel methods for testing graphics drivers for security issues!

Here’s a blog post about the broad area of the project, and here is the job advert.

Please get in touch informally if you are interested and have questions.

We are excited to be starting a new research project, “Automatic Detection of Rendering-Related Security Vulnerabilities in Web Browsers”, funded by the Google Chrome University Research Program.

I’m honoured to be serving as Chair of the Programme Committee for the 2019 European Conference on Object-Oriented Programming (ECOOP).

Last week I gave the BCS Roger Needham Lecture at the Royal Society. A video of the slides + audio is now available:

Our paper “Floating-Point Symbolic Execution: A Case Study in N-version Programming” was recipient of the Best Experience Report award at the ASE conference last week! Here are my co-authors Daniel Liew, Daniel Schemmel and Cristian Cadar collecting the award:

Daniel Liew presented the paper, also co-authored with Raphael Zaehl and Klaus Wehrle, which describes a controlled experiment in which two teams, one at Imperial, the other at RWTH Aachen University, independently developed extensions to the KLEE symbolic execution engine to support floating-point arithmetic, together with independently developed-and-collected benchmarks used to assess the quality of the other team’s tool. This study came about by chance, upon the Imperial and Aachen sites discovering that each other had reached roughly the same stage in separately adding floating-point support to KLEE. We decided to use the opportunity to do an N-version programming study (with N=2), and the paper reports on the experience.

Our paper “Cooperative Kernels: GPU Multitasking for Blocking Algorithms” was selected for a Best Paper Award at the ESEC/FSE conference this week! Here are my co-authors Tyler Sorensen and Hugues Evrard collecting the award:

Tyler presented the paper, and I also presented on a recent IEEE Transactions on Software Engineering paper about candidate-based invariant generation, which was joint work with Adam Betts, Nathan Chong, Pantazis Deligiannis and Jeroen Ketema, all former members of the Multicore group.

This week I gave a tutorial at the CONCUR conference, entitled “Forward Progress on GPU Concurrency”. I gave an overview of what it’s like to program using OpenCL, and demonstrated the GPUVerify tool that we have developed at Imperial. I then did some live coding of a global synchronization barrier, illustrating how one needs to use OpenCL’s memory model to get this to work correctly, and showing how even then there is the possibility of deadlock due to lack of forward progress guarantees by GPU schedulers. I then coded up the discovery protocol we proposed in our OOPSLA 2016 paper to allow a portable barrier to be implemented.

It was fun getting my hands dirty with some low-level OpenCL programming! Thanks to everyone who attended the tutorial.

Jeroen Ketema, Tyler Sorensen, John Wickerson and I wrote an overview paper to accompany the tutorial, giving a summary of the work that we and various collaborators have done over the last 6 years in relation to GPU concurrency. Check out the paper.

I have been promoted to Reader, the most wonderfully-named British academic rank!

A brief interview in the context of my role as Faculty Sponsor for Imperial’s ACM Student Chapter.

We had a really fun seminar at Schloss Dagstuhl on “Analysis and Synthesis of Floating-point Programs”, which I co-organised with Eva Darulova, Zvonimir Rakamaric and Cindy Rubio Gonzalez.

My colleague George Constantinides has written up a really good synopsis of many of the topics discussed at the workshop, and we’ll in due course put together a Dagstuhl report with more details.

Thanks to all who attended and made it a great event.

I’m really excited that our paper, “Automated Testing of Graphics Shader Compilers” will appear at the OOPSLA 2017 conference. This is the culmination of a lot of work, joint with Hugues Evrard, Andrei Lascu, and Paul Thomson. As well as the paper, check out our series of blog posts on the topic, and our repository of shader compiler bugs!

We’re really pleased that in a recent security bulletin, NVIDIA have confirmed that they have fixed an issue that we found with our GLFuzz tool, as reported in this blog post, crediting us for the bug report. NVIDIA summarise the issue as follows: “NVIDIA GPU Display Driver contains a vulnerability in the kernel mode layer handler where an incorrect detection and recovery from an invalid state produced by specific user actions may lead to a denial of service.” They have also filed the issue as CVE-2017-6259.

We have had a paper, “Floating-Point Symbolic Execution: A Case Study in N-version Programming”, accepted at the 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2017). This is joint work with Daniel Liew and Cristian Cadar at Imperial, as well as with collaborators at RWTH Aachen University.

In this work, we conducted a study in conjunction with Aachen, who we discovered were independently undertaking some similar work to us on adding support for floating-point symbolic execution to the KLEE tool. Rather than racing to try to scoop one another, we teamed up to do a rigorous case study on N-version programming (with N=2), to investigate the similar and different design decisions made in each implementation effort.

Two by-products of this work are:

• a suite of C benchmarks that use floating-point in a manner that is likely useful for evaluating symbolic execution tools

• a large number of QF_FPBV and QF_FPABV benchmarks being contributed to the annual SMT-COMP competition - special thanks to Daniel Liew for this contribution

We hope these will be valuable resources for other researchers!

Our paper, “Cooperative Kernels: GPU Multitasking for Blocking Algorithms”, has been accepted at ESEC/FSE 2017, the 11th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering.

This paper, jointly work with Tyler Sorensen and Hugues Evrard, investigates the challenge of how to share a GPU device between competing workloads, such as graphics and compute, despite the fact that GPU schedulers are not usually fair.

Check out the paper!

I am honoured to be the recipient of the 2017 BCS Roger Needham Award.

Apple’s details of the security content of iOS 10.3 includes an acknowledgement of a fix for a security problem that Paul Thomson found using GLFuzz, described in this Medium post.

Apple give the following details about the problem:

Impact: Processing maliciously crafted web content may result in the disclosure of process memory

Description: An information disclosure issue existed in the processing of OpenGL shaders. This issue was addressed through improved memory management.

The issue is logged as CVE-2017-2424.

I’m very much looking forward to lecturing on how to test programming language implementations at the upcoming Programming Languages Implementation Summer School. Please consider attending!

I’m delighted to be part of the organization teams for two Dagstuhl seminar proposals that were recently accepted:

Analysis and Synthesis of Floating-point Programs will be held in August, and I’m co-organising it with Eva Darulova (MPI-SWS – Saarbrücken, DE), Zvonimir Rakamaric (University of Utah – Salt Lake City, US) and Cindy Rubio-Gonzalez (University of California – Davis, US).

Testing and Verification of Compilers will be held in December, and I’m co-organising it with Junjie Chen (Peking University, CN), Andreas Zeller (Universität des Saarlandes, DE) and Hongyu Zhang (Microsoft Research – Beijing, CN).

We’ve completed our series of blog posts on applying GLFuzz to GPUs from various designers: see our overview post, and posts on testing of devices from

• AMD
• Apple
• ARM
• Imagination
• Intel
• NVIDIA
• Qualcomm

Also check out our GitHub repo summarising the various bugs we found.

We are very excited that GLFuzz has been selected as part of the first cohort of security-related projects supported by the ICURe programme for innovation and commercialisation of university research.

Congratulations to Paul Thomson, who successfully defended his PhD thesis, . Thanks to Kostis Sagonas and Sophia Drossopoulou for serving as external and internal examiners.

For his PhD thesis, Paul worked on a large empirical study on concurrency testing, a new approach to schedule-space reduction based on the lazy happens-before relation, the JESS concurrency testing tool for Java, and contributed to the P# project.

Paul also worked on the GPUVerify project, and is a key contributor to our ongoing GLFuzz project for graphics driver testing.

Check out our Medium post on testing Apple’s graphics drivers for the iPhone. And here’s a video showing that a semantics-preserving transformation can lead to garbage being rendered, due to a driver bug:

Check out some work we’ve been doing on candidate-based invariant generation, using the Houdini algorithm.

Congratulations to Pantazis Deligiannis on successfully defending his PhD thesis, Scalable Techniques for Analysing and Testing Asynchronous Software Systems, and thanks to Earl Barr and Peter Pietzuch for acting as external and internal examiners, respectively.

You can check out Pantazis’s work via his papers at ASE, PLDI and FAST.

Time to celebrate!

I’m doing a series of posts on Medium about my work with Andrei Lascu and Paul Thomson on testing OpenGL shader compilers.

This first post gives an introduction to what we’re doing.

In the remaining posts we will visit the main GPU designers—-AMD, ARM, Imagination Technologies, Intel, NVIDIA and Qualcomm—-one by one in alphabetical order.

The post detailing testing of AMD shader compilers is now up, and here’s a video of an issue we found whereby WebGL can bluescreen a machine:

Christopher Lidbury and I have been working for some time on dynamic data race detection for C++11, seeing whether we can do better than the standard ThreadSanitizer tool at following the subtle definition of data race in C++11, and carving out a decent subset of the memory model that we can simulate operationally during dynamic analysis in order to detect races that can only occur under non sequentially consistent behaviour. We have had a paper on this work accepted at POPL 2017, entitled Dynamic Race Detection for C++11, which we’ll make available soon.

We’re really happy to welcome Hugues Evrard to the Multicore Programming Group as a Postdoctoral RA, working on the Reliable Many-Core Programming project.

Tyler Sorensen and I, in collaboration with Mark Batty, Ganesh Gopalakrishnan and Zvonimimr Rakamaric, have had a paper accepted at OOPSLA 2016, entitled Portable Inter-Workgroup Barrier Synchronisation for GPUs. The paper addresses the problem of how to build a barrier that allow threads in distinct workgroups to synchronise, without a priori assumptions on the number of workgroups that the GPU will schedule concurrently. We report experiments showing that an OpenCL implementation of the barrier works effectively across GPUs from NVIDIA, AMD, Intel and ARM.

Paper draft available soon!

Luis Pina and I are organising the 4th edition of the South of England Regional Programming Languages Seminar (S-REPLS 4) at Imperial College London on 27 September. We’re delighted to have Christophe Dubach as our invited speaker. Please consider attending the event, and get in touch if you would like to contribute a talk.

I’m honoured to be one of the invited speakers at the 2016 Workshop on Dynamic Analysis (WODA), part of SPLASH 2016.

This summer I’m giving several outreach lectures that aim to give high school-age children insights into the simple things that make programs go wrong, the impact that this can have, and the relative ease with which one can learn to program to contribute to the situation (for better or worse!). The events are:

• IET Children’s Engineering Lecture: What Makes Software Go Wrong?
• Y11 Project STEM Summer School
• Engineering Summer School for Y9 girls
• Sutton Trust Summer School for Y12 students

Daniel Liew, Cristian Cadar and I received one of the Best Paper Awards at the IEEE International Conference on Software Testing, Verification and Validation (ICST), for our paper Symbooglix: A Symbolic Execution Engine for Boogie Programs.

Check out the Symbooglix tool on GitHub.

Tyler Sorensen and I have had a paper accepted at PLDI 2016 entitled Exposing Errors Related to Weak Memory in GPU Applications. In the work we explain the systematic design of a memory stressing strategy, inspired by heuristics devised in our previous ASPLOS collaborative paper, to expose weak memory bugs in real-world GPU application requiring only minimal source-level modifications. We also show how the method can be used to harden applications against such bugs.

I have been awarded a five year Early Career Fellowship from the Engineering and Physical Sciences Research Council (EPSRC), on the topic of Reliable Many-Core Programming. The project features collaboration with AMD, ARM, Imagination Technologies and NVIDIA, as well as with Prof Albert Cohen at INRIA. I will soon be advertising for a postdoc position on the project, watch this space!

We have had two papers accepted at the 4th International Workshop on OpenCL (IWOCL).

One paper, The Hitchhiker’s Guide to Cross-Platform OpenCL Application Development, led by Tyler Sorensen, describes challenges associated with achieving functional portability for OpenCL applications across a range of devices, some solutions and work-around, and suggestions for enhancements to OpenCL to make it easier to write portable applications.

The other paper, Automatic Test Case Reduction for OpenCL, is based on Moritz Pflanzer‘s MSc thesis, co-supervised by me and Andrei Lascu. The paper describes an extension to the C-Reduce framework to allow automated reduction of OpenCL test cases. The main new contribution here is ShadowKeeper, a memory analysis plugin for Oclgrind. Our extension to C-Reduce is a companion for CLsmith, our Csmith-based OpenCL kernel fuzzer, allowing both generation and reduction of kernels that trigger OpenCL compiler bugs.

We have two upcoming papers associated with ICSE 2016: a paper at Visions of 2025 and Beyond on analysing program analysers (joint with Cristian Cadar), and a paper at the Metamorphic Testing Workshop (MET) on metamorphic testing for graphics compilers (joint with Andrei Lascu).

The research for the MET paper in part led to us entering, with Tyler Sorensen, some images to the Imperial Innovations Art of Research competition; check out our entries here, one of which was highlighted as a staff choice.

This week Andrei Lascu presented our work on integrating the CLsmith OpenCL compiler fuzzing tool with the Collective Knowledge Framework, at the ADAPT workshop, co-located with HiPEAC. Here is the workshop paper.

Daniel Liew, Cristian Cadar and I have had a paper accepted at ICST 2016, the IEEE International Conference on Software Testing, Verification and Validation.

The paper describes the design and evaluation of Symbooglix, a new symbolic execution tool for the Boogie intermediate verification language. This brings KLEE-style dynamic symbolic execution to any programming languages for which a language-to-Boogie translator exists. We evaluated the work using C programs translated into Boogie by SMACK, and GPU kernels translated to Boogie by GPUVerify. Camera-ready will be online soon!

We have been awarded a grant from GCHQ to enable us to buy a zoo of mobile and tablet devices, to ramp up our activities around testing many-core compilers (started in this PLDI paper), and many-core memory models (building on early ideas in this ASPLOS team effort). We shall continue with OpenCL, but are looking ahead to analysing Vulkan drivers as more become available.

We have had a paper entitled Uncovering Bugs in Distributed Storage Systems during Testing (Not in Production!) accepted at FAST 2016, the 14th USENIX Conference on File and Storage Technologies. The paper describes a number of case studies using the P# programming model, originally presented in this PLDI’15 paper, to model components of distributed systems in order to enable controlled testing, allowing discovery and replay of subtle concurrency-related defects in web services.

The work is a collaboration between Imperial, MIT and Microsoft, and was contributed to in large part by PhD students Pantazis Deligiannis and Paul Thomson undertaking internships with Shaz Qadeer and Akash Lal at Microsoft Research in Redmond and Bangalore.

Camera-ready version available soon!

We have been awarded a Technology Transfer Project from the TETRACOM EU FP7 Coordination Action, to undertake transfer of our many-core compiler fuzzing work, described in this PLDI’15 paper, to dividiti. The project, CK/CLsmith: An Automated Testing Framework for Many-Core Vendor Tools, will use the Collective Knowledge framework for management and mining of large test data sets and results obtained by fuzzing many-core APIs, such as OpenCL and Vulkan, across a diverse range of platforms.

I’m coordinating a series of lectures, the Imperial Programming Lectures, kicking off this week. The lectures are open to all students and staff at Imperial, and external folks are welcome (please email me if you are external and would like to come along). The series will kick off with two lectures on the actor programming model and the Pony language, given by Sylvan Clebsch.

Follow the lectures on Twitter.

Sign up to our mailing list.

John Wickerson, Mark Batty and I have been working for some time on formalising the OpenCL 2.0 memory model, which is based on that of C11. Our work has identified opportunities for modifying the formulation of sequentially consistent (SC) atomics in C11 via slight strengthenings that, we argue, make the model simpler to understand and reason about without disallowing executions of interesting programs, nor invalidating standard compilation schemes. We have also identified issues with the OpenCL memory model that make it impossible to implement SC atomics both correctly and efficiently, and have proposed changes to the model that improve this situation.

Our paper on this work, Overhauling SC Atomics in C11 and OpenCL will appear at POPL 2016. Draft available soon!

During the CARP EU project, we designed a new platform-neutral compute intermediate language, PENCIL, for accelerator programming. PENCIL is a restricted subset of a href="https://gcc.gnu.org/onlinedocs/gcc/C-Extensions.html"GNU C99 that has been designed for ease of compilation, incorporating some extensions to support communicating metadata to compilers. The language has been a collaboration between a href="https://who.rocq.inria.fr/Albert.Cohen/"ENS/INRIA, ARM, Imperial and Realeyes, and dividiti are also actively using the language. Our paper on PENCIL will appear at the PACT conference on Parallel Architectures and Compilation Techniques, and the PENCIL language specification is also available.

John Wickerson, Mark Batty and I have collaborated with Brad Beckmann at AMD Research on a formal study of remote-scope promotion, a language feature proposed by AMD in this ASPLOS’15 paper to enable work-stealing to co-exist with efficient intra-work group communication. In our paper, which will appear at OOPSLA’15, we formalised an extension of the OpenCL memory model that caters for remote scopes, scrutinised the implementation of remote scope promotion proposed in the ASPLOS work, and proved that (after some fixes) the implementation faithfully matches the language-level memory model. The formalisation process was really valuable in identifying some subtle bugs related to memory consistency.

An extended version of Paul Thomson‘s Best Student Paper at PPoPP’14 (joint with me and Adam Betts) has been accepted for publication in the new ACM Transactions on Parallel Computing journal. Check out a preprint of the journal paper, Concurrency Testing Using Controlled Schedulers: An Empirical Study, which studies the effectiveness of several techniques for controlled concurrency testing, including preemption bounding, delay bounding and probabilistic concurrency testing, benchmarking them against a straightforward controlled random scheduling approach.

Pantazis Deligiannis, Zvonimir Rakamaric and I have had a paper entitled Fast and Precise Symbolic Analysis of Concurrency Bugs in Device Drivers accepted at the Automated Software Engineering Conference, about our Whoop project. Draft available soon!

This week we are hosting a two day Concurrency Workshop at Imperial. If you’d like to attend, you are very welcome; please indicate via this Doodle poll.

The HiPEAC Network of Excellence provide awards for members who publish in “conferences in which Europe is not strongly represented”, specifically ASPLOS, DAC, FCCM, HPCA, ISCA, MICRO, PLDI and POPL.

The Multicore Programming Group were pleased to receive three mentions in the HiPEAC 2015 Paper Awards, for our paper (with collaborators at UCL, Utah, Oxford and Cambridge) at ASPLOS’15 and our two papers at PLDI’15 (collaborations with Microsoft Research and UCL). You can get the papers here.

We are delighted to welcome Jacek Burys, Giulio Jiang and Peng Peng to the Multicore Programming Group. Jacek, Giulio and Peng will be working with the group this summer as part of Imperial’s Undergraduate Research Opportunities Programme (UROP), on a bunch of exciting ideas related to compiler testing.

It’s quiet in the Multicore Programming Group: Paul Thomson is interning with Akash Lal at Microsoft Research India, Pantazis Deligiannis with Shaz Qadeer at Microsoft Research Redmond, Christopher Lidbury is at Google in Zurich, and Dan Liew is at Google in Mountain View. Luckily we have three of UROP students arriving soon to liven things up.

After a long writing process (and actually not too long a review process), our article The Design and Implementation of a Verification Technique for GPU Kernels has appeared in ACM Transactions on Programming Languages and Systems. Check out the paper here. This extends our original OOPSLA 2012 paper on GPUVerify.

I attended and gave a talk at S-REPLS, the first South of England Regional Programming Languages Seminar, in Cambridge. It was a really cool event, based on the successful Scottish Programming Languages Seminar series. If you do PL research in the South of England, please consider S-REPLS mailing list.

The tools associated with our PLDI papers were accepted by the PLDI Artifact Evaluation Committee. Check out the camera-ready versions of our Many-Core Compiler Fuzzing paper and our paper on Asynchronous Programming, Analysis and Testing with State Machines.

We are excited to have had two papers accepted at the 36th annual ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI).

One paper, entitled Many-Core Compiler Fuzzing, is joint work with Christopher Lidbury, Andrei Lascu and Nathan Chong (current/former members of my research group) and is about the application of random differential testing and equivalence modulo inputs testing to find defects in OpenCL compilers. We found a lot of compiler defects during this project. Check out our CLsmith tool for generation of random OpenCL kernels.

The other paper, entitled Asynchronous Programming, Analysis and Testing with State Machines, is a collaboration with Pantazis Deligiannis, Jeroen Ketema and Paul Thomson at Imperial, and with Akash Lal at Microsoft Research. The paper describes a new language, P#, for asynchronous programming, together with static and dynamic analysis techniques that leverage features of the new language for scalability.
Drafts of both available soon!

The Multicore Programming Group has been awarded a £36,000 grant from GCHQ to fund a seven week intensive project entitled Detecting Vulnerabilities in Compilers for a Massively Parallel Language, which will allow me and two members of my group to extend the OpenCL compiler testing work associated with our upcoming PLDI paper.

I am excited to be on my way to The Vosges to gives an invited talk at Les vingt-sixièmes Journées Francophones des Langages Applicatifs. Unfortunately (or perhaps fortunately for the audience) I will not be delivering my talk in French!

We just submitted the camera-ready version of a paper entitled GPU Concurrency: Weak Behaviours and Programming Assumptions which has been accepted at ASPLOS. This is a collaboration with Jade Alglave at UCL/Microsoft Research, Tyler Sorensen at UCL (and previously at Utah), Daniel Poetzl at Oxford, Mark Batty at Cambridge, Ganesh Gopalakrishnan at Utah, and Jeroen Ketema and John Wickerson at Imperial. A main contribution of the work is to empirically study the memory consistency of GPUs from Nvidia and AMD, showing that weak behaviours can be observed, and illustrating that these can make it difficult to correctly implement software that exploits fine-grained concurrency on GPUs.

Imagination Technologies are sponsoring a PhD studentship at Imperial as part of the HiPEDS Centre for Doctoral Training. The studentship will be supervised jointly by me (in the Department of Computing) and Prof George Constantinides (in the Department of Electrical and Electronic Engineering), and is on Hardware/Software Co-Optimisation of Concurrent Numerical Software. See this description for details of the project and how to apply.

I’m honoured to have been invited to serve on the Programme Committees for CAV 2015 and POPL 2016.

Cristian Cadar, Philippa Gardner and I ran a workshop, INVEST, on an introduction to verification and testing research, at Imperial. The workshop was targeted at late stage undergrad/MSc students and early stage PhD students.

I am delighted that Christopher Lidbury has joined the Multicore Programming Group as a PhD student, and that Andrei Lascu will work with us over the coming months as a Research Assistant. Chris and Andrei spent the summer working with our group under the Imperial Undergraduate Research Opportunities Programme (UROP).

Congratulations to Nathan Chong, who successfully defended his PhD thesis at the end of October. He was supervised jointly with Paul Kelly. Ganesh Gopalakrishnan made the journey to Utah to act as external examiner, and George Constantinides from our neighbouring EEE department was internal examiner. Well done Nathan!

I gave an invited talk at the AVoCS workshop, which was held at the University of Twente. For the proceedings, I wrote a tutorial overview of the GPUVerify method which you can check out here.

I have been awarded funding from GCHQ for a PhD studentship on the topic of automatic detection of concurrency exploits in systems software. This is through their Academic Centres for Excellence in Cyber Security Research (ACEs CSR) programme. I’m looking for excellent candidates for this position. As the project will involve spending some time on site at GCHQ, candidates must be British citizens, and will have to go through some level of security clearance. Contact me if you fit the bill and are interested!

My PhD student Nathan Chong won the Technology Everywhere category at the 2014 UK ICT Pioneers award, sponsored by EPSRC, for his contributions to GPUVerify. Nathan was also selected as overall winner of the competition! See here for the full story.

My PhD student Nathan Chong, whom I co-supervise with Prof Paul Kelly, has reached the finals of the UK ICT Pioneers competition. See here for our Departmental news item on this. To get through to the final, Nathan made this popular science video about his work on GPUVerify.

Jeroen Ketema and I have had a paper on automatically proving termination of GPU kernels accepted at the Workshop on Termination, which will be co-located with CAV 2014 and the Vienna Summer of Logic. Draft available soon!

I am delighted to have been shortlisted for the Best Innovation category in the Imperial College Union Student Academic Choice Awards 2014.

Our paper, Engineering a Static Verification Tool for GPU Kernels, has been accepted at CAV’14.

Ethel Bardsley, John Wickerson and I have had a paper accepted at the International Workshop on OpenCL on KernelInterceptor, an extension to the GPUVerify tool for automatically intercepting kernel invocations at runtime to allow static verification of race-freedom to be applied to each dynamic instance. The paper, KernelInterceptor: automating GPU kernel verification by intercepting and generalising kernel parameters will be presented by Ethel.

We have submitted a paper to CAV’14 describing the engineering experience we’ve gained over the last 2.5 years working on GPUVerify. In the paper we report experiments for a set of more than 500 GPU kernels, with two different SMT solvers and various optimisation levels. A paper is so limiting in the data one can show, thus Nathan Chong knocked up what I think is a very cool web page that allows you to plot our data in various ways to answer questions that are not addressed in the paper itself. Check out the draft paper and plots.

Our paper, Concurrency Testing Using Schedule Bounding: an Empirical Study, received Best Student Paper Award at this year’s PPoPP conference. The empirical study was led and presented by my PhD student Paul Thomson, and co-authored with Adam Betts. In the work we attempted to validate claims made in prior work on systematic concurrency testing using a large, publicly available set of benchmarks. The benchmark set, SCTBench, and the results of our study, are publicly available.

I presented GPUVerify at the UKMAC 2013 conference in Oxford this week. In January, Nathan Chong and Jeroen Ketema are running a tutorial on verification and semantics for GPU kernels at POPL in San Diego, while John Wickerson and Dan Liew are running the Formal Analysis Techniques for GPU Kernels (FAT-GPU) tutorial at HiPEAC in Vienna.

Ethel Bardsley and I have had a paper on our efforts to extend GPUVerify with support for reasoning about warps and atomics accepted to the NFM’14 conference. The paper is entitled Warps and Atomics: Beyond Barrier Synchronization in the Verification of GPU Kernels. This is the culmination of Ethel’s MEng project at Imperial and follow-up UROP placement with my group.

Paul Thomson has made available the benchmarks he painstakingly gathered and adapted for systematic concurrency testing as part of our PPoPP empirical study. Check them out: SCTBench. We hope they will be useful to other researchers interested in concurrency analysis.

We were delighted to hear that we have received a HiPEAC technology transfer award in recognition of our ongoing tech transfer of GPUVerify to ARM, which is also supported by the CARP project.

I’m delighted to have been asked to be one of the invited speakers at the 14th International Workshop on Automated Verification of Critical Systems (AVoCS’14). For me this is very cool as one of my very first papers, 10 years ago, was at AVoCS’04.

My PhD student Paul Thomson, in collaboration with me and Adam Betts, has had a paper entitled “Concurrency Testing Using Schedule Bounding: an Empirical Study” accepted at PPoPP 2014. In this work we used the Maple concurrency testing tool as a framework on which to empirically study techniques for systematic concurrency testing where schedule bounding is used to reduce schedule explosion. We collected a large set of concurrent program benchmarks and used these to empirically study two well-known schedule bounding techniques: preemption bounding and delay bounding. The paper reports on our experimental method and findings.

Nathan Chong, Jeroen Ketema and I have had a paper entitled “A Sound and Complete Abstraction for Reasoning About Parallel Prefix Sums” accepted at POPL 2014. In this work we show how to verify functional correctness of GPU kernel implementations of prefix sums by establishing data race-freedom (in our case using GPUVerify, but in principle using any capable tool) and then running a single test case using a novel abstract domain.

I was delighted to be selected as one of this year’s recipients of an Early Career Award from Intel Corporation, which I received at the Intel European Research and Innovation Conference in Nice (which was nice).

Thanks to Dan Liew‘s efforts, you can now try out the GPUVerify tool through Microsoft Research’s rise4fun service.

These days we are doing some very hands-on work with the Mali GPU series, thanks to the gift of an Arndale developer board from ARM which Dan Liew has been having fun with:

I am honoured to have been invited to serve on the ERC for PLDI 2014.

I’m very pleased to welcome Pantazis Deligiannis, who has joined the Multicore Programming Group to take up a PhD studentship funded by a gift from Intel Corporation.

Ethel Bardsley has just completed her MEng degree at Imperial, and will join the Multicore Programming Group for a 10 week placement under the Undergraduate Research Opportunities Programme (UROP), to work on GPUVerify.

Nathan Chong, Jeroen Ketema, Paul Kelly, Shaz Qadeer and I have had a paper accepted at the OOPSLA conference, part of SPLASH 2013. The paper is about barrier invariants, a shared state abstraction which makes it possible to reason about data-dependent GPU kernels.
This year, OOPSLA featured an artifact evaluation process, separate for paper review, in which authors were invited to submit their tools to be tried out in detail by a committee of researchers.
I think this is a great idea, something that more conferences should consider doing. The artifact evaluation committee, chaired by Matthias Hauswirth and Steve Blackburn, clearly put a great deal of effort into trying out our software. I’m pleased to say that our implementation in GPUVerify gained their stamp of approval:

I was surprised and delighted to win the award for Best Teaching for Undergraduates at Imperial College’s 2013 Student Academic Choice awards. More about the awards.

I have just returned from a Dagstuhl seminar on techniques for improved accelerator programming which I co-organised with Albert Cohen, Marieke Huisman and Joost-Pieter Katoen. The seminar ran in parallel with a seminar on Formal Verification of Distributed Algorithms, and there were some good synergies between the seminars.

I recently recorded some videos about GPUVerify, an analysis technique and tool for OpenCL and CUDA kernels being developed as part of the CARP project. Watch the videos on YouTube:

• Video 1: Introduction and overview
• Video 2: Verification method
• Video 3: Predicated execution and invariant inference

The Multicore Programming Group are soon to embark on an exciting new research project in collaboration with Gernot Heiser at NICTA, Leonid Ryzhyk and Michael Stumm at University of Toronto, and Pavol Cerny at University of Colorado Boulder. The project is funded by a generous gift from Intel Corporation and will focus on verification and synthesis techniques to aid in the development of high-assurance device drivers. We have funding for two PhD students to work on this at Imperial, and are currently recruiting. Advert for these positions with more details.

Adam Betts and I have had a paper on worst case execution time analysis for GPU kernels accepted at the 25th Euromicro Conference on Real Time Systems. Draft available soon!

Dan Liew has jointed the Multicore Programming and Software Reliability groups to undertake a PhD, co-supervised by me and Cristian Cadar. His studentship is partly supported by ARM.

I have been teaching at an École de Recherche on Semantics and Tools for Low-Level Concurrent Programming, at ENS Lyon, presenting techniques for analysing GPU kernels that have been developed during the CARP project. Also speaking at the school were Francesco Zappa Nardelli (INRIA), Mark Batty (Univesity of Cambridge) and Martin Vechev (ETH Zurich).

During the HiPEAC conference, I am giving a half-day tutorial on Formal Analysis Techniques for GPU Kernels, on the verification techniques being developed during the CARP project. The CARP team at ENS Paris will also present a poster on our PENCIL intermediate language during the HiPEAC EU projects day.

We have had a paper on the relationship between interleaving and lock-step semantics for GPU kernels, and applications of this relationship to formal verification, accepted at the ESOP 2013 conference. This is joint work with Peter Collingbourne, Jeroen Ketema and Shaz Qadeer. Check it out.

A position paper, co-authored by many members of the CARP project, has been accepted for presentation at the WOLFHPC workshop. The paper outlines the preliminary design of PENCIL, a new intermediate language for accelerator programming that we are designing as part of CARP. Draft available soon!

A paper co-authored with collaborators at NICTA, Australia (principally Sidney Amani and Leonid Ryzhyk) has been accepted to the Systems Software Verification conference, which will take place in Sydney, Australia, during November. Draft available soon!

EPSRC have agreed to fund a one-year project continuing my research group’s work on formal verification techniques for GPU kernels. During this project we plan to collaborate with a number of partners, including Shaz Qadeer at Microsoft Research, Redmond, Ganesh Gopalakrishnan at the University of Utah, and Peter Sewell at the University of Cambridge. The project will also involve further collaboration with ARM and Rightware, who are partners on CARP.

ARM and EPSRC have generously agreed to fund a PhD studentship at Imperial to investigate techniques for improving the reliability of GPU software. The student will be co-supervised by me and Cristian Cadar, as the studentship spans the interests of the Multicore Programming and Software Reliability groups.

I’ll present a half day tutorial on Formal Analysis Techniques for GPU Kernels (codename FAT-GPU) at the HiPEAC 2013 conference, January 2013. This will describe recent developments in this area arising from the CARP project, as well as techniques from the group of Prof Ganesh Gopalakrishnan at the University of Utah.

Starting in October I will be teaching a new course for final year undergraduates at Imperial, entitled Software Reliability.

Cassie Epps and Egor Kyshtymov, both Imperial undergraduates, are joining the Multicore Programming group for the summer through the Undergraduate Research Opportunities (UROP) scheme.

Our paper on GPUVerify, a technique and tool for verifying race- and divergence-freedom of GPU kernels, has been accepted at the OOPSLA 2012 conference! This is joint work with Adam Betts, Nathan Chong and Paul Thomson at Imperial, and Shaz Qadeer at Microsoft Research. Check it out!

Peter Collinbourne recently submitted his PhD thesis at Imperial, and will be moving to industry in September; in the meantime he has joined the Multicore Programming group for a short postdoc stint. Peter has worked extensively with the KLEE system, including building KLEE-FP, a dynamic symbolic execution tool which supports analysis of OpenCL kernels.

Jeroen Ketema has joined the Multicore Programming Group as a postdoctoral researcher for our EU-funded project, CARP. Jeroen joins us from the University of Twente. Welcome, Jeroen!

I have been visiting the Operating Systems group at Intel, Portland Oregon, to speak at a workshop on Device Driver Synthesis and Reliability.

I recently gave a talk at the First Workshop on Validation Strategies for Software Evolution, organised by Hana Chockler who leads the PINCETTE EU project. The workshop had a great mix of talks from the verification and testing communities, concentrating on how to provide meaningful validation of software systems that are under constant revision (i.e., most systems).

I am about to go to Paris for the HiPEAC 2012 conference, to present a poster on the CARP project. Check out the poster, designed together with Adam Betts (with help from the CARP consortium).

I’m delighted that Adam Betts has joined the Multicore Programming Group to work on the CARP project.

December sees the kickoff of CARP, Correct and Efficient Accelerator Programming, a three year collaborative project funded by the European Commission’s Seventh Framework Programme. I am coordinating the project at Imperial, and the work is in collaboration with seven other European partners from academia and industry. See the project web page for more details!

I’m very pleased that Paul Thomson has started a PhD with me at Imperial. Paul recently completed his MSc in the Department of Computer Science at Oxford, with a project on race detection for concurrent programs using dynamic symbolic execution.

At the end of August I am joining the RiSE group at Microsoft Research in Redmond as a Visiting Researcher, to work for six weeks with Shaz Qadeer and Tom Ball on analysis of concurrent software.

For a while I’ve been working with Matko Botincan and Mike Dodds at the Cambridge Computer Laboratory, and Matthew Parkinson at Microsoft Research Cambridge, on using separation logic-based techniques to prove safety of multicore programs which use asynchronous memory operations. A full paper on this work has just been accepted to the 26th IEEE/ACM International Conference On Automated Software Engineering (ASE 2011). Check it out here.

Philipp Ruemmer, Leopold Haller, Daniel Kroening and I have had a paper accepted to the 18th International Static Analysis Symposium. The paper is on the use of k-induction for verification of imperative software. Among other things, we implemented k-induction in the Boogie verifier, and found it enabled us to verify programs with weaker invariants than standard Boogie requires. Check it out!

In November 2011 I will be joining the faculty at the Department of Computing at Imperial College London as a Lecturer. I am very excited!

Thomas Wahl, Alexander Kaiser, Daniel Kroening and I have had a paper accepted to the 23rd International Conference on Computer Aided Verification, on Symmetry-Aware Predicate Abstraction for Shared Variable Concurrent Programs. Check it out here.

The Royal Society will provide funding for Dragan Bosnacki of Eindhoven University of Technology to visit me at Oxford this summer, to work on the acceleration of formal verification algorithms using multicore systems. This is through the Society’s International Travel Grants scheme.

I have had two short papers accepted to the 2011 ACM SIGPLAN Conference on Principles and Practice of Parallel Programming. They are both on analysing multicore programs that use asynchronous memory operations. One gives preliminary details on an approach using separation logic, and is with Matko Botincan and Mike Dodds at the Cambridge Computer Laboratory, and Matthew Parkinson at Microsoft Research Cambridge. The other is a tool demonstration paper on SCRATCH, the DMA race analysis tool I have designed in collaboration with Daniel Kroening and Philipp Ruemmer at Oxford.

Leopold Haller, Daniel Kroening and I have had a paper accepted at the 2011 conference on Verification, Model Checking and Abstract Interpretation. The paper explores the use of static analysis to aid k-induction as a technique for analysing races in multicore programs that use DMA. Check it out.

George Russell from Codeplay just presented joint work with me, others at Codeplay, and Paul Keir at Glasgow, at the HPPC 2010 workshop, 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.

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.

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.