研究目的

CbC

GearsOSについて

Christie

UnixのFilesystem

GearsFileSystemのディレクトリ

ファイル構造

WordCount

考察

参考文献

付録

GearsOSとは

ファイルシステム未実装

GearsOSのファイルシステム設計

取り入れたい要素

簡単な説明

Code Gear

Data Gear

normal level

meta level

継続性

GearsOSとは

Context

stub

Christieとは

DataGearManager

topology manager

xv6

inode

Treeによるディレクトリ構造(図などでここ詳しく)

Unix Like

非破壊的編集によるBackUp

構成

APIの設計に用いる

機能

GearBox的に処理する

現状

今後の課題

信頼性について

一木さん

アナグラさん

parusuさん

xv6

mindmap

gearsDirectory source

信頼性と拡張性

ノーマルレベルメタレベルの分離

だがOSにおいて重要な機能である

基幹となるディレクトリシステム

ファイル構造

API設計中

backup

log

Cの下位言語

関数呼び出しの代わりに継続を用いる

環境を持たない

関数型言語のtail callスタイルにあたるプログラミング

関数の代わり

_codeで宣言を行う

Input/Output DG

user

kernel

goto

軽量継続

信頼性の保証が目的

全てのCG, DGを参照できるMetaDG

従来OSのプロセスに相当

種類

Context参照の流れ

並列分散通信フレームワーク

CbCとは異なるGearの概念

DGを管理している

key value store

Fileとして用いる

LocalDGMとRemoteDGM

任意のtopologyを生成することができる

分散プログラムを簡潔に書くために必要

静的topology

動的topology

MITで教育用の目的で開発されたOS

Unixの基本構造を持つ

filesystem

CbCによるxv6の書き換えが行われた

RedBlackTree

2つの木を用いる

mkdir

cd

ls

バックアップ機能をOS自体に持たせたいという目的

GearsOSにおける永続データ

I/O stream

logによるバージョン管理

ファイルの中身を読み取り

Unix Fileに対して行う

中間報告の時の図

一木さん図5

File操作の仕組み

GearBoxとは

実装できた部分

課題

分散ファイルシステム

信頼性

shell

path

モデル検査

定理証明

一木 貴裕 ，河野 真治(琉球大学), 情報処理学会システムソフトウェアとオペレーティング・システム研究会(OS), May, 2021

Papers/2020/anatofuz-sigos/

信頼性

Cとの違いは

継続とは

環境とは

tail call スタイルとは

末尾再帰とも言う

jmp命令を用いる

引数付き

普通のgotoと違うところは

環境を持たない

関数呼び出し(call)せず、jmpする

モデル検査

ノーマルレベルメタレベル切り分けがされている

normalレベルのCGから直接参照してしまうとメタレベルを切り分けた意味がなくなってしまう

Metaなのでnormalから直接参照しない

必ずMetaCGから参照される

CodeGearはDataGearの一種であるからMetaDGにMetaCGの参照を入れることが可能

CGとDGの接続に用いられる

UserプロセスにあたるUser Contextが存在する

Kernel Context

User Context

CPU Context

CGがOutputDataGearへデータをoutput

次のCGのstubCodeGearへgoto

stubCGはinputDataGear(前のCGのoutputDG)とOutputDGを参照

CGへgoto

OutputDGへOutput

次のstubCodeGearへgoto

DataGear

CodeGear

CGMが利用するCGのkeyとputされたDG(value)の組み合わせをもつ

LocalはCGM自身が所持するDGのプール

RemoteはCGMが配線されている別のCGMがもつDGのプール

topologyのノードはCGM

ノード同士の通信接続を管理

任意のtopologyとノードの配線ができる

dotファイルに記述し，TopologyManagerに参照させる

dotファイルに記述したノードの数と参加ノードの数が一致した場合に動作する

参加を表明したノードに対し，自動的に配線を行う

inode

DataGearManagerを格納してFileSystemに

API

inumとfile pointer

inumとfilename

filenameのlistを入れることでlsのリスト表示を実装できる

木構造を用いる

ルートノードから変更ノードまでのパスを全てコピー

コピーしたパス上に存在しないノードはコピー元の木構造と共有

keyで参照

競合的アクセス

3つのQueue

git mercurial的

文字数

行数

GearsOSの機能を表現する手法

状態遷移図とクラスダイアグラムを組み合わせたような図

RBTreeの動作test(予定)

GearsOSへのtopologyManagerの実装

ディレクトリ構造の作成

GearsAgda

モデル検査

RedBlackTreeのモデル検査

モデル検査

定理証明

プログラムが実行される際、その出力に影響を与える変数やデータのこと

必要なデータは毎回inputする

処理はcallよりjmpが軽量

OS上の全てのContextを参照できる

ユーザーごとに存在する

実行しているCPUやGPUごとに存在する

atomic

put

get

remove

key: inum

value: file pointer

key: filename

value: inum

RedBlackTree

synchronizedQueue

input

output

main

input -> main -> output のような繋がり

queueの中身は共通してelement

これらのQueueはkeyとペアになっており，keyで参照することができる．

継続性

agda

parusuさんの論文

データをinputしたい場合にこのQueueにput

データを取得したい場合にこのQueueからtake

データそのもの

elementとは

Synchronized QueueかSingleLinkedQueueを選べる