From f1a36463cdd5f37b2517bfe4960fb1d414fa7de1 Mon Sep 17 00:00:00 2001 From: Gan Shen Date: Sun, 31 Mar 2024 20:57:21 -0700 Subject: [PATCH] Update Luke's talk info --- content/lsd-seminar/2024sp.md | 26 +++++++++++++++++++++++++- 1 file changed, 25 insertions(+), 1 deletion(-) diff --git a/content/lsd-seminar/2024sp.md b/content/lsd-seminar/2024sp.md index ff6aee0..1f5adfc 100644 --- a/content/lsd-seminar/2024sp.md +++ b/content/lsd-seminar/2024sp.md @@ -19,7 +19,7 @@ Talks will be advertised on the [ucsc-lsd-seminar-announce](https://groups.googl | Date | Speaker | Title | |------- |--------- |--------- | -| April 5 | Luke Geeson | _TBD_ | +| April 5 | Luke Geeson | Compiler Testing with Relaxed Memory Models | | April 12 | Dan Plyukhin | _TBD_ | | April 19 | Kuru Ismail | _TBD_ | | April 26 | Jennifer Switzer | _TBD_ | @@ -32,4 +32,28 @@ Talks will be advertised on the [ucsc-lsd-seminar-announce](https://groups.googl --- +## April 5 + +**Speaker:** Luke Geeson + +**Title:** Compiler Testing with Relaxed Memory Models + +**Abstract:** Finding bugs is key to the correctness of compilers in wide use today. If the behaviour of a compiled program, as allowed by its architecture memory model, is not a behaviour of the source program under its source model, then there is a bug. This holds for all programs, but we focus on concurrency bugs that occur only with two or more threads of execution. We focus on testing techniques that detect such bugs in C/C++ compilers. + +We seek a testing technique that automatically covers concurrency bugs up to fixed bounds on program sizes and that scales to find bugs in compiled programs with many lines of code. Otherwise, a testing technique can miss bugs. Unfortunately, the state-of-the-art techniques are yet to satisfy all of these properties. + +We present the Téléchat compiler testing tool for concurrent programs. Téléchat compiles a concurrent C/C++ program and compares source and compiled program behaviours using source and architecture memory models. We make three claims: Téléchat improves the state-of-the-art at finding bugs in code generation for multi-threaded execution, it is the first public description of a compiler testing tool for concurrency that is deployed in industry, and it is the first tool that takes a significant step towards the desired properties. We provide experimental evidence suggesting Téléchat finds bugs missed by other state-of-the-art techniques, case studies indicating that Téléchat satisfies the properties, and reports of our experience deploying Téléchat in industry regression testing. + +Based on work to appear in the International Symposium on Code Generation and Optimization (CGO) 2024: +https://conf.researchr.org/info/cgo-2024/accepted-papers + +And recently presented work at The Future of Weak Memory Workshop (POPL) 2024: +https://lukegeeson.com/talks/2024-01-15-POPL24/ + +**Bio:** Luke is a Computer Science PhD student at UCL, supervised by James Brotherston, Earl Barr, and Lee Smith. He is developing techniques to find concurrency bugs in C/C++ compilers using formal models of relaxed memory concurrency. + +He is based in the compiler teams at Arm in Cambridge where he assists engineers with finding bugs and deploying automated concurrency testing as part of an EPSRC grant. Luke's opinions are his own and Arm does not endorse his work. + +--- + [Archive](../)