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!
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 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.
I am honoured to be the recipient of the 2017 BCS Roger Needham Award.
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
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.
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.
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.
Time to celebrate!
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.
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.
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:
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.
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.
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!
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.
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.
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!
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.
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.
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!
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.
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 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).
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.
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.
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!
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!
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.
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.
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.
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.
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.
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.
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.
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).
I am honoured to have been invited to serve on the ERC for PLDI 2014.
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:
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.
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.
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.
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.
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.
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.
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!
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.
Starting in October I will be teaching a new course for final year undergraduates at Imperial, entitled Software Reliability.
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.
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.
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 have been visiting the Operating Systems group at Intel, Portland Oregon, to speak at a workshop on Device Driver Synthesis and Reliability.
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.
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!
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.