Skip to content

SPIN

Jump to bottom Edit New page
oraccha edited this page Jan 14, 2013 · 1 revision

カーネルの拡張にModula-3という型安全な言語を使うことで，コンパイル，リンク時に安全性を保証しようという研究プロジェクト．

  • [http://www.cs.washington.edu/research/projects/spin/www/ 本家]

例えば，アプリケーションやデータのアクセスパターンに応じてページングポリシをカスタマイズするなどということが可能になる．

  • 似た機構としてMach，Chorus，Springなどの外部ページャがあるが，これらはアプリケーションごとにページングポリシを変えられなかったはず．

Modula-3ってマニアックな言語に制限されるのもちょっと．もちろんUnixなど大半のOSはCに制約を受ける訳だけど．

単一言語でシステムを構築するという話ならXeroxのWS JStarのOSであるPilotやCMUのHYDRAがありますね．Lispマシン，Prologマシンも．

  • MLベースのFoxNet．
  • IRISAの[http://www.irisa.fr/compose/ COMPOSE]プロジェクトでもDSL(Domain Specific Language)によるシステムプログラミングの研究が行われているらしい．
  • Javaを使ったアプローチとしてSafeLanguageKernelプロジェクトなどがある．

関連研究として，ネットワークを介してSPINカーネルに拡張コードを追加するPlexusがある．

論文

Brian Bershad, Stefan Savage, Przemyslaw Pardyak, Emin Gun Sirer, David Becker, Marc Fiuczynski, Craig Chambers, Susan Eggers, Extensibility, Safety and Performance in the SPIN Operating System, In Proceedings of 15th ACM SOSP, pp.267-284, 1995. ([http://citeseer.nj.nec.com/bershad95extensibility.html ResearchIndex])

並列プログラムのモデルチェッカ．

Promela という専用言語で書かれたプログラムを実行して安全性を検証する．

  • [http://spinroot.com/spin/whatispin.html ON-THE-FLY, LTL MODEL CHECKING with SPIN]

    • [http://www.asahi-net.or.jp/~hs7m-kwgc/spin/Man/Manual_japanese.html Basic Spin Manual(翻訳)]

  • [http://plan9.bell-labs.com/sys/doc/spin.html Using SPIN]

  • [http://swtch.com/spin/ Spin & Plan 9]

  • [http://nicosia.is.s.u-tokyo.ac.jp/pub/staff/hagiya/kougiroku/vs/spin-etc.txt Spinを使ってみる] . 萩谷先生．

  • [http://www002.upp.so-net.ne.jp/mamewo/spin.html Spin] . 増山隆さんのメモ．

  • [http://truelogic.jp/ TrueLogic, Inc.]

  • [http://anna.fi.muni.cz/divine/ DiVinE]

Add a custom footer
Add a custom sidebar
Clone this wiki locally