The KISS project is exploring novel techniques for analyzing concurrent software.   Traditional automated techniques for finding errors in concurrent programs, such as model checking, explore all possible thread interleavings.  Since the number of thread interleavings increases exponentially with the number of threads, such analyses have high computational complexity.  KISS provides a method to avoid this exponential complexity.  KISS transforms a concurrent program into a sequential program that simulates the execution of a large subset of the behaviors of the concurrent program.  The sequential program is then analyzed by a tool that only needs to understand the semantics of sequential execution.  We currently use the SLAM model checker as the sequential analysis tool.  However, the KISS technique is equally applicable to other sequential analysis tools such as ESP, Metacompilation, and Prefix/Prefast.  Here is a diagram of the KISS architecture:

A noteworthy aspect of KISS is that it will not report false errors.  However, it may miss errors because not all thread interleavings are explored.  We are currently using KISS to detect race conditions in Windows device drivers.  You can find more details about KISS in our upcoming PLDI paper.
 

• S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software. Microsoft Research Technical Report 2004-70, July, 2004. Abstract Postscript
• S. Qadeer and D. Wu. KISS: Keep it Simple and Sequential.  Accepted at the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), 2004. Postscript. Pdf.

Please send inquiries about the KISS project to Shaz Qadeer.