チェシャ猫の消滅定理

数学にプログラミング、素敵なもの何もかも。

2019 年のスライド一挙公開、あるいは 2020 年の方針

あけましておめでとうございます。2019 年は大変お世話になりました。2020 年も張り切っていきましょう。

さて、2019 年には結構な回数の外部発表を行いました。これらの発表内容のうち一部は単独のブログ記事としてまとめてありますが、機を逸してしまって記事化されていないものも相当数あります。そこで本記事では、2019 年中に行った発表を一覧としてまとめてみました。

2019 年の活動実績

2019 年の登壇は全部で 19 件でした。うち(先着や抽選ではなく)CFP に応募して採択されたものは 4 件です。

チェシャ猫が普段活動している領域は、Twitter の Bio にも書いてある通り、大きく「Kubernetes」「Haskell」「形式手法」の三つのカテゴリに分かれています。このカテゴリで登壇内容を分類したところ、以下のようになりました。

CloudNative に関わるもの(12 件)

CloudNative 技術に関しては 12 件の発表を行いました。ほとんどが Kubernetes のスケジューリングをテーマにしています。

この分野は勉強が活発に行われており LT の機会も多かったため、LT で単発の新機能を紹介し、長尺の発表ではそれらの諸機能を体系的にまとめて解説する、という構図になっています。特に Kubernetes Meetup Tokyo で顕著ですが、LT の倍率が高いので運頼みになりがちだったりします。

関数型プログラミングに関わるもの(4 件)

関数型プログラミングに関しては、Haskell および Elm をテーマとして 2 件ずつ計 4 件の発表を行いました。Haskell の 2 件は AltJS である GHCJS を取り上げているため、Elm も含めて 4 件すべてが Web フロントエンドに関する発表ということになります。

形式手法に関わるもの(2 件)

形式手法に関しては、モデル検査と定理証明それぞれ 1 件ずつの発表を行いました。件数としては少ないですが、両者はいずれも CFP 審査を通過して採択されており、かつ持ち時間もそれぞれ 60 分、45 分と長めの発表です。

関連して、いくつかの会社でモデル検査器のハンズオンを開催しました。ツールとしては Alloy を使用し、2 時間ずつ 2 回、計 4 時間で一通りの使い方を学ぶコースです。内容については Pixiv 社の shimashima さんが記事にしてくださっています。

inside.pixiv.blog

本来であればもう少しちゃんとパッケージ化して募集するところではありますが、もし今この記事を読んで興味を持った方がいらっしゃいましたら、ぜひご連絡いただければ幸いです。

その他(1 件)

上記のどのカテゴリにも該当しませんが、型による値レベルの制約を TypeScript で実現する話です。強いていうなら関数型プログラミングが近いかもしれません。

2019 年のスライド一覧

猫でもわかる Scheduling Framework

Kubernetes Meetup Tokyo #16 での発表です。

Kubernetes の Scheduler の拡張点をインタフェースとして切り出し、実行速度を保ったままプラガビリティを提供するためのプロジェクト Scheduling Framework について解説しました。

この発表を行った時点ではごく一部しか実装されておらず、まだまだ先が長そうな印象でしたが、最新の v1.17 ではかなり進展し、既存の kube-scheduler の実装を Framework として置き換える作業も進んでいます。

ccvanishing.hateblo.jp

君だけの最強 Scheduler を作ろう!

Docker Meetup Tokyo #28 での発表です。

Kubernetes の Scheduler をカスタマイズするための方法を複数挙げ、それぞれの守備範囲について解説しました。

上で触れた Scheduling Framework の他にも、もともと kube-scheduler に備わっているポリシーの指定方法や、Webhook として実装する Extender についても触れています。

ccvanishing.hateblo.jp

明日、業務で使える Scheduler Extender

Cloud Native Meetup Tokyo #7 での発表です。

