Formalizing Transistency

Memory transistency models (MTMs) define correct event ordering behaviors that are captured by memory consistency models (MCMs) while also accounting for virtual memory. As virtual memory is commonly implemented in modern processors, it is important to be able to formally define and reason about transistency models in order to verify the correctness and security of their implementations. I have developed a framework, TransForm, for this purpose. TransForm presents a novel vocabulary that can be used to formally specify MTMs, as well as an enhanced litmus test synthesis engine that can be used for formal verification of MTM implementations based on a formal MTM specification. This work has been accepted to ISCA 47.

Avatar
Naorin Hossain
Computer Science PhD Student

My research interests include the use of formal methods for computer security and exploit synthesis as well as correctness verification spanning both hardware and software.