Main Page

From Corensic

Jump to: navigation, search

Contents


Jinx Documentation

About Jinx

Jinx is a tool that accelerates bugs in multithreaded programs. Jinx works by controlling the order in which threads access shared memory. By choosing "unlikely" thread schedules, Jinx can accelerate bugs by orders of magnitude. In addition to bug acceleration, Jinx provides a feature called Jinx Reports, which provide insight into data races inside your program.

It is easy to incorporate Jinx into your workflow. Jinx requires no changes to your IDE or development processes. Jinx produces no false positives, staying out of the way until a bug is produced. Jinx makes errors easier to understand by replacing the randomness of multithreaded debugging sessions with something more like the sequential debugging experience of single threaded code.

How Jinx Aids Development

In a perfectly implemented multithreaded program, every access to shared memory is either performed using special atomic loads and stores, or protected within critical regions guarded by synchronization mechanisms that permit only one thread of control at a time to access shared state. This ensures that all threads only see shared data structures when they are in a consistent state.

Threading bugs are uncontrolled dependencies on the order in which threads access shared memory locations. Some interleavings result in normal operation. Other interleavings produce incorrect behavior. For example, a thread may use a shared data structure when it is incompletely updated or partly deleted by another thread, often leading to a crash.

Not all interleavings are equally likely. There may be only narrow windows of time in which a data structure is inconsistent. These unfortunate cases thus occur only rarely, especially in test setups where the program runs in a tightly controlled environment. Developers can be fooled into believing a program is correct until users in the field complain of mysterious crashes and bugs that are hard to reproduce in tests.

When a program has threading bugs, correct operation is therefore a matter of luck. Usually the program is lucky -- access to shared memory occurs in a fortunate order, and the program works as intended. Unpredictable events like hardware interrupts, execution of other programs, or user actions sometimes cause the program's threads to execute in an unfortunate order, causing the unlucky program to crash.

The more time that elapses between creation and identification and resolution of a defect, the higher the cost associated with that defect. By reducing the time until bugs are detected, Jinx saves you time, money, and reduces the risk of deploying defective software.

Jinx may be used in an ad-hoc fashion to find multithreaded bugs during development. Jinx may also be used in functional testing. Jinx works together with fuzz testing and stress testing to identify concurrency issues as part of a continuous integration process. Jinx can also be used to reproduce hard-to-find concurrency issues in deployed software.

Concurrency bugs are hard to understand. In a single-threaded application, a stack trace or debugger session is usually enough to identify what went wrong. In a concurrent application, non-local reasoning must be employed to imagine what else the program could have been happening to cause the error. Jinx facilitates the resolution of bugs through SmartStop, which intelligently stops your program in the debugger at a point where all the threads involved in a bug are still in relevant locations.


How Jinx Works

Jinx periodically samples the running program, saves (or checkpoints) the program's state, identifies memory locations shared among multiple threads, selects an interleaving of shared memory accesses, and resumes the program, forcing the selected interleaving. If the processor takes an exception, breakpoint, INT3, or calls into Jinx, Jinx stops all threads of the program immediately, a feature called SmartStop..

To identify shared memory locations, Jinx runs a brief slice of the program. Jinx examines the virtual memory tables to identify first pages, then locations, that are shared by multiple threads. Jinx identifies the instructions that access shared locations, and creates a table of possible interleavings. Jinx must select one of these interleavings to apply when the checkpointed program is resumed.

To select an interleaving, Jinx runs a number of experiments called simulations. Each simulation runs a brief slice of the progrma with a different candidate interleaving. Jinx uses a complex heuristic to select among candidate interleavings. However, simulations that produce an exception, breakpoint, INT3, or Jinx assert almost certainly indicate a bug, so Jinx is likely to select this interleaving. To improve performance, Jinx performs many experiments in parallel using all available cores of the processor.

Once Jinx selects an interleaving, Jinx resets the program to the checkpointed state, and allows the program to run, enforcing the selected interleaving. This process is called retiring a simulation into reality in some of the white papers on this web site. Even if the selected simulation does not lead directly to a crash, it may lead to data corruption or other relatively obvious signs of a bug.

Interleavings that are rare in normal execution are selected with about equal probability by Jinx's heuristic, making rare interleavings that expose bugs significantly more probable. The result is that if the program has any threading bugs, it becomes very unlucky.

Here is another description of how Jinx works

How Jinx is Implemented

Jinx uses the virtualization technology in modern Intel and AMD processors. Jinx is an example of a thin hypervisor; a lightweight hypervisor that virtualizes memory and processor access, but not I/O.

Jinx's hypervisor is installed after boot of the operating system, from an application running within the guest operating system. Jinx is typical of a thin hypervisor in that it does not virtualize access to I/O devices, relying instead on its guest operating system to do I/O. (See The Blue Pill for a description of another famous thin hypervisor.)

The following diagram depicts this architecture.

The Jinx Product Architecture
Application Jinx User Interface (Visual Studio Plugin, command line)
Operating System (Windows or Linux)
Disk driver Network driver Jinx driver
Jinx Thin Hypervisor
VT-x or AMD-V -- enabled CPU

Jinx, then, has a hypervisor-mode part, a device driver to handle privileged operations, and a user-mode component that is used primarily to control the hypervisor and alert it to processes that should be tested.

Versions of Jinx are available for both Windows and Linux. If you’re interested in using Jinx on other platforms, please Contact Us and let us know your preferences.

Concurrency Wiki

The Concurrency Wiki is a collection of resources to help you get started and get further information about concurrent and multithreaded programming. Feel free to add more information or suggest more information for others to add. We at Corensic will be adding more information to this section regularly, so check back often.

In this wiki, most uses of the word parallel have been replaced by concurrent. Knowing this may improve your search results.

All external links were current in December 2010.

Here is a full list of topics in the Concurrency Wiki

Views
Personal tools
Corensic
Jinx
Concurrency
Toolbox