はてなブックマーク

こんにちは、チェシャ猫です。 先日開催された CloudNative Days Tokyo 2022 で、SMT ソルバを用いた AWS のネットワーク検査機能、VPC Rechability Analyzer と VPC Network Access Analyzer について話してきました。公募 CFP 枠です。 イベントサイトにて録画も視聴可能です。 event.cloudnativedays.jp 今回の登壇は「事前録画を提出」「当日リモートで登壇」「現地で登壇」のいずれの方式が選択可能だったのですが、自分は現地で登壇しました。 現地参加者全員が一つの部屋に集まる Keynote では意外と人がいるなという印象でしたが、午後のブレイクアウトセッションでは 6 部屋あったこともあり、自分のセッションの現地参加者は 10 数人程度でした。 完全オフラインだった頃の熱気には及びませんが、

こんにちは、チェシャ猫です。 先日開催された AWS Dev Day 2022 Japan で、サーバーレスコンピューティングの形式化について発表してきました。公募 CFP 枠です。 www.youtube.com github.com ちなみに会場は観葉植物が生い茂る Amazon 品川オフィスで、講演者向けには個室の楽屋が用意されており（滞在時間は講演直前の 15 分程度ですが）、全体的にとてもゴージャスな感じでした。配信設備も本格的でしたが、話す側としては照明が眩しくてやりづらかったです。 講演概要 AWS Lambda を初めとするサーバーレスコンピューティング基盤には、 複数の関数が同時に実行され共有リソースにアクセスしうる、本質的に並行システムである Warm Start により関数インスタンスが内部状態を残したまま再利用されうる 一つのリクエストに対して複数回の実行が行われう

こんにちは、チェシャ猫です。 先日開催された AWS Dev Day Online Japan 2021 で、AWS の VPC Reachability Analyzer とそのバックエンドである Tiros について発表してきました。公募 CFP 枠です。 www.youtube.com 講演概要 このプレゼンの大きな目標は、VPC Reachability Analyzer のバックエンドである検査エンジン Tiros の論文 [Bac19] を解説することです。そのための道筋として、Section 1 で VPC Reachability Analyzer の機能を簡単に紹介した後、Section 2 でその要素技術である SMT ソルバの仕組みを解説し、最後に Section 3 として VPC ネットワークの意味論を SMT ソルバ用にエンコーディングする方針について解説します

こんにちは、チェシャ猫です。 先日開催された DevOpsDays Tokyo 2021 で Infrastructure as Code のテストについて発表してきました。公募 CFP 枠です。 今回の発表は、昨年の CloudOperatorDays Tokyo 2020 での講演をほぼそのまま再現しています。内容については前回登壇時に詳細な解説記事を書いたので、こちらもご参照ください。 ccvanishing.hateblo.jp オンサイト登壇 ここしばらく、どのカンファレンスもリモート開催がデフォルトになっていましたが、今回は久しぶりに会場まで行って登壇してきました。最後にオンサイトでプレゼンしたのが 2020 年の 3 月 26 日 なので、実に 1 年ぶりです。 実際には会場で参加していたのはほぼ関係者オンリーで、各ホールに数人ずつといった程度の人数でした。ただ登壇する側とし

こんにちは、チェシャ猫です。 インフラ技術のカンファレンス July Tech Festa 2021 winter で、形式手法ツール TLA+ が CockroachDB の設計に使用された事例について発表してきました。公募 CFP 枠です。 www.youtube.com 今回の登壇は、昨年の CloudNative Days Tokyo 2020 と同じ題材を扱っています。ただ、前回より持ち時間が長くなった分、前回のスライドで説明不足だった部分を拡充してあります。特に、CockroachDB 以外の TLA+ 採用事例や、分散システムにおける Chaos Engineering の位置付けについて解説を追加しました。 なお、前回の登壇報告は以下の記事をご参照ください。 ccvanishing.hateblo.jp 当日出た質問 実時間を含む性質 今回の時相論理では「いつか成り立つ」と

