BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Automated Full-Stack Memory Model Verification with the Check suit
 e - Yatin Manerkar\, Princeton University
DTSTART:20180719T130000Z
DTEND:20180719T140000Z
UID:TALK106882@talks.cam.ac.uk
CONTACT:Victor Gomes
DESCRIPTION:Memory models constrain the values that can be read by loads i
 n shared-memory parallel systems. They are defined for high-level language
 s (like C11 and Java) and instruction set architectures (ISAs) like x86-TS
 O\, ARM\, RISC-V\, and Power. If any layer of the hardware-software stack 
 does not maintain the guarantees required by the memory model at that laye
 r's interface\, then parallel programs may not run correctly on the system
 . This necessitates full-stack memory model verification from high-level l
 anguages all the way down to processor RTL (register transfer language).\n
 \nIn this talk\, I will describe techniques for full-stack memory model ve
 rification using tools from the Check suite developed by myself and others
 . In particular\, I will focus on the CCICheck\, TriCheck\, and RTLCheck t
 ools.\n\nAt the core of the Check suite is its ability to model hardware i
 mplementations as a set of microarchitectural ordering axioms (invariants)
  in the domain-specific µspec language. This allows for efficient microar
 chitectural verification using happens-before graphs. The axioms can descr
 ibe a variety of microarchitectural orderings\, including those related to
  coherence protocols. While coherence and consistency are usually verified
  independently\, their implementations are often closely coupled\, which i
 ncreases the possibility of bugs. To help mitigate these issues\, CCICheck
  allows designers to verify that their coherence protocol and pipeline wor
 k correctly together to implement the consistency model of the processor.\
 n\nThe TriCheck tool allows designers of an ISA to reason about the abilit
 y of their intended hardware implementations to efficiently support high-l
 evel language requirements. TriCheck was utilised to detect deficiencies i
 n the initial draft RISC-V ISA memory model that prevented it from support
 ing the C11 high-level language. TriCheck also discovered two counterexamp
 les to compiler mappings from C11 to ARMv7 and Power that were previously 
 thought to be proven correct.\n\nThe microarchitectural models of the Chec
 k suite are only valid if their axioms are actually maintained by the unde
 rlying implementation\, which is written in RTL like Verilog. RTLCheck\, t
 he newest addition to the Check suite\, enables automated translation of t
 he microarchitectural axioms to SystemVerilog Assertions (SVA) for a given
  litmus test. The generated assertions can then be automatically checked b
 y a commercial RTL verifier like JasperGold to ensure that the RTL maintai
 ns the microarchitectural axioms for that litmus test. The translation fro
 m µspec to SVA is complicated by semantic mismatches between the axiomati
 c nature of µspec and the temporal worldview of SVA\, and RTLCheck uses n
 ovel techniques to bridge this gap.\n\nThe combination of CCICheck\, TriCh
 eck\, and RTLCheck with the rest of the Check suite provide system designe
 rs and implementers with the ability to conduct automated full-stack memor
 y model verification of their systems for suites of litmus tests\, greatly
  reducing the possibility of memory model bugs in their systems.\n\n*Bio:*
 \n\nYatin Manerkar is a fourth-year PhD candidate in the Department of Com
 puter Science at Princeton University\, advised by Prof. Margaret Martonos
 i. Yatin’s research interests lie in the use of formal methods to verify
  parallel systems\, specifically focusing on verification of memory model 
 implementations at multiple levels of the hardware-software stack. He hold
 s a BASc in Computer Engineering from the University of Waterloo and an M.
 S. from the University of Michigan\, and has also worked full-time at Qual
 comm Research. Yatin’s work has led to the discovery of bugs in a lazy c
 oherence protocol\, a "proven-correct" C11 atomic compiler mapping\, a com
 mercial compiler\, and an open-source processor. He has also contributed t
 o the development of the RISC-V ISA's memory model by finding deficiencies
  in its draft specification\, and is currently a member of the RISC-V Memo
 ry Model Task Group. Yatin is a recipient of Princeton’s Wallace Memoria
 l Fellowship.
LOCATION:FW26
END:VEVENT
END:VCALENDAR