diff options
| -rw-r--r-- | src/a.tex | 7 |
1 files changed, 5 insertions, 2 deletions
@@ -172,12 +172,15 @@ An SC may succeed if no store from another hart, nor a write from some other device, to the reservation set 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 and data size, but +Note this LR might have had a different effective address and data size, but reserved the SC's address as part of the reservation set. +\begin{commentary} 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. +\end{commentary} + The SC must fail if the address is not within the reservation set of the most recent LR in program order. The SC must fail if a store from another hart, or a write from some other @@ -303,7 +306,7 @@ the following properties: \item The LR and SC addresses must lie within a memory region with the {\em LR/SC eventuality} property. The execution environment is responsible for communicating which regions have this property. -\item The SC must be to the same virtual address and of the same data size as +\item The SC must be to the same effective address and of the same data size as the latest LR executed by the same hart. \end{itemize} |