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.
TransForm is part of the Check Tool Suite.
Naorin Hossain
Computer Science PhD Candidate
My research interests include hardware security and correctness verification for modern systems.