[LLVMdev] Reviving the new LLVM concurrency model

[Jianzhou Zhao]

On Mon, Aug 22, 2011 at 3:02 PM, Eli Friedman <eli.friedman at gmail.com> wrote:
> On Mon, Aug 22, 2011 at 11:17 AM, Jianzhou Zhao <jianzhou at seas.upenn.edu> wrote:
>> On Mon, Aug 22, 2011 at 1:02 PM, Eli Friedman <eli.friedman at gmail.com> wrote:
>>> On Mon, Aug 22, 2011 at 9:55 AM, Jianzhou Zhao <jianzhou at seas.upenn.edu> wrote:
>>>> In the definition of 'monotonic' ordering,
>>>> ... "If an address is written monotonically by one thread, and other
>>>> threads monotonically read that address repeatedly, the other threads
>>>> must eventually see the write"...
>>>
>>> It's supposed to mean that if you have a something like looks like a
>>> spinloop with monotonic reads, it shouldn't spin forever if the value
>>> changes.  I'll take another look at rewording that.
>>>
>>>> Does this mean if a thread does multi-writes monotonically, monotonic
>>>> reads from other threads should see all of them? But intuitively, it
>>>> seems to be fine for a read to ``miss'' some of the writes as long as
>>>> the writes seen are monotonic in the sense that later reads should see
>>>> the same write of earlier reads, or any write monotonically after the
>>>> writes seen.
>>>>
>>>> In the case there is only one monotonic write, what does 'eventually'
>>>> mean? Can we know a write must be seen when some condition holds, for
>>>> example, a number of instructions executed, the thread that did the
>>>> write executes a fence, ...?
>>>>
>>>> C++ memory model does not have ``unordered'', and "monotonic", but
>>>> have "modification ordering" (is it same to the relaxed atomic
>>>> variables the LLVM IR mentions?). If I am compiling C++ to LLVM, can
>>>> all modification atomic be compiled to monotonic? And when should we
>>>> use "unordered"?
>>>
>>> http://llvm.org/docs/Atomics.html is an attempt to make things much
>>> more straightforward than the stuff in LangRef.
>>
>> This is cool.
>>
>> At the end of the "optimization outside atomic" section there are
>> discussions about "returning undef". Is it the following correct?
>> * a store/store data race in LLVM leads to undefined behaviors,
>
> What exactly is a store-store "race"?  That sounds wrong.

If a program has two stores that are not ordered by happens-before
relations, does the program have undefined behaviors?

At the end of the "optimization outside atomic" section

...
However, LLVM is not allowed to transform the former to the latter: it
could introduce undefined behavior if another thread can access x at
the same time.
...

Is the ``undefined behavior'' introduced by the addition write "x =
xtemp"? For example, if a[i] is always false in the original program,
there is no the write.
But I don't think "int xtemp = x;" can introduce undefined behavior,
if LLVM does not take load/store race as undefined. Am I correct?

>
>> * a store/load data race does not result in undefined behavior, but
>> the load returns undef
>> * if two memory accesses are of data races, then at least one of them
>> is NonAtomic.
>
> The model isn't really defined in terms of races, but these two sound
> roughly correct.
>
>> My question is suppose a load L and a store S have a data race, and L
>> runs earlier than S in an execution, L is well-ordered with earlier
>> writes by happens-before, then at the point when L runs, but S has not
>> run yet, should the L also return undef or what ever write it can see
>> w/o races so far?
>>
>> Although non-synchronized writes from other threads may propagate to
>> another thread in different orders, but the writes that a read from a
>> different thread can see should have already executed before the read
>> (in a global time). So in the above case, it seems fine to allow the
>> load to return a 'defined' value. Is there any case that makes 'undef'
>> possible?
>
> If there is a load and a store to the same address with no
> happens-before relationship, the load returns undef.  "L runs earlier
> than S in an execution" doesn't make sense; if the load and store
> aren't atomic, the compiler is allowed to, for example, rematerialize
> the load, so that it happens both before and after the store.
>
>
> -Eli
>



-- 
Jianzhou