#技術書典 16 で Go を使って #自作モデル検査器 をつくる本を頒布します - チェシャ猫の消滅定理
こんにちは、チェシャ猫です。 今回、技術書典 16 にて、新刊『モデル検査器をつくる〜Goで実装して学ぶ形式手法〜』を頒布します。 techbookfest.org どんな本？ ただツールを使うだけの形式手法から、君の手でつくる形式手法へ。Go 言語でモデル検査器を実装しながら学ぼう！ 書名の通り、Go でモデル検査器を実装する本です。Pramo 言語と名づけた本書オリジナルのモデリング言語を定義し、その可視化器と検査器を作成します。 Pramo 言語は、ある種のマルチスレッドをサポートするプログラミング言語であり、Go の埋め込み DSL として記述されます。例えば有名な「食事する哲学者」は以下のように実装されます。 func badPhilosopher(name procName, right, left lockName, hold varName) process { retur
AWS Dev Day 2022 Japan に「サーバーレスは操作的意味論の夢を見るか？」というタイトルで登壇してきました - チェシャ猫の消滅定理
こんにちは、チェシャ猫です。 先日開催された AWS Dev Day 2022 Japan で、サーバーレスコンピューティングの形式化について発表してきました。公募 CFP 枠です。 www.youtube.com github.com ちなみに会場は観葉植物が生い茂る Amazon 品川オフィスで、講演者向けには個室の楽屋が用意されており（滞在時間は講演直前の 15 分程度ですが）、全体的にとてもゴージャスな感じでした。配信設備も本格的でしたが、話す側としては照明が眩しくてやりづらかったです。 講演概要 AWS Lambda を初めとするサーバーレスコンピューティング基盤には、 複数の関数が同時に実行され共有リソースにアクセスしうる、本質的に並行システムである Warm Start により関数インスタンスが内部状態を残したまま再利用されうる 一つのリクエストに対して複数回の実行が行われう
VPC Reachability Analyzer と形式手法 - チェシャ猫の消滅定理
こんにちは、チェシャ猫です。 先日開催された 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 ソルバ用にエンコーディングする方針について解説します
July Tech Festa 2021 で IAM Access Analyzer と Zelkova について話してきました - チェシャ猫の消滅定理
こんにちは、チェシャ猫です。 先日開催された July Tech Festa 2021 で、AWS のアクセス制御検査ツール Zelkova について発表してきました。公募 CFP 枠です。 techfesta.connpass.com 講演概要 www.youtube.com 一般に、AWS 上のリソース設定を変更したときに何が起こるのかを事前に検査するのは難しい作業です。特に、複数の設定がマージされた結果として最終的なアクセス許可が決まるような場合、単独の項目をルールベースでチェックするだけでは限界があります。 今回の発表中では、インフラに対する検査の水準を以下の 3 つのレベルに分けて定式化しました。 Level 1：構文論的な検査。テンプレートが文法的に正しいかどうかを確かめる Level 2：ヒューリスティックな検査。意図した性質が成り立つかどうかを、特定の設定項目に関する条件と
Kubernetes: kube-scheduler をソースコードレベルで理解する - チェシャ猫の消滅定理
はじめに Kubernetes において、Pod を配置するための Node を決定する手続きをスケジューリングと呼び、デフォルトのクラスタでは kube-scheduler がその責務を担っています。本記事ではこの kube-scheduler のソースコードを時系列に沿って追いつつ、どのようなロジックで Pod を配置する Node が決定されるのかを解説します。 なお、本記事は Kubernetes の内部実装について学ぶ勉強会 Kubernetes Internal #3 の補足資料を意図して執筆されました。本文中で参照しているソースコードのバージョンは v1.19.4 です。 Kubernetes Internal #3 録画 スケジューラの概要 ソースコードを読むに先立つ予備知識として、スケジューリングの大まかな流れと Scheduling Framework の概要に触れてお
CloudNative Days Tokyo 2020 で CockroachDB と TLA+ について話してきました - チェシャ猫の消滅定理
こんにちは、チェシャ猫です。先日行われた CloudNative Days Tokyo 2020 で、形式手法ツール TLA+ が CockroachDB の設計に使用された事例について発表してきました。公募 CFP 枠です。 講演概要 CockroachDB は、Google Spanner の系譜に連なるいわゆる NewSQL データベースの一種です。 強い一貫性や ACID トランザクションといった従来の関係データベースが持つ「良い特徴」を残したまま、従来の関係データベースが苦手としていた水平スケーリングにも優れるのが特徴です。CockroachDB 自身は「地理分散 (geo-distributed) データベース」を標榜しています。 このような CockroachDB の特徴は、内部のデータ保持の方法に由来します。データは内部的には Key-Value レコードの形を取っていて、
【#CODT2020 解説】Infrastructure as Code の静的テスト戦略 - チェシャ猫の消滅定理
こんにちは、チェシャ猫です。先日行われた 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 に限らず広く運用がテーマにされていますが、セッションのラインナップを見る限り、他のイベントよりもオンプレミス・エンタープライズ的な色が強く出ているように感じられます。 ちなみに、チェシャ猫の発表は事前ア
状態機械を合成してデッドロックを検出できる Go 言語パッケージを作ってみました - チェシャ猫の消滅定理
はじめに マルチスレッドで動作するプログラムの設計は難しい問題です。個々のスレッドの動作は単純に見えても、複数が並行して動作する場合の動作は組み合わせ論的に複雑になります。また、タイミングに依存する不具合は狙って再現することが難しく、通常の単体テストによる検出にも限界があります。 そんなとき、有効な手法がモデル検査です。システムの取りうる状態をあらかじめ網羅的に探索することで、「実際に動作させた際にごく低い確率で踏むバグ」であっても、動作させることなく設計段階で発見することが可能になります。 ところでちょうど先日、デッドロック発見器を自作するハンズオンに参加する機会がありました。内容は非常にシンプルなモデル検査器を実装するというもので、せっかくなのでそのときの成果物を Go のパッケージとしてまとめたものを以下に公開しました。 github.com 以下、このパッケージで何ができるのかを具
Fun Fun Functional (1) で Haskell と Firebase を使ってライブコーディングしてきました - チェシャ猫の消滅定理
先日行われた 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) の仕組みが提供され
Kubernetes Meetup Tokyo #16 で Scheduling Framework について話してきました - チェシャ猫の消滅定理
先日行われた Kubernetes Meetup Tokyo #16 で、現在 Scheduling SIG で進められているプロジェクト Scheduling Framework について発表してきました。 Kubernetes では、Pod をどの Node に配置するかを決める手続きをスケジューリングと呼びます。 古典的な Kubernetes の用途、すなわち通常の long-running なサーバ群の管理においては、Pod のスケジューリングは比較的シンプルな問題でした。すなわち、Node の障害時でも可用性が保てるように Pod を複数の Node に散らし、一度立ち上がった Pod は基本的に動き続ける、というシナリオです。 しかし、Kubernetes は既にコンテナスケジューラのデファクトを獲得し、様々な性質を持ったアプリケーションがデプロイされる基盤となりました。この
Kubernetes Meetup Tokyo #10 で Pod の Preemption について話してきました - チェシャ猫の消滅定理
だいぶ日が空いてしまって今更ですが、先日行われた Kubernetes Meetup Tokyo #10 で、v1.8*1 から導入された新機能 Preemption について発表してきました。 Preemption は、Kubernetes クラスタのリソースが不足した際に、優先度が低い Pod を追い出して優先度が高い Pod の稼働を保証する仕組みです。 当日は時間が不足気味だったので、説明不十分だったかなと思われる点についていくつか補足しておきます。 Priority の指定について スライド中では詳しく説明しませんでしたが、ユーザは直接 Pod（や Deployment 中の Pod Template）に対して Priority を指定するのではなく、 Priority の値を保持する PriorityClass を作成する Pod Template には priorityCla
猫でもわかる Vertical Pod Autoscaler - チェシャ猫の消滅定理
先日行われた Kubernetes Meetup Tokyo #13 で、Vertical Pod Autoscaler (VPA) について発表してきました。 VPA は、各コンテナの Resource Request の値を自動的に調整してくれるコンポーネント群です。必要とするリソース（CPU、メモリ）量があらかじめ推測しにくいアプリケーションに対して、実績に基づいてそれらしい値を決めたい場合に効果を発揮します。 本記事ではスライドの補足として、VPA が動作する流れをクラスタ上での実際の挙動を通じて確認し、また内部実装についても踏み込んで解説します。 なお、本記事中で引用している仕様やソースコードは執筆時点で最新のコミット ab9c27e を基準にしています。 github.com はじめに Kubernetes の Pod には、コンテナごとにリソース使用量を指定する機能があります
elm/time の使い方 - チェシャ猫の消滅定理
はじめに 先日、Elm v0.19 がリリースされました。公式ライブラリのリポジトリが elm-lang から elm に変更され、その中身も大きく再構成されています。 本記事では、これらの変更のうち特に時刻や日付の扱いに関する部分について、新しい API の使い方を含めて簡単に解説します。 v0.18 における時刻の扱い v0.18 では、時刻を扱う機能は標準パッケージ elm-lang/core の中で提供されていました。時刻を扱う Time モジュールと日付を扱う Date モジュールで、それぞれデータ型や関数が定義されているのが特徴です。 なお、旧バージョンのライブラリは現在 Elm Packages の検索にはヒットしない ので、中身を確認するためには直接 URL にアクセスする必要があります。 旧 Time モジュール Time - core 5.1.1 時刻を扱う Time
詳解！ Elm における Fuzzing - チェシャ猫の消滅定理
先日行われた We Are JavaScripters! @23rd で、Elm のテストフレームワーク elm-test に搭載されている Fuzzing 機能について発表してきました。 Fuzzing を利用するとテストデータを自動で生成することができるため、例えば「encode と decode を行うと元に戻る」といった、入力に依存しない 関数の性質に関するテスト をより簡単かつ効率的に実装することができます。 さらに、後で詳しく解説する通り、elm-test の Fuzzer にはバグが起こりやすいエッジケースを集中的に生成してくれるというメリットもあります。 elm-test の使い方は、すでに偉大なる先達によって大部分が解説済みです。普通にテストする上では、これらの内容を押さえておけば困ることはないでしょう。 [Elm] Fuzzer でテストデータを量産しよう (by ji
July Tech Festa 2018 で分散システムの検証について話してきました / #JTF2018 - チェシャ猫の消滅定理
先日行われた July Tech Festa 2018 で、モデル検査を使った分散アルゴリズムの検証について発表してきました。 前半はオートマトンによるシステムの記述と検査の基礎について、後半は三種類のツール SPIN、TLA+、P による記述方法の紹介、といった内容です。 後半のソースコード紹介が散文的な感じになってしまって、いまいちメリットが伝わらない感じだったので、次回があればもっとエモいスライドにしようと思います。 分散アルゴリズムの形式化 定理証明による検証 今回の話の流れとして「分散システムにはモデル検査が有効」と述べていますが、必ずしも定理証明が分散システムの検証に向かないという趣旨ではありません。 例えば、定理証明器 Coq によって分散システムを証明するためのフレームワークとして Verdi が開発されています。 github.com さらに、Coq は実行可能なコードも
猫でもわかる rkt + Kubernetes - チェシャ猫の消滅定理
このエントリは 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 ライブラリ time-machine を作ってみました - チェシャ猫の消滅定理
主としてテスト時のために、現在時刻を操作する 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 作成の動機 一般論として、現在時刻に依存する関数やメソッドはテストが難しくなります。例えば次の関数
Kubernetes Meetup Tokyo #7 で Serverless について話してきました - チェシャ猫の消滅定理
先日行われた Kubernetes Meetup Tokyo #7 で、Kubernetes 上で動作する Serverless フレームワークについて発表してきました。 Kubernetes でも Serverless したい！ #k8sjp from y_taka_23 www.slideshare.net Serverless on Kubernetes を謳うツールはいくつかありますが、今回はそのうち Kubeless と Fission に焦点を当て、それぞれのアーキテクチャの違いを比較してみました。 当日の補足 Twitter 上で反応をもらった点についていくつか補足します。 Function の合成 うーん、これをピタゴラ装置に仕立て上げる部分が別に必要なのかどうかが知りたい #k8sjp— Ken Ojiri (@kenojiri) 2017年10月12日 回答になっている
Haskell ライブラリにスターを送るツール thank-you-stars を作ってみました - チェシャ猫の消滅定理
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 で Haskell on JVM について話してきました - チェシャ猫の消滅定理
先日行われた 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 そのものと無関係なテーマ、かつ時間的に最後の枠というこ
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
