doc: tn13: Reword hybrid solution section
authorSimon Gerber <simon.gerber@inf.ethz.ch>
Fri, 2 Jun 2017 10:32:49 +0000 (12:32 +0200)
committerSimon Gerber <simon.gerber@inf.ethz.ch>
Fri, 2 Jun 2017 11:57:47 +0000 (13:57 +0200)
Signed-off-by: Simon Gerber <simon.gerber@inf.ethz.ch>

doc/013-capability-mgmt/CapMgmt.tex

index ef2aec8..fe19cd0 100644 (file)
@@ -1530,30 +1530,34 @@ Use a sequencer. This will order whole operations.
 
 \subsection{Hybrid}
 
-We can, of course, to combine facets of each of the previously discussed
+We can, of course, combine facets of each of the previously discussed
 approaches to build a hybrid approach which combines some (or all) of them.
 
-The approach discussed in chapters two and three of Mark Nevill's master's
+The solution discussed in chapters two and three of Mark Nevill's master's
 thesis~\cite{Nevill2012}, is one such hybrid approach, which combines locking,
 per capability sequencing, and two-phase commit.
 Additionally, Mark's solution does not require any additional requirements on
 Barrelfish's message channels, and works flawlessly with SSF message
 semantics.
 
-We only give a brief overview of the approach here, and refer the curious
-reader to Mark's thesis which discusses the approach in-depth.
+We only give a brief overview of the solution here, and refer to Mark's thesis
+which discusses the solution in depth, giving invariants, pre- and
+post-conditions, and algorithm sketches for each operation.
 
-The key concept for this approach is that, for each capability, of which there
+The key concept for this solution is that, for each capability, of which there
 can exist arbitrarily many copies, one core in the system is chosen as the
 capability's owner, or sequencer.
-All operations on a capability that need synchronization have to be proxied
-through the capability's owner.
+All operations on any copy of a capability that need synchronization have to
+be proxied through the capability's owner -- this is the sequencer aspect of
+the solution.
+
 We use locks to eliminate possible conflicts between operations, and merge
 overlapping deletes and revokes to avoid deadlocks.
+
 Delete and revoke employ a form of two-phase commit, which is implemented as a
 \emph{mark} and \emph{sweep} algorithm.
 Other operations treat capabilities that have been marked for deletion as
-already deleted, which eliminates many otherwise conflicting operations.
+already deleted, which avoids many otherwise conflicting operation sequences.
 
 \subsection{Comparison}
 Compare the approaches