2021年まとめ
2021年も引き続きコロナだった。しかし、ワクチン接種があったため、命の心配をすることはなくなったので、比較的平穏に生きることができた。今年は、やはり「さようなら全てのエヴァンゲリオン」だろう。エヴァが終わるのは感慨深いものがある。
研究関連は、『並行プログラミング入門』オライリー・ジャパンを出版できたことと、特許がようやく認められたことである。特許は、2017年に出願したもので、出願は前所属の先輩にお任せしていたため、すっかり忘れていた。出願から認められるまでの期間が長すぎる。研究開発に数年単位でかかり、特許が認められるまでさらに数年かかるため、3年や5年の研究開発計画では、とても長期的な視点は持てない。
このくそったれな環境をサバイブするためには、短期的視点な論文を量産した方が良く、自分のように特許を出願したり専門書を書いたりするのは時流と完全に逆行している。技術革新が起きる間隔が指数的に短くなっている現状、マクロで重要なのは、多くの人々が先端技術にリーチでき、技術のアップデートができることだ。以前ならば100年に一度のレベルのパラダイムシフトが、いまでは数十年に一度の頻度で起きているが、これに社会は全く追従できていない。重要なのは研究ではなく、コモンセンスのアップデートで、それには書籍と教育が最適だ。これらに、少しでも貢献できていれば良いのだけれど。（研究ももちろん重要だけど）
それでは、さようなら2021年。みなさん良いお年を。
2021年の成果は以下の通り。2021年はRust漬けだったので、2022年は圏論と組み込みをやっていきたい。
特許
- 井上 朋哉, 高野 祐輝, 三輪 信介, 特許第6888234号, 検索装置, 検索プログラム, 及び検索方法（2017年5月22日出願）
本
- 高野 祐輝, "並行プログラミング入門", オライリー・ジャパン, Aug. 2021.
外部講演
- 高野 祐輝, "並行プログラミング入門とRustを用いた低レベルプログラミング", 組込みマルチコアサミット, Nov. 2021
国際会議（査読あり）
- Sai Veerya Mahadevan, Yuuki Takano, and Atsuko Miyaji, "PRSafe: Primitive Recursive Function based Domain Specific Language using LLVM", International Conference on Electronics, Information, and Communication, pp.377-380, Jan. 2021
国内研究会
- 劉 小竜, 高野 祐輝, 宮地 充子, "セッション型を用いたプロセス間の安全な通信プロトコルの設計と実装", 情報通信システムセキュリティ研究会 (ICSS2021-50), 2021年11月
- 金谷 延幸, 津田 侑, 高野 祐輝, 藤原 吉唯, 伊沢 亮一, 井上 大介, "FPGAによるソフトウェア解析環境「Iana」の提案", Computer Security Group (CSEC2021-93), 2021年5月
- 斎藤 文弥, 高野 祐輝, 宮地 充子, "Coqを用いたソフトウェアスイッチの設計と実装", Computer Security Group (CSEC2021-03), 2021年3月
- 尾崎 純平, 高野 祐輝, 宮地 充子, "Rust言語用動的メモリアロケータの検査フレームワークの提案", Computer Security Group (CSEC2021-03), 2021年3月
- 竹中 幹, 高野 祐輝, 宮地 充子, "多様なネットワークで利用可能な低レイテンシ欺瞞的防御システムの設計と実装", Symposium on Cryptography and Information Security (SCIS) 2021, 2021年1月
『並行プログラミング入門』を執筆しました
これは、Rust Advent Calendar 2021 (2)の25日目の記事です。
https://qiita.com/advent-calendar/2021/rust
2021年8月にオライリー・ジャパンより出版された『並行プログラミング入門』を執筆しました。
執筆から出版まで
本書のGitリポジトリのコミットログでは、2018年の2月10日に初コミットがあるため、2021年8月21日の出版日まで、実に3年6ヶ月もかかったことになります。これほどかかったのは、執筆にかけるための時間がそれほどとれなかったのと、何より内容が難しいと言うのが大きいと思います。並行プログラミングについては、Webや書籍等含めて、様々な文献で言及されてはいるものの、それを体系的にまとめているものがないため、執筆はかなり難しかったです。
『The Art of Multiprocessor Programming』という本もあるにはあるのですが、これはJavaとロックフリーに偏っていて、もっと広範囲な内容が無いという不満もありました。より具体的に言うと、アセンブリによるアトミック処理、グリーンスレッド、π計算などのトピックも並行プログラミングでは重要なトピックですが、それらの説明はありません。これらを含んだ、もっと包括的な本が出版されないかとずっと思っていたのですが、一向に出版される気配がなかったため、一念発起して書きはじめました。
書き始めたは良いものの、なかなか時間はとれず、夜寝る前の10〜11時ぐらいに毎日少しだけ書いていました。盆と正月はかき入れ時で、集中して執筆する時間がとれるチャンスですが、365日働いているようなものなので、それはそれで大変でした。また、3年間1人でずっと孤独に執筆するというのもなかなか大変な作業でした。実際、あまりにつらくて、半年ほど執筆していない期間もあったようにも思います。昔は、専門書は草や花のように勝手に生えてくるような感覚でいましたが、専門書を書くために大変な労力が注ぎ込まれているのを体感した次第です。
本書では、実装に重きを置いていますが、最も注力したのは概念的な説明でして、たとえば、並行や並列とは一体何かや、プロセスとは一体何かという根本的なところを説明するのに大変労力がかかりました。これらを説明するために、技術書だけではなく哲学書なんかにも目を通していたので、大変な時間がかかってしまいました。多くの方にとっては、こういう抽象論は興味外かもしれませんが、「Philosophy of Concurrent Programming」は本書の大きな特徴だと思います。
そんなこんなはありましたが、2021年の8月にようやく出版でき、嬉しい限りです。ただ、誤植がややあったのは申し訳ないです。今回、誤植報告をGitHubからpull requestできるようにしたのですが、読者の皆さんから多くプルリクいただき、異常な速度で正誤表が出来上がっていきました。本当に感謝しかありません。
Rustとわたし
『並行プログラミング入門』執筆に当たり重要視したのは、やはりRustです。Rustは本当に良い言語で、アセンブリのような低レベルな記述から、mapとfold、async/awaitと言った記述までカバーできて本当に素晴らしいです。asm!マクロはインラインアセンブリの記述としては突出した書きやすさだと思います。asm!目当てにRustを使っていると言っても過言ではありません（言い過ぎ）。
『並行プログラミング入門』を書くからには、OSぐらいは一度実装しておく必要があると感じ、昨年、2020年には、RustでOS、ファームウェアなどを実装してみましたが、その知見は本書にも活かされています。こういうマニアックな事をやっていると、初学者置いてけぼりな事を書きたくなるのですが、そういう欲求を抑え、重要で基本的な事を書くことに注力するのはなかなか大変でした。マニアックな技術は、論文という形でいつか発表できたらなと思います。近々、学生と共に成果発表はできそうではあります。いや、できるかな、できたらいいなあ。
また、『並行プログラミング入門』を執筆したご縁で、オライリー・ジャパンから2022年1月19日発売予定の『プログラミングRust 第2版』の査読もさせて頂きました。この本は重要なことしか書かれていないので、是非、こちらも手に取って頂ければと思います。『入門Python 3 第2版』は800ページ、『JavaScript 第7版』は784ページありますが、『プログラミングRust 第2版』は688ページしか無いので、Rustは覚える事も少なくて簡単なプログラミング言語です。688ページを2週間程度で読むのは結構大変でした。
先日、阪急梅田の紀伊国屋に行ったら、Rustの棚ができていたのでRustの注目がますます高まりつつありますね。
おまけ：Linux next with Rust
書籍の話ばかりではなんなので、もう少し技術的な話題もしたいと思います。最近、RustがLinuxカーネルに利用されそうな気配が出てきました。そこで、実際にLinux nextをRustでコンパイルして、動かしてみました。
結論から書くと以下の通りです。
- Rust 1.57.0 Stableでコンパイル可能に
- 動的メモリ確保に失敗した場合のパニックは対処済み
Rust 1.57.0 Stable
ちょっと前まではRustのnightlyかbetaでないとコンパイルができなかったのですが、最近、Rust 1.57.0 Stableでコンパイルできるようになっていました。ただ、Stable版だと、asm!が使えないので気になるところではあります。asm!の安定化がそろそろらしいので、大変待ち遠しいです。
動的メモリ確保とパニック
Rustのstdは動的メモリ確保に失敗した際にはパニックとなります。仮想メモリを利用している場合は、動的メモリ確保が失敗することはあまりなく、ページフォルトが起きた段階でメモリが足りなくなりスワップが発生し、更にスワップ領域も足りなくなってくるとLinuxの場合はOOMキラーに殺されます。このように、一般的な環境だと動的メモリ確保失敗の動作をパニックとするのでほとんど問題は無いのですが、カーネルだとパニックは問題で、2021年の頭頃にこの問題が指摘されていました。
2021年4月15日 パニックお断り―Linus，"Rust for Linux"の盛り上がりに釘を刺す：Linux Daily Topics｜gihyo.jp … 技術評論社
この問題は、既に解決済みのようです。たとえば、Vecだとpushというメソッドがありますが、これは内部的で動的メモリ確保を行う可能性があります。LinuxのRustでは、Vecにtry_pushというResult値を返すメソッドが追加されており、カーネルモジュールなどの実装にはこれらを利用することができます。これらがRustの本家にも追加されると、ベアメタルや組み込みプログラミングにもRustが使いやすくなるので、是非導入して欲しいところです。ライセンス的に難しそうな気もしますが。
実行結果
簡単な実行結果ではありますが、カーネルコンフィグと、rust_minimalというRustで書かれたサンプルカーネルモジュールのロードとアンロードのスクリーンショットを貼っておきます。実験環境は、仮想環境内のDebian 11上で、Linux nextをRust 1.57.0でコンパイルしてインストールしています。
ただし、現状では、カーネルコンフィグのMODVERSIONSをオフにしないとRustが有効化されないようなので、まだまだ課題はあるかなと言う感じです。ぱっと見た感じ、足りない実装も結構ありそうな感じでした。しかし、Rustなので、カーネルコードなのに非常に読みやすいです。今後に期待ですね。
Hello, World!
サンプルコードがいくつかあったので、それをベースにmiscキャラクタデバイスを実装してみました。readすると、"Hello, World!"を表示するだけの簡単なデバイスです。コードは以下の通りで、注目すべき点はread関数と、data.write_slice(hello)?; という箇所です。readするとこの関数が呼ばれて、引数のIoBufferWriterにデータを書き出すとユーザランドにデータが渡されます。簡単ですね。
// rust_hello.rs // SPDX-License-Identifier: GPL-2.0 //! Rust miscellaneous device sample #![no_std] #![feature(allocator_api, global_asm)] use kernel::prelude::*; use kernel::{ file::File, file_operations::{FileOpener, FileOperations}, io_buffer::IoBufferWriter, miscdev, }; module! { type: RustMiscdev, name: b"rust_hello", author: b"Yuuki Takano", description: b"Hello, World! in Rust", license: b"GPL v2", } #[derive(Clone)] struct Hello; impl FileOpener<Hello> for Hello { fn open(shared: &Hello, _file: &File) -> Result<Self::Wrapper> { Ok(Box::try_new(shared.clone())?) } } impl FileOperations for Hello { kernel::declare_file_operations!(read); fn read( _shared: &Hello, file: &File, data: &mut impl IoBufferWriter, _offset: u64, ) -> Result<usize> { pr_info!("rust_hello: read, pos = {}", file.pos()); if file.pos() == 0 { let hello = b"Hello, World!\n"; data.write_slice(hello)?; Ok(hello.len()) } else { Ok(0) } } } struct RustMiscdev { _dev: Pin<Box<miscdev::Registration<Hello>>>, } impl KernelModule for RustMiscdev { fn init(name: &'static CStr, _module: &'static ThisModule) -> Result<Self> { pr_info!("Hello, World! in Rust (init)\n"); Ok(RustMiscdev { _dev: miscdev::Registration::new_pinned::<Hello>(name, None, Hello)?, }) } } impl Drop for RustMiscdev { fn drop(&mut self) { pr_info!("Hello, World! in Rust (exit)\n"); } }
これを実行すると以下のようになります。catで/dev/rust_helloを実行すると、ちゃんと、"Hello, World!"が表示されます。
$ sudo insmod rust_hello.ko $ ls /dev/rust_hello /dev/rust_hello $ sudo cat /dev/rust_hello Hello, World! $ sudo sh -c "dmesg | tail -n 1" [512769.908740] rust_hello: rust_hello: read, pos = 0
つづいて、カーネルモジュール内でパニックを起こしてみます。コードは以下の通り修正しています。
--- a/samples/rust/rust_hello.rs +++ b/samples/rust/rust_hello.rs @@ -56,6 +56,7 @@ struct RustMiscdev { impl KernelModule for RustMiscdev { fn init(name: &'static CStr, _module: &'static ThisModule) -> Result<Self> { + panic!("panic!"); pr_info!("Hello, World! in Rust (init)\n"); Ok(RustMiscdev {
これをコンパイルして、insmodしてみると、insmodがセグフォで死にます。rmmod -fも効かず、大変なことになりました。カーネルプログラミングは怖いですね。
$ sudo insmod rust_hello.ko Message from syslogd@DebianKern at Dec 13 23:58:20 ... kernel:[513053.695576] rust_kernel: panicked at 'panic!', samples/rust/rust_hello.rs:59:9 zsh: segmentation fault sudo insmod rust_hello.ko $ cat /proc/modules | grep rust rust_hello 20480 1 - Loading 0x0000000000000000 (E+) $ sudo rmmod -f rust_hello rmmod: ERROR: ../libkmod/libkmod-module.c:799 kmod_module_remove_module() could not remove 'rust_hello': Device or resource busy rmmod: ERROR: could not remove module rust_hello: Device or resource busy
上のコードを書く際、Cargo.tomlのない環境だったのでVSCode + rust-analyzerの使い方がわからず、vimで書いていました。rust-analyzerに飼い慣らされた自分には、なかなかつらい環境です。rust-analyzerを使う方法はあるような気もしますが、今回はそこまで深掘りできずです。
それでは今回はこの辺で。皆さん、メリークリスマス！良いお年を。
次回作にもご期待ください。
俺たちの戦いは始まったばかりだ！
TLA+ on VSCodeで再帰ロックアルゴリズムを検証してみた
TLA+を使って『並行プログラミング入門』4.4章にある再帰ロックのアルゴリズムを検証してみました。TLA+は公式のGUIアプリも用意されているのですが、今回はVSCodeを利用してみました。公式のGUIアプリはエディタが微妙なのですが、VSCodeを使うとサクサク書けます。そのかわり、各種設定を設定ファイルに書く必要があります。
検証内容は「デッドロックしない」と「クリティカルセクションを実行中のプロセスは高々1つ」です。
TLA+と再帰ロックのアルゴリズムは以下を参照してください。
アルゴリズムの実装
次に、reclock.tlaを作成します。reclock.tlaにはPlusCalでアルゴリズムを記述します。具体的には、reclock.tlaというファイルを以下のように作成します。
------------------------------ MODULE reclock ------------------------------
EXTENDS Integers, TLC, Sequences, FiniteSets
CONSTANTS MAX_REC, PIDS
(*--algorithm lock
variables
locking = {}, \* ロック中のプロセス集合。検証用の変数
\* アルゴリズム用の変数
lock = FALSE,
id = 0,
cnt = 0;
\* ロック獲得
procedure acquire()
begin
Acquire:
if lock /\ id = self then
A0: cnt := cnt + 1;
else
TAS:
await lock = FALSE;
lock := TRUE;
locking := locking \union {self};
A1: id := self;
A2: cnt := cnt + 1;
end if;
A3: return
end procedure;
\* ロック開放
procedure release()
begin
Release:
cnt := cnt - 1;
R0:
if cnt = 0 then
R1: id := 0;
R2: lock := FALSE;
locking := locking \ {self};
end if;
R3: return;
end procedure;
\* 再帰ロック
procedure recursive_lock()
begin
RecLock:
either
Rec:
if cnt < MAX_REC then \* 最大MAX_REC回まで再帰ロック
RL0:
call lock_unlock() \* 再帰ロック
end if;
or
NotRec:
skip;
end either;
RL1: return;
end procedure;
procedure lock_unlock()
begin
Lock:
call acquire(); \* ロック獲得
L0: call recursive_lock(); \* 再帰ロック
L1: call release(); \* ロック開放
L2: return;
end procedure;
fair process pid \in PIDS
begin
T1:
call lock_unlock()
end process;
end algorithm;*)
TypeInvariant ==
/\ MAX_REC \in Int
/\ PIDS \subseteq Int
AtMostOne == Cardinality(locking) <= 1
=============================================================================つづいて、F1からTLA+: Parse Moduleを選択すると、TLA+の論理式がreclock.tlaに追記され、設定ファイルのreclock.cfgが出力されます。reclock.cfgに必要な設定を追加してきます。
reclock.cfgには、以下のように定数や検証する不変条件を追記します。「\* Add statements after this line.」という行より下が、今回追加した行です。定数と不変条件を設定します。
SPECIFICATION Spec
\* Add statements after this line.
CONSTANTS
PIDS = {1, 2, 3}
MAX_REC = 5
INVARIANTS
AtMostOne
TypeInvariant
検査
次に、再びF1からTLA+: Check model with TLCを選択して検査します。
検査に成功すると、以下のように出力されます。検査に失敗した場合は反例が表示されます。
以上簡単ですね。色々なものが検証できそうです。
【読書】三体を読んだぞ！
三体問題は物理学で有名な問題で、2つの物体が相互作用する場合はその挙動は解析的に解くことが出来るが、これが3つ以上となると解析的に解くことが出来ないという問題である。三体は、この三体問題をテーマとした中国発のSFで、以前からその噂は耳にしていた。しかし、分厚い書籍が5冊もあるので読むのを躊躇していたが、気がつくと2ヶ月弱であっという間に5冊すべて読み終えてしまった！三体、恐ろしい子！
三体Ⅱ 黒暗森林（上）
三体Ⅱ 黒暗森林（下）
三体Ⅲ 死神永生 下
三体Ⅲ 死神永生 上
翻訳が良い
三体のまず素晴らしいのは、翻訳が大変素晴らしくて非常になめらかに読めることだと思う。個人的な経験上、海外作品は翻訳がどうもあわなくて読み通せないことがしばしばあったが、三体に限って言うとそう言ったことはなくてすらすら読めた。まるで日本人が書いたような読み口である。
ただ、やはり海外作品なので、はじめは人名を覚えるのがつらかった。たとえば、葉文潔はイェ・ウェンジェと読むのだが、これを覚えるのが本当に難儀していた。しかし、葉文潔をヨウ・ブンケツと音読みで覚えることで解決した。本書の中では葉文潔（イェ・ウェンジェ）と読み方が降ってあるが、私のように人名を覚えるのは苦手な人は、本格的な読み方は諦めて音読みで覚えておくと読みやすいのではと思う。
三体III 死神永生が好き
三体は全部で5巻あり、そのうち三体、三体II 暗黒森林（上）、三体II 暗黒森林（下）の3冊で1つのストーリー、三体III 死神永生（上）、三体III 死神永生（下）の2冊でもう1つのストーリーという構成となっている。中国では三体II 暗黒森林の評判が良いようだけれど、個人的には死神永生の方が好きだ。
もちろん暗黒森林もとても面白くて、我々の軍隊があれであれされるところなどは本当に面白くて、夜も眠れず気がついたら明け方になっていました。おかげさまで次の日が本当につらくて、ひどい目に遭った。おのれ。
暗黒森林はどちらかというと、我々現代人でも共感できそうなストーリー仕立てになっているのに対して、死神永生は色々なところを超越してしまっていて涅槃にたどり着いてしまったような感覚がある。そんなストーリーなので、まったく良くわからない人もいるかもしれないが、個人的にはこのSF感丸出しの展開は大変好みで、生とは、死とは、宇宙とはなにかみたいなことを考えながらやっぱり夜も寝られない日々を送っていた。○○に落下し続ける科学者の話だったり、空間がアレするような話だったり、本当に面白くてこれはとんでもないものを読んでしまったという感じがある。宇宙の話が好きな人は是非読んで欲しいSF作品だ。
いやあ、SFって本当に良いですね。
Schemeによる第一不完全性定理の実装
『知の限界』という本を買ったら第一不完全性定理をLispで実装する方法が載っていた。しかし、そのコードはSchemeでは動かないように思えたので、Schemeで実装をしてみた。不完全性定理では、コード中の引数に自身のコード渡して、自己言及的なゲーデル文Gを構成して証明するのだが、S式はコードもただのデータなので、こういうことが出来るのかと感心した。本書では、第一不完全性定理以外にも、不動点や停止問題のLisp実装も示されており、それらはここで示すコードと本書を読めばSchemeで実装可能に思う。
ただし、本書は面白いが、第一不完全性定理の説明などはほとんどないため、そもそも第一不完全性定理を知らない場合は、理解するのは難しそうではある。
![知の限界[復刻改装版] (00)](https://m.media-amazon.com/images/I/41T1WdHOpEL._SL500_.jpg "知の限界[復刻改装版] (00)")
Schemeによる再実装
Schemeで再実装したものは以下の通りとなる。
まず、「「xはxである」という文は証明できない」というgを考える。文なのでS式で返す。
(define (L x y) (cons x (cons y '()))) ;; 「xはxである」は証明できない (define g '(lambda (x) (L 'is-unprovable (L x x))))
つぎに、S式を評価するための補助関数を以下のように定義する。
;; (eval l) (define (eval0 l) (eval l '())) ;; 1ステップだけ評価 ;; (eval ((car l) (cdr l))) (define (eval1 l) (apply (eval0 (car l)) (cdr l)))
とすると、ゲーデル文G = (g g)はSchemeでは以下のようになる。
((eval0 g) g)
第一不完全性定理はGもnot Gも証明できないようなGが存在するというものなので、証明してみる。
まず、G = (is-unprovable G)となることを確認する。
;; ゲーデル文G ;; g(x) = 「xはxである」は証明できない ;; G = g(g) = 「「xはxである」は証明できない」に自身を代入した文は証明できない (let ( (G ((eval0 g) g)) ) (print "\n以下のようなGを考える（Gはゲーデル文）。") (print "G = (g g)") (print " = " G) (print " ;; 上式の引数を簡約") (print " ;; (L (car G) (eval1 (cadr G)))") (print " = " (L (car G) (eval1 (cadr G)))) (print " ;; Gと上式の引数が同じ") (print " ;; (equal? G (eval1 (cadr G))) = " (equal? G (eval1 (cadr G)))) (print " = " (L 'is-unprovable 'G) " ; Gは証明できない") )
以下のようなGを考える（Gはゲーデル文）。
G = (g g)
= (is-unprovable ((lambda (x) (L 'is-unprovable (L x x))) (lambda (x) (L 'is-unprovable (L x x)))))
;; 上式の引数を簡約
;; (L (car G) (eval1 (cadr G)))
= (is-unprovable
(is-unprovable ((lambda (x) (L 'is-unprovable (L x x))) (lambda (x) (L 'is-unprovable (L x x))))))
;; Gと上式の引数が同じ
;; (equal? G (eval1 (cadr G))) = #t
= (is-unprovable G) ; Gは証明できないあとは、一般的な第一不完全性定理通り、以下のように証明できる。この部分は本書には載っていない。
Gを証明可能と仮定する。すると、(is-unprovable G)が正しいと証明可能となる。つまり、Gは証明できないと証明できることになる。背理法よりGは証明不可能。
not Gを証明可能と仮定する。ここで、
not G = not (is-provable G) = (provable G)
となる。これより、not Gが証明可能となると、Gも証明可能でなければならなので矛盾。背理法よりnot Gが証明不可能。
Gもnot Gも証明できない。Q.E.D.
ソースコード
ソースコードは以下にある。
github.com
これは、Gaucheで実行することができ、実行すると以下のように出力される。
$ gosh incomplete_theorem.scm
第一不完全性定理：Gもnot Gも証明できないようなGが存在する
g = (lambda (x) (L 'is-unprovable (L x x)))
とする。
以下のようなGを考える（Gはゲーデル文）。
G = (g g)
= (is-unprovable ((lambda (x) (L 'is-unprovable (L x x))) (lambda (x) (L 'is-unprovable (L x x)))))
;; 上式の引数を簡約
;; (L (car G) (eval1 (cadr G)))
= (is-unprovable (is-unprovable ((lambda (x) (L 'is-unprovable (L x x))) (lambda (x) (L 'is-unprovable (L x x))))))
;; Gと上式の引数が同じ
;; (equal? G (eval1 (cadr G))) = #t
= (is-unprovable G) ; Gは証明できない
Gを証明可能と仮定する。
すると、(is-unprovable G)が正しいと証明可能となる。
つまり、Gは証明できないと証明できることになる。
背理法よりGは証明不可能。
not Gを証明可能と仮定する。
ここで、
not G = not (is-provable G)
= (provable G)
となる。
これより、not Gが証明可能となると、Gも証明可能でなければならなので矛盾。
背理法よりnot Gが証明不可能。
Gもnot Gも証明できない。Q.E.D.
『実践TLA+』を読んだ
ざっくりというならば、モデル検査とは、仕様を（様相）論理式に落とし込んで、その仕様がモデルを満たしているかを検査するための方法論である。TLA+はモデル検査用のツールであり、仕様や実装の正しさを検証することができる。
自分はモデル検査ツールはNuSMVとAlloyを使ったことがあるのだが、TLA+は使ったことがなかった。というのも、使おうとしたことはあるが、論理式はわかるもののGUIの使い方がわからなかったため放置していた。
最近、『実践TLA+』という書籍が出版されたため、TLA+に再挑戦してみることにした。実践TLA+では、GUIの使い方もきちんと説明されているために、すんなりと利用することができたと思う。
TLA+は時相論理という論理をベースにしているのだが、これは一般のプログラマにはとっつきにくい。そこで、TLA+では、手続き型言語に近い記述であるPlusCalを導入していて、比較的書きやすくなっている。実際にいくつかのコードを動かしてみたが、PlusCalから時相論理での記述を自動的に生成してくれるため大変便利である。また、公平性やデッドロックなどの検査も自動で行えるのがよいと感じた。
『実践TLA+』を読んで、全然わからなかったという人は、おそらく、論理式やモデル検査の知識が乏しいか、並行プログラミングの知識が乏しいかのどちらかか、もしくはその両方であると思われる。時相論理を使ったモデル検査の入門としては、『モデル検査 初級編―基礎から実践まで4日で学べる―』でNuSMVをやってみるとよいと思う（この本ではSPINというツールでも説明しているのでそちらでもよい）。これを読めば、時相論理、モデル検査の基本がわかるので、TLA+への足がかりになるはずである。
並行プログラミングがわからない場合は、宣伝になってしまうが、私の書いた『並行プログラミング入門』がよいと思う。たとえば、『並行プログラミング入門』の3.9でパン屋のアルゴリズムが、『実践TLA+』の6.4でデッカーのアルゴリズムがある。これらアルゴリズムはアトミック命令を使わない同期処理方法である。また、『並行プログラミング入門』の6.1.1と『実践TLA+』の6.1.2で、弱い公平性と強い公平性について説明がある。このように、内容が重なる部分が多く、両方を読むとより知識が確かなものになる。『実践TAL+』で得た知見を用いると『並行プログラミング入門』にあるアルゴリズムを検証できるはずなので、挑戦してみるのも面白そうだ。
理論的なところを知りたい場合は、論理学の教科書で様相論理や時相論理を勉強すればよいが、使う分にはそこまでは必要ないだろう。
個人的には、『実践TLA+』の最後の11章で説明している、分散コンピューティングMapReduceでのLivenessなども検証しているのが面白いと感じた。分散処理なプログラミングをしているときに、ノード故障に対応するために、ハートビートを送ったりと小手先のテクニックを駆使しても、いざ故障が発生した場合に全く動かないという事はざらにある。そういう小手先のテクニックを確かにテストできるのは大変有意義に思う。
『禅とオートバイ修理技術』を読んで美について考えた
ハヤカワの本が安売りしていたので、禅とオートバイ修理技術という本を読んでみた。クオリティの話をしながらアメリカをオートバイで横断していくロードムービー的な話なのだが、懐かしようなやたら難しいような、それでいて引き込まれ考えさせられるような不思議な本だった。1974年にアメリカで発売された本だが、今でもその内容は色あせないのは、やはり主題が普遍的だからだろう。
クオリティ
この本の主題にクオリティの話があるが、正直分からなかった。いや、正確には、わかったとわからないを繰り返しながらアメリカを旅していくような気分になっていた。これは、自分の読解力が足りないというよりかは、そもそも著者自身も本の中でわかったとわからないを繰り返しているのでしょうがないとは思う。
最終的には著者はある到達点へたどり着いているぽいが、自分がそこへたどり着いたかは分からない。工学的な意味でクオリティを考えると、ある尺度に照らし合わせてその善し悪しを定量的に測れる指標ではある。たとえば、大きい方がクオリティが高いと決めると、AカップよりEカップの方がクオリティが高い。しかし、これはその尺度を定義したことによって恣意的に生まれたクオリティで、小さい方が希少価値がありステータスだという考えももちろんできる。
ということは、クオリティというのはこういう恣意的な定義がされる前に実在するように思える。
芸術の美と科学の美
クオリティと似たように言葉に、美というものがある。美とはおそらく芸術や音楽などに主に用いられる言葉である。ではあるが、技術者や科学者と接してみると、数式やプログラムのソースコードに美を見いだしている。たとえば、オイラーの公式の美しさや、巨大なシステム設計の美しさとかに彼らは美を感じているのだ。とすると、ここで疑問が浮かんでくる。芸術の美と科学の美は同じモノなのか？
この本でもこの問題についてはさらりと述べられているが、それほど考察はされていなかったので、ここで自分なりの回答を示したいと思う。美はおそらく、この本でいうところのクオリティよりも具象化されたモノなので、クオリティの理解には到達しないまでも近づいているのではと思う。
美であるが、端的に言うなら調和に集約されるのではないかと思う。おそらく、芸術的な美にまず求められるのは、ごく短時間で調和を感じられることではないだろうか。まず人が見て整っている、整列している、ある種の関係がバランスよい、意外な関係で成り立っているなどと、調和が理解出来るときに、人は芸術的な美を感じるのではないか。逆に、科学的な美は、長い時間かけて習得した事実と照らし合わせて、対象に調和が認められるときに美を感じるのではないかと思う。ということは、芸術的な美も科学的な美もその本質的なところは同じであるように思われる。もちろん、芸術にも何かしらの技法が凄くてそれに関して美しさを感じる人々もいるだろうが、そうするとそれはどんどん科学の美に近づいていくのではないだろうか。
では、調和が客観世界に存在するのか、主観世界にしか存在しないかという疑問が次に出てくる。これがなかなか難しくて、調和というのはおそらく、なにかしら数値化、数式化できるように思える。しかし、それを感じるセンス、教養がなければ美を感じることはできず、何人たりとも感じられない調和は美しいのかという疑問がわく。つまり、オイラーの公式が発見される前でもオイラーの公式は美しいのかという疑問が出てくる。ここまでくると自分には手の負えない問題となるのだが、本書ではたどり着いているようだ。色即是空、空即是色。
アンドロイドの感じる美
芸術的な美と科学の美について、同じだが理解に必要な時間的なスケールが重要ではないかと述べた。これはもしかしたら、速いがヒューリスティクスな思考回路であるシステム1と、遅いが論理的な思考回路であるシステム2のどちらで調和を感じるかかもしれない。システム1とシステム2とは、ファスト&スローで詳解されている思考回路の区別であるが、これと調和、美は関係ありそうだ。
とすると、もしもヒューリスティクスではなく、論理思考のみ行うアンドロイドが誕生したら、調和の受け取り方は大夫異なった様になりそうだ。コンピュータの場合、探索は幅優先か深さ優先かで行われるが、大勢のアンドロイドが幅方向で探索しているのにもかかわらず、ある気の狂ったアンドロイドが深さ優先で探索しつづけて、ある意外な調和を発見したときにのみ美しいと思われるのかもしれない。というわけで、アンドロイドの美は、人間の美とは一見全く違うモノにはなりそうではあるが、その本質は変わらないような気もする。将来は、人間は、アンドロイドの感じる美について講釈を受けて、全くわからんと言っていそうである。
以上が本書を読んで感じたことだが、明確な答えというものにたどり着いたという実感はないが、近づいたかなと言う感じである。世界は難しい。