はじめに Kubernetes において、Pod を配置するための Node を決定する手続きをスケジューリングと呼び、デフォルトのクラスタでは kube-scheduler がその責務を担っています。本記事ではこの kube-scheduler のソースコードを時系列に沿って追いつつ、どのようなロジックで Pod を配置する Node が決定されるのかを解説します。 なお、本記事は Kubernetes の内部実装について学ぶ勉強会 Kubernetes Internal #3 の補足資料を意図して執筆されました。本文中で参照しているソースコードのバージョンは v1.19.4 です。 Kubernetes Internal #3 録画 スケジューラの概要 ソースコードを読むに先立つ予備知識として、スケジューリングの大まかな流れと Scheduling Framework の概要に触れてお

こんにちは、チェシャ猫です。先日行われた第 7 回 Web System Architecture 研究会で形式手法について発表してきました。 普段、形式手法について登壇する際は具体例な検証例を出すことが多いですが、今回は理論側に寄せたサーベイになっています。 はじめに 本セッションでは、安全性-活性分解 (safety-liveness decomposition) と呼ばれる一連の結果について解説する。安全性-活性分解は、システムの仕様が与えられた時、それを安全性 (safety) および活性 (liveness) と呼ばれる、よりシンプルな特徴付けを持つクラスに分解して扱うための方法論である。さらにセッションの後半では、安全性と活性の組み合わせ以外にも提案されている派生的な特徴付けについても述べる。 Web アプリケーションと形式手法 システムやプログラムの性質を何らかの数学的な対象

こんにちは、チェシャ猫です。先日行われた CloudNative Days Tokyo 2020 で、形式手法ツール TLA+ が CockroachDB の設計に使用された事例について発表してきました。公募 CFP 枠です。 講演概要 CockroachDB は、Google Spanner の系譜に連なるいわゆる NewSQL データベースの一種です。 強い一貫性や ACID トランザクションといった従来の関係データベースが持つ「良い特徴」を残したまま、従来の関係データベースが苦手としていた水平スケーリングにも優れるのが特徴です。CockroachDB 自身は「地理分散 (geo-distributed) データベース」を標榜しています。 このような CockroachDB の特徴は、内部のデータ保持の方法に由来します。データは内部的には Key-Value レコードの形を取っていて、

こんにちは、チェシャ猫です。先日行われた Cloud Operator Days Tokyo 2020 で、Infrastructure as Code のテストについて発表してきました。公募 CFP 枠です。 Cloud Operator Days Tokyo 2020 は今回が初開催のイベントですが、昨年 CloudNative Days Tokyo と併設されていた OpenStack Days Tokyo が前身となっているようです。 ASCII.jp：ふれあえるオンラインイベント「Cloud Operator Days Tokyo 2020」は泥臭い？ 今年は OpenStack に限らず広く運用がテーマにされていますが、セッションのラインナップを見る限り、他のイベントよりもオンプレミス・エンタープライズ的な色が強く出ているように感じられます。 ちなみに、チェシャ猫の発表は事前ア

あけましておめでとうございます。2019 年は大変お世話になりました。2020 年も張り切っていきましょう。 さて、2019 年には結構な回数の外部発表を行いました。これらの発表内容のうち一部は単独のブログ記事としてまとめてありますが、機を逸してしまって記事化されていないものも相当数あります。そこで本記事では、2019 年中に行った発表を一覧としてまとめてみました。 2019 年の活動実績 2019 年の登壇は全部で 19 件でした。うち（先着や抽選ではなく）CFP に応募して採択されたものは 4 件です。 チェシャ猫が普段活動している領域は、Twitter の Bio にも書いてある通り、大きく「Kubernetes」「Haskell」「形式手法」の三つのカテゴリに分かれています。このカテゴリで登壇内容を分類したところ、以下のようになりました。 CloudNative に関わるもの（12

