From 22a0383af387e761b52f521a63c6e45f7fff7f74 Mon Sep 17 00:00:00 2001 From: Krste Asanovic Date: Tue, 7 Aug 2018 22:34:49 -0700 Subject: Clarified A definitions. --- src/a.tex | 45 ++++++++++++++++++--------------------------- src/riscv-spec.tex | 4 ++-- 2 files changed, 20 insertions(+), 29 deletions(-) diff --git a/src/a.tex b/src/a.tex index b2bd899..0dac426 100644 --- a/src/a.tex +++ b/src/a.tex @@ -167,7 +167,7 @@ lost, but eventually the atomic sequence can complete. We restricted the length of LR/SC sequences to fit within 64 contiguous instruction bytes in the base ISA to avoid undue restrictions on instruction cache and TLB size and associativity. Similarly, we disallowed other loads -and stores within the sequences to avoid restrictions on data cache +and stores within the sequences to avoid restrictions on data-cache associativity. The restrictions on branches and jumps limits the time that can be spent in the sequence. Floating-point operations and integer multiply/divide were disallowed to simplify the operating @@ -178,30 +178,27 @@ Although software is not forbidden from using LR/SC sequences that do not meet the forward-progress constraints, portable software must detect the case that the sequence repeatedly fails, then fall back to an alternate code sequence that does not run afoul of the forward-progress constraints. -Implementations are permitted to simply always fail any LR/SC sequences that do -not meet the forward-progress guarantees. +Implementations are permitted to simply always fail any LR/SC sequence that does +not meet the forward-progress guarantee. \end{commentary} -Certain LR/SC sequences that do not meet the forward progress -guarantees may succeed on some implementations. An implementation can -reserve an arbitrary subset of the memory space on each LR. 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 +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. The precise statement of the atomicity requirements for -successful LR/SC sequences is defined by the Atomicity Axiom in -Section~\ref{sec:rvwmo}. - -In the standard A extension, an SC must fail if there is another SC (to -any address) between the LR and the SC in program order. In other -words, multiple outstanding reservations are not permitted. +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 @@ -209,12 +206,6 @@ during a preemptive context switch to forcibly yield any existing load reservation. \end{commentary} -\begin{commentary} -The specification explicitly allows implementations to support more -powerful implementations with wider guarantees, provided they do not -void the atomicity guarantees for the constrained sequences. -\end{commentary} - LR/SC can be used to construct lock-free data structures. An example using LR/SC to implement a compare-and-swap function is shown in Figure~\ref{cas}. If inlined, compare-and-swap functionality need diff --git a/src/riscv-spec.tex b/src/riscv-spec.tex index 8648fd5..02d77bf 100644 --- a/src/riscv-spec.tex +++ b/src/riscv-spec.tex @@ -74,13 +74,13 @@ Andrew Waterman and Krste Asanovi\'{c}, RISC-V Foundation, May 2017. \input{rv32e} \input{rv64} \input{rv128} -\input{csr} -\input{rvwmo} \input{m} \input{a} +\input{csr} \input{f} \input{d} \input{q} +\input{rvwmo} \input{l} \input{c} \input{b} -- cgit v1.1