Log in

(no subject)

Some types of formal methods are heavily used, especially static-analysis techniques, but also runtime techniques such as lock-dependency checking. Although the more-general formal methods currently have severe program-size limitations, they are exceedingly powerful. Recent work is also promising to relax current program-size limitations somewhat, especially in the common case where the analysis targets a specific property or assertion rather than attempting to capture the program's full behavior. In particular, I highly recommend recent work by Alglave, Kroening, and Tautschnig (http://www.kroening.com/papers/cav2013-wpo.pdf), which synthesizes logic expressions instead of explicitly visiting every possible state. This results in impressive reductions in analysis time and the size of code that can be analyzed. To give you some idea, one piece of code that they analyze in this paper is the Linux kernel's RCU implementation, albeit for one of RCU's less-involved properties.

Finally, I often use programmatic combinations of these techniques. For example, consider the (thankfully rare) case of an RCU bug that takes ten hours of rcutorture testing to locate. The event logs would be truly huge, and would be chock full of irrelevant information. Worse yet, the high event rate over such a long period of time would likely result in ring-buffer overflows, greatly complicating analysis of the combined trace logs. So I have occasionally used a staged approach, where I record high-event-rate information from each test iteration into a per-thread structure, then trace the contents of this structure only if an error is detected. I also sometimes place printf() statements prior to assertions or breakpoints, or, alternatively, invoke functions from the debugger after the breakpoint/assertion in order to print relevant state. I sometimes also use formal methods in conjunction with testing, proving that which can most readily be proven and testing that which can most readily be tested.

Now onto the unlabeled question #3. First, at any given time, current debugging techniques will sometimes prove insufficient -- but for sequential programs as well as for parallel programs. Therefore, there will always be some opportunity to advance the state of the art. The big question is therefore "In which direction should we take our next step?" I have tended to favor small evolutionary steps in response to problems that I encounter, but larger steps are also important, with the Linux kernel's lock-dependency checker ("lockdep") being but one case in point.

Does the hardware approach described in your paper qualify as a valuable larger step? This is of course hard to say. However, back in the days before caches moved onto the CPU chip, I made heavy use of logic analyzers, mostly for fine-grained performance analysis. These days, I use tracing instead, which has the advantage of covering all CPUs rather than just the one that the logic analyzer is connected to, a limitation that your approach might overcome. I could imagine a per-CPU logic analyzer being quite useful, but it is not yet clear to me whether or not it would provide sufficient advantages over light-weight event tracing. Possible advantages include fine-grained timing, lower overhead, and greater access to CPU state. Possible disadvantages include too-small event buffers (thus the possibility of overflow), limited flexibility (including limited collection-time event analysis), and the time delay to get the hardware and corresponding tools in place.

Over to you! ;-)

Comment Form

No HTML allowed in subject


Notice! This user has turned on the option that logs your IP address when posting. 

(will be screened)