After the success of the last compiler social, Tobias Grosser’s research group is hosting another compiler social in the University of Cambridge’s Computer Laboratory.
Date: 19 June 2024
Time: 15:00 (Talk), 16:00-20:00 (Social)
Location: William Gates Building, 15 JJ Thomson Ave, Cambridge CB3 0FD
Rooms: LT1 (Talk), Foyer (Social)
Hosts: Markus Böck, Anton Lydike, Tobias Grosser
If you’d like to attend please make sure to register Here (important to get the food order right)
https://grosser.science/compiler-social-2024-06-19/
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.
There will be a yet to be announced talk at 3 PM followed by socializing in the hallway with food and drinks from 4 to 8 PM.
Please see the website for information how to get to the Computer Laboratory.
The event is also in LLVM’s community calendar: Cambridge Compiler Social at the Computer Labratory
CC @rengolin @davidchisnall @AnastasiaStulova
5 Likes
Update: Starting off our compiler social will be a talk by Yann Herklotz (EPFL) titled:
Hyperblock Scheduling for Verified High-Level Synthesis
Abstract:
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
For anyone curious, the day before the social, June 18th, there is also an event celebrating Computer Architecture in the same venue as the social: https://www.cst.cam.ac.uk/news/celebrating-computer-architecture