Transcript Nils Klarlund

Software checking:
the performance gap
Nils Klarlund
Lucent Technologies
Bell Labs
Advances in symbolic reasoning
 Chess
 Hardware verification
 Software verification
Chess
 Did deep insights into chess make
Deep Blue win over Kasparov?
 No, in fact, the designers of Deep
Blue bristled publicly when asked
about how artificial intelligence
contributed to their work
 Raw computational power won; it’s a
brute force search problem
Hardware verification
 Is any abstraction theorem, symbolic
representation, theoretical advance key?
 Crunching SAT formulas that arise in
practice is fortuitously an activity that fit
within processor caches (as shown by
Chaff,…)
 This means: the insane expense, of several
hundred cycles, of following a pointer is
overcome
 We’ve been happily riding Moore’s Law for
what is a search problem
Software verification
 Here’s what we typically do:
 Make elaborate abstractions that cut
away enormous amounts of information
 configuration files, contents of databases,…
 Then, repeat
 Carry out symbolic computations that
involve hashing, pointers, more hashing,
more pointers,…
 Search for a solution, counter example,…
 We lost the enormous efficiency of
executing the program
Record & reverse
computations for search?
 A modern CPU executes 2Gips
 Couldn’t we just record them?
 If so, we could maintain a machine
instruction stack for reverse execution that
would allow the original program to become
an “efficient” search algorithm—at least for
depth-first strategies
 Why? Restarting a program is very
expensive; stack allows for backtracking
 Of course, search space is unimaginably big
Recording & backtracking
has been done for debuggers!
 Instrumented code executes only 5
times slower
 How much memory:
 Say, generate 8 bytes/instruction
 16Gb/s
 A modern supercomputer could
record several hundred seconds of
computation!
Main points
 A software quality approach that never
“goes abstract” from the user’s perspective
 Everything is concrete & feasible
 A natural extension of testing, one of two
ways in which bugs are found
 Integrates with state-of-the art debuggers
 Research: how to automatically guide the
search
 Static analysis: by constraints, computed from
static analysis; we need assertions, contracts,…
 Workflow:formal methods