Formal methods can provide strong correctness guarantees for today's computing systems, but their usage is often restricted to formal methods experts. Formal verification is then bottlenecked on these experts, limiting its effectiveness. This problem is acute in computer architecture, since many architects do not have formal methods expertise.
In this talk, I will present recent work with my students and collaborators that reduces the barriers to entry for computer architects to use formal methods. First, I will discuss our work on automatically generating formal microarchitectural models of hardware. These models are necessary for microarchitectural verification, and generally need to be written by hand by formal methods experts. In contrast, our work can automatically generate such models from accessible inputs like test programs and execution traces or from hardware RTL implementations. These models can then be used for formal verification of memory consistency and hardware security using known automated verification techniques. I will also speak briefly on our technique for automated verification of cyber-physical systems written in the Lingua Franca coordination language.
Meanwhile, we also need to develop formal models and verification techniques for emerging architectures that significantly change the hardware-software interface. As an example, I will discuss our ongoing work on developing a verified programming model for a recent non-traditional memory hierarchy. I will conclude with our work on automatically converting axiomatic formal models to their operational equivalents, enabling each type of model to be used for the tasks it handles best.
Yatin Manerkar is an Assistant Professor in the Computer Science and Engineering division at the University of Michigan. He was previously a postdoctoral scholar with Prof. Sanjit Seshia at UC Berkeley and did his PhD at Princeton University under Prof. Margaret Martonosi. Yatin's research lies on the boundary between computer architecture and formal methods, covering areas such as concurrency, hardware security, and formal synthesis. His work has led to the discovery of bugs in a lazy coherence protocol, a "proven-correct" compiler mapping for C/C++11 atomics, a commercial compiler, and an open-source processor. Yatin's research has been recognised with multiple best paper nominations, and three of his papers have been recognised as IEEE Micro Top Picks or Honorable Mentions for their high potential impact. His PhD dissertation also received an Honorable Mention for the 2021 ACM SIGARCH/IEEE CS TCCA Outstanding Dissertation Award.