• Jonas Oberhauser's avatar
    tools: memory-model: Make plain accesses carry dependencies · 9ba7d3b3
    Jonas Oberhauser authored
    As reported by Viktor, plain accesses in LKMM are weaker than
    accesses to registers: the latter carry dependencies but the former
    do not. This is exemplified in the following snippet:
    
      int r = READ_ONCE(*x);
      WRITE_ONCE(*y, r);
    
    Here a data dependency links the READ_ONCE() to the WRITE_ONCE(),
    preserving their order, because the model treats r as a register.
    If r is turned into a memory location accessed by plain accesses,
    however, the link is broken and the order between READ_ONCE() and
    WRITE_ONCE() is no longer preserved.
    
    This is too conservative, since any optimizations on plain
    accesses that might break dependencies are also possible on
    registers; it also contradicts the intuitive notion of "dependency"
    as the data stored by the WRITE_ONCE() does depend on the data read
    by the READ_ONCE(), independently of whether r is a register or a
    memory location.
    
    This is resolved by redefining all dependencies to include
    dependencies carried by memo...
    9ba7d3b3
dep+plain.litmus 628 Bytes