diff options
| author | Thomas Schwinge <thomas@schwinge.name> | 2010-12-21 11:41:13 +0100 |
|---|---|---|
| committer | Thomas Schwinge <thomas@schwinge.name> | 2010-12-21 11:41:13 +0100 |
| commit | eb383acc9c9cbc41bba971d3274843f9fc2f3816 (patch) | |
| tree | 20001185d4200d444467c98b45da54e9f5b81225 /microkernel/l4.mdwn | |
| parent | 2707251d04c59ce44048209d9d47737dd31e793c (diff) | |
| download | web-eb383acc9c9cbc41bba971d3274843f9fc2f3816.tar.gz web-eb383acc9c9cbc41bba971d3274843f9fc2f3816.tar.bz2 web-eb383acc9c9cbc41bba971d3274843f9fc2f3816.zip | |
open_issues/resource_management_problems: Elaborate.
Diffstat (limited to 'microkernel/l4.mdwn')
| -rw-r--r-- | microkernel/l4.mdwn | 14 |
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." + +"""]] |