diff options
Diffstat (limited to 'microkernel')
| -rw-r--r-- | microkernel/coyotos.mdwn | 30 | ||||
| -rw-r--r-- | microkernel/l4.mdwn | 21 |
2 files changed, 51 insertions, 0 deletions
diff --git a/microkernel/coyotos.mdwn b/microkernel/coyotos.mdwn new file mode 100644 index 00000000..5ecea688 --- /dev/null +++ b/microkernel/coyotos.mdwn @@ -0,0 +1,30 @@ +[[!meta copyright="Copyright © 2006, 2007, 2008, 2010 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]]."]]"""]] + +[[!meta title="Coyotos"]] + +[*Coyotos*](http://www.coyotos.org/) is a microkernel and OS and the successor +of [[EROS]], that itself is the successor of [[KeyKOS]]. A more complete +history can be found [here](http://www.coyotos.org/history.html). Its main +objectives are to correcte some shortcomings of [[EROS]], demonstrate that an +atomic kernel design scales well, and (eventually) to completely formally +verify both the kernel and critical system components by writing them in a new +language called [bitc](http://www.bitc-lang.org/). + +Coyotos is an orthogonally [[persistent|persistency]] pure [[capability]] +system. It uses [[continuation]]-based unbuffered asynchronous [[IPC]] +(actually it's synchronous [[IPC]] with asynchronous [[system calls]]). + +TODO: explain these terms and (more important) their consequences on system +design. + +The coyotos microkernel specification can be found +[here](http://www.coyotos.org/docs/ukernel/spec.html). diff --git a/microkernel/l4.mdwn b/microkernel/l4.mdwn new file mode 100644 index 00000000..970407be --- /dev/null +++ b/microkernel/l4.mdwn @@ -0,0 +1,21 @@ +[[!meta copyright="Copyright © 2004, 2006, 2007, 2008, 2010 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. + +There was a GNU/Hurd [[history/port_to_L4]], which is now stalled. |