Hi there! I am a second-year doctoral student supervised by Timothy Roscoe (Mothy) in the Systems Group at ETH Zurich.
My research focuses on applying formal methods to ensure the correct and efficient operation of flexibly-composed cache-coherent systems, which are enabled by CXL and other emerging coherent interconnect standards. I am working on the derivation of formal interoperability guarantees through the verification of abstract coherence endpoint specifications, the exhaustive conformance testing of in-silicon implementations against those specifications and the compositionality of the resulting conformance properties. I am also investigating how we can leverage this formal interoperability framework to increase implementation freedom and let manufacturers customise their coherence endpoints to match the specialisation of their devices.
I am very happy to be a part of the Enzian project, which serves both as inspiration and main experimental platform for my work. Enzian coherently attaches a Xilinx FPGA to Cavium's ThunderX1 CPU by leveraging the latter's native NUMA cache coherence protocol. During the development of our initial FPGA-side protocol implementation, we have experienced the interoperability challenges of coherent interconnects first-hand. Since the FPGA-side protocol remains fully reconfigurable, the Enzian platform is uniquely suited to the study of and experimentation with future cache coherent systems.
PDF
DOI
PDF
DOI
PDF
DOI