Compiler Social Cambridge - 19 June 2024
Date: 19 June 2024
Time: 15:00 - 20:00 (1h talk followed by 4h socializing)
Location: William Gates Building, 15 JJ Thomson Ave, Cambridge CB3 0FD
Rooms: LT1 (Talk), The Street (Social)
Hosts: Markus Böck, Anton Lydike, Tobias Grosser
⮕ Register Here (important to get the food order right)
Join us for a relaxed chat about compilers, while socializing over snacks and refreshments. Our social is open to students, academics, professional developers and really anyone interested in compilation. We welcome beginners as well as experts. Our social is an unguided space offered for you to get to know people, try out some new ideas, get feedback on your code, or pair-program on a difficult program. Come with just a paper notebook or bring your laptop to hack on some in-progress patches.
This social is traditionally organized by the LLVM community, but is open to all (potential) compiler enthusiasts.
Talk - Hyperblock Scheduling for Verified High-Level Synthesis
High-level synthesis (HLS) is the automatic compilation of software programs into custom hardware designs. With programmable hardware devices (such as FPGAs) now widespread, HLS is increasingly relied upon, but existing HLS tools are too unreliable for safety- and security-critical applications. We partially addressed this concern by building Vericert, a prototype HLS tool that is proven correct in Coq (à la CompCert), but it cannot compete performance-wise with unverified tools.
In this talk I'll report on our efforts to close this performance gap, thus obtaining the first practical verified HLS tool. We achieve this by implementing a flexible operation scheduler based on hyperblocks (basic blocks of predicated instructions) that supports operation chaining (packing dependent operations into a single clock cycle). Correctness is proven via translation validation: each schedule is checked using a Coq-verified validator that uses a SAT solver to reason about predicates. Avoiding exponential blow-up in this validation process was a key challenge. Experiments on the PolyBench/C suite indicate that scheduling makes Vericert-generated hardware 2.1× faster, thus bringing Vericert into competition with a state-of-the-art open-source HLS tool when a similar set of optimisations is enabled.
About Yann Herklotz
Yann is a postdoc at EPFL in the verification and computer architecture (VCA) lab led by Thomas Bourgeat. He is working on dynamic high-level synthesis, as well as on the verification of hardware designs using interactive theorem provers, trying to make hardware proofs more compositional and scale better with the design size. Before that he was a PhD student supervised by John Wickerson at Imperial College, working on verified high-level synthesis and building Vericert with the aim of generating optimised hardware designs from verified software, thereby moving verification to a higher level.
Celebrating Computer Architecture - 18 June 2024
The day before the social, June 18th, the computer laboratory will be hosting an event for celebrating Computer Architecture: https://www.cst.cam.ac.uk/news/celebrating-computer-architecture
History
The LLVM Compiler Social Cambridge has a long history. Over the years it was by members of the LLVM community in local pubs, at Microsoft Research, Graphcore and in many other venues. Similar events are hosted in the Bay Area, Paris, Zurich, Berlin, and numerous other cities worldwide.
How to get there
Public transport
After arriving at Cambridge Railway Station, take either the U1 or U2 Universal buses towards "Girton Corner/Eddington" until "William Gates Building". Alternatively, take the X3 towards Huntingdon until "Cam Uni Vet School".
Cycling and Car
Cycling from the Railway Station to the William Gates Building takes about 20 minutes with cycling paths available for the majority of the path. Parking spaces and Bicycle racks are available in front of the building. The building is easily reachable from the M11.