  We address the problem of verifying safety properties of concurrent programs
running over the Total Store Order (TSO) memory model. Known decision
procedures for this model are based on complex encodings of store buffers as
lossy channels. These procedures assume that the number of processes is fixed.
However, it is important in general to prove the correctness of a
system/algorithm in a parametric way with an arbitrarily large number of
processes.
  In this paper, we introduce an alternative (yet equivalent) semantics to the
classical one for the TSO semantics that is more amenable to efficient
algorithmic verification and for the extension to parametric verification. For
that, we adopt a dual view where load buffers are used instead of store
buffers. The flow of information is now from the memory to load buffers. We
show that this new semantics allows (1) to simplify drastically the safety
analysis under TSO, (2) to obtain a spectacular gain in efficiency and
scalability compared to existing procedures, and (3) to extend easily the
decision procedure to the parametric case, which allows obtaining a new
decidability result, and more importantly, a verification algorithm that is
more general and more efficient in practice than the one for bounded instances.
