My research focuses on formal verification of memory consistency model implementations, from high-level languages through ISA and microarchitecture down to actual hardware implementations. Most recently, I have worked on extending microarchitectural verification techniques that use happens-before graphs to allow for verification of actual processor RTL. I have also worked on extending microarchitectural verification techniques to the interface between coherence protocols and the rest of a microarchitecture, enabling the detection of bugs caused by the interaction of pipelines and coherence protocols. In addition, I have contributed to our group's work on full-stack memory model verification with a view to ISA memory model design.
I interned at AMD Research in Bellevue in 2015, where my work dealt with AMD's Remote-Scope-Promotion (RSP) technology. AMD recently proposed scoped synchronization operations for heterogeneous systems, which only guarantee ordering up to a certain scope. In general, the smaller the scope of synchronization, the lower the overhead. Remote-scope promotion allows scoped synchronization to dynamically occur at a larger scope only when necessary. This allows the larger scope to be used for cases such as work-stealing without the overhead of also using the larger scope in the common case. My work at AMD involved exploring the scalability of RSP and attempting to improve its efficiency.
Prior to my research at Princeton, I worked on the Computational Sprinting project under Prof. Tom Wenisch while at the University of Michigan. While there, I investigated the thermal limits and potential for sprinting on consumer-level mobile devices. During my year at Qualcomm Research, I wrote embedded and kernel-level software to enable the research of new LTE wireless technologies.