DEV Community: YT

形式手法の話

YT — Fri, 30 Jul 2021 15:46:14 +0000

背景

社内で形式手法の勉強会が行われた。このリンクの内容。全3回のうちの第1回らしい。
形式手法は知ってはいたけど、非常にコストが高く実務的ではないという認識だった。この勉強会は、クラウドなど産業界で実際に使われている事例を紹介して、興味を持つことを目指しているようだった。

勉強会のスライドを読み進めると、上記リンク中の参考資料1「Amazon Web Services はどのように形式手法を利用したか」を読むよう記載されており、読んでみると非常に興味深いものだった。
勉強会第一回の内容と合わせて、面白いと思ったところをまとめてみる。

AWSでの形式手法の利用

報道されるような重要なシステムでの大規模障害の原因は様々で、対処方法も複数ある。
仕様の誤りに形式手法で対応できれば、正確な仕様を元にした実装とテストができ、障害を防ぐことができる。
障害発生後の原因は調査しやすいが、障害発生前に防ぐことは難しい。形式手法ならそれができる。
クラウドのような大規模かつ複雑な並列・分散システムでは、ハードウェアや人間のエラーも想定しなければならない。このような複雑な仕様を、検証可能で表現力のある形式手法で取り扱うことが必要となっている。

形式手法で検証可能な仕様が記載されれば、そこから実装を生成することもできるかもしれない。その場合、実装する人間は仕事が少なくなるかもしれない。
しかし、仕様を作成する仕事は創造性が求められ、これは人間にしかできない。

Amazon Web Services はどのように形式手法を利用したか

形式手法ではない、業界で一般的な方法では、大規模分散システムのレアケースを未然に発見することはできなかった。
この問題を解決することを目標として、代替手段を探し始めた。

複雑な仕様を厳密に記述しつつ、記述量を抑制するソリューションとして、TLA+を見出した。
TLA+は離散数学に基づいた形式的仕様記述言語で、モデルチェッカーはもちろん、疑似コードを置き換える表現力を持つPlusCal言語を備えている。

設計にTLA+を使うことの副次的な利点として、人間の設計手法を向上させることがある。
TLAによらない既存の手法では、まずビジネス要求に応える最短のハッピーケースを設計し、その後でエンジニア個人の知識と経験に基づき問題点の検討を行う。この場合、能力を超える複雑な問題を見つけることはできない。
TLA+の場合はまず「正しく進むには何が必要か」というシステム特性を、安全性と生存性の観点から記述することから始まる。次に、ハードウェアの異常や人間のミスなど、起こりうる動的イベントを特定する。その後、モデルチェッカーで仕様の正しさを確認する。
前者は「うまくいかないもの」をアドホックに見つけ、後者は「正しく進むために必要なもの」を厳密に特定する。

形式手法はまた、仕様が安全であること、または安全ではないことを、事前に知ることができる。
さらに、優れたドキュメントとして機能する。

さらに、設計の正確でテスト可能な、十分にコメントされた記述は、優れた形式のドキュメントである。というのも、AWS システムのライフタイムには期限がないため、このことは、重要である。
時間が経過し、ビジネスの成⻑とともにチームも成⻑する。そのため、我々は定期的に新しい人々をシステムに慣れさせる必要がある。この教育は効果的でなければならない。微妙なバグを作らないようにするには、すべてのエンジニアがシステムの同じメンタルモデルを持つことが必要なのだが、その共有モデルは、精密で正確で完全である必要がある。
エンジニアはさまざまな方法でメンタルモデルを形成する。互いに話し合ったり、設計ドキュメントを読んだり、コードを読んだり、バグ修正や小さな機能を実装したりする。しかし、会話や設計のドキュメントはあいまいであったり不完全であったりする。実行可能コードが大きすぎてすぐに理解できなかったり、あるいはそのコードは意図したデザインを正確に反映していない場合があるのだ。対照的に、形式仕様は、正確で短く、ツールを使用して調査や実験ができる。

TLA+に向いていないこともある。AWSのインフラはハード・リアルタイムスケジューリングをサポートしておらず、サービスに対しては一定以上の遅延をエラーとみなすソフト・リアルタイムスケジューリングが要求されている。
TLA+では安全上の特性として応答時間の上限を設定できるが、このギャップを埋めるには至っていない。

AWSでの形式手法の導入経緯

バグを防ぐ手法を模索する上で、形式手法はROIが低いという偏見があり、当初は検討されていなかった。
ある時、形式手法言語Alloyによって分散システムのメンバーシップ・プロトコルChordの不具合を見つけたことで、有用性を認識した。
Allowの表現力不足を解決する方法を模索していた際、LamportのFast Paxos論文のAppendixにTLA+仕様が記載されていることを見つけた。
Paxosアルゴリズム作成者がTLA+を作ったという事実は、TLA+の実用性を確信させるものだった。

Lamport, L. Fast Paxos. Distrib. Comput. 19, 79–103 (2006). https://doi.org/10.1007/s00446-006-0005-x
※自分は論文へのアクセス権を持っていないので未確認

発見者はAmazonの同僚にTLA+を薦めたが、必要性がなく導入はされなかった。
しかしDynamoDBで採用され、TLA＋の学習と仕様記述を2週間で行い、8Coreと23GBのEC2インスタンス10台でモデルチェッカーの分散バージョンを実行して、データが失われるバグを発見した。
このDynamoDBでの成功と、社内へのプレゼンテーションの工夫によって、TLA+を伝える試みを改善させた。

エンジニアは「検証」ではなくデバッグの観点から考えるため、プレゼンテーションでは「設計のデバッグ」と呼んだ[18]。こうしたメタファーを続けながら、エンジニアは、「徹底的にテスト可能な疑似コード」と呼ぶと、TLA+の概念と実用的な価値をより簡単に把握できることに気づいた。形式手法は実践的ではないと広く見られていたため、最初は「形式」、「検証」、「証明」という言葉を使うのを避けた。また、我々は、最初に TLA が何を表すのかについて言及することは避けた。

このような活動によって、S3のチームから導入サポートの依頼があった。

結果として、2011年から現在に至るまで、AWSでは形式手法が用いられている。

Rustで自作OS 6日目

YT — Sun, 11 Jul 2021 09:15:01 +0000

引き続き第3章 boot loaderを進める。
https://os.phil-opp.com/ja/minimal-rust-kernel/#kaneruwoshi-xing-suru
bootloader crateというものがあるらしいけど、まずは自作を試みる。
でも参考にはする。

私達のカーネルをELFファイルにコンパイルする。
依存であるbootloaderをスタンドアロンの実行ファイルとしてコンパイルする。
カーネルのELFファイルのバイト列をブートローダーにリンクする。

たぶんリンクはlld、それ以外はcargo(rustc)で進める。

まずはELF形式のカーネルをビルドする。
ビルド設定をtarget.jsonとして作成する。

{
  "llvm-target": "x86_64-unknown-none",
  "data-layout": "e-m:e-i64:64-f80:128-n8:16:32:64-S128",
  "arch": "x86_64",
  "target-endian": "little",
  "target-pointer-width": "64",
  "target-c-int-width": "32",
  "os": "none",
  "executables": true,
  "linker-flavor": "ld.lld",
  "linker": "rust-lld",
  "panic-strategy": "abort",
  "disable-redzone": true,
  "features": "-mmx,-sse,+soft-float",
  "exe-suffix": ".elf"
}

コマンド build --target target.json --package kernel --bin kernel でビルドできる。
macOSの場合、binutilsのgreadelfでバイナリを確認できる。

$ brew install binutils
$ /usr/local/Cellar/binutils/2.36.1/bin/greadelf -h ../target/target/debug/kernel.elf
ELF Header:
  Magic:   7f 45 4c 46 02 01 01 00 00 00 00 00 00 00 00 00 
  Class:                             ELF64
  Data:                              2's complement, little endian
  Version:                           1 (current)
  OS/ABI:                            UNIX - System V
  ABI Version:                       0
  Type:                              EXEC (Executable file)
  Machine:                           Advanced Micro Devices X86-64
  Version:                           0x1
  Entry point address:               0x201120
  Start of program headers:          64 (bytes into file)
  Start of section headers:          4472 (bytes into file)
  Flags:                             0x0
  Size of this header:               64 (bytes)
  Size of program headers:           56 (bytes)
  Number of program headers:         4
  Size of section headers:           64 (bytes)
  Number of section headers:         15
  Section header string table index: 13

Entry point addressが自作OS本とは合っていないが、とりあえずboot loaderにカーネルを読み込む処理を実装する。

調べてたら先駆者を見つけた。
https://natsutan.hatenablog.com/entry/2021/04/14/190451
この人はCのUEFIアプリからRustのカーネルを読んでいるようだけど、自分は全部Rustでやってみたい。

上記ブログの参考ブログは全部Rustでやってた。
https://www.akiradeveloper.com/post/mikanos-rust/

このカーネルファイルは、0x100000に配置されるようにビルドされているため、 UEFIによってアドレス指定方式でページをアロケートして、そこに書きます。

これが全てっぽい。

自作OS本と https://github.com/akiradeveloper/MikanOS.rs/blob/master/boot/src/main.rs を見ながら進める。

一通り書いた時点で起動してみると、QEMUがpanicした。

ディレクトリ構成を修正すると、panicせず起動できたようだ。

今日の進捗 -> https://github.com/ytannai/kabos/tree/8e5091cbb471ca660dab44091051d79d692692c2

Rustで自作OS 5日目

YT — Tue, 06 Jul 2021 14:40:48 +0000

昨日に引き続き第3章 boot loader。なんとか今日こそ起動したい。
昨日見たブログの次の章を読んでいく。
https://os.phil-opp.com/ja/minimal-rust-kernel/

しかしながら、私達のターゲットシステムには、いくつか特殊な設定パラメータが必要になります（例えば、その下ではOSが走っていない、など）。なので、既存のtarget tripleはどれも当てはまりません。ありがたいことに、RustではJSONファイルを使って独自のターゲットを定義できます。

サンプルにあったJSONはカスタムターゲットの設定ファイルだった。どうりでtarget tripleに無いはずだ。
kernelにも同じJSONを配置して試してみる。

そもそもELFの知識が足りな気がするので、ブログと自作OS本を読み進める。

カスタムターゲットの指定方法がわからなかったんだけど、--targetオプションに規定のtarget tripleではなく、JSONファイル名（おそらくパス）を設定すれば良いらしい。

cargo build --target x86_64-none-elf.json --package kernel --bin kernel

あんまり関係ないけど、SIMDのデメリットが載ってて参考になった。Apache ArrowとかSIMDちょっと興味あったので。

しかし、大きなSIMDレジスタをOSカーネルで使うことは性能上の問題に繋がります。その理由は、カーネルは、割り込まれたプログラムを再開する前に、すべてのレジスタを元に戻さないといけないためです。これは、カーネルがSIMDの状態のすべてを、システムコールやハードウェア割り込みがあるたびにメインメモリに保存しないといけないということを意味します。

話はkernelに戻って、やっとcore見つからないエラーが出たので、ブログの通りbuild-std設定を入れて進める。

ブログだとUEFIについて描いてないし、ELFじゃないので、ここを自作OS本と合わせる必要がありそう。

Rustで自作OS 4日目

YT — Mon, 05 Jul 2021 14:48:02 +0000

第3章 boot loaderをやっていく。まずはデバッグで使うQEMU Monitorの有効化。起動時のオプションに-monitor stdioをつければ、プロンプトが返ってきて操作ができる。

QEMU 5.2.0 monitor - type 'help' for more information
(qemu) info registers
iininfinfoinfo info rinfo reinfo reginfo regiinfo regisinfo registinfo registeinfo registerinfo registers
RAX=0000000000000000 RBX=0000000000000000 RCX=0000000000000000 RDX=0000000007ed5e20
RSI=0000000007233018 RDI=0000000007233018 RBP=0000000007234418 RSP=0000000007ec1360
R8 =0000000006211630 R9 =0000000000001000 R10=0000000007e00000 R11=0000000007ed6ea0
R12=0000000007ec1588 R13=0000000007ec1598 R14=0000000007ec1708 R15=0000000000000000
RIP=000000000620f72f RFL=00000202 [-------] CPL=0 II=0 A20=1 SMM=0 HLT=0
ES =0030 0000000000000000 ffffffff 00cf9300 DPL=0 DS   [-WA]
CS =0038 0000000000000000 ffffffff 00af9a00 DPL=0 CS64 [-R-]
SS =0030 0000000000000000 ffffffff 00cf9300 DPL=0 DS   [-WA]
DS =0030 0000000000000000 ffffffff 00cf9300 DPL=0 DS   [-WA]
FS =0030 0000000000000000 ffffffff 00cf9300 DPL=0 DS   [-WA]
GS =0030 0000000000000000 ffffffff 00cf9300 DPL=0 DS   [-WA]
LDT=0000 0000000000000000 0000ffff 00008200 DPL=0 LDT
TR =0000 0000000000000000 0000ffff 00008b00 DPL=0 TSS64-busy
GDT=     0000000007bee698 00000047
IDT=     000000000782e018 00000fff
CR0=80000033 CR2=0000000000000000 CR3=0000000007c01000 CR4=00000668
DR0=0000000000000000 DR1=0000000000000000 DR2=0000000000000000 DR3=0000000000000000 
DR6=00000000ffff0ff0 DR7=0000000000000400
EFER=0000000000000500
FCW=037f FSW=0000 [ST=0] FTW=00 MXCSR=00001f80
FPR0=0000000000000000 0000 FPR1=0000000000000000 0000
FPR2=0000000000000000 0000 FPR3=0000000000000000 0000
FPR4=0000000000000000 0000 FPR5=0000000000000000 0000
FPR6=0000000000000000 0000 FPR7=0000000000000000 0000
XMM00=00000000069940180000000000000000 XMM01=00000000000000000000000000000000
XMM02=00000000000000000000000000000000 XMM03=00000000000000000000000000000000
XMM04=00000000000000000000000000000000 XMM05=00000000000000000000000000000000
XMM06=00000000000000000000000000000000 XMM07=00000000000000000000000000000000
XMM08=00000000000000000000000000000000 XMM09=00000000000000000000000000000000
XMM10=00000000000000000000000000000000 XMM11=00000000000000000000000000000000
XMM12=00000000000000000000000000000000 XMM13=00000000000000000000000000000000
XMM14=00000000000000000000000000000000 XMM15=00000000000000000000000000000000
(qemu)

次に、既存のUEFIアプリをboot loaderとして、haltするだけの最小のカーネルを作ってロードする。boot loaderはプロジェクトのルートにmain.rsとして配置しているので、カーネルはsrcディレクトリを作ってそこに置く。

rustにもexternがある。externなしだとABIがRustのものになるが、extern "C"するとSystem ABIになる。ドキュメントにはFFI用途と書いてあるが、自作OS用途でも大丈夫なはず。

ちなみにNightlyだとllvm_asmもあるらしい。
https://doc.rust-lang.org/unstable-book/library-features/llvm-asm.html

ここからはloaderとkernelを分けて作るために、cargoのworkspace機能を使うことにした。
StackOverflowによると、tokioが参考になるらしい。

workspaceでtagetがrootに一個だけなのは仕様らしい。
https://doc.rust-lang.org/book/ch14-03-cargo-workspaces.html

The workspace has one target directory at the top level for the compiled artifacts to be placed into; the adder package doesn’t have its own target directory. Even if we were to run cargo build from inside the adder directory, the compiled artifacts would still end up in add/target rather than add/adder/target. Cargo structures the target directory in a workspace like this because the crates in a workspace are meant to depend on each other. If each crate had its own target directory, each crate would have to recompile each of the other crates in the workspace to have the artifacts in its own target directory. By sharing one target directory, the crates can avoid unnecessary rebuilding.

freestandingオプションを探してたら、ちょうどそれのサイトを見つけた。
https://os.phil-opp.com/ja/freestanding-rust-binary/
必要なことは全部ここに書いてあった。

