On Mon, Aug 22, 2011 at 6: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.Some of the descriptions in LangRef and http://llvm.org/docs/Atomics.html are like 1) monotonic atomic to the same location are totally ordered 2) all SC atomic to to any location are totally ordered 3) monotonic loads should see monotonic stores monotonically ... However, these conditions can be broken if any of them are 'interferenced' by non-atomic memory accesses, since that can turn some of the atomic loads to be undef (with any values). So it is unlikely forming a total order any more. So, do these properties hold only for data race free atomics? For example, T1: T2: a: sc store 1 to location x b: non-atomic store 2 to x c: sc store 3 to y d: r1 = sc load from y e: r2 = sc load from x Here, r2 still returns undef, since e can see a non-atomic store although from happens-before. Then a c d e may not be totally ordered.> > -Eli >-- Jianzhou
On Mon, Aug 22, 2011 at 4:20 PM, Jianzhou Zhao <jianzhou at seas.upenn.edu> wrote:> On Mon, Aug 22, 2011 at 6: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. > > Some of the descriptions in LangRef and > http://llvm.org/docs/Atomics.html are like > 1) monotonic atomic to the same location are totally ordered > 2) all SC atomic to to any location are totally ordered > 3) monotonic loads should see monotonic stores monotonically > ... > > However, these conditions can be broken if any of them are > 'interferenced' by non-atomic memory accesses, since that can turn > some of the atomic loads to be undef (with any values). So it is > unlikely forming a total order any more. > > So, do these properties hold only for data race free atomics? For example, > > T1: T2: > a: sc store 1 to location x > b: non-atomic store 2 to x > c: sc store 3 to y > d: r1 = sc load from y > e: r2 = sc load from x > > Here, r2 still returns undef, since e can see a non-atomic store > although from happens-before. Then a c d e may not be totally ordered.Say r1==3, so we're guaranteed that 'e' happens after 'b'. Since neither a nor b happens before the other, and at least one of them is not atomic, r2==undef. The seq_cst ordering a, c, d, e is consistent with the observable results. That's true whether printing r2 prints 1, 2, or 47 since undef can be observed as any value. Jeffrey
On Mon, Aug 22, 2011 at 7:35 PM, Jeffrey Yasskin <jyasskin at google.com> wrote:> On Mon, Aug 22, 2011 at 4:20 PM, Jianzhou Zhao <jianzhou at seas.upenn.edu> wrote: >> On Mon, Aug 22, 2011 at 6: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. >> >> Some of the descriptions in LangRef and >> http://llvm.org/docs/Atomics.html are like >> 1) monotonic atomic to the same location are totally ordered >> 2) all SC atomic to to any location are totally ordered >> 3) monotonic loads should see monotonic stores monotonically >> ... >> >> However, these conditions can be broken if any of them are >> 'interferenced' by non-atomic memory accesses, since that can turn >> some of the atomic loads to be undef (with any values). So it is >> unlikely forming a total order any more. >> >> So, do these properties hold only for data race free atomics? For example, >> >> T1: T2: >> a: sc store 1 to location x >> b: non-atomic store 2 to x >> c: sc store 3 to y >> d: r1 = sc load from y >> e: r2 = sc load from x >> >> Here, r2 still returns undef, since e can see a non-atomic store >> although from happens-before. Then a c d e may not be totally ordered. > > Say r1==3, so we're guaranteed that 'e' happens after 'b'. Since > neither a nor b happens before the other, and at least one of them is > not atomic, r2==undef. The seq_cst ordering a, c, d, e is consistent > with the observable results. That's true whether printing r2 prints 1, > 2, or 47 since undef can be observed as any value.My confusion is the difference between SC and AcquireRelease. The text says ... SequentiallyConsistent SequentiallyConsistent (seq_cst in IR) provides Acquire semantics for loads and Release semantics for stores. Additionally, it guarantees that a total ordering exists between all SequentiallyConsistent operations. ... Here, what does the total ordering mean? Does it mean given a sequence of SC atomic in the total order, an SC load should return the recent SC store from the sequence? This is like the meaning of Sequential consistent memory model---any SC stores should be visible to all SC loads immediately in the same order. In the above program, we have the SC atomics sc store 1 to x sc store 3 to y sc load from y = 3 sc load from x = 47 or undef Here, no matter how we order them, there is no way to place a store 47 to x before load x with 47. Did I make a wrong assumption?> > Jeffrey >-- Jianzhou