10. – 13. Dezember 2017, Dagstuhl Seminar 17502
Testing and Verification of Compilers
Auskunft zu diesem Dagstuhl Seminar erteilen
Simone Schilke zu administrativen Fragen
Marc Herbstritt zu wissenschaftlichen Fragen
Compilers are important because they are widely used in software development. Buggy compilers may lead to unintended behaviours of developed programs, which may in turn cause software failures or even disasters in safety-critical domains. Furthermore, compiler defects make software very hard to debug, because developers can scarcely determine whether a failure is caused by the software they are developing or by the compiler they are using. Therefore, guaranteeing the quality of compilers is critical.
Compiler testing plays a critical role in compiler quality assurance. There are three inherent factors influencing compiler testing: test inputs of compilers, test oracles, and the efficiency of compiler testing. Research on compiler testing has been focusing on these three factors. Furthermore, compiler verification is also an effective way to guarantee the quality of compilers. In particular, there has been tremendous progress on building verified compilers from scratch (a notable example is the CompCert project).
The aim of this Dagstuhl seminar is to bring together researchers and practitioners from various sub-disciplines of computer science to brainstorm and discuss on the topic of testing and verification of compilers. In particular, we propose the following five research questions to structure the seminar and drive discussion:
RQ1: To what extent do compiler defects pose a security and reliability threat? It is clear that compiler bugs can harm software reliability and pose a threat to cyber-security in principle. There is a lack of empirical evidence and investigative techniques to assess the extent to which this is a problem in practice.
RQ2: How can we prioritise the compiler defects detected by automated testing to optimise for developer time? It is time-consuming for compiler developers to investigate and fix bug reports, thus research is required to both to provide concise reports (so that issues are easy to investigate), and to prioritise reporting serious issues (minimising time spent understanding issues that are ultimately deemed to have very low priority).
RQ3: How do the myriad techniques for compiler testing compare in their efficiency and efficacy? Random differential testing, equivalence modulo inputs testing, bounded-exhaustive program generation and symbolic testing have all been applied with success to reveal defects in compilers, and variations on program generation to fuel these techniques include creating purely synthetic programs as well as the creation of programs from existing code fragments. Comparing these techniques in terms of the rate of detected defects, the seriousness of detected defects, and their complementarity, is an important open problem that the seminar will address.
RQ4: Is analysis of program analysers feasible more generally? Compilers are one example of a programming language processing tool. In general, there is a need for program analysis tools (including refactoring engines, static property checkers, and dynamic sanitisers) to be tested. We will discuss opportunities for generalising methods for compiler testing to apply in this broader context.
RQ5: Can the gap between compiler testing and compiler verification be bridged? The compiler testing community focuses on automated testing of industrial-strength optimising compilers, e.g., GCC and LLVM. In parallel, there has been tremendous progress on building verified compilers from scratch, e.g., CompCert. Researchers in these two communities have tended to operate separately, since the techniques required are rather different. Nevertheless, given the overarching aim for compiler reliability that drives both sorts of effort, we will explore new research directions for driving unreliable compilers towards a correct, and potentially verifiable, state, through automated testing.
Creative Commons BY 3.0 DE
Junjie Chen and Alastair F. Donaldson and Andreas Zeller and Hongyu Zhang
- Programming Languages / Compiler
- Software Engineering
- Verification / Logic
- Compiler Testing
- Compiler Verification
- Program Analysis
- Program Optimization
- Code Generation