From eb383acc9c9cbc41bba971d3274843f9fc2f3816 Mon Sep 17 00:00:00 2001 From: Thomas Schwinge Date: Tue, 21 Dec 2010 11:41:13 +0100 Subject: open_issues/resource_management_problems: Elaborate. --- microkernel/l4.mdwn | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'microkernel') 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." + +"""]] -- cgit v1.2.3