From a4c6b9f7d2ba139bd1ad8b5d66da8a0a0b0aba4d Mon Sep 17 00:00:00 2001 From: Andrew Waterman Date: Sat, 3 Aug 2019 18:07:27 -0700 Subject: Avoid using "virtual address" in normative text of unprivileged spec (#430) --- src/a.tex | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/a.tex b/src/a.tex index b069f7e..ca21955 100644 --- a/src/a.tex +++ b/src/a.tex @@ -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} -- cgit v1.1