|
|
Sudheendra Hangal's Home Page |
My permanent email address is hangal AT cs.stanford.edu
Publications page
I am a co-founder of Magic Lamp Software.
Formerly, I worked for Sun's Scalable Systems Group as a processor verification architect. This involved developing innovative strategies for verifying Sun's processors and systems. Verification is one of the biggest challenges in designing complex processors like the Niagara series.
Some of the new technologies I pioneered while at Sun are in the following areas:
1) Verification of multiprocessor systems: We devised a program called TSOtool to verify memory consistency in shared memory multiprocessors. TSOtool can reason about the results of a randomly generated multiprocessor program with data races and check that the system is following the axioms of the memory model. It has exposed bugs in every Sun processor designed in the last few years. (ISCA-04 Slides, Paper)
Some follow-on work describes efficient algorithms for verifying memory consistency. (SPAA-05 paper)
In our HPCA-06 paper, Chaiyasit Manovit and I presented a study of complete algorithms for verifying memory consistency. We showed the surprising result that, even though the problem is known to be NP-complete for popular memory models such as SC and TSO, a simple backtracking based heuristic works well, as long as it employs constraint inference during search. Our complete algorithm runs only marginally slower than an incomplete algorithm which may miss errors.
At PACT-06, we presented an extension of TSOtool to the important problem of verifying transactional memory (TM) systems. While there is much research on TM, there has been little work so far on how to practically build and verify these systems. We formulate an axiomatic framework to specify TM systems similar to the ones for memory consistency, and show how a straightforward extension of our verification algorithm can be applied to TM. We used this approach to successfully find some bugs in the Stanford "all transactions all the time" TM system called TCC. (PACT-06 paper)
Sit Manovit's PhD thesis is an excellent summary of all the above work.
2) Enabling formal verification: IODINE is a technique to automatically extract invariants from hardware design simulations. The idea was motivated by the challenge of using formal verification in practice on large microprocessor designs: no one person has the time or ability to write down all the program invariants, and manually written invariants are always subject to human blind spots and biases. IODINE proved that it can infer accurate and relevant invariants for hardware designs, including protocol diagrams and design structures such as FIFOs. (DAC-2005 paper, slides)
3) Fast and Accurate simulation: We developed a technique to checkpoint architectural state of a program on a C-level processor simulator and restart on a verilog model of the processor. This is very useful to measure performance of the design and find design bugs before tapeout. We used it successfully to predict performance of the picoJava and UltraJava (MAJC) processors, and moreover exposed design bugs before tapeout. (IEEE Micro Paper)
I also developed a cool debugging tool called DIDUCE at Stanford (jointly with my advisor, Monica Lam), which is based on inferring dynamic invariants from program runs. "Presumed invariants" from DIDUCE can be used in in a variety of ways. One way is to turn these invariants into assertions or warnings to tell programmers when the program does something anomalous, which could represent an error or a corner-case - useful information in either case. Our ICSE-2002 paper describes how we used it to find bugs in four large software systems we had no prior knowledge about.
(Papers have associated copyrights)
Released Software: (Coming soon)
Slides for some external talks:
Sun's Processor Roadmap, TSOtool, DIDUCE, IODINE, Verifying Memory Consistency, Dynamic Analysis (coming soon)
Pet Peeves and what's cool:
I'm also interested in Human-computer interaction these days. I love the
ambient orb and
similar "glanceable," calm user interface devices.
With the proliferation of WiFi, every point in people's homes
is on the network anyway; and using intelligent devices
allows creation of a variety of interesting applications, without
having to pay for proprietary Ambient "channels". (An idea that is demonstrated by the Chumby.)
The Stanford Reader is the result of a study of interaction techniques to ease the task of reading long documents on a mobile device.
Some useful notes on setting up and using an OLPC. However, the general state of software on this laptop is disappointing.
Suman Sangam, an ecological farm on the outskirts of Dharwad, India.
RISKS is sometimes funny, sometimes sad, and always a good storehouse for ideas on problem detection.
News Media: Deccan Herald e-paper (Greasemonkey script that re-lays out the pages and makes reading easier), Tehelka e-mag, NDTV Live
My Sun blog is out of date and probably going away soon.