Mercurial > hg > Papers > 2020 > anatofuz-sigos

comparison paper/anatofuz-sigos.md @ 12:60693eee5ee3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
update
author anatofuz <anatofuz@cr.ie.u-ryukyu.ac.jp>
date Thu, 30 Apr 2020 19:19:08 +0900
parents 1e8d8d32fe30
children cce07a6da420
comparison
equal deleted inserted replaced
11:1e8d8d32fe30 12:60693eee5ee3
17 実装のソースコードと検証用のソースコードは近いセマンティクスでプログラミングする必要がある。 17 実装のソースコードと検証用のソースコードは近いセマンティクスでプログラミングする必要がある。
18 18
19 実装用の言語と証明用の言語の両方に適した言語としてContinuation Based C(CbC)がある。 19 実装用の言語と証明用の言語の両方に適した言語としてContinuation Based C(CbC)がある。
20 CbCはCと互換性のあるCの下位言語であり、 状態遷移をベースとした記述に適したプログラミング言語である。 20 CbCはCと互換性のあるCの下位言語であり、 状態遷移をベースとした記述に適したプログラミング言語である。
21 Cとの互換性のために、 CbCのプログラムをコンパイルすることで動作可能なバイナリに変換が可能である。 21 Cとの互換性のために、 CbCのプログラムをコンパイルすることで動作可能なバイナリに変換が可能である。
22 すなわちCbCを用いて状態遷移を基本とした単位でプログラミングをすると、 形式手法で証明が可能かつ実際に動作するコードをプログラミングできる。 22 すなわちCbCを用いて状態遷移を基本とした単位でプログラミングをすると、 形式手法で証明が可能かつ実際に動作するコードを記述できる。
23 23
24 現在小さなunixであるxv6 kernelをCbCを用いて再実装している。 24 現在小さなunixであるxv6 kernelをCbCを用いて再実装している。
25 再実装の為には、 既存のxv6 kernelの処理の状態遷移を分析し、継続を用いたプログラムに変換していく必要がある。 25 再実装の為には、 既存のxv6 kernelの処理の状態遷移を分析し、継続を用いたプログラムに変換していく必要がある。
26 本論文ではこの書き換えに伴って得られたxv6 kernelの継続を分析し、 現在のCbCによる書き換えについて述べる。 26 本論文ではこの書き換えに伴って得られたxv6 kernelの継続を分析し、 現在のCbCによる書き換えについて述べる。
27 27
28 # xv6 kernel
28 29
30 xv6とはマサチューセッツ工科大学でv6 OSを元に開発された教育用のUNIX OSである。
31 xv6はANSI Cで実装されており、 x86アーキテクチャ上で動作する。
32 Raspberry Pi上での動作を目的としたARMアーキテクチャのバージョンも存在する。
33 本論文では最終的にRaspberry Pi上での動作を目指しているために、 ARMアーキテクチャ上で動作するxv6を扱う。
34
35 xv6は小規模なOSだがファイルシステム、 プロセス、システムコールなどのUNIXの基本的な機能を持つ。
36 またユーザー空間とカーネル空間が分離されており、 シェルやlsなどのユーザーコマンドも存在する。
37
38 本論文ではxv6のファイルシステム関連の内部処理と、システムコール実行時に実行される処理について分析を行う。
39 xv6 kernelのファイルシステムは階層構造で表現されており、 最も低レベルなものにディスク階層、 抽象度が最も高いレベルのものにファイルディスクリプタがある。