summaryrefslogtreecommitdiff
path: root/microkernel/l4.mdwn
blob: de3114971cb83f09549f433accdb5c275546a9ff (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
[[!meta copyright="Copyright © 2004, 2006, 2007, 2008, 2010, 2011, 2012 Free
Software Foundation, Inc."]]

[[!meta license="""[[!toggle id="license" text="GFDL 1.2+"]][[!toggleable
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]]."]]"""]]

The [*L4* microkernel](http://l4ka.org/) is an attempt to create a very small
high performace core which provides basic memory management, task and context
switching, and little else.

[L4Ka Pistachio Home](http://l4ka.org/projects/pistachio/).

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 [[port to L4|history/port_to_another_microkernel]], which
is now stalled.


# IRC, freenode, #hurd, 2012-08-02

    <mcsim> If someone interested, there is a channel with lectures about
      Genode and L4: http://www.youtube.com/user/drsartakov?feature=watch


[[!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."

"""]]