From tjoccam@crash.cts.com Sun Oct 31 15:49:05 2004 From: Lawrence Dickson To: dyke.stiles@helios.ece.usu.edu, occam , Java Threads Date: Thu, 26 Oct 2000 15:20:30 -0700 Subject: Re: Provably correct OS? X-Mailer: Mail User's Shell (7.2.6 1995-03-03) Message-ID: <200010262220.PAA23842@cts.com> 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@ece.usu.edu } 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