Re: Provably correct OS?

[tjoccam@xxxxxxxxxxxxx (Lawrence Dickson)]

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...?
Larry Dickson
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.
} 
} http://www.eros-os.org/
} 
} (It really isn't a porn site, but searching for EROS will get you
} several...)
} 
} Dyke.
} 
} -- 
} ======================================================================
} 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