Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add initial value of Figure A.13 #529

Closed
wants to merge 1 commit into from
Closed

Add initial value of Figure A.13 #529

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
18 changes: 10 additions & 8 deletions src/memory.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -668,7 +668,7 @@ \subsection{Syntactic Dependencies (Rules~\ref{ppo:addr}--\ref{ppo:ctrl})}
{
\tt\small
\begin{tabular}{cl||cl}
\multicolumn{4}{c}{Initial values: 0(s0)=1; 0(s1)=1} \\
\multicolumn{4}{c}{Initial values: 0(s0)=1; 0(s1)=1; 0(s2)=1} \\
\\
\multicolumn{2}{c}{Hart 0} & \multicolumn{2}{c}{Hart 1} \\
\hline
Expand Down Expand Up @@ -1067,7 +1067,9 @@ \section{Code Porting and Mapping Guidelines}
(c) sd x0,0(s1)
...
loop:
(d) amoswap.d.aq a1,t1,0(s1)
(d) lr.d.aq a1,0(s1)
bnez a1,loop
sc.d a1,t1,0(s1)
bnez a1,loop
(e) lw a2,0(s2)
\end{verbbox}
Expand Down Expand Up @@ -1311,9 +1313,9 @@ \section{Implementation Guidelines}

As written, if the load ~(d) reads value~$1$, then (a) must precede (f) in the global memory order:
\begin{itemize}
\item (a) precedes (c) in the global memory order because of rule 2
\item (a) precedes (c) in the global memory order because of rule 4
\item (c) precedes (d) in the global memory order because of the Load Value axiom
\item (d) precedes (e) in the global memory order because of rule 7
\item (d) precedes (e) in the global memory order because of rule 10
\item (e) precedes (f) in the global memory order because of rule 1
\end{itemize}
In other words the final value of the memory location whose address is in {\tt s0} must be~$2$ (the value written by the store~(f)) and cannot be~$3$ (the value written by the store~(a)).
Expand Down Expand Up @@ -1354,7 +1356,7 @@ \subsection{Mixed-size RSW}
& & (g) & lw a4,4(s2) \\
& & & xor a5,a4,a4 \\
& & & add s0,s0,a5 \\
& & (h) & sw a2,0(s0) \\
& & (h) & sw t1,0(s0) \\
\hline
\multicolumn{4}{c}{Outcome: {\tt a0=1}, {\tt a1=1}, {\tt a2=0}, {\tt a3=1}, {\tt a4=0}}
\end{tabular}
Expand All @@ -1374,9 +1376,9 @@ \subsection{Mixed-size RSW}
(b) & fence rw,rw & (e) & lw a2,4(s1) \\
(c) & sw t1,0(s1) & & xor a3,a2,a2 \\
& & & add s0,s0,a3 \\
& & (f) & sw a2,0(s0) \\
& & (f) & sw t1,0(s0) \\
\hline
\multicolumn{4}{c}{Outcome: {\tt a0=0}, {\tt a1=1}, {\tt a2=0}}
\multicolumn{4}{c}{Outcome: {\tt a0=1}, {\tt a1=1}, {\tt a2=0}}
\end{tabular}
}
\caption{Mixed-size discrepancy (permitted by axiomatic models, forbidden by operational model)}
Expand All @@ -1397,7 +1399,7 @@ \subsection{Mixed-size RSW}
& & & add s0,s0,a3 \\
& & (g) & sw a2,0(s0) \\
\hline
\multicolumn{4}{c}{Outcome: {\tt a0=1}, {\tt a1=0x100000001}, {\tt a1=1}}
\multicolumn{4}{c}{Outcome: {\tt a0=1}, {\tt a1=0x100000001}, {\tt a2=1}}
\end{tabular}
}
\caption{Mixed-size discrepancy (permitted by axiomatic models, forbidden by operational model)}
Expand Down