[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Provably correct OS?
Dyke and all,
I glanced at it and it does look like our stuff...
"(persistent) object and access rights" looks like
"process and channels" ... device drivers are
implemented as processes (threads) ... the
periodic snapshots look like a high priority
(Transputer) process looking at low priority ones,
though it's not clear how they can deal with
ongoing interrrupts during the shot snapping...
kernel shares scheduler with user sounds like
user can do REAL PROGRAMMING in Ring 0 which
is a giant gap in current OS's.
Write an occam compiler for it, someone...?
On Oct 26, 3:31pm, Dyke Stiles wrote:
} Subject: Provably correct OS?
} Hi -
} Is anyone familiar with the EROS package? It claims to be for
} real-time systems, and some (at least) properties seem to have been
} verified formally.
} (It really isn't a porn site, but searching for EROS will get you
} Dyke Stiles >>>>>> new address!!>>> dyke.stiles@xxxxxxxxxxx
} Professor and Chair, Graduate Committee
} Department of Electrical and Computer Engineering
} 4120 Old Main Hill
} Utah State University
} Logan UT 84322-4120
} Voice: +1-435-797-2840 FAX: +1-435-797-3054
} Work: http://www.engineering.usu.edu/ece/research/rtpc/
} Play: http://www.engineering.usu.edu/ece/research/rtpc/utah/utah.html
}-- End of excerpt from Dyke Stiles