RE: [PATCH] tools: memory-model: Make plain accesses carry dependencies

[Jonas Oberhauser <jonas.oberhauser@huawei.com>]

Hi Alan,

-----Original Message-----
From: Alan Stern [mailto:stern@rowland.harvard.edu] 
Sent: Thursday, December 1, 2022 9:21 PM


> > In my opinion it is already an example of OOTA, which I would define as an
> >    rfi | ctrl | addr | data | fence
> > cycle.

> That's not an unreasonable point of view (if you put rfe *rather than* rfi), 

I wanted to very explicitly add rfi, because the lack of consideration of rfi is partially the issue in these examples.
But in being preoccupied with doing so I forgot rfe, thanks for catching that --- the correct version should be 
    rfi | rfe | ctrl | addr | data | fence
modulo anything else I've forgotten.
	
> but to me OOTA suggests something more: a value arising as if by magic rather than as a result of a computation.  In your version of the litmus test there is WRITE_ONCE(*y, 1), so it's a little understandable that you could end up with 1 as the final values of x and y.  But in my version, no values get computed anywhere, so the final value of x and y might just as easily be 1 or 56789 -- it literally arises "out of thin air".

Maybe one can distinguish further between OOTA values (which are arbitrary, not-computed values) and more generally OOTA behaviors.

How do you feel about examples like the one below:

void *y[2];
void *x[2] = { (void*)&y[1], (void*)&y[0] };

P0() {
    void **t = (void**)(x[0]);
    *t = (void*)(t-1);
}
P1() {
    void **u = (void**)(x[1]);	
    *u = (void*)(u+1);
}

In this test case the locations x[0] and x[1] exist in the program and are accessed, but their addresses are never (explicitly) taken or stored anywhere.
Nevertheless t=&x[1] and u=&x[0] could happen in an appropriately weak memory model (if the data races make you unhappy, you can add relaxed atomic/marked accesses); but not arbitrary values --- if t is not &x[1], it must be &y[1].

To me, OOTA suggests simply that the computation can not happen "organically" in a step-by-step way, but can only pop into existence as a whole, "out of thin air" (unless one allows for very aggressive speculation and rollback).

In this context I always picture the famous Baron Münchhausen, who pulled himself from mire by his own hair. (Which is an obviously false story because gentlemen at that time were wearing wigs, and a wig could not possibly carry his weight...)

best wishes,
jonas