No próximo dia 27 de Março, pelas 11h00 na sala FC6 029 do DCC FCUP, Martin Berger irá dar uma palestra intitulada "Pydrofoil: compiling formal semantics of processors to fast software models".
A palestra é organizada pelo DCC-FCUP.
Short Bio
Martin Berger is an Associate Professor in the Department of Informatics at the University of Sussex. His research focuses on programming languages, verification, logic, and security. Webpage: https://users.sussex.ac.uk/~mfb21/
Title
Pydrofoil: compiling formal semantics of processors to fast software models
Abstract
A processor’s functionality is defined by its instruction set architecture (ISA), which specifies the machine language interpreted by the hardware. Accurate and comprehensive ISA specifications are essential for processor design, compiler development, and verification. Instruction set simulators (ISSs), also called functional models, provide software-based models of processor behaviour. The efficiency of ISS execution directly impacts processor development speed and associated costs. Traditionally, ISSs were manually implemented, a process that becomes increasingly time-consuming and error-prone as ISA complexity grows. To address this scalability challenge, architecture definition languages (ADLs) emerged, allowing for automated ISS generation from formal ISA descriptions. Many older and widely used ADLs, such as SystemC, extend beyond pure ISA specification to incorporate microarchitectural details, including pipelining information. This integration, while providing comprehensive modeling capabilities, typically uses low-level language constructs, such as C++ classes and macros, which introduce complexity into the specification and verification process. Recent years saw the rise of high-level DSL for ISA description, in particular Sail (https://github.com/rems-project/sail) which has become the official specification language for RISC-V (https://github.com/riscv/sail-riscv/tree/master/model). However, the Sail-generated ISS is very slow. In this talk, we show how to use a tracing-JIT compiler to compile from Sail to an ISS and achieve > 230x speedup. Paper draft: https://arxiv.org/abs/2503.04389