报告题目:Certifying Concurrent Programs with Interrupts 报告人:冯新宇教授 中国科学技术大学 时间:1月14日(星期五)10:00 –11:00 地点:蒙民伟楼109会议室 摘要: Hardware interrupts are widely used in the world's critical software systems to support preemptive threads, device drivers, operating system kernels, and hypervisors. Handling interrupts properly is an essential component of low-level system programming. Unfortunately, interrupts are also extremely hard to reason about: they dramatically alter the program control flow and complicate the invariants in low-level concurrent code (e.g., implementation of synchronization primitives). In this talk, I will present an extension of separation logic for certifying low-level system programs involving both hardware interrupts and preemptive threads. We show that enabling and disabling interrupts can be formalized precisely using simple ownership-transfer semantics, and the same technique also extends to the concurrent setting. By carefully reasoning about the interaction among interrupt handlers, context switching, and synchronization libraries, we are able to certify a preemptive thread implementation and a large number of common synchronization primitives. The work provides a foundation for reasoning about interrupt-based kernel programs and makes an important advance toward building fully certified operating system kernels and hypervisors. 个人简介: 冯新宇,1978年生;中国科学技术大学教授,博士生导师。分别于1999年和2002年在南京大学获学士和硕士学位;2007年于耶鲁大学获博士学位。2007年9月至2010年5月于Toyota Technological Institute at Chicago (TTIC)任研究助理教授(Research Assistant Professor)。2010年5月加入中国科学技术大学计算机科学与技术学院任教授。主要从事程序验证、并发理论、程序设计语言理论方面的研究,在 POPL、PLDI、ESOP和CONCUR等知名国际会议和期刊上发表论文10余篇。担任APLAS 2011、APLAS 2008和TASE 2009的程序委员会成员。
|