I am a research assistant in the Multicore Programming Group at Imperial College London. I am interested in automated bug finding (automated testing). I have recently been working on GLFuzz, a framework for automatically finding bugs in shader compilers. Our recent bug-finding effort found over 50 bugs in GPU drivers across all the main GPU vendors (AMD, ARM, Apple, Intel, Imagination, NVIDIA, Qualcomm). Some of these can be seen in our blog posts.

Tools

  • LazyLocks: A systematic concurrency testing tool that I created for finding concurrency bugs in Java programs. It uses dynamic bytecode instrumentation (via the ASM library) and supports various techniques, such as (lazy) dynamic partial-order reduction (DPOR), sleep sets, etc.
  • Maple: I have modified this concurrency testing tool that tests pthread programs. I added delay bounding and made various other changes when using it in our empirical study of schedule bounding techniques.
  • GPUVerify: I am a key contributor to this tool. GPUVerify verifies the absence of data races and barrier divergence in OpenCL and CUDA programs. See the video demo.

Publications

  • Paul Thomson and Alastair F. Donaldson, Concurrency Testing Using Controlled Schedulers: an Empirical Study, Invited submission to ACM Transactions on Parallel Computing (TOPC'15), 2015, Submitted
  • P. Deligiannis, A.F. Donaldson, J. Ketema, A. Lal, P. Thomson. Asynchronous Programming, Analysis and Testing with State Machines, 36th annual ACM SIGPLAN conference on Programming Language Design and Implementation (PLDI'15)
  • Paul Thomson and Alastair F. Donaldson, The Lazy Happens-Before Relation: Better Partial-Order Reduction for Systematic Concurrency Testing, 20th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP'15), 2015, To appear
  • (Best Student Paper Award, PPoPP 2014) Paul Thomson, Alastair F. Donaldson, Adam Betts, Concurrency Testing Using Schedule Bounding: an Empirical Study, 19th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP'14), 2014
  • Adam Betts, Nathan Chong, Alastair F. Donaldson, Shaz Qadeer, Paul Thomson, GPUVerify: a Verifier for GPU Kernels, Proceedings of the 27th Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'12), pp.113-132, 2012

Teaching

  • Software Reliability (440) -- a final year MEng course on software verification and testing. I created the second coursework in which students must implement a bounded model checker and static program verifier for Simple C programs. The tool must use the Houdini algorithm to automatically generate simple loop invariants. I also gave a guest lecture on Systematic Concurrency Testing.

Service

  • PPoPP 2015 Artifact Evaluation Committee.

Other tools that I have worked with

  • KLEE/Cloud9: I modified Cloud9, which is a symbolic execution tool for multithreaded programs. I added symbolic data race detection and basic partial-order reduction (happens-before graph caching).

contact

Email: paul.thomsonX@imperial.ac.uk [replace X with 11]