今天是:
实验室公告
  • 1 我室名誉主任,我国著名计算机科学家,南京大学教授、博士生导师徐家福先生于2018年1月16日10时在南京不幸逝世,享年94岁。
  • 2 我室在2017年信息领域国家重点实验室评估中获评优秀类实验室!
学术动态
文件下载

学术报告(冯新宇)

报告题目: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的程序委员会成员。



[ 返回|BACK ]
版权所有 (C) 南京大学计算机软件新技术国家重点实验室
[电话] 025-89683467 [邮箱] keysoftlab@nju.edu.cn [地址]江苏省南京市栖霞区仙林大道163号计算机科学与技术楼