これまでと同じく Kubernetes の Scheduler カスタマイズをテーマに据えていますが、この発表では Extender に焦点を絞り、4 箇所あるそれぞれの各頂点でどのような設定が可能なのかについて解説しています。

なお、スライド中で「実行中の Job が Preemption で中断される問題」について言及していますが、後になって Extender 以外にも Preempting を抑制する機能として PreemptingPolicy の設定が導入されました。これについては Docker Meetup Tokyo #31 で触れています。

雲の世界の共通語 CloudEvents って何?

Cloud Native Developer JP #11 での発表です。

Event-driven なアーキテクチャは Serverless 界隈でよくみられますが、その仕様は各ベンダごとにバラバラで相互運用性がありません。この問題を解決するために、イベント仕様の規格策定を目指す CNCF プロジェクト CloudEvents について概要を解説しました。

ちなみに CloudEvents 自体その後も継続してバージョンアップが行われており、Knative や Argo CD などが新しいバージョンに対応しているようです。

サンプルで学ぶ The Elm Architecture

Meguro.es #21 での発表です。なお、上に貼ったスライドは別イベントの際のものですが、内容の大筋は共通しています。

ミニマルなカウンタアプリを例として、The Elm Architecture と呼ばれる状態管理の仕組み、および外部 JavaScript ライブラリとの連携について解説しています。

GHCJS Miso による Haskell + Firebase 10 分間クッキング

Fun Fun Functional #1 での発表です。

GHCJS を使用すると、HaskellソースコードJavaScriptコンパイルしてブラウザ上で動かすことができます。この発表ではさらに Elm 風のアーキテクチャを持つフレームワーク Miso および JavaScript 呼び出しのための DSL である JSaddle を使用して、Firebase Realtime DB をバックエンドとした簡単なチャットアプリをライブコーディングで実装しました。

ccvanishing.hateblo.jp

Kubernetes v1.15 の新機能で Preemption を制御せよ

Docker Meetup Tokyo #31 での発表です。

Kubernetes には、Node のリソースに余裕がないときに優先度の高い Pod が作成された場合、すでに稼働している優先度の低い Pod の立ち退かせてリソースを確保する機能が備わっており、この機能は Preemption と呼ばれます。

Preemption はクラスタのリソース効率を高める上では重要ですが、同時に実行中の Job が中断されて途中結果が失われる可能性を含んでいます。この問題を解決するため、v1.15 では Preemption を抑制するための PreemptingPolicy と呼ばれる設定項目が導入されました。

ccvanishing.hateblo.jp

そのコンテナ、もっと「賢く」置けますよ?

CloudNative Days Tokyo 2019 での発表です。

Kubernetes の Scheduler に関して包括的に解説を行なっています。内容としてはそれまでに LT 等で触れたものがほとんどで新規性はありませんが、スケジューラについてあまり知らない人であってもこのスライドの内容を抑えれば一通りの知識が得られるよう、スケジューラの役割から始まって、大枠から徐々に解像度を上げることで学習曲線が緩やかになるように構成が工夫してあります。

ccvanishing.hateblo.jp

CircleCI + Kind による Kubetentes E2E テスト

CircleCI Community Meetup LT 大会 での発表です。

Kind は、Kubernetes の Node をコンテナ化することで、マルチノードクラスタをローカルで簡単に立ち上げられるようにするツールです。要するにコンテナが動く環境ならどこでも使い捨ての Kuberentes クラスタを作成することができるわけで、発表中ではこの Kind を CircleCI 上で起動させて E2E テストを行う方法を解説しました。

形式手法による分散システムの検証

builderscon tokyo 2019 での発表です。

例えば決済処理がマイクロサービスに分割されている場合、複数のサービスに対して整合性を保ったままコマンドを発行するには工夫が必要です。この発表では一つの手法として TCC (Try-Confirm/Cancel) パターンを取り上げ、TLA+ を用いたモデリングと検査について解説しています。

余談ですが、この発表はタイムテーブル的に超人気セッションの裏番組になってしまい、集客が厳しかったです。こちらを聞いてくれた方の反応は割と好意的だったので、内容自体はよかったと信じたい。

TypeScript における型レベルバリデーション

We Are JavaScripters! @36th での発表です。

TypeScript は構造的部分型を持つため、一部の型引数を使用せず捨てる、いわゆる幽霊型を作成しようとしてもコンパイル時にチェックが効きません。そこで、区別したい型ごとに異なるフィールドを持たせた Branded Type を利用する方法を解説しています。

Kind で量産する使い捨て Kubernetes

CI/CD Test Night #5 での発表です。

CircleCI Community Meetup と同じく Kind を利用した E2E テストに関する発表ですが、今回はイベントの趣旨に合わせて「CI を Kubernetes で行う場合にどうやってクラスタを準備するか」という視点から解説しています。

従来、CI 用に Kubernetes クラスタが必要な場合、選択肢は「Pull Request ごとに Namespace を作成」もしくは「Pull Request ごとにマネージドクラスタを振り出し」のいずれかでしたが、Kind の登場により、簡単にクラスタを立ち上げて使い捨てることが可能になりました。

ライブで学ぶ The Elm Architecture

Meguro.es #23 での発表で、Meguro.es #21 の続編のような形になっています。

内容自体は前回と似ており、簡単なチャットアプリで The Elm Architecture の仕組みを説明しています。ただし今回は単に図解するだけでなく、ライブコーディングの要領でその場で一つづつ機能を追加していくことで、各動作がどのように実装されるのかについて順を追って解説しました。

GHCJS による Web フロントエンド開発

Haskell Day 2019 での発表です。

内容は Fun Fun Functional #1 での発表をよりリッチにしたものです。Firebase Realtime DB によるリアルタイムチャット機能に加えて Firebase Authentication を使用した Google ログインを提供し、会場にいた参加者にその場で書き込んでもらうデモを行いました。デモで使用したアプリケーションは以下に公開されています。

github.com

賢く「散らす」ための Topology Spread Constraints

Kubernetes Meetup Tokyo #25 での発表です。

この発表では、Kubernetes v1.16 でアルファ機能となった Topology Spread Constraints を取り上げました。複数の Node に Pod が分散している状況であっても、それらの Node が同じ Availability Zone やラックにホスティングされていた場合、障害により Pod が全滅する可能性があります。この問題を解決するため、Topology Spread では Node に Label を付与してグループ化し、そのグループ単位での Pod の分散方法を指定することができます。

CloudNative を学ぶにはまず KInd より始めよ

CloudNative Developer JP #13 での発表です。

ここまでにも何度か取り上げている Kind と、Topology Spread Constraints を組み合わせて発表しました。Topology Spread Constraints は実はかなりピーキーな機能で、設定を誤ると条件を満たす Node が見つからずに Pod が配置できない状態に陥ることがあります。ローカルに Kind で Kubernetes クラスタを作成した上でこの問題を実際に再現し、さらに修正するデモを行いました。

テスト駆動開発から証明駆動開発へ

July Tech Festa 2019 での発表です。

builderscon tokyo 2019 では TLA+ によるモデル検査を扱いましたが、こちらのテーマは定理証明です。

前半では builderscon と同様、通常のテストと分散システムとの相性の悪さについて述べ、分散システムに用いられるカオスエンジニアリングと対比する形で形式手法の考え方を導入します。また後半では、Curry-Howard 対応について触れたあと、Coq とそのフレームワークである Verdi を使用して分散システムを証明する仕組みを概説しています。

kube-batch による Gang Scheduling

Kubernetes Invitational Meetup Tokyo #4 での発表です。

複数の Pod が通信し合って実行を進めるような Job をデプロイする場合、一部の Pod だけが先に配置された状態で Node のリソースを使い切ってしまうと、後続の Pod が配置できずにデッドロックに陥ることがあります。これを防ぐため、特定のグループに属する Pod を一度に全て配置するか、あるいは全て Pending のまま留めるかという All of Nothing の配置戦略を Gand Scheduling あるいは CoScheduling と呼びます。

今回紹介した kube-batch は Gang Scheduling を実現する特殊スケジューラの一種です。Gang Scheduling 以外にも、複数のキューを定義してクラスタのリソースをキュー間で均等に配分するなどの機能が提供されています。

「詰める」と「散らす」の動力学

OpenShift.Run 2019 での発表です。

内容としては CloudNative Days Tokyo 2019 を元にした上で、いくつかの要素を追加して再構成しています。特に、CloudNative Days Tokyo 2019 時点では実装されていなかった Topology Spread Constraints への言及が追加されていますが、これは Pod の分散戦略を考える上で非常に重要な要素です。

ccvanishing.hateblo.jp

2020 年の方針

さほど具体的になっているわけではありませんが、今後の展開についていくつか考えていることがあるので、振り返りのついでにここで表明しておきたいと思います。

カテゴリ間の連携

冒頭で述べた通り、現在のチェシャ猫の活動カテゴリは「Kubernetes を中心とした CloudNative 技術」「Haskell をはじめとする関数型プログラミング」「形式手法、特にモデル検査」の三つに分かれています。しかし残念なことに、現状それぞれのカテゴリでそれぞれ登壇するに留まっており、複数カテゴリを扱っていることがうまく活かせていません。

そこで 2020 年は、これらの知見をうまくつなぎ合わせることを目標にしたいと思います。三つのうち関数型プログラミングと形式手法は比較的近い分野ですが、これらと CloudNative を組み合わせようとする人はあまり見ないため、独自色が出せる部分なのではないかと睨んでいます。

より具体的には、「CloudNative + 形式手法」の組み合わせでもう少し面白いことができないかを検討中です。あるいはその過程で定理証明を採用することになれば、おそらくは Extraction の関係で実装には関数型プログラミング言語を使用することになるでしょう。いずれにせよ、複数カテゴリを横断したネタを作るのが目標です。

登壇以外の活動の充実

2019 年の活動は登壇に偏りすぎました。

今回並べた 19 件のスライドには、他に日本語情報が存在しないようなトピックも相当量含まれており、それなりに価値があるものだと自負しています。しかしブログのような散文と比較したとき、登壇スライドに載せられる(あるいは載せるべき)情報量はどうしても限られており、また検索性にも乏しいことから、インターネット上に蓄積される情報源としてはどうしても劣ります。

また、登壇だけにエフォートを割いていると、結局のところ「単に新しい情報を発掘してきて解説する人」になりがちで、自分自身、居心地の悪さを感じることが少なくありませんでした。少し前に Qiita で話題になった「Web エンジニア業界に感じた違和感」とも共通するものがあります。

そこで 2020 年は、もう少し実務的な取り組みに力を入れたいと思います。より具体的には、kubernetes/kuberetens をはじめとする OSS へのソースコード貢献を継続的に行うのが目標です。また、登壇した際にはスライド公開に加えて、扱った要素技術について、ある程度踏み込んだ解説を参照可能な形でブログに記録しておきたいところです。

海外カンファレンスでの登壇

読んで字の如く、一度はやってみたい海外登壇です。まったくノープランですが、とりあえず出せそうなカンファレンスを見つけるところから始めたいと思います。

まとめ

本記事では、2019 年に行った計 19 回の外部発表について、スライド公開までで終わっていてブログ化されていなかったものも含め、簡単な解説を付けて一覧にしました。

さらに 2020 年の活動方針として「CloudNative と形式手法の統合を狙うこと」「登壇以外の活動にも力を入れること」「海外カンファレンスで登壇すること」の三つを設定しました。

ここで設定した 2020 年の目標が果たして達成されるのか、判明するのはまた 1 年先ですが、それはまた別の話。