Yuting Wang’s team published the research result in “POPL 2022”

Recently, a group of researchers led by Dr. Yuting Wang in the John Hopcroft Center for Computer Science at Shanghai Jiao Tong University (SJTU) has made important progress towards verified compilation of realistic imperative programming languages. A related paper titled "Verified Compilation of C Programs with a Nominal Memory Model" has been accepted to the ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2022). This work is the result of a collaboration between Dr.Wang's research group and the group led by Dr. Zhong Shao at Yale University. Shanghai Jiao Tong University is the institution of the first author Yuting Wang.


POPL is the longest-running international conference in programming languages and one of the most prestigious. It is also ranked as an A-tier conference by CCF (China Computer Federation). It primarily focuses on the fundamental principles in programming languages and programming systems and covers research directions ranging from the design, definition and analysis of programming languages, to program verification, compilers, and many others. Among the papers accepted to POPL every year, there is usually only 1-3 from academic institutions located in China. There is a total of 65 papers accepted to POPL worldwide in 2022.

图片1.png

Compiler verification is an indispensable technique for construction of trustworthy software based on formal methods. Before source programs can be executed on hardware, they must first be compiled to executable forms. Only if the correctness of this compilation process is formally verified, i.e., the semantics of source programs are proved to be preserved at the target level, could we be absolutely sure that source programs will work correctly when they are actually executed.


As a key constituent of program semantics, memory models play a critical role in the verification of compilation of imperative programming languages (e.g., C/C++/Java). The group of researchers at SJTU and Yale observed significant inflexibilities in the memory models used in the existing work on verified compilation---especially with regard to their representation of memory space. These inflexibilities not only incur much complexity in compiler verification, but also prevent formal description of modular and concurrent semantics for realistic imperative programs.


Based on the above observations, the researchers developed a novel approach to generalizing the traditional block-based memory model by adopting the concepts in nominal techniques (i.e., atomic names and how they "support" named objects) to represent memory space. This results in a new memory model which they designate as the nominal memory model. Compared to the traditional memory model, the nominal memory model provides a uniform representation to different kinds of memory space through the abstract interfaces of atomic names and supports. Therefore, it provides a framework for describing program semantics with different memory structures, based on which verified compilation of complex programs can be achieved with significant less overhead.


Based on the above ideas, the researchers implemented the nominal memory model in CompCert---the state-of-the-art verified C compiler (https://compcert.org/)---and proved the correctness of the full compilation phases of CompCert. This results in Nominal CompCert---the first verified C compiler that supports a uniform abstraction of memory space. Furthermore, they have developed several extensions on top of Nominal CompCert for reducing the complexity in the verification of key compilation passes of C programs and for better supporting compiler verification for modular and open programs (as shown in the Figure). This work provides a solid foundation for developing flexible and extensible verification techniques for compositional compilation of concurrent programs. It also has the potential to greatly simplify the techniques for program verification in general which rely on traditional block-based memory models.


Biography:

图片2.png

Yuting Wang is currently a tenure-track associate professor in the School of Electronic Information and Electrical Engineering (SEIEE), Shanghai Jiao Tong University. He was a postdoctoral researcher in the Department of Computer Science at Yale University from 2016-2019, supervised by Dr. Zhong Shao. He obtained a Ph.D. degree in Computer Science at the University of Minnesota, Twin Cities, under the advisory of Dr. Gopalan Nadathur. His research interests include the theories underlying programming languages and formal verification, and their applications to critical system software such as compilers and operating system kernels. His recent work has been published in several premier international conferences on programming languages and verification, including POPL, CAV, OOPSLA and ESOP. He is also one of the main developer of the Abella system, an interactive theorem prover particularly suitable for formalization and verification of meta-properties of programming systems. Abella has been successfully applied to several academic projects on programming languages and logics, whose results are published in renowned conferences and journals in programming languages including ICFP and JFP.

Personal website: https://jhc.sjtu.edu.cn/~yutingwang/


[ 2021-12-06 ]