Week of March 30Week of April 6Week of April 13Week of April 20

Computer Science and Engineering

Progressive Automated Formal Verification of Hardware and Software Systems

Tuesday, March 31, 2020; 10:00am
Via Zoom
Speaker: YATIN MANERKAR from Princeton University

ABSTRACT Modern computing systems are increasing in complexity, making it challenging to ensure their correctness. Automated formal verification can provide strong correctness guarantees based on mathematical proofs but presents a number of challenges. The models used in such verification may be far removed from real implementations, and they may have trouble scaling to the size of real-world systems. In addition, their correctness guarantees may not cover all possible programs. In this talk, I will discuss how my PhD research has addressed each of these challenges for the verification of Memory Consistency Model (MCM) properties in parallel systems. MCMs specify the ordering and visibility rules for memory operations in parallel programs, so MCM verification is critical to parallel system correctness. My MCM verification work spans the hardware/software stack, and the tools I have developed are designed to be employed at different points in the design timeline. Together, they provide "Progressive Automated Formal Verification", or automated formal verification throughout the system design process. My MCM work has discovered bugs in a "proven-correct" compiler mapping for C/C++11 atomics, the draft RISC-V ISA's memory model, a commercial compiler, a lazy coherence protocol, and an open-source processor. I will conclude with my plans for future work, which include developing new methodologies and tools for the principled design and verification of emerging heterogeneous parallel hardware, applying progressive verification to distributed and cyber-physical systems, and automating the generation of formal hardware specifications. BIOGRAPHY Yatin Manerkar is a final-year PhD candidate in the Princeton Computer Science Department, advised by Prof. Margaret Martonosi. He holds a BASc in Computer Engineering from the University of Waterloo and an M.S. in Computer Science and Engineering from the University of Michigan. He also worked full-time at Qualcomm Research for one year. Yatin's research develops automated formal methodologies and tools for the design and verification of computing systems. His work has been recognized with two best paper nominations, and three of his papers have been honored for their high potential impact as either Top Picks or Honorable Mentions in IEEE Micro's annual "Top Picks" issue. Yatin is a recipient of the Wallace Memorial Fellowship, one of Princeton's highest graduate honors awarded to approximately 25 PhD students annually for a senior year of their doctoral studies. He also received the 2019 Award for Excellence from Princeton's School of Engineering and Applied Science.


Hosted by: Jack Sampson,  Computer Science and Engineering  (jms1257@psu.edu)

Redesigning Storage Systems for Modern Storage Hardware

Thursday, April 2, 2020; 10:00am
Via Zoom
Speaker: ABUTALIB AGHAYEV from Carnegie Mellon

ABSTRACT The interface with which we access storage devices---the "block" interface---was first introduced with hard disk drives three decades ago. Since then, it has been the dominant standard for persistent storage devices. Almost all storage software, such as file systems and databases, that manage raw storage devices are built using this interface. The block interface has served us well until recently, but it is quickly approaching the end of its useful life. With recent technological changes in the manufacturing of hard disk drives and solid-state drives, preserving the same block interface comes at the expense of lost performance, increased device cost, and limited device lifetime. In this talk, I will describe technological changes leading to these problems, demonstrate the overhead of keeping the block interface on modern hardware, and show how these problems can be avoided using a newly proposed "zone" interface. BIOGRAPHY Abutalib Aghayev is a Ph.D. candidate in the Computer Science Department at Carnegie Mellon University, advised by George Amvrosiadis and Greg Ganger. He has a broad research interests in computer systems, including storage and file systems, distributed systems, and operating systems. He is the recipient of Hima and Jive Fellowship and a Best Paper award at USENIX FAST conference.


Hosted by: Timothy Zhu,  Computer Science and Engineering  (timothyz@cse.psu.edu)

If you would like to receive a weekly email about upcoming seminars, please log in here to sign up.