From 91623403f0a3a4334963dd5c05f80fae43cbc263 Mon Sep 17 00:00:00 2001 From: Shaked Flur Date: Thu, 2 Aug 2018 19:35:04 +0100 Subject: Minor change to the operational memory model (#216) * Minor syntactic change to the operational memory model * Minor tweak to the previous change. --- src/memory-model-operational.tex | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/memory-model-operational.tex b/src/memory-model-operational.tex index 3790b2c..d0ce212 100644 --- a/src/memory-model-operational.tex +++ b/src/memory-model-operational.tex @@ -560,7 +560,8 @@ An AMO instruction instance $i$ in state {\sc Pending\_mem\_loads}({\it load\_co \item \nameref{omm:prop_store} \item \nameref{omm:complete_stores} \end{enumerate} -Action: perform the above sequence of transitions, one after the other, with no intervening transitions. +and in addition, the condition of \nameref{omm:finish}, with the exception of not requiring $i$ to be in state {\sc Plain}({\sc Done}), holds after those transitions. +Action: perform the above sequence of transitions (this does not include \nameref{omm:finish}), one after the other, with no intervening transitions. \begin{commentary} Notice that program-order-previous stores cannot be forwarded to the load of an AMO. -- cgit v1.1