Re: GSoC 2017

[Joseph Myers <joseph at codesourcery dot com>]

On Fri, 10 Mar 2017, Vasantha Ganesh wrote:

> I would like to make a change to the same project. Can we make use of
> `property based testing' instead of traditional unit tests? We can use
> this method to perform formal verification of the functions. This was

I don't think formal verification, in the sense of taking existing C 
implementations of libm functions not designed to be proved correct and 
proving them correct, is suitable for GSoC; it's a research-level problem.

> initially introduced to Haskell but it was adopted to other languages.
> Here is a paper about property based testing for Haskell
> (http://www.eecs.northwestern.edu/~robby/courses/395-495-2009-fall/quick.pdf).
> Although property based testing can be effective, there are no well
> maintained libraries for C. Here is a popular property based testing
> library for C (https://github.com/silentbicycle/theft). Here is a
> popular library for C++ (https://github.com/emil-e/rapidcheck).

In general we're very wary of introducing new dependencies to the glibc 
build.  Especially dependencies on the glibc host as opposed to on the 
build system, because of how those complicate bootstrapping.  Thus we 
don't require GMP/MPFR/MPC on the glibc host, and don't require them on 
the build system either for testing (expectations are checked in, and 
while GCC will be linked with build GMP/MPFR/MPC there is no expectation 
of the development headers / libraries being installed; very little gets 
built for the build system rather than the host at all in the course of 
glibc build and testing).

> So the project would include making the `property based testing'
> library feature complete and writing proper docs, then working on the
> testing of the math functions themselves. When it comes to writing the
> tests, we don't have to worry about the edges cases but we have to
> worry about the properties of the function.

The relevant properties of libm functions are that the outputs are within 
a certain number of ulps of an expected result determined with MPFR / MPC, 
with various constraints on exceptions and errno setting as documented in 
the manual and implemented in the gen-auto-libm-tests machinery.

The easiest way of testing those properties is to generate tests 
externally to glibc as textual data that can go in the gen-auto-libm-tests 
inputs, then to run gen-auto-libm-tests to determine the associated 
expectations and then run the glibc tests.  I've done random test 
generation like that to find glibc bugs.  Note however that any sort of 
uniform random inputs from floating-point representations may *not* be 
very good at finding the cases actually likely to trigger bugs.  As an 
alternative that has also found glibc bugs (and bugs in other libm 
implementations) and independently implements logic for what expected 
results are, see Paul Zimmermann's mpcheck work (harder to use in cross 
compilation cases since it requires MPFR on the glibc host, not just the 
build system).

I think there's scope for more projects that attempt to generate random 
inputs likely to cause problems for libm functions, but with the 
expectation that the generator program itself is not part of the glibc 
build and test process; rather, when it finds bugs, those are fixed and 
the tests added to the existing auto-libm-test-*.  Also, such projects 
could usefully look for test inputs that cover code branches not covered 
(or not well-covered) by present test inputs in the glibc testsuite, even 
where the existing function implementations are in fact accurate for those 
inputs.  The old GSoC proposal was about improving coverage through manual 
review, but I expect various existing fuzzing / code coverage tools could 
be adapted to search for inputs that improve code coverage in the 
testsuite.  Such searches would best be run on several different platforms 
using different floating-point formats and function implementations.

-- 
Joseph S. Myers
joseph@codesourcery.com