Lines Matching refs:t

61 proper format for litmus tests.  They don't include a header line, the
63 not passed by pointers, and they don't have an "exists" clause at the
89 memory locations, things aren't so simple.
149 completion, and real code generally doesn't bother to copy values into
258 (i.e., the order in which certain events occur) but it doesn't have to
308 write event is omitted for executions where it doesn't occur, such as
369 that in the MP example, the compiler won't reorder P0's write event to
486 have R ->po X. It wouldn't make sense for a computation to depend
487 somehow on a value that doesn't get loaded from shared memory until
492 between two accesses is purely syntactic if the second access doesn't
529 of undefined behavior. Therefore the compiler doesn't have to worry
533 be undefined anyway, so the compiler doesn't care!) Thus the value
558 read from a single store. It doesn't apply properly in the presence
811 time to process the stores that it receives, and a store can't be used
815 doesn't matter for the memory model. But on Alpha, the local caches
824 Executing a fence (or memory barrier) instruction doesn't require a
887 though smp_wmb() isn't A-cumulative. The cumul-fence relation is
910 maintaining cache coherence and the fact that a CPU can't operate on a
1090 then ignore the result if it turns out that the second load shouldn't
1185 At first glance this doesn't seem to make sense. We know that the
1187 to ptr does. And since P1 can't execute its second load
1190 second load executed. So why doesn't r2 end up equal to 1?
1199 program order, it appears that they aren't.
1269 doesn't mean that W has to execute after R. All that's necessary is
1376 Since an instruction can't execute before itself, we are forced to
1523 be nested, although we won't make use of this fact.
1587 are pretty obvious, as in the example above, but the details aren't
1597 obscure, and we won't give it here. It is closely related to the pb
1598 relation, and the details don't matter unless you want to comb through
1620 Z's CPU before Z begins but doesn't propagate to some other CPU until
1691 CPUs. (Perhaps this fact should lead us to say that rcu-fence isn't
1708 Justifying the axiom isn't easy, but it is in fact a valid
1709 formalization of the Grace Period Guarantee. We won't attempt to go
1714 critical section but doesn't propagate to some other CPU until after
1899 that matching calls don't have to execute on the same CPU.
1954 Fortunately this won't matter, assuming that litmus tests never do
2063 spinlock_t s, t;
2072 spin_lock(&t);
2074 spin_unlock(&t);
2225 doesn't try to predict all possible outcomes of code containing plain
2263 If two memory accesses aren't concurrent then one must execute before
2264 the other. Therefore the LKMM decides two accesses aren't concurrent
2270 no danger of X and Y being concurrent. After all, Y can't have any
2272 propagated Y from its own CPU to X's CPU, which won't happen until
2365 Fortunately, the compiler isn't completely free; it is subject to some
2375 code, the barrier() function is a compiler barrier. It doesn't give
2393 The LKMM doesn't say much about the barrier() function, but it does
2438 r1 will be 0, so V will not be executed and ipso facto won't
2488 (This may be overly cautious. We don't know of any examples where a
2496 a concurrent load from that location. Two concurrent loads don't
2497 constitute a race (they can't interfere with each other), but a store
2501 load, on the other hand, is acceptable because doing so won't create a
2514 stipulation, since after all, the CPU can't perform the load of *p
2539 (In this example the rcu_read_lock() and rcu_read_unlock() calls don't
2540 really do anything, because there aren't any grace periods. They are
2582 be on different CPUs, and fences don't link events on different CPUs.
2583 Well, normal fences don't -- but rcu-fence can! Here's an example:
2616 isn't w-post-bounded by any marked accesses.
2620 stores don't race if W can be linked to W' by a
2633 two accesses don't race if R can be linked to W by an
2654 various relation must not contain a cycle) doesn't apply to plain
2656 they don't make sense even for plain accesses.
2689 This section covers material that didn't quite fit anywhere in the
2692 The descriptions in this document don't always match the formal
2695 optional, and it doesn't require the events linked by the relation to
2705 calls. In the formal model, these events aren't actually both reads
2710 Although we didn't mention it above, the instruction execution
2711 ordering provided by the smp_rmb() fence doesn't apply to read events
2724 no further involvement from the CPU. Since the CPU doesn't ever read
2809 you it is not, but the model won't mention that this is because P1