Skip to content

Commit

Permalink
Update Luke's talk info
Browse files Browse the repository at this point in the history
  • Loading branch information
gshen42 authored Apr 1, 2024
1 parent f436686 commit f1a3646
Showing 1 changed file with 25 additions and 1 deletion.
26 changes: 25 additions & 1 deletion content/lsd-seminar/2024sp.md
Original file line number Diff line number Diff line change
Expand Up @@ -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_ |
Expand All @@ -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](../)

0 comments on commit f1a3646

Please sign in to comment.