-
Notifications
You must be signed in to change notification settings - Fork 6
/
app-cheri-concentrate-listings.tex
58 lines (42 loc) · 3.62 KB
/
app-cheri-concentrate-listings.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
\chapter{CHERI Concentrate Listings}
\label{app:cheri-128-listings}
The cheri-cap-lib~\cite{CHERI-cheri-cap-lib} open-source library has been used in all of our open-source~\cite{CHERI-cheri-cpu,CHERI-Piccolo,CHERI-Flute,CHERI-Toooba} implementations and contains certain notable algorithms which have been highly optimised and verified to a significant degree.
These algorithms are well documented by their contents, so several are reproduced in their current form\footnote{\input{cheri_concentrate_listings/conc_version}} here to serve as reference to anyone implementing CHERI Concentrate compression in any model or microarchitecture.
\section{GetTop}
\label{sec:cheri-128-listings-gettop}
This \emph{GetTop} function for compressed capabilities is very similar to the \emph{GetBase} function which uses \emph{baseBits} rather than \emph{topBits}.
There is a significant divergence from line 11 where we discern between a top of 0 and a top of $2^{64}$.
It has been non-trivial to develop an algorithm that is both correct and fast enough for all uses in our implementations.
\lstinputlisting[language=bluespec]{cheri_concentrate_listings/conc_getTopFat.bsv}
\section{CapInBounds}
\label{sec:cheri-128-listings-capinbounds}
\emph{CapInBounds} detects if the current address of a capability is within its bounds.
This function does not decode the Top and Base of the capability,
but operates directly on compressed fields saving both time and logic.
\lstinputlisting[language=bluespec]{cheri_concentrate_listings/conc_capInBounds.bsv}
\section{IncOffset}
\label{sec:cheri-128-listings-incoffset}
The IncOffset function from cheri-cap-lib is shared between the IncOffset operation and the SetOffset operation as these two can be made to largely share logic.
The IncOffset function is almost entirely composed of the \emph{fast representable check}~\cite{Woodruff2019}, as the only change to the capability in a non-faulting case is to add the increment to the address.
This check determines if the resulting capability will decode as having the same bounds after the address modification, invalidating the capability if this might not be the case.
As this check is conservative, the boundary conditions are specified in the CHERI architecture in Section~\ref{sec:cheri-concentrate-fast-representable-limit-checking}.
This check is intended to run alongside the add of the address in execute unit.
\lstinputlisting[language=bluespec]{cheri_concentrate_listings/conc_incOffsetFat.bsv}
\section{SetAddress}
\label{sec:cheri-128-listings-setaddress}
This \emph{SetAddress} function assigns a new address to the address field
of a capability.
It is almost entirely composed of a \emph{fast representable check} which asserts
that the bounds will continue to decode to the same value after the assignment
without actually decoding either of the bounds, which is slow.
If the bounds would change, the capability is invalidated.
\lstinputlisting[language=bluespec]{cheri_concentrate_listings/conc_setAddress.bsv}
\section{SetBounds}
\label{sec:cheri-128-listings-setbounds}
The \emph{SetBounds} function sets a new base and length of a capability, performing
and necessary rounding.
This function actually returns a data structure which includes not only the new capability,
but a flag indicating if rounding was necessary (to facilitate \emph{CSetBoundsExact}),
a mask that could be applied to a pointer to align it with the supplied length (to facilitate \emph{CRepresentableAlignmentMask}),
as well as the length that was actually achieved after rounding (to facilitate \emph{CRoundRepresentableLength}).
\lstinputlisting[language=bluespec]{cheri_concentrate_listings/conc_setBoundsFat.bsv}