http://www.dagstuhl.de/17502

December 10 – 13 , 2017, Dagstuhl Seminar 17502

Testing and Verification of Compilers

Organizers

Junjie Chen (Peking University, CN)
Alastair F. Donaldson (Imperial College London, GB)
Andreas Zeller (Universität des Saarlandes, DE)
Hongyu Zhang (Microsoft Research – Beijing, CN)

For support, please contact

Simone Schilke for administrative matters

Marc Herbstritt for scientific matters

Motivation

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.

License
  Creative Commons BY 3.0 DE
  Junjie Chen and Alastair F. Donaldson and Andreas Zeller and Hongyu Zhang

Classification

  • Programming Languages / Compiler
  • Software Engineering
  • Verification / Logic

Keywords

  • Compiler Testing
  • Compiler Verification
  • Program Analysis
  • Program Optimization
  • Code Generation

Book exhibition

Books from the participants of the current Seminar 

Book exhibition in the library, ground floor, during the seminar week.

Documentation

In the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.

 

Download overview leaflet (PDF).

Publications

Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.