#論文 #未読

あだむっち先生のとこの論文。POPL'16。もちろん Coq

概要

いまのネットサービスはノードのクラッシュとかネットワークの分断とか起きても生きていないといけないよね

因果一貫性 causal consistency は、このようなサービスに要求される強めの一貫性の一つだよ

一貫性を持つ KVS とかね

Chaper というフレームワークを作ったよ

因果一貫性の検証

複製可能なKVS実装とそのクライアントの検証のため

KVSの実装とそのクライアントが正しい実装である条件を形式化したよ

因果一貫性に関する (斬新な) 操作的意味論を作ったよ

(斬新な) 証明テクニックを使って、2つのKVS実装の因果一貫性を証明したよ

2つ、というのは、KVSの実装2つなのか、サーバとクライアントの2つなのか、わからない

シンプルな自動モデル検査器も作ったよ

クライアント用

独立してサーバとクライアントの検証をしたので、これらの実装は正しいことが言えるよ

フレームワークは Coq で作って OCaml に抽出してビルドして実行できるようになってるよ