先日行われた OpenShift コミュニティのイベント OpenShift.run 2019 にて、Kubernetes Scheduler とその関連ツールについて講演してきました。公募 CFP 枠です。 OpenShift のイベントでありながら、OpenShift についてはまったく触れずひたすら Kubernetes の内部実装を解説する異色の登壇でした。実際、40 分枠の講演の中で（RedHat 社以外も含め）ベンダニュートラルな立場で登壇したのは自分だけだったようです。これは私見ですが、逆に言えばそういう内容でも CFP 採択されているというのは、運営側も「単なるマーケティングイベントにしない」というスタンスなのかなと思います。 なお今回の発表は、CloudNative Days Tokyo 2019 での講演が元になっています。こちらについては参考文献や当日出た質問など補足

はじめに マルチスレッドで動作するプログラムの設計は難しい問題です。個々のスレッドの動作は単純に見えても、複数が並行して動作する場合の動作は組み合わせ論的に複雑になります。また、タイミングに依存する不具合は狙って再現することが難しく、通常の単体テストによる検出にも限界があります。 そんなとき、有効な手法がモデル検査です。システムの取りうる状態をあらかじめ網羅的に探索することで、「実際に動作させた際にごく低い確率で踏むバグ」であっても、動作させることなく設計段階で発見することが可能になります。 ところでちょうど先日、デッドロック発見器を自作するハンズオンに参加する機会がありました。内容は非常にシンプルなモデル検査器を実装するというもので、せっかくなのでそのときの成果物を Go のパッケージとしてまとめたものを以下に公開しました。 github.com 以下、このパッケージで何ができるのかを具

先日行われた Fun Fun Functional (1) で、Haskell と Firebase を使った Web アプリの作り方について発表してきました。 使用した要素技術は、GHCJS 上のフレームワーク Miso と、Fireabse SDK を呼び出すための DSL である JSaddle です。 GHCJS は Haskell のソースコードを JavaScript に変換するコンパイラで、GHC をフォークすることによって開発されています。 github.com Miso は GHCJS 上で The Elm Architecture を実装するためのフレームワークです。Miso では事実上サーバサイドで書けない Elm と異なり、サーバサイドとの Model の共有や、初回アクセス時の HTML をサーバ側で構築するサーバサイドレンダリング (SSR) の仕組みが提供され

先日行われた July Tech Festa 2018 で、モデル検査を使った分散アルゴリズムの検証について発表してきました。 前半はオートマトンによるシステムの記述と検査の基礎について、後半は三種類のツール SPIN、TLA+、P による記述方法の紹介、といった内容です。 後半のソースコード紹介が散文的な感じになってしまって、いまいちメリットが伝わらない感じだったので、次回があればもっとエモいスライドにしようと思います。 分散アルゴリズムの形式化 定理証明による検証 今回の話の流れとして「分散システムにはモデル検査が有効」と述べていますが、必ずしも定理証明が分散システムの検証に向かないという趣旨ではありません。 例えば、定理証明器 Coq によって分散システムを証明するためのフレームワークとして Verdi が開発されています。 github.com さらに、Coq は実行可能なコードも

だいぶ日が空いてしまって今更ですが、先日行われた Kubernetes Meetup Tokyo #10 で、v1.8*1 から導入された新機能 Preemption について発表してきました。 Preemption は、Kubernetes クラスタのリソースが不足した際に、優先度が低い Pod を追い出して優先度が高い Pod の稼働を保証する仕組みです。 当日は時間が不足気味だったので、説明不十分だったかなと思われる点についていくつか補足しておきます。 Priority の指定について スライド中では詳しく説明しませんでしたが、ユーザは直接 Pod（や Deployment 中の Pod Template）に対して Priority を指定するのではなく、 Priority の値を保持する PriorityClass を作成する Pod Template には priorityCla

だいぶ日が空いてしまって今更ですが、先日行われた JAWS DAYS 2018 で登壇してきました*1。モデル検査器 Alloy を使って AWS の IAM を検証してみるという内容です。 形式手法 × AWS というテーマではこれまでにもいくつかのイベントで発表していますが、題材はネットワーク関連の検証がメインでした。 ccvanishing.hateblo.jp ccvanishing.hateblo.jp ccvanishing.hateblo.jp さすがに同じことばかり話していても芸がないので、今回は新ネタとして IAM を投入してみました。CFP も Security Slot で採択されています。 現状と既存手法の限界 IAM 設定の難しさ いや、説明するまでもなく実際ややこしいですよね。一つ一つはさほど複雑ではないんですが、多数の設定項目が互いに影響し合うため最終的な影響

このエントリは Kubernetes Advent Calendar 2017 の 23 日目の記事です。ちなみに昨日は takezaki さんの「GCBを利用したContinuous Delivery環境」でした。 LT で使用したスライド 先日、市ヶ谷Geek★Night #16 の 10 分 LT 枠で、CoreOS 社によるコンテナ実装 rkt とその Kubernetes 連携について発表してきました。今回のエントリはこの LT の内容を補足しつつ、実際に手を動かして rkt を試せるような構成にしてあります。 Hello, rkt! rkt は、Docker の対抗馬として CoreOS によって開発されたコンテナ管理ツールです。プロジェクトの初期は普通に Rocket という名前でコマンド名が rkt という扱いでしたが、途中からツールの名前自体が rkt に変更されました。

主としてテスト時のために、現在時刻を操作する Haskell ライブラリを作成しました。Hackage にも登録済みです。 github.com 試しに次のコードを実行してみましょう。getCurrentTime しているはずなのに、返ってくる値が 1985 年 10 月 26 日になっているはずです。 module Main where import Control.Monad.TimeMachine import Control.Monad.Trans ( liftIO ) main :: IO () main = backTo (the future) $ do t <- getCurrentTime liftIO . putStrLn $ "We are at " ++ show t 作成の動機 一般論として、現在時刻に依存する関数やメソッドはテストが難しくなります。例えば次の関数

Haskell の GitHub レポジトリを眺めてみると、有名ライブラリであってもスター数が意外と少ないことがあります。かの Yesod ですら本記事執筆時点で 1,794 個であり、Rails の 36,933 個や Django の 28,165 個と比較すると文字通り桁違いです。 スター数は必ずしも OSS としての評価や価値を反映しませんし、そもそも Haskell ユーザの絶対数が少ないからと言ってしまえばそれまでなのですが、若干寂しい感じがしません？ 一方、先日 id:teppeis さんが 依存しているライブラリにスターを送る npm ツール を公開されていました。そこで真似して作ってみた Haskell 版が以下です。 github.com セットアップ後、自分の Cabal / Stack プロジェクトのルートディレクトリで実行するだけで OK。package.caba

先日行われた JJUG CCC 2017 Spring で、JVM 上で動作する Haskell について発表してきました。 思ったほど怖くない！ Haskell on JVM 超入門 #jjug_ccc #ccc_l8 from y_taka_23 www.slideshare.net メインになるコンテンツはふたつの JVM 言語、Frege と Eta です。 今回はあくまでも Java のイベントなので、発表前半では Haskell の基本概念、特にモナドについてそれなりの時間を割いて説明してみました。さらにそれを踏まえて後半ではモナドを利用した Java ライブラリの呼び出しに焦点を当て、Frege と Eta それぞれの戦略の違いについて解説しています。 そもそも Haskell on JVM というマニアックで Java そのものと無関係なテーマ、かつ時間的に最後の枠というこ

先日、ニコニコ超会議内で行われた「超技術書典」にて、LiquidHaskell の同人誌でサークル参加してきました。 lh101.dodgsonlabs.com 技術書典 2 ではそこそこの部数が出た ので Haskell 同人誌の需要はゼロではないと踏んでいたのですが、びっくりするぐらい売れません でした。とりあえず後に続く人が同じ轍を踏まないように、今回の様子について記録しておきます。 頒布物 頒布した同人誌は以下の 2 種類です。前者は技術書典 2 で頒布したものの増刷、後者は id:kazeula さんから委託を受けた新刊です。 入門 LiquidHaskell −篩型による静的コード解析− GHCJS 入門 −Haskell による JavaScript 開発− 持ち込んだ（冊子版の）部数と実際に売れた部数は以下の通りでした。 入門 LiquidHaskell : 持ち込み 12

