diff options
| -rw-r--r-- | src/a.tex | 45 |
1 files changed, 25 insertions, 20 deletions
@@ -86,9 +86,10 @@ Complex atomic memory operations on a single memory word are performed with the load-reserved (LR) and store-conditional (SC) instructions. LR loads a word from the address in {\em rs1}, places the sign-extended value in {\em rd}, and registers a reservation on the -memory address. SC writes a word in {\em rs2} to the address in {\em - rs1}, provided a valid reservation still exists on that address. SC -writes zero to {\em rd} on success or a nonzero code on failure. +memory address and a range of bytes including at least all bytes of +the addressed word. SC writes a word in {\em rs2} to the address in +{\em rs1}, provided a valid reservation still exists on that address. +SC writes zero to {\em rd} on success or a nonzero code on failure. \begin{commentary} Both compare-and-swap (CAS) and LR/SC can be used to build lock-free @@ -182,23 +183,27 @@ Implementations are permitted to simply always fail any LR/SC sequence that does not meet the forward-progress guarantee. \end{commentary} -An implementation can reserve an arbitrary larger subset of the memory -space on each LR, provided the memory range includes all bytes of the -addressed data word. An SC may succeed if no store from another hart -to the address range reserved by the LR can be observed to have -occurred between the LR and the SC, and if there is no other SC -between the LR and itself in program order. Note this LR might have -had a different address argument, but reserved the SC's address as -part of the memory subset. Following this model, in systems with -memory translation, an SC is allowed to succeed if the earlier LR -reserved the same location using an alias with a different virtual -address, but is also allowed to fail if the virtual address is -different. The SC must fail if a store from another hart to the -address range reserved by the LR can be observed to occur between the -LR and the SC. An SC must fail if there is another SC (to any -address) between the LR and the SC in program order. The precise -statement of the atomicity requirements for successful LR/SC sequences -is defined by the Atomicity Axiom in Section~\ref{sec:rvwmo}. +An implementation can reserve an arbitrarily large subset of the +address space on each LR, provided the memory range includes all bytes +of the addressed data word. The reserved address range does not have +to be constant on each dynamic invocation of a static LR instruction, +or on each time a given address and data word size are used by an LR. +An SC can only pair with the most recent LR in program order. An SC +may succeed if no store from another hart to the address range +reserved by the LR can be observed to have occurred between the LR and +the SC, and if there is no other SC between the LR and itself in +program order. Note this LR might have had a different address +argument, but reserved the SC's address as part of the memory subset. +Following this model, in systems with memory translation, an SC is +allowed to succeed if the earlier LR reserved the same location using +an alias with a different virtual address, but is also allowed to fail +if the virtual address is different. The SC must fail if a store from +another hart to the address range reserved by the LR can be observed +to occur between the LR and the SC. An SC must fail if there is +another SC (to any address) between the LR and the SC in program +order. The precise statement of the atomicity requirements for +successful LR/SC sequences is defined by the Atomicity Axiom in +Section~\ref{sec:rvwmo}. \begin{commentary} A store-conditional instruction to a scratch word of memory should be used |