BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Compiler Testing with Relaxed Memory Models with L. Geeson - Luke 
 Geeson
DTSTART:20240220T170000Z
DTEND:20240220T180000Z
UID:TALK211675@talks.cam.ac.uk
CONTACT:Tobias Grosser
DESCRIPTION:Finding bugs is key to the correctness of compilers in wide us
 e today. If the behaviour of a compiled program\, as allowed by its archit
 ecture memory model\, is not a behaviour of the source program under its s
 ource model\, then there is a bug. This holds for all programs\, but we fo
 cus on concurrency bugs that occur only with two or more threads of execut
 ion. We focus on testing techniques that detect such bugs in C/C++ compile
 rs.\nWe seek a testing technique that automatically covers concurrency bug
 s up to fixed bounds on program sizes and that scales to find bugs in comp
 iled programs with many lines of code. Otherwise\, a testing technique can
  miss bugs. Unfortunately\, the state-of-the-art techniques are yet to sat
 isfy all of these properties.\nWe present the Téléchat compiler testing 
 tool for concurrent programs. Téléchat compiles a concurrent C/C++ progr
 am and compares source and compiled program behaviours using source and ar
 chitecture memory models. We make three claims: Téléchat improves the st
 ate-of-the-art at finding bugs in code generation for multi-threaded execu
 tion\, it is the first public description of a compiler testing tool for c
 oncurrency that is deployed in industry\, and it is the first tool that ta
 kes a significant step towards the desired properties. We provide experime
 ntal evidence suggesting Téléchat finds bugs missed by other state-of-th
 e-art techniques\, case studies indicating that Téléchat satisfies the p
 roperties\, and reports of our experience deploying Téléchat in industry
  regression testing.
LOCATION:SN08\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR