On 12/04/2018 11:23, Andrea Parri wrote:
>> - smp_store_mb() is missing
> Good point. In fact, we could add this to the model as well:
> following Peter's remark/the generic implementation,

Good idea.  smp_store_mb() can save some clock cycles in the relatively
common idiom

        write a                         write b
        read b                          read a
        if (b)                          if (a)
          wake 'em                        we've been woken

> Yeah, those 'Ordering is cumulative', 'Ordering propagates' could
> mean different things to different readers... IMO, we may even omit
> such information; this doc. does not certainly aim for completeness,
> after all. OTOH, we ought to refrain from making this doc. an excuse
> to transform (what it is really) high-school maths into some black
> magic.
FWIW, what I miss in explanation.txt (and to some extent in the paper)
is a clear pointer to litmus tests that rely on cumulativity and
propagation.  In the meanwhile I'll send some patches.  Thanks for the
feedback, as it also helps validating my understanding of the model.



Reply via email to