+<!-- ======================================================================= -->
+<h3>
+ <a name="memmodel">Memory Model for Concurrent Operations</a>
+</h3>
+
+<div>
+
+<p>The LLVM IR does not define any way to start parallel threads of execution
+or to register signal handlers. Nonetheless, there are platform-specific
+ways to create them, and we define LLVM IR's behavior in their presence. This
+model is inspired by the C++0x memory model.</p>
+
+<p>For a more informal introduction to this model, see the
+<a href="Atomics.html">LLVM Atomic Instructions and Concurrency Guide</a>.
+
+<p>We define a <i>happens-before</i> partial order as the least partial order
+that</p>
+<ul>
+ <li>Is a superset of single-thread program order, and</li>
+ <li>When a <i>synchronizes-with</i> <tt>b</tt>, includes an edge from
+ <tt>a</tt> to <tt>b</tt>. <i>Synchronizes-with</i> pairs are introduced
+ by platform-specific techniques, like pthread locks, thread
+ creation, thread joining, etc., and by atomic instructions.
+ (See also <a href="#ordering">Atomic Memory Ordering Constraints</a>).
+ </li>
+</ul>
+
+<p>Note that program order does not introduce <i>happens-before</i> edges
+between a thread and signals executing inside that thread.</p>
+
+<p>Every (defined) read operation (load instructions, memcpy, atomic
+loads/read-modify-writes, etc.) <var>R</var> reads a series of bytes written by
+(defined) write operations (store instructions, atomic
+stores/read-modify-writes, memcpy, etc.). For the purposes of this section,
+initialized globals are considered to have a write of the initializer which is
+atomic and happens before any other read or write of the memory in question.
+For each byte of a read <var>R</var>, <var>R<sub>byte</sub></var> may see
+any write to the same byte, except:</p>
+
+<ul>
+ <li>If <var>write<sub>1</sub></var> happens before
+ <var>write<sub>2</sub></var>, and <var>write<sub>2</sub></var> happens
+ before <var>R<sub>byte</sub></var>, then <var>R<sub>byte</sub></var>
+ does not see <var>write<sub>1</sub></var>.
+ <li>If <var>R<sub>byte</sub></var> happens before
+ <var>write<sub>3</sub></var>, then <var>R<sub>byte</sub></var> does not
+ see <var>write<sub>3</sub></var>.
+</ul>
+
+<p>Given that definition, <var>R<sub>byte</sub></var> is defined as follows:
+<ul>
+ <li>If <var>R</var> is volatile, the result is target-dependent. (Volatile
+ is supposed to give guarantees which can support
+ <code>sig_atomic_t</code> in C/C++, and may be used for accesses to
+ addresses which do not behave like normal memory. It does not generally
+ provide cross-thread synchronization.)
+ <li>Otherwise, if there is no write to the same byte that happens before
+ <var>R<sub>byte</sub></var>, <var>R<sub>byte</sub></var> returns
+ <tt>undef</tt> for that byte.
+ <li>Otherwise, if <var>R<sub>byte</sub></var> may see exactly one write,
+ <var>R<sub>byte</sub></var> returns the value written by that
+ write.</li>
+ <li>Otherwise, if <var>R</var> is atomic, and all the writes
+ <var>R<sub>byte</sub></var> may see are atomic, it chooses one of the
+ values written. See the <a href="#ordering">Atomic Memory Ordering
+ Constraints</a> section for additional constraints on how the choice
+ is made.
+ <li>Otherwise <var>R<sub>byte</sub></var> returns <tt>undef</tt>.</li>
+</ul>
+
+<p><var>R</var> returns the value composed of the series of bytes it read.
+This implies that some bytes within the value may be <tt>undef</tt>
+<b>without</b> the entire value being <tt>undef</tt>. Note that this only
+defines the semantics of the operation; it doesn't mean that targets will
+emit more than one instruction to read the series of bytes.</p>
+
+<p>Note that in cases where none of the atomic intrinsics are used, this model
+places only one restriction on IR transformations on top of what is required
+for single-threaded execution: introducing a store to a byte which might not
+otherwise be stored is not allowed in general. (Specifically, in the case
+where another thread might write to and read from an address, introducing a
+store can change a load that may see exactly one write into a load that may
+see multiple writes.)</p>
+
+<!-- FIXME: This model assumes all targets where concurrency is relevant have
+a byte-size store which doesn't affect adjacent bytes. As far as I can tell,
+none of the backends currently in the tree fall into this category; however,
+there might be targets which care. If there are, we want a paragraph
+like the following:
+
+Targets may specify that stores narrower than a certain width are not
+available; on such a target, for the purposes of this model, treat any
+non-atomic write with an alignment or width less than the minimum width
+as if it writes to the relevant surrounding bytes.
+-->
+
+</div>
+
+<!-- ======================================================================= -->
+<h3>
+ <a name="ordering">Atomic Memory Ordering Constraints</a>
+</h3>
+
+<div>
+
+<p>Atomic instructions (<a href="#i_cmpxchg"><code>cmpxchg</code></a>,
+<a href="#i_atomicrmw"><code>atomicrmw</code></a>,
+<a href="#i_fence"><code>fence</code></a>,
+<a href="#i_load"><code>atomic load</code></a>, and
+<a href="#i_store"><code>atomic store</code></a>) take an ordering parameter
+that determines which other atomic instructions on the same address they
+<i>synchronize with</i>. These semantics are borrowed from Java and C++0x,
+but are somewhat more colloquial. If these descriptions aren't precise enough,
+check those specs (see spec references in the
+<a href="Atomic.html#introduction">atomics guide</a>).
+<a href="#i_fence"><code>fence</code></a> instructions
+treat these orderings somewhat differently since they don't take an address.
+See that instruction's documentation for details.</p>
+
+<p>For a simpler introduction to the ordering constraints, see the
+<a href="Atomics.html">LLVM Atomic Instructions and Concurrency Guide</a>.</p>
+
+<dl>
+<dt><code>unordered</code></dt>
+<dd>The set of values that can be read is governed by the happens-before
+partial order. A value cannot be read unless some operation wrote it.
+This is intended to provide a guarantee strong enough to model Java's
+non-volatile shared variables. This ordering cannot be specified for
+read-modify-write operations; it is not strong enough to make them atomic
+in any interesting way.</dd>
+<dt><code>monotonic</code></dt>
+<dd>In addition to the guarantees of <code>unordered</code>, there is a single
+total order for modifications by <code>monotonic</code> operations on each
+address. All modification orders must be compatible with the happens-before
+order. There is no guarantee that the modification orders can be combined to
+a global total order for the whole program (and this often will not be
+possible). The read in an atomic read-modify-write operation
+(<a href="#i_cmpxchg"><code>cmpxchg</code></a> and
+<a href="#i_atomicrmw"><code>atomicrmw</code></a>)
+reads the value in the modification order immediately before the value it
+writes. If one atomic read happens before another atomic read of the same
+address, the later read must see the same value or a later value in the
+address's modification order. This disallows reordering of
+<code>monotonic</code> (or stronger) operations on the same address. If an
+address is written <code>monotonic</code>ally by one thread, and other threads
+<code>monotonic</code>ally read that address repeatedly, the other threads must
+eventually see the write. This corresponds to the C++0x/C1x
+<code>memory_order_relaxed</code>.</dd>
+<dt><code>acquire</code></dt>
+<dd>In addition to the guarantees of <code>monotonic</code>,
+a <i>synchronizes-with</i> edge may be formed with a <code>release</code>
+operation. This is intended to model C++'s <code>memory_order_acquire</code>.</dd>
+<dt><code>release</code></dt>
+<dd>In addition to the guarantees of <code>monotonic</code>, if this operation
+writes a value which is subsequently read by an <code>acquire</code> operation,
+it <i>synchronizes-with</i> that operation. (This isn't a complete
+description; see the C++0x definition of a release sequence.) This corresponds
+to the C++0x/C1x <code>memory_order_release</code>.</dd>
+<dt><code>acq_rel</code> (acquire+release)</dt><dd>Acts as both an
+<code>acquire</code> and <code>release</code> operation on its address.
+This corresponds to the C++0x/C1x <code>memory_order_acq_rel</code>.</dd>
+<dt><code>seq_cst</code> (sequentially consistent)</dt><dd>
+<dd>In addition to the guarantees of <code>acq_rel</code>
+(<code>acquire</code> for an operation which only reads, <code>release</code>
+for an operation which only writes), there is a global total order on all
+sequentially-consistent operations on all addresses, which is consistent with
+the <i>happens-before</i> partial order and with the modification orders of
+all the affected addresses. Each sequentially-consistent read sees the last
+preceding write to the same address in this global order. This corresponds
+to the C++0x/C1x <code>memory_order_seq_cst</code> and Java volatile.</dd>
+</dl>
+
+<p id="singlethread">If an atomic operation is marked <code>singlethread</code>,
+it only <i>synchronizes with</i> or participates in modification and seq_cst
+total orderings with other operations running in the same thread (for example,
+in signal handlers).</p>
+
+</div>
+
+</div>
+