We present an effective dynamic analysis for finding a broad class of deadlocks, including the well-studied lock-only deadlocks as well as the less-studied, but no less widespread or insidious, deadlocks involving condition variables. Our analysis consists of two stages. In the first stage, our analysis observes a multi-threaded program execution and generates a simple multi-threaded program, called a trace program, that only records operations observed during the execution that are deemed relevant to finding deadlocks. Such operations include lock acquire and release, wait and notify, thread start and join, and change of values of user-identified synchronization predicates associated with condition variables. In the second stage, our analysis uses an off-the-shelf model checker to explore all possible thread interleavings of the trace program and check if any of them deadlocks. A key advantage of our technique is that it discards most of the program logic which usually causes state-s...