summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorThomas Schwinge <thomas@schwinge.name>2010-12-21 11:41:13 +0100
committerThomas Schwinge <thomas@schwinge.name>2010-12-21 11:41:13 +0100
commiteb383acc9c9cbc41bba971d3274843f9fc2f3816 (patch)
tree20001185d4200d444467c98b45da54e9f5b81225
parent2707251d04c59ce44048209d9d47737dd31e793c (diff)
open_issues/resource_management_problems: Elaborate.
-rw-r--r--microkernel/l4.mdwn14
-rw-r--r--open_issues/resource_management_problems.mdwn44
2 files changed, 53 insertions, 5 deletions
diff --git a/microkernel/l4.mdwn b/microkernel/l4.mdwn
index 970407be..45929842 100644
--- a/microkernel/l4.mdwn
+++ b/microkernel/l4.mdwn
@@ -18,4 +18,18 @@ switching, and little else.
See [l4.verified](http://nicta.com.au/research/projects/l4.verified) for work
on formally verifying an L4 microkernel.
+ * {{$sel4}}
+
There was a GNU/Hurd [[history/port_to_L4]], which is now stalled.
+
+
+[[!ymlfront data="""
+
+sel4:
+
+ "G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin,
+ D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and
+ S. Winwood. seL4: Formal verification of an OS kernel. In Proceedings of
+ the ACM Symposium on OS Principles, Big Sky, MT, USA, October 2009."
+
+"""]]
diff --git a/open_issues/resource_management_problems.mdwn b/open_issues/resource_management_problems.mdwn
index 1723d7d3..3a36514e 100644
--- a/open_issues/resource_management_problems.mdwn
+++ b/open_issues/resource_management_problems.mdwn
@@ -6,8 +6,8 @@ id="license" text="Permission is granted to copy, distribute and/or modify this
document under the terms of the GNU Free Documentation License, Version 1.2 or
any later version published by the Free Software Foundation; with no Invariant
Sections, no Front-Cover Texts, and no Back-Cover Texts. A copy of the license
-is included in the section entitled
-[[GNU Free Documentation License|/fdl]]."]]"""]]
+is included in the section entitled [[GNU Free Documentation
+License|/fdl]]."]]"""]]
[[!tag open_issue_gnumach open_issue_hurd open_issue_viengoos]]
@@ -22,8 +22,42 @@ These issues are what Neal Walfield is working on with his new kernel
[[microkernel/viengoos]].
-# Examples
+# Kernel
- * [[configure max command line length]]
+Inside the [[kernel]], there is commonly a need to allocate resources according
+to externally induced demand, dynamically. For example, for memory-management
+data structures (page tables), process table entries, thread control blocks,
+[[capability]] tables, incoming network packages, blocks that are read in from
+disk, the keyboard type-ahead buffer for a in-kernel keyboard driver. Some of
+these are due to actions driven by user-space requests, others are due to
+actions internal to the the kernel itself. Some of these buffers can be sized
+statically (keyboard type-ahead buffer), and are thus unproblematic. Others
+are not, and should thus be attributed to their user space entities. In the
+latter (ideal) case, all resources -- that is, including those needed inside
+the kernel -- that a user space task needs for execution are provided by itself
+(and, in turn, provided by its parent / principal), and the kernel itself does
+not need to allocate any resources dynamically out of an its own memory pool.
+This avoids issues like [[microkernel/Mach]]'s [[zalloc_panics]] upon user
+space processes allocating too many [[microkernel/mach/port]]s, for example.
+
+[[!toggleable id=fof_plos09 text="""[[!template id=note
+text="*[[fof\_plos09|microkernel/barrelfish]]*:
+{{$microkernel/barrelfish#fof_plos09}}"]]"""]]
+
+[[!toggleable id=sel4 text="""[[!template id=note
+text="[[*sel4*|microkernel/l4]]: {{$microkernel/l4#sel4}}"]]"""]]
+
+In [[!toggle id=fof_plos09 text="[fof\_plos09]"]], the authors describe in
+section 3 how they model their [[capability]] system according to [[!toggle
+id=sel4 text="[sel4]"]] using a *retype* operation that *takes an existing
+capability and produces one or more derived capabilities [...] used to create
+new kernel-level memory objects (such as page tables or execution contexts)
+from capabilities to raw regions of RAM*.
- * [[zalloc_panics]]
+This is, of course, non-trivial to implement, and also requires changing the
+[[RPC]] interfaces, for example, but it is a valid approach, a research topic.
+
+
+# Further Examples
+
+ * [[configure max command line length]]