40年来首次| 南京大学冯新宇、梁红瑾团队荣获PLDI 2019杰出论文奖

本文转载自：TOP大学来了

TOP导语

"TOP大学来了"小编按，6月26日在美国凤凰城举行了第40届程序设计语言设计与实现会议（ACM SIGPLAN Conference on Programming Language Design and Implementation，PLDI 2019），在本届大会上来自于南京大学计算机科学与技术系程序设计语言研究组冯新宇教授、梁红瑾副教授及其团队的论文“Towards Certified Separate Compilation for Concurrent Programs”荣获本次会议的杰出论文奖（Distinguished Paper Award）。下一届会议将于2020年在英国伦敦举行。

"TOP大学来了"小编了解到，南京大学计算机科学与技术系程序设计语言研究组冯新宇教授、梁红瑾副教授及其团队此次所获得的奖项，为PLDI创办40年来中国大陆科研院所为第一单位的论文首次获得PLDI Distinguished Paper Award。据小编了解，此前中国科学院同英特尔合作的一篇2004年的PLDI会议论文，花费了两个团队共15人两年的工作量，这也是当时中国单位第一次参加PLDI会议的论文(非第一作者)。

T

O

P

科

研

PLDI 会议介绍

PLDI: 是ACM(中文名：计算机协会，Association for Computing Machinery )旗下的计算机专业会议涵盖了计算机科学的几个主要分支最高水平的会议之一。全称为：ACM Conference on Programming Language Design and Implementation，每年一次。主要关注编程语言的设计与实现等方面的研究工作，在国内外学术界具有很高的影响。

Towards Certified Separate Compilation for Concurrent Programs

“TOP大学来了”编辑

2019/06/26   Abstract

Certified separate compilation is important for establishing end-to-end guarantees for certified systems consisting of multiple program modules. There has been much work building certified compilers for sequential programs. In this paper, we propose a language-independent framework consisting of the key semantics components and lemmas that bridge the verification gap between the compilers for sequential programs and those for (race-free) concurrent programs, so that the existing verification work for the former can be reused. One of the key contributions of the framework is a novel footprint-preserving compositional simulation as the compilation correctness criterion. The framework also provides a new mechanism to support confined benign races which are usually found in efficient implementations of synchronization primitives.

With our framework, we develop CASCompCert, which extends CompCert for certified separate compilation of race-free concurrent Clight programs. It also allows linking of concurrent Clight modules with x86-TSO implementations of synchronization primitives containing benign races. All our work has been implemented in the Coq proof assistant.

人物简历

冯新宇，男，1978年生；现任南京大学计算机科学与技术系教授，博士生导师，程序设计语言研究组负责人。分别于1999年和2002年在南京大学获学士和硕士学位；2007年于耶鲁大学获博士学位。曾在中国科学技术大学计算机科学与技术学院任教授，2001年7月至2002年1月于香港理工大学担任研究助理。2007年9月至2010年5月于ToyotaTechnologicalInstituteatChicago(TTIC)任研究助理教授（ResearchAssistantProfessor）。主要从事程序验证、并发理论、程序设计语言理论方面的研究，在POPL、PLDI、ESOP、ICFP和CONCUR等知名国际会议和期刊上发表论文10余篇。担任APLAS'11,LOLA'11,TASE'09和APLAS'08的程序委员会成员。

人物简介

梁红瑾，女，现任南京大学计算机科学与技术系副教授，2014年博士毕业于中国科学技术大学，研究方向：程序设计语言。攻博期间，曾获得“中科院院长特别奖”、“中科院优博论文，2015年CCF优秀博士论文奖，2012年度微软学者、曾被美国麻省理工学院评选为2015年度电子与计算机领域“学术新星”（Rising Stars）等多项荣誉。

TOP大学来了（ID:topuniversity） 

审核、撰稿：大可