Separating data into lock-protected resources is an established paradigm of multi-threaded programming. Programs following that paradigm are verified by approaches that are typically rooted in a verification method of Owicki and Gries. For any such approach there are properties whose proof is only feasible if the user provides good auxiliary variables. What properties can be proven without the burden of inventing auxiliary variables? We partially describe the set of such properties by showing (a) the absence of exact characterization in terms of abstract interpretation, (b) a nontrivial superset, containing properties that can be proven by abstract interpretation with a form of Cartesian abstraction, and (c) a nontrivial subset, containing properties that can be proven by abstract interpretation with another form of Cartesian abstraction.