|
From: Julian S. <js...@ac...> - 2012-08-01 19:16:34
|
> I am interested in the accuracy of the V-Bit calculations So am I. > 1. Is there anyone who is working on Memcheck V-Bit Verification? It has been looked at informally from time to time, but there has never been a formal study of it, as far as I know. It would be really great to have more analysis of it. Even better would be to have a test suite, since a formal proof is a one-time thing that becomes invalid as soon as the Memcheck code changes. Florian Krohm worked on tester which is at https://bugs.kde.org/show_bug.cgi?id=300102 Not sure of its current status though. > 2. Is there a more updated list of operations in addition to the > ones described in the original USENIX ATC paper in 2005? That paper is quite out of date on the details, although the basic ideas are still valid. To see the set of primitive operations which give 95% of the complexity in Memcheck instrumentation, have a look in VEX/pub/libvex_ir.h, at the type IROp. ----- Can you say a bit more about what your goals are? ----- It would be nice to have a way to test Memcheck's V-bit propagation through each IROp individually -- that would provide a way to do the abovementioned regression test. This requires 2 parts: first, a way to set and get V bits on arbitrary pieces of memory. That is easy -- the VALGRIND_GET_VBITS and VALGRIND_SET_VBITS client requests. The second thing that is required is a way to write an instruction that passes its operands though an IROp that is specified in a test program, and no others -- so they can be tested individually. One way we could achieve this is to extend the "Special" instruction mechanism (eg, see guest_amd64_toIR.c and search for "Special") so that it will accept a pseudo-instruction with a specified IR op in the middle of it. J |