Compiler Social - 04.12.24

Date: 4 December 2024
Time: 16:00 - 20:00 (1h talk followed by 3h socializing)
Location: William Gates Building, 15 JJ Thomson Ave, Cambridge CB3 0FD
Rooms: LT1 (Talks), The Street (Social)
Hosts: Luisa Cicolini, Emma Urquhart, Tobias Grosser

⮕ Register Here

Join us for a relaxed chat about compilers, while socializing over 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.

For our Christmas Social we will have a series of quick talks presenting our group's research related to hardware.

Talk 1 - Formal Semantics for MLIR Dialects

MLIR is a recent compiler infrastructure project that aims to provide a unified way of defining SSA compiler IRs and transformations. It is designed to be modular and extensible, allowing for the definition of custom IRs. However, MLIR is primarily focused on syntax, and does not provide a way to define the semantics of operations in a formal way. This makes it difficult to reason about the correctness of transformations and analyses, and is a barrier to the development of formal verification tools for MLIR-based compilers. In this talk, we will introduce a set of semantics dialects, based on SMT-LIB, which allows to define the semantics of MLIR dialects as a compiler transformation. We will show how we can use these semantics dialects to give semantics of core MLIR dialects, such as arith, comb, and memref, and how we can use this new abstraction to define formal verification tooling such as a translation validation tool, a peephole rewrite verifier and synthetizer, and a dataflow analysis verifier.

Bio:

Mathieu Fehr is a final-year PhD student at the University of Edinburgh, currently visiting at the University of Cambridge. A large part of his research focuses on improving the accessibility of compiler technology, which includes the design and development of xDSL, a smoother entry-point for MLIR. His broader research interests encompass advancing declarative approaches in compiler design to facilitate formal reasoning and enable an ecosystem of compilation tools, including verifiers, fuzzers, and superoptimizers.

Talk 2 - Arcilator: fast and cycle-accurate hardware simulation in CIRCT

Arcilator is a cycle-accurate hardware simulator in CIRCT that eliminates the need to export the design to Verilog and use a third-party OSS or proprietary simulator. It supports all frontend languages that are fully lowered to CIRCT's core representation, currently including Chisel and a subset of SystemVerilog. We will discuss the design and implementation of Arcilator and the novel IR that connects CIRCT's core representation to LLVM IR. Moreover, we will show that it already delivers performance comparable to Verilator, and explore future developments of Arcilator.

Bio:

Martin Erhart is a Senior Engineer at SiFive working on compilers for hardware design and verification. He got his MSc in Computer Science at ETH Zurich, and has gained valuable experience in compiler research and development through internships with Google Research, SiFive, and Oracle Labs, in addition to his academic endeavors. Martin has been actively contributing to CIRCT since its inception.

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.