Lines Matching refs:model

40 The Linux-kernel memory consistency model (LKMM) is rather complex and
43 version of the model; they are extremely terse and their meanings are
47 for people who want to understand how the model was designed.  It does
70 A memory consistency model (or just memory model, for short) is
78 for the loads, the model will predict whether it is possible for the
153 A memory model will predict what values P1 might obtain for its loads
157 Some predictions are trivial.  For instance, no sane memory model would
182 The first widely cited memory model, and the simplest to understand,
183 is Sequential Consistency.  According to this model, systems behave as
188 program source for each CPU.  The model says that the value obtained
213 Consistency memory model; doing so would rule out too many valuable
218 x86 and SPARC follow yet a different memory model: TSO (Total Store
219 Ordering).  This model predicts that the undesired outcome for the MP
276 In short, if a memory model requires certain accesses to be ordered,
278 if those accesses would form a cycle, then the memory model predicts
289 statements in a more abstract form, namely, events.  The model
314 memory model.  They only affect the model's predictions indirectly.
317 index, the address where the value gets stored), but the memory model
322 describe in the following sections.  The memory model requires certain
350 read, write, and fence events used by the model are close in spirit to
384 compiler to undermine the memory model.  Here is an example.  Suppose
412 model's original prediction could be invalidated by the compiler.
421 memory model cannot assume there is a fixed program order relation
550 unaligned accesses in a memory model, but the LKMM currently does not
602 the rules of the Sequential Consistency memory model.  (According to
607 Any reasonable memory model will include cache coherence.  Indeed, our
762 doesn't matter for the memory model.  But on Alpha, the local caches
767 restarted under certain circumstances.  The memory model ignores these
846 The operational model requires that whenever W and W' are both stores
882 	the operational model's rules regarding cache coherence.
968 The operational model already includes a description of one such
1065 (Interestingly, an early ARMv8 memory model, now obsolete, proposed
1066 allowing out-of-order writes like this to occur.  The model avoided
1173 the same CPU).  As we have already seen, the operational model allows
1217 order.  We can deduce this from the operational model; if P0's load
1783 in the formal model, added in order to make tools run faster.
1914 not arise from the operational model.  Nevertheless, kernel developers
1934 making such code very difficult for a memory model to handle.
2014 part of the memory model.  The hard part is telling whether they may
2308 This is a situation where the compiler can undermine the memory model,
2330 which would invalidate the memory model's assumption, since the CPU
2416 rules used by the operational model to ensure cache coherence (that
2455 hb anyway, and where the formal model adds prop into hb, it includes
2461 calls.  In the formal model, these events aren't actually both reads
2534 executions, some of which deadlock, the model will report only on the
2558 you it is not, but the model won't mention that this is because P1