I am a PhD student in the Multicore Programming Group at Imperial College London. I am interested in automatically finding bugs in concurrent software. I have recently been looking at improving dynamic partial-order reduction (DPOR) by ignoring dependencies between mutex operations.

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).

Concurrency analysis techniques are becoming more important than ever due to the pervasiveness of multicore platforms. One successful approach is systematic concurrency testing (SCT), also known as stateless model checking, which has been implemented in a variety of tools, including CHESS, Verisoft, INSPECT and Maple. Unfortunately, SCT is not scalable without additional techniques. I am interested in evaluating and improving both the sound and unsound techniques, such as schedule bounding, the PCT algorithm and dynamic partial-order reduction.

contact

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