[LLVMdev] LLVM Concurrency and Undef

[Jeffrey Yasskin]

On Mon, Aug 22, 2011 at 5:46 PM, Eli Friedman <eli.friedman at gmail.com> wrote:
> On Mon, Aug 22, 2011 at 5:29 PM, Jianzhou Zhao <jianzhou at seas.upenn.edu> wrote:
>> On Mon, Aug 22, 2011 at 7:27 PM, Jeffrey Yasskin <jyasskin at google.com> wrote:
>>> On Mon, Aug 22, 2011 at 3:49 PM, Eli Friedman <eli.friedman at gmail.com> wrote:
>>>> On Mon, Aug 22, 2011 at 3:40 PM, Jianzhou Zhao <jianzhou at seas.upenn.edu> wrote:
>>>>> On Mon, Aug 22, 2011 at 6:08 PM, Eli Friedman <eli.friedman at gmail.com> wrote:
>>>>>> On Mon, Aug 22, 2011 at 2:49 PM, Santosh Nagarakatte
>>>>>> <santosh.nagarakatte at gmail.com> wrote:
>>>>>>> Hi all,
>>>>>>>
>>>>>>> I have been trying to understand the use of undef in both sequential
>>>>>>> and concurrent programs.
>>>>>>>
>>>>>>> >From the LLVM Language Reference Manual, I see the following
>>>>>>> definition of undef.
>>>>>>> "Undef can be used anywhere a constant is expected, and indicates that
>>>>>>> the user of the value may receive an unspecified bit-pattern".
>>>>>>>  LLVM Language Reference manual also demonstrates how optimizers can
>>>>>>> use these undef values to  optimize the program.
>>>>>>>
>>>>>>> However, on the other hand, with the LLVM Atomics and Concurrency
>>>>>>> Guide states that
>>>>>>> If code accesses a memory location from multiple threads at the same
>>>>>>> time, the resulting loads return 'undef'.
>>>>>>> This is different from the C++ memory model, which provides undefined
>>>>>>> behavior. What is the rationale for returning an undef on racing
>>>>>>> reads?
>>>>>>>
>>>>>>> LLVM Atomics and Concurrency guide also states the following
>>>>>>> "Note that speculative loads are allowed; a load which is part of a
>>>>>>> race returns undef, but does not have undefined behavior"
>>>>>>>
>>>>>>> If the speculative loads returns an undef and the returned value is
>>>>>>> used, then it results in an undefined behavior. Am I correct?
>>>>>>
>>>>>> It behaves like any other undef value... which do often lead to
>>>>>> undefined behavior.
>>>>>>
>>>>>>> If so, what is the purpose of returning an undef with a speculative load?
>>>>>>> Is it to ensure that the subsequent uses of the value of the
>>>>>>> speculatively introduced load is caught/detected by the optimization?
>>>>>>
>>>>>> The point is primarily to allow optimizations like LICM to introduce
>>>>>> loads whose value is never used.  It also keeps consistent semantics
>>>>>> through CodeGen, where some targets widen loads.
>>>>>>
>>>>>>> Is it possible to separate the "undef" in a sequential setting and
>>>>>>> "undef" with speculative loads in a concurrent setting with separate
>>>>>>> undefs?
>>>>>>
>>>>>> The intention is that they should have the same semantics.
>>>>>
>>>>> Suppose there are three threads T1, T2 and T3,
>>>>> T1 (S1 )stores to a location l as non-atomic,
>>>>> T2 then (S2)stores to l as SC-atomic,
>>>>> later T3 (L3)loads from l as SC-atomic.
>>>>>
>>>>> I think the load @ T3 should return undef, since it can see both
>>>>> writes from T1 T2. Then the question is if the SC store @ T2 --- S2
>>>>> and the SC load @ T3 --- L3 introduces an acq/rel (synchronized-with)
>>>>> edge.
>>>>>
>>>>> This will affect if later conflicting accesses are ordered or not, and
>>>>> whether memory accesses are ordered makes load return undef or not.
>>>>>
>>>>> If the S2 and L3 still introduces an SW edge, the next question is
>>>>> suppose there is a later SC-load L3' @ T3, does it also return undef?
>>>>> But this potentially makes the SC atomic sequence S2 L3 L3'
>>>>> inconsistent --- later SC loads can read different writes from earlier
>>>>> loads if there are no SC-stores in between.
>>>>>
>>>>> So I think data-races SC/acq/rel atomics cannot introduce SW edges.
>>>>> Intuitively if the locations designed for locks are used by non-atomic
>>>>> memory accesses, the locks cannot behave correctly. Is it correct?
>>>>
>>>> Yes, that is correct.  I am now convinced that it is worthwhile to
>>>> include the definition of how SW edges form in LangRef.
>>>
>>> It's already there:
>>>
>>> "We define a happens-before partial order as the least partial order that
>>>
>>> * Is a superset of single-thread program order, and
>>> * When a synchronizes-with b, includes an edge from a to b.
>>> Synchronizes-with pairs are introduced by platform-specific
>>> techniques, like pthread locks, thread creation, thread joining, etc.,
>>> and by atomic instructions. (See also Atomic Memory Ordering
>>> Constraints)."
>>>
>>> ...
>>>
>>> "acquire - In addition to the guarantees of monotonic, if this
>>> operation reads a value written by a release atomic operation, it
>>> synchronizes-with that operation."
>>>
>>> (Strictly, the release operation synchronizes-with the acquire, not
>>> the other way around.)
>>>
>>> Since atomic/non-atomic races are defined to return undef from the
>>> load, even if the load has seq_cst ordering, the load never reads a
>>> value written, so none of the stores synchronize with the load.
>>
>> A undef can be replaced by any concrete value. If the undef returned
>> from the racy SC load happens to be instantiated by a value of the
>> latest SC store, does it consider as "... reads a value written by
>> ..."? I think our answer is still no, right?
>
> Right; semantically, undef isn't any concrete value, even though
> backends are forced to eventually turn it into one.

Yep. Note also that 'undef' isn't even necessarily a _single_ arbitrary value.

http://llvm.org/docs/LangRef.html#undefvalues says "This example
points out that two 'undef' operands are not necessarily the same.
This can be surprising to people (and also matches C semantics) where
they assume that "X^X" is always zero, even if X is undefined. This
isn't true for a number of reasons, but the short answer is that an
'undef' "variable" can arbitrarily change its value over its "live
range"."