Testing Components for Thread Safety

A safety checking system for testing a component for thread safety, comprising:

• a test generating module configured to provide a test that identifies operations performed by two or more threads;
• a coarse-grained observation-generation module configured to generate and record a set of coarse-grained observations for the test, each coarse-grained observation being generated based on an assumption that the component exhibits linearizability as the component interacts with said two or more threads;
• a data store for storing the set of coarse-grained observations;
• a fine-grained observation-generation module configured to generate and record a set of fine-grained observations for the test, each fine-grained observation being generated without constraint as to whether the component exhibits linearizability;
• a search module configured to determine whether each of the fine-grained observations has a counterpart entry in the set of coarse-grained observations, and identify each fine-grained observation that does not have a counterpart entry as a potential linearizability error in the component;
• and
• a stateless model checker module for use by the coarse-grained observation-generation module and the fine-grained observation-generation module, configured to enumerate entries in the set of coarse-grained observations and entries in the set of fine-grained observations.

A computer readable medium for storing computer readable instructions, the computer readable instructions providing a safety checking system when executed by one or more processing devices, the computer readable instructions comprising:

• coarse-grained observation generating logic configured to generate and record a set of coarse-grained observations for a test performed on a component, each coarse-grained observation being generated based on an assumption that that operations take place atomically within the component as the component interacts with two or more threads;
• fine-grained observation-generation logic configured to generate and record a set of fine-grained observations for the test, each fine-grained observation being generated without constraint as to whether operations take place atomically within the component;
• and
• logic configured to determine whether each of the fine-grained observations has a counterpart entry in the set of coarse-grained observations, and to identify each fine-grained observation that does not have a counterpart entry as a potential linearizability error in the component.