diff options
Diffstat (limited to 'algorithm.tex')
| -rw-r--r-- | algorithm.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/algorithm.tex b/algorithm.tex index 5ed47ad..f0c8ca2 100644 --- a/algorithm.tex +++ b/algorithm.tex @@ -288,7 +288,7 @@ However, the memory model that \compcert{} uses for its intermediate languages i % Mention that this optimisation is not performed sometimes (clang -03). -Many of the \compcert{} instructions map well to hardware, but \texttt{Oshrximm} is expensive if implemented na\"ively. The problem is that in \compcert{} it is specified as a signed division: +Many of the \compcert{} instructions map well to hardware, but \texttt{Oshrximm} (efficient signed division by a power of two using a logical shift) is expensive if implemented na\"ively. The problem is that in \compcert{} it is specified as a signed division: \begin{equation*} \texttt{Oshrximm } x\ y = \text{round\_towards\_zero}\left(\frac{x}{2^{y}}\right) \end{equation*} |