doc: tn13: add KCB to cap types

Signed-off-by: Simon Gerber <simon.gerber@inf.ethz.ch>

diff --git a/doc/013-capability-mgmt/type_system.tex b/doc/013-capability-mgmt/type_system.tex
index b16994c..7730636 100644 (file)
--- a/doc/013-capability-mgmt/type_system.tex
+++ b/doc/013-capability-mgmt/type_system.tex
@@ -809,3 +809,37 @@ Further Kernel capability invocations that we will have to document:
   \item \verb|KernelCmd_Get_platform|: Get architecture platform.
 \end{itemize}
 
+\subsection{Kernel Control Block}
+A kernel control block capability captures all the state for a single CPU
+driver.  This allows us to do interesting operations such as rebooting a core
+at runtime~\cite{Coreboot:Zellweger2014}.
+A kernel control block is structured according to the \verb|struct kcb|
+defined in the CPU driver code.
+
+\begin{description}
+\item[Origin] Retyping from RAM type capabilities
+
+\item[Retypability] No
+
+\item[Mint parameters] No
+
+\item[Interpretation of rights] \note{Explain rights and rights mask.
+  Capability rights and rights masks are currently not implemented.
+  This means that every user domain holding a capability has full
+  rights to it.}
+
+\item[Transferability to another core] Yes, between cores that share memory.
+  When transferred to another core, can be scheduled on that core.
+
+\item[Last copy deleted] \note{NYI}
+
+\item[Concrete representations] The in-memory representation is as follows:
+    
+  \begin{lstlisting}[language=Mackerel]
+    datatype KernelControlBlock "Represents a CPU driver's state" {
+      kcb     64  "Kernel address of the KCB represented by this capability"
+    };
+    \end{lstlisting}
+\end{description}
+
+\note{Need to discuss invocations on KCB}

diff --git a/doc/style/barrelfish.bib b/doc/style/barrelfish.bib
index fa0f601..e13316a 100644 (file)
--- a/doc/style/barrelfish.bib
+++ b/doc/style/barrelfish.bib
@@ -1373,3 +1373,19 @@ D. E. Long and Carlos Maltzahn},
  month = may,
  url = {http://www.barrelfish.org/publications/nevill-master-capabilities.pdf}
 }
+
+@inproceedings{Coreboot:Zellweger2014,
+ author = {Zellweger, Gerd and Gerber, Simon and Kourtis, Kornilios and Roscoe, Timothy},
+ title = {Decoupling Cores, Kernels, and Operating Systems},
+ booktitle = {Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation},
+ series = {OSDI'14},
+ year = {2014},
+ isbn = {978-1-931971-16-4},
+ location = {Broomfield, CO},
+ pages = {17--31},
+ numpages = {15},
+ url = {http://dl.acm.org/citation.cfm?id=2685048.2685051},
+ acmid = {2685051},
+ publisher = {USENIX Association},
+ address = {Berkeley, CA, USA},
+}