このエントリは Haskell Advent Calendar 2016 および Formal Method Advent Calendar 2016 の 23 日目の投稿です。のはずでしたがすでに日付が変わりました。謹んでお詫び申し上げます。 ちなみに 22 日目の担当者はそれぞれ Haskell Advent Calendar 2016 : heredocsの紹介 - Qiita Formal Method Advent Calendar 2016 : 農夫 山羊 キャベツ 狼 - Qiita です。偶然ですが同じ方が執筆担当ですね。 さて、本エントリでは Haskell の型の表現力をより豊かにする仕組み、 LiquidHaskell について概要を紹介します。使用するサンプルコードは Samples of Verification by LiquidHaskell · GitHub

先日、毎年恒例のなごや LT 大会 NGK2016B / 名古屋合同懇親会 2016 忘年会 で発表してきました。 机上の Kubernetes - 形式手法で見るコンテナオーケストレーション #NGK2016B from y_taka_23 www.slideshare.net 当日の動画は NGK 2016B LT #2 - YouTube から見ることができます。 ちなみに NGK での発表は 4 年連続 4 回目です。今回も含めてすべてモデル検査が題材になっています。 NGK2013B : Alloy ではじめる簡単モデル検査 NGK2014B : 猫でもわかる！ モデル検査器 SPIN 入門 (ブログ記事) NGK2015B : AWS は形式手法の夢を見るか？ - モデル検査器 Alloy によるインフラ設計 (ブログ記事) Kubernetes に関わる役者たち さすがに 5

先日行われた JAWS FESTA 東海道 2016 で登壇してきました。 形式手法と AWS のおいしい関係。- モデル検査器 Alloy によるインフラ設計技法 #jawsfesta from y_taka_23 www.slideshare.net テーマは以前 AWS Summit で発表したものと同じですが、前回が 5 分の LT だったのに比べて今回は 25 分の枠を頂きました。そこで、形式手法を用いる動機を中心に据えた前回と比較して、以下のような実践的なトピックを充実させてあります。 Alloy を使うためにの最低限必要な言語機能を知る シンプルな Web サーバ周りのネットワークについて、仕様から設計を導出する ちなみに前回の AWS Summit 2016 での発表に関してはこちらから。 ccvanishing.hateblo.jp 寄せられた質問 発表後に頂いたいくつか

先日行われた AWS Summit Tokyo 2016 で、形式手法のインフラ設計への応用について発表してきました。 形式手法で捗る！インフラ構成の設計と検証 from y_taka_23 www.slideshare.net モデル検査器 Alloy を利用して AWS の設定を検査する、という内容の LT で、昨年 12 月の NGK2015B でも同じテーマについて話しています。よければ以下の記事も合わせてお読みください。 ccvanishing.hateblo.jp NGK2015B の発表ではサンプルコードの紹介に比較的時間を割いているのに対して、今回の発表では「動機」の部分によりウェイトを置いた構成になっています。 なぜ形式手法なのか？ 今回のテーマを一言でまとめると以下のようになります。 インフラ構成が「秘伝のタレ」と化すのをどう防ぐべきか？ ある程度の規模のインフラを長期

先日、毎年恒例のなごや LT 大会 NGK2015B / 名古屋合同懇親会 2015 忘年会 で発表してきました。 AWS は形式手法の夢を見るか？ - モデル検査器 Alloy によるインフラ設計 from y_taka_23 www.slideshare.net 当日の動画は [3] NGK2015B（名古屋合同懇親会 2015 忘年会） - YouTube から見ることができます。 TL;DR AWS でインフラ運用中 でも設定が大人の都合でカオスになりがちだったりして辛い よろしい、ならば形式手法だ サンプルコードを動かしてみよう！ まずはインストールしてみる 公式ページ Alloy - download から、jar ファイルで提供されているものをダウンロードしましょう。 java -jar alloy4.2.jar でウィンドウが起動すれば OK です。 なお、dmg 版も提供