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.
3 months ago
PLDI 2021 song (May 2021)
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:
Paper on transformation-based compiler testing and spirv-fuzz accepted at PLDI (April 2021)
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.