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:
