#
CbCXV6上の状態遷移ベースでのプロトコルの実装
#
研究目的
- 検証を利用して信頼性を確保するGearsOSを開発中
- xv6をベースにGearsOSの実装が進んでいる
- 現在のOSに欠かせないネットワーク通信/USBなどのプロトコルを高信頼性で実装したい
- プロコトルは巨大な状態遷移マシンと捉えると、CbC/Gearsでの記述に適している
- 実際にxv6上にCbCベースでプロトコルを実装し、検証可能かどうかを試作する
#
やったこと
- LLVMのバグ撮り
- growi backup関連の調査など
- シス管issue関連
- OS研究会のネタ決め
- 雑誌執筆
#
OS研究会
- タイトルと概要考えました
- 証明に適した実装と実装に適した実装を切り替えるところまで書くべき?
- とはいえ証明に適した実装が何なのかが怪しい気がする
#
title
「継続を中心とした言語によるxv6のモジュール化」
「xv6の構成要素の継続の分析」
#
概要
OS自体そのものは高い信頼性が求められるが、 OSを構成するすべての処理をテストするのは困難である。
テストを利用して信頼性を高めるのではなく、 OSの状態を状態遷移を基本としたモデルに変換し形式手法を用いて信頼性を高めたい。
状態遷移単位での記述に適した言語であるCbCを用いて、小さなunixであるxv6 kernelの書き換えを行う。
この際に、すべてのOSの処理を状態遷移単位での記述を行うと、プログラミングする上での実装が煩雑になってしまう。
そこで状態遷移の集合をモジュール化することで拡張性を保証、かつ実装が簡易化されるInterfaceを導入した。
本稿ではxv6kernelに導入したCbCInterfaceの解説及び、 xv6 kernelへの実装について述べる。
#
Pintos
#
LLVM
#
TailCallElim
- 先週はTailCallElimをPassに加える際の型が異なっておりコンパイルできなかった
1
2
3
4
5
6
7
8
9
10
11
12
|
/// The indirect function call promotion pass.
class PGOIndirectCallPromotion : public PassInfoMixin<PGOIndirectCallPromotion> {
public:
PGOIndirectCallPromotion(bool IsInLTO = false, bool SamplePGO = false)
: InLTO(IsInLTO), SamplePGO(SamplePGO) {}
PreservedAnalyses run(Module &M, ModuleAnalysisManager &AM);
private:
bool InLTO;
bool SamplePGO;
};
|
llvm/include/llvm/Transforms/Scalar/TailRecursionElimination.hな方
1
2
3
4
|
struct TailCallElimPass : PassInfoMixin<TailCallElimPass> {
PreservedAnalyses run(Function &F, FunctionAnalysisManager &AM);
};
}
|
- passの追加は2種類の追加の方法があるらしい
- 今の所使われているものがこの2種類
- コンパイル時に
runの型がどうのこうの言われた場合、この追加の方法が逆になっているらしい
1
2
|
FPM.addPass(TailCallElimPass());
PM.add(createTailCallEliminationPass(true));
|
#
現状
- OptLevelが関係している部分を修正して回っているが、効果がない
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
|
--- a/clang/lib/CodeGen/BackendUtil.cpp Tue Apr 14 15:43:20 2020 +0900
+++ b/clang/lib/CodeGen/BackendUtil.cpp Tue Apr 14 17:43:32 2020 +0900
@@ -315,6 +315,10 @@
PM.add(createGVNPass());
PM.add(createInstructionCombiningPass());
PM.add(createDeadStoreEliminationPass());
+#ifndef noCbC
+ } else {
+ PM.add(createTailCallEliminationPass(true));
+#endif
}
}
diff -r 980e56f2e095 llvm/lib/Passes/PassBuilder.cpp
--- a/llvm/lib/Passes/PassBuilder.cpp Tue Apr 14 15:43:20 2020 +0900
+++ b/llvm/lib/Passes/PassBuilder.cpp Tue Apr 14 17:43:32 2020 +0900
@@ -451,7 +451,6 @@
// TODO: Investigate the cost/benefit of tail call elimination on debugging.
#ifndef noCbC
- FPM.addPass(SROA());
FPM.addPass(TailCallElimPass());
#else
if (Level.getSpeedupLevel() > 1)
@@ -610,6 +609,9 @@
FPM.addPass(EarlyCSEPass()); // Catch trivial redundancies.
FPM.addPass(SimplifyCFGPass()); // Merge & remove basic blocks.
FPM.addPass(InstCombinePass()); // Combine silly sequences.
+#ifndef noCbC
+ FPM.addPass(TailCallElimPass());
+#endif
invokePeepholeEPCallbacks(FPM, Level);
CGPipeline.addPass(createCGSCCToFunctionPassAdaptor(std::move(FPM)));
@@ -1161,8 +1163,15 @@
MPM.addPass(LowerTypeTestsPass(nullptr, ImportSummary));
}
- if (Level == OptimizationLevel::O0)
+ if (Level == OptimizationLevel::O0) {
+#ifndef noCbC
+ FunctionPassManager FPM(DebugLogging);
+ FPM.addPass(TailCallElimPass());
+ MPM.addPass(createModuleToFunctionPassAdaptor(std::move(FPM)));
+ MPM.addPass(ForceFunctionAttrsPass());
+#endif
return MPM;
+ }
|
TailCallElimPass()の追加でない可能性が存在している気がする- 具体的なPassの種類の特定はまだできていない
- 以前発見したPassの一覧を出すコマンドはあまり効果が無かったような…
#
growi backup
- 一応web越しでbackupはできるが、コマンドベースでgrowiの階層に則ってmarkdownを撮りたい
- APIを実際に叩いて検証してみたところ、publicなエントリはダウンロードできる
- 公開範囲が設定されているエントリはダウンロードできないらしい
- backupツール書くならpublicなものという制約は付きそう
- 使ってるの僕とryokkaさんの修論とかくらいだからまぁ…
- 元気があるときにぼちぼち
#
minio
- mattermostの外部ファイルを逃がす目的でいれたs3互換なオブジェクトストレージ
- golangで書かれている
- 元気に今の頃動いている
- ユーザーからは次の順で外部ファイルにアクセスがいく
- mattermostのAPIに対してアクセス
- mattermost側がDBからminioのオブジェクトを特定
- mattermostがminioのオブジェクトgetしてユーザーにかえしている
- その為一般ユーザーからはminioの存在が認知できない
#
時間割スクリプト
- コロナ騒ぎでシラバスに更新があるケースがあるらしく、 時間割のhtmlを取得するとこをサブコマンド化した
- goroutineで取得する
- 爆速すぎるのでsleepをしたほうが良いのではという気がしている