Skip to content Skip to navigation

Distinguished paper at ICSE 2016

Wednesday, April 13, 2016

Congratulations to Ph.D. student David Menendez and Prof. Santosh Nagarakatte for receiving an ACM SIGSOFT Distinguished Paper Award for their paper Termination-Checking for LLVM Peephole Optimizations at ICSE’16, the 38th International Conference on Software Engineering, to be held May 14-22, 2016, in Austin, Texas. ICSE is the premier venue for research in software engineering. This year, ICSE accepted 101 papers for publication out of 530 submissions, and 9 of the accepted papers were designated ACM SIGSOFT Distinguished papers.

http://2016.icse.cs.txstate.edu/program/awards

David and Santosh’s paper concerns mainstream compilers, which contain a large number of peephole optimizations that perform algebraic simplification of the input program with local rewriting of the code. These optimizations are a persistent source of bugs.

In prior research, David and Santosh, together with two other collaborators, developed Alive, a domain-specific language for expressing peephole optimizations in LLVM. Alive addresses a part of the problem by automatically verifying the correctness of these optimizations and generating C++ code for use with LLVM. Incidentally, Alive was published at PLDI’15, the premier venue for research in programming language design and implementation, where it received a distinguished paper award.

http://www.cs.rutgers.edu/news/articles/2015/04/10/pldi-2015-distinguished-paper/

David and Santosh’s ICSE’16 paper identifies a class of non-termination bugs that arise when a suite of peephole optimizations is executed until a fixed point. An optimization can undo the effect of another optimization in the suite, which results in non-terminating compilation. Their paper (1) proposes a methodology to detect non-termination bugs with a suite of peephole optimizations, (2) identifies the necessary condition to ensure termination while composing peephole optimizations, and (3) provides debugging support by generating concrete input programs that cause non-terminating compilation. They discovered 184 optimization sequences, involving 38 optimizations, that cause non-terminating compilation in LLVM with Alive-generated C++ code.

The paper will be available from David’s and Santosh’s homepages, here: 

http://paul.rutgers.edu/~davemm/

http://www.cs.rutgers.edu/~santosh.nagarakatte/