Byron Cook: Terminator - Proving Good Things Will Eventually Happen

Posted By: Charles | Jul 12th, 2007 @ 8:31 AM

Here's another installment from MSR Cambridge (much more to come). This time, I was lucky enough to get some time with Byron Cook, 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. Terminator 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!

Tags: C++, Drivers, MS Research, MSR Cambridge 10Years, Programming

Rating:

Views (11,835)

Comments (6)

Downloads

keeron

Very interesting... (although, would've loved a "deep dive" type of thing where we could get some white boarding / demos).

Any research paper / samples (even better - existing technologies) on this subject?

rizzo

I had the same question and then found these links, which have pointers to papers:

http://research.microsoft.com/~bycook
http://research.microsoft.com/terminator

Tominator2005

I'm really sorry, but since the topic of this video is programming and C++ related. I just had to say this.

this^->AddressOfPapers = %here; // \/

http://research.microsoft.com/~bycook
http://research.microsoft.com/terminator

And yes I know, I really have got too much time on my hands.
But when your unemployed, thats life.

Im going to watch the video later.

Im interested in all programming languages, I've tried everything from Pascal to C++.

Many Thanks
Tom

Charles

These links are provided in the description text....

Charles

keeron wrote:

Very interesting... (although, would've loved a "deep dive" type of thing where we could get some white boarding / demos).

Any research paper / samples (even better - existing technologies) on this subject?

Byron will be in Redmond this summer and I'll do a Going Deep episode with him on Terminator. That ought to provide the "deep dive" you're looking for.
C

tolaat

This Byron is a cool guy.

Liveness is not dead - it just smells funny.