  We study the safety verification problem for parameterized systems under the
release-acquire (RA) semantics. It has been shown that the problem is
intractable for systems with unlimited access to atomic compare-and-swap (CAS)
instructions. We show that, from a verification perspective where approximate
results help, this is overly pessimistic. We study parameterized systems
consisting of an unbounded number of environment threads executing identical
but CAS-free programs and a fixed number of distinguished threads that are
unrestricted.
  Our first contribution is a new semantics that considerably simplifies RA but
is still equivalent for the above systems as far as safety verification is
concerned. We apply this (general) result to two subclasses of our model. We
show that safety verification is only \pspace-complete for the bounded model
checking problem where the distinguished threads are loop-free. Interestingly,
we can still afford the unbounded environment. We show that the complexity
jumps to \nexp-complete for thread-modular verification where an unrestricted
distinguished `ego' thread interacts with an environment of CAS-free threads
plus loop-free distinguished threads (as in the earlier setting). Besides the
usefulness for verification, the results are strong in that they delineate the
tractability border for an established semantics.
