takaha.siの技術メモ

勉強したことをお伝えします。ちょっとでも誰かの役に立てればいいな…

Let's Encryptの証明書失効から学ぶループと末尾再帰の関係

この間、Let's Encryptがバグで300万近くの証明書を失効させたというニュース流れました。 事の詳しい顛末は以下のBlogにかかれています。かなり詳しく書かれており、どのようなコードでバグが出たのか?というところまで解説されています。 jovi0608.hatena…

TLC Model CheckerをCUI(コマンドライン)で使う

TLC Model Checkerとは形式仕様記述言語であるTLA+のモデル検査ツールです。TLA+で書かれた仕様の不変式のviolationやLivenessやSafety 特性のviolationの検出などをしてくれます。 そんで、このTLC Model Checkerというのは、CUIで使えたほうが便利だと思う…

TLA+の社内勉強会スライド公開します

Raftを使ってDFSを作るという仕事を数年前ぐらいから続けています。そのためか最近、形式仕様記述(特にTLA+)とかModel checkingとかTheorem provingとかが私の中でアツいです。TLA+とかAlloyとかVDM++とかSpin周りのやつです。 ソフトウェアの仕様を形式仕…

プログラムの正しさを数学的に証明する形式検証への招待

principia.connpass.com Twitter眺めてたら面白そうなセミナーがあったので申し込んだ。 私はオブジェクトストレージではないPOSIX IFな分散ファイルシステムを作るという面白い仕事をもう数年間ぐらい続けている。 その関係で最近TLA+とTLC Model Checkerを…

scalaのtraitの危険性

踏んだのでメモ Scalaにはtraitという機能があります。 traitは「それ単体で動作することはなく、他classを拡張(mixin)するか、他classから継承されることによって動作するエンティティ」と定義して良いと思います。 JavaのInterfaceにたとえられることも…

10GbE時代に向けたNAS環境を構築する

時代はテンジー 8年前ぐらいにQNAP社のTS-439 Pro II+を購入してから、ずっとこれで満足してました。しかし、システム領域のFlashが不穏なエラーを吐き出しはじめたのでそろそろ買い替え時かと思い立ちました。容量もそろそろいっぱいになってきましたし。。。 …