|
From: <lo...@sy...> - 2012-08-01 21:12:56
|
Thank you for the information. Basically what motivated my initial question is that we think we have a formal model to verify some of the v bit calculations, In particular the improved and and the add rules are sound. We are currently working on verifying the rest of the rules as well. Verifying rules involves first converting the rules to SMT and then using a SMT solver to prove its correctness against the model. Of course we do need some external experts to verify that our model and methods are actually correct. To that extent we are planning to submit the work as a peer reviewed publication. Thus, please excuse our vagueness at this time. However, if anyone is interested in more detailed discussions on this topic, would like to volunteer to help review the work, or have suggestions as to a good venue for publication please send me an email. Thank you all. Lok ----- Reply message ----- From: "Julian Seward" <js...@ac...> To: <val...@li...> Cc: "Lok Kwong Yan" <lo...@sy...> Subject: [Valgrind-developers] V-Bit Verification Date: Wed, Aug 1, 2012 3:08 pm > 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 |