Here's another installment from
(much more to come). This time, I was lucky enough to get some time with
, a researcher in MSR's Programming Principles and Tools group focusing on static analysis of system code to hunt for algorithms and code fragments that will most
likely induce a system state lovingly referred to by all as a Hang. You know, when nothing seems to work anymore, you can't use your mouse or keyboard, windows are frozen in time and you resort to a hard reboot. Well, what is a hang, exactly? How is a hang
directly related to events? Did you know that a typical hang is event-related (never ending event response) caused by kernel mode code (drivers mostly) that never, well, terminates?
Byron and team have written a very interesting tool that analyzes code, tests it against proofs of correctness (mathematical proofs, indeed) and alerts developers at design time that some code they've written is heading down a very slippery slope that will
end in a hang.
is proof based. OK. How does Terminator work, you ask? Proofs? It's all about prooving termination.
Please tune in and find out. This is a really
cool introduction to the notion of
mathematically prooving that good things will eventually happen in code
PS. I just found out that, like myself, Byron is an Evergreen State College alumnus. Small world!