SPIN Operating System hamanaka 2001/06/20.

Slides:



Advertisements
Similar presentations
Webプロキシサーバにおける 動的資源管理方式の提案と実装
Advertisements

動画像品質調整機能を組み込んだ プロキシキャッシングシステムの 実装と評価
S. Tsuboi(1), H. Mizutani(1), N. Takeuchi(2) T. Arai (3), Y. Yanaka(3)
榮樂 英樹 LilyVM と仮想化技術 榮樂 英樹
Webサービスに関する基本用語 Masatoshi Ohishi / NAOJ & Sokendai
ポゼッションシステム: Javaによる 適応的アプリケーション環境
Windows Azure 仮想マシン 入門.
全体ミーティング (4/25) 村田雅之.
ASE 2011 Software Model Checking
COPPER/FINESSE System構築
データベース工学 データベースとは データモデル 関係データベースとSQL 物理データベース編成とインデクス
卒業研究テーマ ユビキタスネットワーク社会における 情報受取メディア選択を可能とする 電子書籍に関する研究
SSR 論文調査 Safety and Cyber-Physical Systems
2009年 3月 17日 法政大学 常盤祐司、児玉靖司、八名和夫、Ivan Ho、Billy Pham
ネットワーク構成法 スケール 第6回 11月19日.
Solid State Transformer (SST)
Object Group ANalizer Graduate School of Information Science and Technology, Osaka University OGAN visualizes representative interactions between a pair.
協調型システムアーキテクチャモデルの研究
研究背景 クラウドコンピューティングサービスの普及 マルチテナント方式を採用 データセンタの需要が増加
都市情報学専攻 情報基盤研究分野  M04UC513  藤田昭人
視覚的な分散アプリケーション 構築ツールuBlockの開発
Telnet, rlogin などの仮想端末 ftp などのファイル転送 rpc, nfs
コンピュータ ネットワークシステムトラック
ML 演習 第 7 回 新井淳也、中村宇佑、前田俊行 2011/05/31.
動画像ストリーミングサービスのための プロキシキャッシングシステムの 設計と実装および評価
UML入門 UML PRESS vol.1 より 時松誠治 2003年5月19日.
SAP & SQL Server テクニカルアーキテクチャ概要 マイクロソフト株式会社 SAP/Microsoft コンピテンスセンター
Provisioning on Multiple Network(NIC) env
Possible Damping Ring Timing
XSL-FO + MathML MathML表示、PDF生成、SVG生成
The new trend in PC/AT architecture
Solving Shape-Analysis Problems in Languages with Destructive Updating
サーバ負荷分散におけるOpenFlowを用いた省電力法
型付きアセンブリ言語を用いた安全なカーネル拡張
卒業論文に向けて(5) 学部4年生 島本 大輔 2004年12月14日.
大阪大学 大学院情報科学研究科 博士前期課程2年 宮原研究室 土居 聡
Lazy Release Consistency
プログラミング言語入門 手続き型言語としてのJava
映像配信サーバ入門 金山典世 稚内北星学園大学情報メディア学部
“Survey of System Virtualization Techniques” by Robert Rose のまとめ
識別子の命名支援を目的とした動詞-目的語関係の辞書構築
NTTPCCommunications,Inc. 波多浩昭
KMSF-CODEアーキテクチャ における動的QOS制御
プログラミング言語入門.
Java Operating Systems
Java Bytecode Modification and Applet Security
データベース工学 生研 戦略情報融合研究センタ 喜連川 優.
Javaプログラムの変更を支援する 影響波及解析システム
豊田正史(Masashi Toyoda) 福地健太郎(Kentarou Fukuchi)
端末およびサービス透過的な 情報閲覧支援システムの構築
ATLAS実験イベントビルダへの 品質保証機能の適用と性能評価
DS4000 EXP700 ESM ファームウエア更新手順 (ファームウエアレベル 9326)
Improvement of bootup time using Power Management - Project Update -
仮想ネットワークを考慮した SoftIRQ制御によるCPU割当ての手法
Peer-to-Peerシステムにおける動的な木構造の生成による検索の高速化
tranService Next Generation
iSeries Site 人事・給与C/S版のハードウェア・ソフトウェア要件
全体ミーティング (5/23) 村田雅之.
Type Systems and Programming Languages ; chapter 13 “Reference”
Mondriaan Memory Protection の調査
九州大学のキャンパスネットワークを事例にL1~L3を学ぶ Study on L1,L2 and L3 with case of Campus Network of Kyushu Univ. 岡村耕二 Koji OKAMURA.
卒業論文に向けて(3) 学部4年生 島本 大輔 2004年11月11日.
複雑度メトリクスを用いた JAVAプログラム品質特性の実験的評価
Microsoft Office Project Server 2007
回帰テストにおける実行系列の差分の効率的な検出手法
Cluster EG Face To Face meeting 3rd
全体ミーティング(9/15) 村田雅之.
L4-Linux のメモリ管理における問題点とその解決策
1.2 言語処理の諸観点 (1)言語処理の利用分野
Static Enforcement of Security with Types
Presentation transcript:

SPIN Operating System hamanaka 2001/06/20

SPIN Research Project SPIN は University of Washington で開発 様々な団体や企業が参画(資金提供など) DEC, ARPA, Intel, IBM, etc. 現在行われている research project Security for extensible systems Transaction Support Dynamic Compilation Unix Emulation Application-Controlled Caching Safe Programmable and Integrated Network Environment

構成 背景 用途 目標 & アプローチ SPINの構成 extension code The Core Systems 性能評価

背景 application のOSへの要求の多様化 cf. multimedia, database, network ⇒ application specific なインターフェース   (サービス)を動的に作成できるインフラがあると嬉しい

用途 Application-specific … inter-process communication virtual memory user-level scheduling network protocol file systems and buffer cache management etc.

SPINの目標 extensible, safe, efficient なOSの構築 user codeを動的にkernel内に install かつ flexibility, safety, efficiency は保つ

アプローチ language と runtime service の利点を利用 SPIN のよってたつ technique low-cost, fine-grained, protected access SPIN のよってたつ technique co-location enforced modularity logical protection domain dynamic call binding Modula-3 で実装 object-oriented, type-safe language

SPINの構成 extension services core system services dynamic linker など 機能拡張のための  枠組み core system services memory accessなど 最も基本的なサービス extension service core system service extension code dynamic linker verifier kernel

application の形態 すべて user space すべて kernel space core system service extension code application 1. 2. 3.

The Extension Services system code と user code を安全に結びつける ソフトウェアインフラを提供 次の2つのモデル Protection Model efficient, fine grained access control of resources Extension Model extension definable at Procedure Call granularity language-level service, static type checking, dynamic linking で実現

<Protection Model> extension code ごとのaccess control機構 language level で実現 virtual memory system ではない 用語(概念) capability protection domain core system service extension code kernel

capability resource への pointer language level の pointer で実装 core system service extension code resource への pointer ここで resource は a system object an interface a collection of interface language level の pointer で実装 user-level への受け渡し可 externalized reference (別紙参照) application capability externalized capability 1 2 kernel

protection domain codeから参照される(可能な)名前の集合 symbolic table のようなもの kernel 名前: program symbols domain 外の名前にはアクセス不可 can be intersecting or disjoint (capability による参照される) obj inter2 inter1 inter1 ext2 ext1 ext2 obj inter1 inter2 kernel

protection domainの操作 Create: object file から作成 CreateFromModule:   現在のmoduleから作成 Resolve:       domain中の名前と実体を関連付け Combine:      domain の union 作成 (別紙参照) obj inter2 inter1 inter1 ext2 inter1 ext1 ext2 obj inter1 inter2 kernel

export and import of domain in-kernel nameserver へ登録 明示的に domain を export authorizer も登録可 Module間の直接渡し domain は capability で参照

<Extensional Model> System提供のサービス変更機構 概要 event & handlerによる拡張の定義 dispatcher で event に対し handlerを登録 条件実行のために guardを利用 access control のために authority利用 (別紙参照)

Event 本来はSystemからのメッセージ SPIN では event は procedure signature で定義 event raise は procedure call に相当 ⇒ procedure call の粒度でサービスを提供

