Strengthen atomic_compare_exchange seq_cst failure mapping

The Zacas extension defines different ordering behavior when an amocas fails:
> The memory operation performed by an AMOCAS.W/D/Q, when not successful, has
> acquire semantics if aq bit is 1 but does not have release semantics,
> regardless of rl.

This requires a leading fence to maintain A6C compatability for both the RVWMO
and Ztso memory models. The A7 mappings can use the non-fenced versions.

See issue riscv-non-isa#444 for more context and litmus tests.

Resolves riscv-non-isa#444.

Author: patrick-rivos

riscv-atomic.adoc

@@ -107,7 +107,7 @@ the `lr` and `sc` instructions.
 
 |`atomic_<op>(memory_order_acq_rel)` |`amo<op>.{w\|d}.aqrl` |4
 
-|`atomic_<op>(memory_order_seq_cst)` |`amo<op>.{w\|d}.aqrl` |4
+|`atomic_<op>(memory_order_seq_cst)` |`amo<op>.{w\|d}.aqrl` |4, 5
 
 |===
 
@@ -148,6 +148,11 @@ mappings with code generated by a compiler using those older mappings.
 
 4) Currently only directly possible for 32- and 64-bit operands.
 
+5) atomic_compare_exchange operations with a memory_order_seq_cst failure
+ordering are considered to have a note 3 annotation.
+To remove the note 3 annotation the amocas operation must be prepended with a
+leading fence (`fence rw,rw; amocas.{w\|d}.aqrl`).
+
 == Ztso atomics mappings
 
 This specifies additional mappings of C and {Cpp} atomic operations to RISC-V
@@ -157,7 +162,8 @@ For each construct, we provide a mapping that assumes only the A and Ztso
 extension.
 
 All mappings interoperate correctly with the RVWMO mappings, and with the
-original "Table A.6" mappings.
+original "Table A.6" mappings, _except_ that mappings marked with note 3 do not
+interoperate with the original "Table A.6" mappings.
 
 We present the mappings as a table in 3 sections, as above.
 
@@ -167,32 +173,32 @@ We present the mappings as a table in 3 sections, as above.
 |===
 |C/{Cpp} Construct |Ztso Mapping |Notes
 
-|`atomic_load(memory_order_acquire)` |`l{b\|h\|w\|d}` | 5
+|`atomic_load(memory_order_acquire)` |`l{b\|h\|w\|d}` | 6
 
-|`atomic_load(memory_order_seq_cst)` |`fence rw,rw; l{b\|h\|w\|d}` | 5
+|`atomic_load(memory_order_seq_cst)` |`fence rw,rw; l{b\|h\|w\|d}` | 6
 
-|`atomic_store(memory_order_release)` |`s{b\|h\|w\|d}` | 5
+|`atomic_store(memory_order_release)` |`s{b\|h\|w\|d}` | 6
 
-|`atomic_store(memory_order_seq_cst)` |`s{b\|h\|w\|d}; fence rw, rw` | 5
+|`atomic_store(memory_order_seq_cst)` |`s{b\|h\|w\|d}; fence rw, rw` | 6
 
-|`atomic_thread_fence(memory_order_acquire)` |`nop` | 5
+|`atomic_thread_fence(memory_order_acquire)` |`nop` | 6
 
-|`atomic_thread_fence(memory_order_release)` |`nop` | 5
+|`atomic_thread_fence(memory_order_release)` |`nop` | 6
 
-|`atomic_thread_fence(memory_order_acq_rel)` |`nop` | 5
+|`atomic_thread_fence(memory_order_acq_rel)` |`nop` | 6
 |===
 
 [cols="<20,<20,<4",options="header",]
 |===
 |C/{Cpp} Construct |Ztso AMO Mapping |Notes
 
-|`atomic_<op>(memory_order_acquire)` |`amo<op>.{w\|d}` |4, 5
+|`atomic_<op>(memory_order_acquire)` |`amo<op>.{w\|d}` |4, 6
 
-|`atomic_<op>(memory_order_release)` |`amo<op>.{w\|d}` |4, 5
+|`atomic_<op>(memory_order_release)` |`amo<op>.{w\|d}` |4, 6
 
-|`atomic_<op>(memory_order_acq_rel)` |`amo<op>.{w\|d}` |4, 5
+|`atomic_<op>(memory_order_acq_rel)` |`amo<op>.{w\|d}` |4, 6
 
-|`atomic_<op>(memory_order_seq_cst)` |`amo<op>.{w\|d}` |4, 5
+|`atomic_<op>(memory_order_seq_cst)` |`amo<op>.{w\|d}` |4, 5, 6
 
 |===
 
@@ -201,21 +207,26 @@ We present the mappings as a table in 3 sections, as above.
 |C/{Cpp} Construct |Ztso LR/SC Mapping |Notes
 
 |`atomic_<op>(memory_order_acquire)`
-|`loop:lr.{w\|d}; <op>; sc.{w\|d}; bnez loop` |4, 5
+|`loop:lr.{w\|d}; <op>; sc.{w\|d}; bnez loop` |4, 6
 
 |`atomic_<op>(memory_order_release)`
-|`loop:lr.{w\|d}; <op>; sc.{w\|d}; bnez loop` |4, 5
+|`loop:lr.{w\|d}; <op>; sc.{w\|d}; bnez loop` |4, 6
 
 |`atomic_<op>(memory_order_acq_rel)`
-|`loop:lr.{w\|d}; <op>; sc.{w\|d}; bnez loop` |4, 5
+|`loop:lr.{w\|d}; <op>; sc.{w\|d}; bnez loop` |4, 6
 
 |===
 
 === Meaning of notes in table
 
 4) Currently only directly possible for 32- and 64-bit operands.
 
-5) Requires the Ztso extension.
+5) atomic_compare_exchange operations with a memory_order_seq_cst failure
+ordering are considered to have a note 3 annotation.
+To remove the note 3 annotation the amocas operation must be prepended with a
+leading fence (`fence rw,rw; amocas.{w\|d}`).
+
+6) Requires the Ztso extension.
 
 == Other conventions