Profile picture

I am a fourth-year PhD student in the Princeton Computer Science department, advised by Prof. Margaret Martonosi. My area of research is computer architecture, and my specific interests include memory consistency models, cache coherence, dark silicon, and heterogeneous multicores.

Before joining Princeton, I completed my BASc in Computer Engineering at the University of Waterloo and a M.S. in Computer Science and Engineering at the University of Michigan. I also worked full-time at Qualcomm Research for one year.

Outside research, I enjoy playing chess, listening to classical music, and reading historical fiction.

My resumé can be found here.

Research

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.

Publications



Conference Publications

  • Yatin A. Manerkar, Daniel Lustig, Margaret Martonosi, and Michael Pellauer. RTLCheck: Verifying the Memory Consistency of RTL Designs. The 50th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO), October 2017.
    [PDF] [Slides] [Poster] [GitHub]

  • Caroline Trippel, Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. TriCheck: Memory Model Verification at the Trisection of Software, Hardware, and ISA. The 22nd International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), April 2017.
    [PDF]

  • Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. CCICheck: Using µhb Graphs to Verify the Coherence-Consistency Interface. The 48th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO), December 2015.
    Nominated for best paper.
    [PDF] [Slides] [Poster] [GitHub]

Non-Refereed Publications

  • Yatin A. Manerkar, Caroline Trippel, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. Counterexamples and Proof Loophole for the C/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings. CoRR abs/1611.01507, November 2016.
    [PDF]

Talks



  • C11 Compiler Mappings: Exploration, Verification, and Counterexamples.
    Dagstuhl Seminar 16471: Concurrency with Weak Memory Models. November 2016.
    [Slides]

Links