summaryrefslogtreecommitdiff
path: root/microkernel/coyotos.mdwn
blob: fec023bac36e0567a85c7f8253355c005ee4a537 (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
[[!meta copyright="Copyright © 2006, 2007, 2008, 2010, 2011 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).

There once was the idea of a GNU/Hurd [[port using the Coyotos
microkernel|history/port_to_another_microkernel]], but this didn't come live.