Rust コンパイラが _start という名前の関数を実際に出力するように、#[no_mangle] attributeを用いて名前修飾を無効にします。

戻り値の型である ! は関数が発散している、つまり値を返すことができないことを意味しています。エントリポイントはどの関数からも呼び出されず、OS またはブートローダから直接呼び出されるので、これは必須です。なので、値を返す代わりに、エントリポイントは例えば OS の exit システムコールを呼び出します。

と思ったんだけど、x86_64-eflをターゲットにしたカーネルのコンパイルができなかったので今日はここまで。

Rustで自作OS 3日目

YT — Sun, 04 Jul 2021 09:39:19 +0000

"第2章 EDK II入門とメモリマップ"を進めていく。
自作OS本を読んだところ、USBブートするためにBoot Loaderを作っていくようで、昨日までで作ったUEFIアプリをEDK IIで書き直すらしい。
昨日出てきたOVMFはUEFI BIOSのOSS実装で、EDK IIはUEFI BIOS上で動くアプリだけでなく、UEFI BIOS自体を開発するためにも使われるとのこと。

Rustで書くときにどうすれば良いのか調べたが、いまいちピンとこない。そもそもUEFIとEDK IIがよく分かってない。

uefi crateを使った昨日時点で.efi出力が得られている。
Enabling Rust for UEFI Firmware - Webinar
rust-osdev/bootloader

osdev-jpを見ると、

スタンドアロンの UEFI アプリは UEFI Shell が起動する前に起動することができます。OS のブートローダーを作る場合などはスタンドアロンとして構成します。

スタンドアロンの UEFI アプリのエントリポイントは一般的な C 言語プログラムと違い、EFI_HANDLE と EFI_SYSTEM_TABLE * を引数として受け取ります。

ということは、昨日までのuefi crateを使ったUEFIアプリはこの特徴を満たしているのでは？なんなら使用可能メモリを表示する過程でメモリマップを取得しているのでは？

#![no_std]
#![no_main]
#![feature(asm)]
#![feature(abi_efiapi)]
#![feature(alloc)]

extern crate uefi;
extern crate uefi_services;
extern crate rlibc;
extern crate alloc;
extern crate log;

use uefi::prelude::*;
use crate::alloc::vec::Vec;
use uefi::table::boot::MemoryType;
use log::info;

const EFI_PAGE_SIZE: u64 = 0x1000;

#[entry]
fn uefi_start(_image_handler: uefi::Handle, system_table: SystemTable<Boot>) -> Status {
    uefi_services::init(&system_table).expect_success("Failed to initialize utils");
    system_table
        .stdout()
        .reset(false)
        .expect_success("Failed to reset output buffer");
    {
        let rev = system_table.uefi_revision();
        let (major, minor) = (rev.major(), rev.minor());
        info!("UEFI {}.{}", major, minor);
        memory_map(&system_table.boot_services());
    }
    loop{};
    Status::SUCCESS;
}

fn memory_map(bt: &BootServices) {
    let map_size = bt.memory_map_size();
    let mut buffer = Vec::with_capacity(map_size);
    unsafe {
        buffer.set_len(map_size);
    }

    let (_k, desc_iter) = bt
        .memory_map(&mut buffer)
        .expect_success("Failed to retrieve UEFI memory map");

    let descriptors = desc_iter.copied().collect::<Vec<_>>();

    assert!(!descriptors.is_empty(), "Memory map is empty");

    info!("efi: usable memory ranges ({} total)", descriptors.len());
    descriptors
        .iter()
        .for_each(|descriptor| match descriptor.ty {
            MemoryType::CONVENTIONAL => {
                let size = descriptor.page_count * EFI_PAGE_SIZE;
                let end_address = descriptor.phys_start + size;
                info!(
                    "> {:#x} - {:#x} ({} KiB)",
                    descriptor.phys_start, end_address, size
                );
            }
            _ => {}
        })
}

適当に写経してたからuefi::table::bootとか使ってるのに気づかなかった。
この構成でブートローダーとして機能するかはわからないので、とりあえず本を読み進める。
元になったブログでもメモリマップ取得までやってたので、UEFIアプリのHello Worldは画面表示だけでなくメモリマップまでなのかもしれない。
ちなみに自作OS本ではメモリマップをファイルに保存するUEFIアプリを作ってた。

