Page 152 - DCAP308_OBJECT_ORIENTED_ANALYSIS_AND_DESIGN

Object Oriented Analysis and Design

Notes CHESS can detect deadlocks and races but relies on programmer assertions for other state
verification. It also expects all programs to terminate and that there is a fairness guarantee
(forward progress) for all threads. Thus, if the program enters a state of continuous loop,
it reports a livelock.
2. The Intel Thread Checker: This is a dynamic analysis tool for finding deadlocks (including
potential deadlocks), stalls, data races, and incorrect uses of the native Windows
synchronization APIs. The Thread Checker needs to instrument either the source code or
the compiled binary to make every memory reference and every standard Win32
synchronization primitive observable. At run time, the instrumented binary provides
sufficient information for the analyzer to construct a partial-order of execution. The tool
then performs a “happens-before” analysis on the partial order. Please refer to the “Race
Detection Algorithms” sidebar for more information on happens-before analysis.
For performance and scalability reasons, instead of remembering all accesses to a shared
variable, the tool only remembers recent accesses. This helps to improve the tool’s efficiency
while analyzing long-running applications. However, the side effect is that it will miss
some bugs. It’s a trade-off, and perhaps it’s more important to find many bugs in
long-running applications than to find all bugs in a very short-lived application.
The only other big drawback of the tool is that it can’t account for synchronization via
interlocked operations, such as those used in custom spin locks.

Did u know? For applications that use only standard synchronization primitives, this is
probably one of the best-supported test tools available for concurrency testing native
applications.
3. Chord: This is a flow-insensitive, context-sensitive static analysis tool for Java. Being
flow-insensitive allows it be far more scalable than other static tools, but at the cost of
losing precision. It also takes into account the specific synchronization primitives available
in Java. The algorithm used is very involved and would require the introduction of many
concepts.
4. KISS: Developed by Microsoft Research, this model checker tool is for concurrent C
programs. Since state space explodes quickly in a concurrent system, KISS transforms a
concurrent C program into a sequential program that simulates the execution of
interleaving. A sequential model checker is then used to perform the analysis.
The application is instrumented with statements that convert the concurrent program to a
sequential program, with KISS assuming the responsibility of controlling the
non-determinism. The non-determinism context switching is bounded by similar principles
described in CHESS above. The programmer is supposed to introduce asserts which
validate concurrency assumptions. The tool does not report false positives. The tool is a
research prototype and has been used by the Windows driver team, which primarily uses
C code.
5. Zing: This tool is a pure model checker meant for design verification of concurrent programs.
Zing has its own custom language that is used to describe complex states and transition,
and it is fully capable of modeling concurrent state machines. Like other model checkers,
Zing provides a comprehensive way to verify designs; it also helps build confidence in the
quality of the design since you can verify assumptions and formally prove the presence or
absence of certain conditions. It also contends with concurrent state space explosion by
innovative reduction techniques.

146 LOVELY PROFESSIONAL UNIVERSITY