Abstract
Concurrent components are required to be "thread safe" - which informally requires that the component behaves correctly (or at the bare minimum, does not crash) when called concurrently by multiple threads. In this talk, I will attempt to formalize this informal notion and claim that thread safety is a generalized form of linearizability, a correctness criteria introduced by Herlihy and Wing in 1990. I will then provide an automatic method for checking the linearizability of concurrent components and demonstrate results from checking the thread safety of the latest version of the .NET CLR concurrency library. The key challenge in linearizability checking is the specification of "correct" sequential behavior, which can be time-consuming and error-prone for large components. Our method does not require the user to provide such a specification.