EDK IIを使ってるかは分からないが、今回の場合はueif crateを使ってboot loaderを作れればそれで良さそう。

Rustで自作OS 2日目

YT — Sat, 03 Jul 2021 07:08:56 +0000

今日は文字を表示するUEFIアプリを作るところから。自作OS本ではまだ1日目。
https://gil0mendes.io/blog/an-efi-app-a-bit-rusty/#the-app-itself を進めていく。
Hello Worldに手を加えるところから。
#![...]はattributeのようで、#![no_std] is a crate-level attribute that indicates that the crate will link to the core-crate instead of the std-crate.とのこと。ベアメタル環境ではつける必要がある。

#![feature(asm)]でインラインアセンブリを書けるようにする(The Rust Unstable Book)。
#![feature(abi_efapi)]のページはタイトルだけで中身からっぽだった。

#![no_std]              // std libを使わない
#![no_main]             // UEFI向けエントリポイントに変更する
#![feature(asm)]        // inline assemblyを呼べる
#![feature(abi_efiapi)] // よくわからないがABIを揃えるような名前

extern crate uefi;
extern crate uefi_services;

use uefi::prelude::*;

#[entry]
fn uefi_start(_image_handler: uefi::Handle, system_table: SystemTable<Boot>) -> Status {
    loop{};
    Status::SUCCESS;
}

これを元ブログのPythonスクリプトでbuild & runするんだけど、OVMFのファイルが生成されなくて失敗した。
OFMFについて調べる。

元ブログを読み返すと、見落としがあることがわかった。

QEMU doesn’t come with OVMF, so it requires to installing it on your PC or get a pre-built image from the Internet, it’s possible to download it from my test repository.

元リポジトリからダウンロードしてくるとrunコマンドでQEMUが動いた。

次は文字を表示させる。

log crateを入れてinfo!マクロでログを表示できるようになった。

Rustで自作OS 1日目

YT — Tue, 29 Jun 2021 15:40:12 +0000

最近コード書いてなかったので、Rustの勉強を兼ねて自作OS本をやってみる。
https://www.amazon.co.jp/dp/B08Z3MNR9J

環境はIntel macとIntelliJ。
適当にリポジトリを作ってRustのHello Worldが動くように設定を終わらせる。
https://github.com/ytannai/kabos

自作OS本はUEFIアプリをCで書くサンプルから始まるんだけど、Rustで書き直すところで止まった。

ちなみにCargo.tomlでeditionという、バージョン的なものを指定できるらしい。

普通にrustup initしたら2018だったので、試しに2021をしてみたらnaightlyにする必要があるようなので、rustup toolchain install nightlyでrelease channelを変えてみる。
インストールしたらrustup default nightlyで適用する。*envの機能を公式でサポートしてるのが良い。

この時点でCargo.tomlは以下のようになっている。これでHello Worldを再実行できた。

cargo-features = ["edition2021"]

[package]
name = "kabos"
version = "0.1.0"
edition = "2021"

# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

[dependencies]

[[bin]]
name = "kabos"
path = "main.rs"

IntelliJがよく統合されていて、今のところ快適。

で、UEFIに戻る。ライブラリが見つかった。
https://github.com/rust-osdev/uefi-rs
このREADMEにあるブログを参考に、Cargo.tomlのdependenciesセクションへ依存関係を追加する。あと、unstable featureを使う設定もする。

[dependencies]
uefi = "0.11.0"
uefi-services = "0.8.0"

[unstable]
build-std = ["core", "compiler_builtins", "alloc"]

この時点でもう一度Hello Worldを実行してみる。実行はできるが、依存が増えたからかコンパイルに少し時間がかかるようになった。
キャッシュされるのか、初回だけのようだ。

依存にrlibcも追加すると、いよいよベアメタル感が出てくる。

もう眠いので今日はここまで。次回はUEFIアプリの実装。
https://gil0mendes.io/blog/an-efi-app-a-bit-rusty/#the-app-itself