Handler event raiseに応じて実行されるprocedure 拡張サービスの実体 event と同じ型 event に対して dispatcher で登録 一つのeventに対して複数登録可 intrinsic handler: event と同名の handlerで必ず実行される

Guard handler に関連付けられるpredicate filter の役割 handler の実行前に評価 true: handler を実行 false: handler を無視 一つのhandlerに対して複数登録可 引数の型はeventと同じ: 返り値は boolean guard 内で副作用不可

Authority intrinsic handler を定義する module event に対する access control を行う dispatcher による authorizer の登録 handler の install, 実行 を制御 handler へ 新たな guard の不可

Dispatcher handler 実行のコア部分 runtime code generation で最適化 handler一つかつsynchronous: event raise == procedure call handler の inline化など

その他 handler 実行のordering可 複数 handler の場合の返り値 決定機構をもつ First, Last, Next, After で明示的に指定 複数 handler の場合の返り値 result handler が決定

その他 handler の実行は次の2パターン handlerが多すぎる場合 asynchronous synchronous with time limitation 後者は “EPHEMERAL” のannotationを付加 handlerが多すぎる場合 メモリ使用量膨大 対応は future work

The Core Services 以上は拡張codeを扱う枠組みの話 いくつかの core serviceを用意 memory management thread management これらを利用してapplication特化の機能を実現

memory management 3つのコンポーネントに分解 これらを用いて様々な実装可 physical storage naming translation  (別紙参照) これらを用いて様々な実装可 UNIX address space semantics を実装

thread management SPINでは “strand” を実装 これを用いて Thread Package 作成可 (別紙参照) DEC OSF/1 kernel thread Mach C-Threads Modula-3 thread

性能評価 次の4つの点に注目 System size Microbenchmarks Netwoking End-to-end performance

性能評価 環境: DEC Alpha 133MHz XAP 3000/400 workstations, each machine 64 MBs of memory, 512KB unified external cache, HP C2247-300 1GB disk-drive, 10Mb/sec Lance Ethernet interface, FORE TCA-100 155Mb/sec ATM adapter card connected to FORE ASX-200 switch.

System size (別紙参照) sys : extensibility machinery, domains, naming, linking, dispatching core : virtual memory and scheduling rt : DEC SRC Modula-3 runtime lib : subset of Modula-3 library and mundane data structures sal : low level interface of device drivers and MMU.

Microbenchmarks (別紙参照) Protected communication Thread management Virtual memory SPINの優位性 kernel extension(Translation.ProtectionFault)の利用 一連のinteractionがapplicationに高速に反映

Networking (別紙参照) Latency and Bandwidth Protocol forwarding

End-to-end performance (別紙参照) Video Streaming Server-Client Server: 3つの拡張 Client: 1つの拡張

Extension size (別紙参照) 機能が複雑になるにつれsizeも増大

まとめ SPIN operating systemは 機能拡張のための効率的な機構 および 拡張可能な機能の core set を提供 extensible かつ safe かつ good performance を達成

Reference(1/2) “Extensibility, Safety and Performance in the SPIN Operating System”, Brian Bershad, Stefan Savage, Przemyslaw Pardyak, Emin Gun Sirer, David Becker, Marc Fiuczynski, Craig Chambers, Susan Eggers, in Proceedings of the 15th ACM Symposium on Operating System Principles (SOSP-15), Copper Mountain, CO. pp. 267--284. “Dynamic Binding for an Extensible System”, Przemyslaw Pardyak, Brian Bershad, in Proceedings of the Second USENIX Symposium on Operating Systems Design and Implementation (OSDI), Seattle, WA, pp. 201-212, October 1996.

Reference(2/2) “Safe Dynamic Linking in an Extensible Operating System” , Emin Gun Sirer, Marc Fiuczynski, Przemyslaw Pardyak, Brian Bershad, Appeared in the Workshop on Compiler Support for System Software, February 1996. “SPIN - An Extensible Microkernel for Application-specific Operating System Services”, Brian Bershad, Craig Chambers, Susan Eggers, Chris Maeda, Dylan McNamee, Przemyslaw Pardyak, Stefan Savage, Emin Gun Sirer, University of Washington, Technical Report TR-94-03-03.

自分の研究との絡み