  Canonical abstraction is a static analysis technique that represents states
as 3-valued logical structures, and produces finite abstract systems. Despite
providing a finite bound, these abstractions may still suffer from the state
explosion problem. Notably, for concurrent programs with arbitrary
interleaving, if threads in a state are abstracted based on their location,
then the number of locations will be a combinatorial factor in the size of the
statespace. We present an approach using canonical abstraction that avoids this
state explosion by "collapsing" all of the threads in a state into a single
abstract representative. Properties of threads that would be lost by the
abstraction, but are needed for verification, are retained by defining
conditional "soft invariant" instrumentation predicates. This technique is used
to adapt previous models for verifying linearizability of nonblocking
concurrent data structure algorithms, resulting in exponentially smaller
statespaces.
