summaryrefslogtreecommitdiff
path: root/microkernel/l4.mdwn
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 /microkernel/l4.mdwn
parent2707251d04c59ce44048209d9d47737dd31e793c (diff)
open_issues/resource_management_problems: Elaborate.
Diffstat (limited to 'microkernel/l4.mdwn')
-rw-r--r--microkernel/l4.mdwn14
1 files changed, 14 insertions, 0 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."
+
+"""]]