Madan Musuvathi

Yup, CHESS is not there yet. We are working on a modified version of CHESS that works like App Verifier - you can attach it to any EXE or a daemon

Hi Chris,
 CHESS is specifically designed for a the unit-testing scenario. Thus, you cannot apply it "out-of-the-box" on existing long-running programs. In return, CHESS can give you guaranteed coverage of interleavings.
 A lot of folks have given similar feedback saying that they would rather give up coverage guarantees if they dont have to refactor their existing tests. we are working on a tool called Cuzz that would serve that purpose. Cuzz would work very much like AppVerifier and you can attach it to any EXE or a windows service.

madan

Hi Flatliner
 CHESS adds preemptions during the program execution. CHESS attaches to your program and schedules one thread at a time (like what would happen if your program ran on a uni processor). CHESS then inserts context switches when it stops executing one thread to start executing another thread. There are two kinds of context switches. One that is "forced" on CHESS, when the current thread blocks (on a lock, say) or it dies. The second kind of context switch, called a preemption, is soemthing that CHESS forces on the program. The current thread can continue to execute, but CHESS preempts its execution to switch to another thread. We have found that such unexpected preemptions are the sources of bugs in concurrent programs.

madan

Hi Duke
 We used the formula just to provide intuition for how big the exploration space is with and without preemption bounding. Also, you can think of k as the maximum number of steps in any thread and you would get an upper-bound.
 CHESS uses a lot of algorithms/heuristics to figure out which instruction is a valuable place for preemptions. For instance, we can show it is not necessary to preempt at instructions that do not access shared memory. In fact, you can extend this argument to show that it is only necessary to preempt before synchronization points (lock ops, semaphore ops, CreateThread, ...) and at instructions that participate in a data race.

madan