プレイングマネージャーをやめてPdMに専念した一年をふりかえる

プロダクトマネジメント キャリア

およそ一年前、プレイングマネージャーをやめてプロダクトマネージャー（以下、PdM）に専念することにしました。PdMとしての仕事が大きくなってきて、自分が開発に関わっているとそこがボトルネックになりそうだったのが理由でした。自分のキャリア上の転換点になりそうなので、一年をふりかえります。

決断することが仕事ということ

PdMの仕事は、プロダクトで事業を成功に導くこと、だと捉えています。技術的にすごいものをつくっても顧客の価値につながるかは別だし、顧客に喜ばれるからといってビジネスのことを忘れていては事業としてうまくいきません。顧客、ビジネス、技術の3つを考慮して何が顧客の価値なのかを見つけ、プロダクトとしてどう届けるかを決め、どのようにプロダクトを進化させて事業を成功させるか、を考えなければなりません。プロダクトのさまざまな観点で決断を下しましたが、その決断が良かったのかどうか、不安になることが多かったです。自分が携わっているサービスは特定の領域のBtoB SaaSで、これまで異なる領域で仕事をしてきた自分にとって不案内な領域で決断を下すのは心理的にきつかったです。

加えて、プレイングマネージャーをやめてPdMに専念するということは、自分の仕事はこの決断で評価される*1、ということです。エンジニアを兼ねているときはプログラムを書くことでも成果を出すことができましたが、良い決断を下さないと成果が何もない（またはマイナスのこともある）という状況です。プレッシャーがかかる状況でした。空いた時間にプログラムを書いて成果を出すこともできたかもしれませんが、今年はPdMに専念すると決めていたので、空いた時間は自分の決断の質を高めるために時間を使うことにしました。顧客の課題やそれを解くのに使われる手法について勉強しました。おかげで年初より少しだけ自信をもって決断を下せるようになりました。

プロダクトのステークホルダーを同じ方向に向かわせる

PdMが決断したからといって、その決断どおりにすぐに物事が進むわけではありません。誰かに作ってもらい、誰かに売ってもらう必要があります。プロダクトに関わる人はたくさんいて、エンジニア、セールス、サポート、経営陣などがあげられます。人それぞれにその人の立場なりの考えがあり、ときにはPdMが下した決断と食い違うことがあります。食い違うまではいかなくても、疑問に思われることがあります。こういった疑問を解消することは、PdMの大切な仕事の一部だと思います。こういった疑問は、往々にしてそれぞれの人とPdMで見えている範囲が異なっていることから生じることが多かったように思います。PdMは、ひとりの顧客ではなく全体、今だけでなく将来を見て決断を下すことが多いので、そういった決断の背景を繰り返し説明することが大事だなと思いました。

自分がコントロールできることに集中する

いつでも自分が決断したどおりに物事が進むわけではありません。説明が伝わらないこともあれば、外的要因でうまくいかないことはありました。自分はつねに結果が伴わないといけないと思うことが多かったのですが、それだとつらいことが多かったです。なので考え方を少し変えて、結果が伴わなった場合はそういうものだと捉えて自分ができる範囲で必要な施策を考えて打つ努力をする、として意識的に自分がコントロールできることに集中するようにしました。おかげでストレスが少し減ったように思います。

相談できるの大事

プロダクトにPdMはひとりです。最後の決断は自分がする、という意気込みで仕事をしてきましたが、ひとりで抱え込んでしまうとつらいです。自分の場合は幸運にも相談相手を持つことができたので、かなり助かりました。プロダクトの戦略やプライシング、説明の仕方などいろんなことを相談できたことで仕事の質もあがったし、ストレスもかなり軽減できました。最近は個人的な相談相手だったものからさらに取り組みを進めてProdOpsという小さなチームをつくって、このチームでプロダクトに関する議論をしています。このあたりは、メリッサの『プロダクトマネジメント ―ビルドトラップを避け顧客に価値を届ける』を参考にしています。

プロダクトマネジメント ―ビルドトラップを避け顧客に価値を届ける

プロダクトマネジメント ―ビルドトラップを避け顧客に価値を届ける

Amazon

来年にむけて

プレイングマネージャーをやめてみていろいろ分かったこともありました。プログラムをつくるの楽しいんだな、というのを再発見したり、自分より広い視野で会社全体のことを決定している経営陣ってすごいプレッシャーだなと思ったり。来年以降もPdM専念を続けることになると思いますが、今年くらいの仕事をあまりプレッシャーを感じずに普通にできるようにしたいな、と思ってます。目下の目標は領域に関する知識をもっと身につけることです。

*1:実際の評価はもっとさまざまな観点で評価されるのですが、ここが大事だと思ってました

Amazon S3の軽量形式手法

形式手法 テスト

本記事は、形式検証 / 形式手法 Advent Calendar 2021 の 19 日目の記事です。

Amazon S3が形式手法を採用した論文 "Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3" を読みました。

論文全体については、yohei-aさんがブログ記事で主要な部分を訳してくれています。本記事では自分なりのまとめに加えて、自分の形式手法導入の経験から思うところについても書いてみます。

論文は、Amazon S3の新しいKey ValueストレージのShardStoreの正当性を軽量形式手法で検証した話です。論文の主張をまとめると、

  • 実装に使用した言語（Rust）と同じ言語で仕様となるリファレンスモデルを記述した。
  • 検証したい性質によってツールを使い分けた。機能的な正しさおよびクラッシュ整合性の検証には、リファレンスモデルを用いたProperty based testing, 並行実行の検証には（こちらも実装言語そのままで検査できる）ステートレスなモデル検査器を使用。
  • 開発初期は形式手法の専門家がリードしたが、エンジニアリングチームを教育して、彼ら自身でリファレンスモデルを維持、開発できるようにした。

です。これを読むと「なるほど、これは良さそうだ」と思い挑戦したくなるかもしません。しかし、いざ適用するとなると、悩ましい選択に直面するでしょう。例えば、今回の例では

  • 専用のモデリング言語か、実装言語か
  • 検証すべき性質はどの程度にすると効果的か
  • リファレンスモデルの抽象度はどの程度に保つか

などです。論文ではそのあたりもつぶさに解説してあり、大変参考になります。彼らは変更され続けるシステムのため、エンジニアリングチーム自身が維持できることを主眼に選択しました。個人的には、専用の言語でも教育すればふつうのエンジニアでも使用することはできるようになると思います。言語よりむしろ検証したい性質をどこまで書くか？の選択が難しく、そのあたりはどの言語でモデリングしても問題としては残ります。ただ、プログラミング言語を使うことでCIに導入するのが簡単だったでしょうし、単体テストのモックとしても使えた、ということでプラスの面も大きかったのでしょう。こういった設計選択には形式手法の専門家の経験、助言がかなり役に立ちます。

軽量とありますが、一部でモデル検査や証明を使っていて現実的に導入できるものを全方位で取り組んでるように見えます。自らモデル検査器を開発したり、つよつよな解決法も見られますが、本論文で紹介されている一部でも導入することで効果は得られるでしょう。関連する事例*1やツールも参考になりそうでした。

個人的に今回の事例が成功している要因として、以下が大きかったと思います。

  • 世界中のシステムのインフラであるため高い品質が求められ、それを実現することにそれ相応の工数をかけることが妥当であるという合意形成がなされていそう。
  • 実装は効率、ロバスト性など高い非機能要求を実現するために複雑である一方、抽象度をあげた仕様は比較的単純である。
  • 導入初期に形式手法の専門家の援助があり、早い段階で結果で示すことができた。

特に最後の点が大きいと思います。どんな手法でもそうですが早く結果で示すことが一番効果的です。それを達成するのに専門家の支援は大きいと思いますが、一般の開発現場ではなかなか手に入らないというのが現実でしょう。しかし、こういった論文が公開させることでノウハウが共有されれば専門家の支援なくともうまくやれる現場が出てくるかもしません。

以下、重要そうだなと思ったポイントあげておきます。

  • フルの形式手法を適用するには非現実的とかんがえて、より弱い正当性の保証をねらって軽量形式手法を適用した。
  • 実行可能なリファレンスモデル。これはシステムの期待する振る舞いを定義する。実装言語と同じ言語で書かれ、エンジニアチーム自身がメンテナンス、サイズは実装の約1%。ユニットテストのモックとしても使われ、新しいコードを書くときに効果的に変更されるようにした。
  • すべての検査は自動化されていて、検証のためのインフラはコンパクト（コードベースの12%）。従来のテスト手法やコードレビューでは見つけられない16個の不具合を発見。
  • リファレンスモデルでは、限られた方法でしか失敗させられない（追加してないキーの読み出しに失敗するとか）。IOエラーやリソース枯渇のエラーはリファレンスモデルには省略した。Availabilityやパフォーマンステストを犠牲にすることになるが、モデルをシンプルに保つことを選択した。
  • リファレンスモデルを実装言語と同じにしたのは設計上の選択。他のモデリング専用言語（Alloy, Promela, Pなど）を検討したが、エンジニアの認知コストと学習コストを抑えるための選択。
  • リファレンスモデル自身の検証にPrustiを使用した。例えば、LSM-treeのリファレンスモデルでは、キーバリューのペアが削除させるのはdelete操作のときのみを証明した。
  • リファレンスモデルと振る舞いが等しいことをどこまで検査するかは難しい。
  • カバレッジを上げるために入力にバイアスをかけた。例えば、PutとGetの操作に渡されるキーが一致することは稀なので、ほとんどのGetは失敗する（成功するテストがほとんどされない）。Putしたキーが選ばれやすく確率をあげる。しかし、やりすぎてはいけない。そもそも形式手法を採用する目的は自分たちが想定してないことを見つけてくれることを期待しているので、バイアスをかけすぎて自分たちの想定内しかテストされないという事態は避けねばならない。
  • Disk IOエラーの適合テストではチェックを緩めた。実装はどこでエラーが起きたかでその後の振る舞いが異なるが、それをリファレンスモデルで再現しようとすると複雑になるため。エラー時にはフラグを立てて、結果がある程度一致しないことを許した（例えば、エラー時のGetでは何もデータを返さないのを許容するが、誤ったデータを返すことは許容しない）。
  • リソース枯渇に関してはプロパティベースなテストを適用しないことにした。実装に伴うメタデータなどのオーバーヘッドを抽象モデルに入れることが難しいので。

  • クラッシュ整合性を検査するのに、仕様として2.2節で説明したDependencyについてふたつの特性を定義した。

    • 永続性。Dependencyがクラッシュする前に操作が永続的であったとならば、クラッシュ後に読み取り可能である
    • 前進性。クラッシュがないシャットダウンの後は、すべてのDependencyは永続的であるべき*2

  • 前進性は、決して完了しない操作をはじくことができる。実装が返すDependencyはクラッシュ整合性を満たすためにより強いこともありうるが、永続性により弱すぎないことを保証する。

  • DirtyRebootという操作を追加してクラッシュを模擬。揮発性メモリのどこが永続化されるかコンポーネントレベルで指定可能にした。それより細かいブロックレベルの指定はテストが遅くなる割に効果が薄いのでデフォルトでは使用していない。
  • Rust内に残るundafeのコードを検証するためにMiri interpreterを使用した。並行プリミティブをサポートするために手を加えた。
  • デシリアライズの検証にはCruxを用いて、パニックが起こらないことを証明した。
  • すべてのバグは自動化されたツールにより発見された。デバッグがエンジニアにより行われるのは従来どおりだが、ツールが最小の反例を示すことでそれを助けた。この手法がバグを防ぐことに有効だった。エンジニアたちはこの検査で見つけたバグをコードレビューで見つけられないと語った。
  • 形式手法の専門家がふたりフルタイムで9ヶ月、3人目は3ヶ月参加。彼らはリファレンスモデルとテストハーネスの初期の開発をリードした。その後はエンジニアリングチーム自身（全員が形式手法の経験なし）が開発した。git blameによるとエンジニアリングチームによるコード編集はテストハーネスの18%。
  • 本手法でもバグを見逃すことがある。実際、今回のツールでは見つけるべきバグが見つけられず、コードレビューのときに見つけたものがあった。これはキャシュを導入する変更で、はじめテストハーネスでのキャシュサイズを大きくしていたため見つけられなかった。キャシュサイズを小さくすると見つけられるようになった。この件がきっかけになり、カバレッジ計測を入れることになった。
  • 開発の早い段階で導入すること。ひとつのコンポーネントからはじめて、リファレンスモデルを作ったらすぐにコードベースに統合し、エンジニアを教育機関すること。これにより、早期にバグを発見した。この結果、エンジニアの興味を強く引くことになった。
  • リファレンスモデルをコードベースに統合しておくことは、時間の経過とともにコードが変更される状況において検証を有効に保つのに欠かせない。実装言語と同じRustでモデルを書くことはオーバーヘッドを少なくし、エンジニアに仕様を書かせるためのひとつの方法である。

*1:形式手法は事例に乏しいと言われることがありますが、どれも2015年から2020年あたりで最近になって増えてきたのかな、という印象を持ちました。

*2:永続性の条件は、含意を含むので前件が満たすものをテストしておくことは大事。そうでないと永続的な操作がひとつもなくても条件を満たしてしまう

AWSにおける形式手法

形式手法

AWSにおける形式手法の記事（https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf）を読んだ。特に重要だと思われる示唆を3つあげると以下の通り。

  • 産業界では長年形式手法は多大な工数をかけて比較的容易なコードの断片を検証するというイメージがあったが、これはまったくの誤り。現実の問題に適用可能である
  • アマゾンでは10の現実のシステムに適用して、すべてで効果が得られた。難解なバグの発見したり、正当性を犠牲にすることなく確信を持って最適化を施せた
  • 7つのチームでTLA+を使用。エンジニアは2−3週間で学習することができる

以下は、読んでいる途中で書きだした要点。

  • AWSでは2011年以降形式仕様とモデル検査を使用している
  • 複雑な分散システムを検証するにあたって、従来の手法 ― 設計レビュー、コードレビュー、静的解析、ストレステスト、フォルトインジェクションテストなどだけでは確信を得るには不十分だった
  • システム設計で厄介な（見つけにくい）バグを見つけるには正確な記述が必要。従来のダイヤグラムは曖昧でテストできない。一方、ソースコードは非曖昧であるが詳細すぎる
  • そこで見つけたのがTLA+. TLA+ではシステムが持つべき特性と設計を同じ言語でかける。あらゆる抽象度で記述できて、検証は数学を使って推論してもいいし、モデル検査で検査してもいい
  • 産業界では長年形式手法は多大な工数をかけて比較的容易なコードの断片を検証するというイメージがあったが、これはまったくの誤りだった
  • アマゾンでは10の現実のシステムに適用して、すべてで効果が得られた。難解なバグの発見したり、正当性を犠牲にすることなく確信を持って最適化を施せた
  • 7つのチームでTLA+を使用。エンジニアは2−3週間で学習することができる
  • 形式手法適用の良い効果として、良い設計のやり方が身につく。たいていのエンジニアがやる、正常ケースを考える、それから思いつく異常ケースに対応するでは網羅できない。システムが持つべき特性を書いてから設計し、検査する。その方がずっと設計エラーが少なくなる
  • 形式仕様を書くことでシステム稼働中ずっと恩恵が得られる。リリース後の機能追加やパフォーマンス改善のため変更を加えるときは「この変更は安全か？」を常に問われる。形式仕様とモデル検査がなければこの質問に自信をもって答えられない
  • こうした形式仕様とモデル検査を使った検証を経て開発者がシステムについて深く理解することができることも大きな利点のひとつ
  • テスト可能な形式仕様はすばらしいドキュメントでもある
  • 形式仕様で扱えなかった問題として、「徐々に低下するパフォーマンス問題」がある。これは論理的な誤りではないが、ユーザ視点からすると問題となる。TLA+ではリアルタイム安全性として応答時間の上限を扱うことができるが、OSやネットワークなどのハードウェアリアルタイムをサポートしていないインフラ上のソフトウェアには適さない。結局、その部分については別の手法を使った
  • 形式手法を始める前は、バグの発見のためにアサートを使っていたが、アサートはバグの影響を最小限に留めようとするが、ユーザデータの損失などを引き起こしたあとの状態からは回復させられない。これらのバグは避けなければならない
  • 最初は形式手法は候補ではなかったが、Pamela Zaveの論文で現実世界の問題に適用されていることを知り調査開始
  • 最初はAlloyを検討したが、自分たちのユースケースでは表現力が不足しているとしてTLA+を採用するに至る
  • DEC/Compaqにおけるキャッシュコヒーレンスの実例があったのもTLA+を採用するのに後押しになった
  • TLA+の表現力の高さはモデル検査の使用を考えるときに逆にその検査器の言語に変換できないことが考えられたが、実際には問題にはならなかった
  • 2012年、アマゾンはDynamoDBをローンチする。このDynamoDBでの適用が最初の大きな成功。
  • 開発者であるT.R.はフォルトインジェクションのテスト、ストレステストを行うも、それだけでは不十分とし設計を検証するためにTLA+を使う。TLA+で仕様を書き、TLCモデル検査で検証を行った。それにより、他の方法では見つけられなかった厄介なバグを発見。これは設計レビュー、コードレビュー、テストをすべてかいくぐってきたバグ。T.R.はこれらのバグを直して修正版のアルゴリズムをすべてモデル検査で検証。
  • T.R.曰く、形式仕様の記述と検査によるやり方は信頼できるし、非形式的な証明を書いたり検査するのに比べて時間もかからない。TLA+を使った方が市場へのリリースは早くできる
  • T.R.はDynamoDBローンチ後も新機能やパフォーマンス改善のときには既存のモデルに変更を加えて検査した
  • DynamoDBでの成功後、これをもっと広めるために社内のエンジニア向けに「設計をデバッグする」というタイトルでプレゼンする。エンジニアの先入観をさけるため、「形式」「検証」「証明」という用語は避けた。
  • プレゼン後、S3のチームが興味を示す。このチームでは状態遷移図で書かれたドキュメントがあり、これを網羅的にテストするJavaコードがあったが、もちろんこれはTLA+で置き換え可能。開発者のF.Z.は自分たちの問題にはTLA+よりPulsCalがより生産的として、そちらを使用。F.Z.はモデル検査で2つのバグを発見
  • その後マネジメントがTLA+を後押し。F.Z.は他のチームが仕様記述するのを手伝った。TLA+が早く広まった要因の一つは、この学んだ人がすぐに教える側に回れることにもある。
  • B.M.はすでに発見されていたバグの修正に関する仕様を記述して検査。それによりこの修正が別のバグを含んでいることを発見。さらにアルゴリズムのドキュメントの曖昧性をいくつか発見した。
  • M.B.とM.D.もPlusCalとTLA+を使用。M.B.はPlusCalで3つのバグを発見、M.D.はロックフリーの検査をPlusCalで行った。
  • Amazonでは、従来の設計文書をインクリメンタルにTLA+とPlusCalを使った記述に変更していった。この過程では、モデル検査をしたり仕様を書ききる前にシステムに関する重要な気付きが得られる。あるアルゴリズムでは、これにより大幅な最適化の案が得られた。
  • さらに最近になってTLA+はデータモデリングの優れたツールでもあることが分かった
  • TLA+を学ぶエンジニアはしばしばこう問う「検証した設計から実行可能な正しいコードはどうやって得るのか？」と。答えは「得られない」だ。しかし、形式手法はいくつもの方法で助けてくれる。例えば、
    • 形式手法は正しい設計を得るのを助けてくれる。正しい実装を得るにはまず正しい設計が必要。誤った設計からは誤った実装しか生まれない。
    • 形式手法は設計を深く理解することを助けてくれる。正しい実装は設計への深い理解から生まれる
    • 形式手法は、開発者が自己診断する実装を得るのを助けてくれる。システムが満たす不変条件がアサートで書かれる。形式手法はこの不変条件を見つけるのを助けてくれる。これにより良いアサートが組み込まれ、コードの品質が向上する
  • やりたいことは高い抽象度で書かれた仕様に対して、実装がその仕様を満たすか検証する、もしくは、仕様からコード生成することだが、既存の静的解析ツールは局所的な問題を指摘するだけでシステムワイドな検証をしてくれない
  • AWSにおいて形式手法は大成功を収めた。他の手法では発見できなかったバグを発見し、今では多くのチームがTLA+で仕様を書いている。経営陣もTLA+の使用を後押し。
  • 設計者は（検査したい）システムの振る舞いをモデルで表現する必要があるが、これは獲得するのが難しいという課題もある

認定スクラムマスター研修受けてきました

認定スクラムマスター研修受けてきました。平鍋さんのブログでジェフが来日すると知って、「これは受けたい！」と思い、次の瞬間にはボスに承認してくださいメールを書いてました。

http://www.scrum.esm.co.jp/

研修はとても良かったです。自分なりにスクラムを導入してやってきたつもりでしたが、まだまだ足りない点をたくさん見つけることができました。僕は、スクラムの利点は実績値をもとに確度の高い見通しを得て、不確実性にうまく対処できることだと思っていたのですが、それはスクラムのひとつの側面にすぎなくて、目的は顧客に届ける価値を最大化する、そのために圧倒的な生産性をもつ自己成長できるチームをつくることにあるんだと理解しました。

スクラムはシンプルなのに習得が難しいと言われることがありますが、本当にその通りだなあと。原理、原則はすごくシンプルでどうしてそれがうまくいくかはそれとなく理解できる、でも、それを実践するとなるとなかなかできないことも。言うは易し、行うは難し、です。

普段うまく対処できてないことについて経験豊富なスクラムマスターに直接質問できたので、個人的に非常に実りの多い研修でした。

関係者のみなさん、お疲れ様でした & ありがとうございました

形式的仕様記述の適用事例を通して得た仕様記述のコツ

形式手法

これはFormal Method Advent Calendar 2016の25日目の記事です。

今年6月、国立情報学研究所で「恊働ロボットCOROの開発における形式的仕様の適用事例」というタイトルで形式手法の適用事例について発表しました。資料はこちらです。

http://www.slideshare.net/liferobotics/coro-63631016/1

開発対象となるシステムの仕様を形式的に記述するということは自分にとっても初の挑戦であったので、実際に適用してわかったことがたくさんありました。発表資料でのいくつか書いていますが、本記事では仕様の書き方で自分が発見したことに焦点をあてて説明します。

不変条件はなるべく明記した方がよい

発表資料でも触れていますが、仕様を理解する上で不変条件はとても重要な役割を果たします。今回、自分たちが採用した仕様は状態遷移モデルをもとにしているため、振る舞いはイベントに対する遷移として記述します。状態遷移モデルに変数を導入することで、変数がないプリミティブなモデルから見たら複数ある遷移をひとつの遷移として書くことができます。しかし、その場合各変数が遷移後にどのような状態になっているかを明記しなければなりません。これを事後条件で記述します。たとえば、
あるボタンが押されたら、別のボタンがDisableになって操作不能になるとしましょう。このとき、ボタンのEnable/Disable状態を表す変数をブール型の変数で表すとすると、遷移の事後条件には以下のような記述が必要です。

button_enabled' = False;

ここで、button_enabled がブール型の変数で、Falseは偽を表すブール型の値です。button_enabled' のように変数に ' がついている場合は事後の変数を表します。=は等号であり、代入演算子ではありません。この場合は、事前の状態に関係になく False になりますが、一般的には事後条件は事前の状態との関係で表されます。たとえば、ボタンのEnable/Disableが切り替わるような操作があった場合は以下のように書きます。

button_enabled' = not button_enabled;

ここで、not はブールの否定演算子です。このように変数を導入することで本来は各変数がとりうる値ごとに状態として記述する必要があるものが、変数を含むより大きな状態に着目して仕様を記述することができます。自分たちの場合は、GUIアプリケーションの画面を大きな状態として捉えて、その画面内の振る舞いを記述するのに変数をつかって記述しました。

さて、このように各遷移を書いていくと、どの遷移の事後条件でも成り立つものを見つけることができます。それをもっとよく考えてみると実は大きな状態にいる間（自分たちの例では画面）ずっと成り立つ条件を見つけることができます。それが（その状態での）不変条件です。不変条件はその名の通り変わらない条件で、さまざまなものを対象にすることができます。たとえば、システムが動いている間すべての状態（自分たちの例でいうとすべての画面）で成り立つ不変条件はシステムの不変条件です。また、不変条件はなにも仕様だけの話ではなく、プログラムのループが実行している間成り立つ条件もありこれをループの不変条件と呼びます。われわれがつくるシステム（プログラム）は動くことに価値があるのですが、不変条件はその中で変わらない条件を表します。ちょっと不思議ですが、この不変条件が仕様の理解にとっても役に立つのです。

というのは、実はさきほど述べた各遷移をよく見て不変条件を見つけるというのは稀で、むしろ各遷移で成り立つルールがあってそれに違反しないように各遷移の事後条件を書くことの方が多いからです。で、このルールが不変条件そのものです。仕様を決めるときに、各遷移の詳細を決める前に方針のようなものを決めることがあります。たとえば、ロボットが動いている時はボタンをDisableにして操作不能にしよう、とかです。こういう方針を不変条件で書いておくことは非常に大切です。なぜなら、不変条件を書かないとロボットを動かし始める遷移の事後条件をすべて見てどういう条件が成り立つか発見しないといけないからです。仕様を理解する上で最初に合意されるこういった方針やルールは非常に役に立つものです。これを不変条件として表します。

robot_state = State_Moving => button_enabled = False;

この不変条件が陽に記述されないと、どういうルールがあるのか読み解くのに苦労します。

共通の振る舞いは一箇所で記述が済むように何らかの支援があると良い（だろう）

もうひとつは、これだ！とまだ解が出たわけではないのですが、書くうえで非常に苦労したことから得たことです。上で述べたように今回各画面を大きな状態として捉えて遷移を記述しました。しかし中には全画面で共通の振る舞いというものがあります。今回は、これを何も工夫せず各画面で書くようにしました。しかし、これはあまり良い選択ではありませんでした。

一つ目の理由は、単純に記述がめんどくさいということです。共通のものは一箇所の記述で済ませたいというのがプログラマの心理としては当然です。修正するときの手間はエディタの機能で頑張ってもらうとしても面倒なことはかわりません。

二つ目の理由は読む方も大変だということです。各画面にちらばって書いてあると不変条件と同じように全部を見ないと共通だと言えないので、本当に同じ振る舞いか？というのを確認するのが大変になります。ここでも例をあげて説明しましょう。たとえば、どの画面にいてもあるHWボタンを押したらロボットが停止する、というような仕様を書くとしましょう。このとき、全画面で以下のような事後条件をもつ遷移を記述しないといけません。

robot_state' = State_Stop;

しかし、画面がいくつもある場合、全画面のそのイベントの遷移を見て、すべてが上記の記述ならば確かにいつでも停止状態にするということがわかります。もし、ひとつの画面でも

robot_state' = robot_state;

というように、ロボットの状態が変わらないと書いてあった場合は、その画面だけは異なる振る舞いになります。これが意図したものなのか、実は記述ミスなのかは補足がないと確信がもてないでしょう。

最初に仕様記述の文法を考えたときに一つ目の理由は頭にはありましたが（逆に二番目は気づいてなかった）、それでも各画面で書くように決めた理由はあります。それは、あまり仕様に構造を持ち込みたくないと考えていたからです。各状態で書くものを一箇所の記述にすむようにするということは、それが各画面で書いたものと等価である記法を考えないといけません。オブジェクト指向でいうところの継承のようなモデルを採用する案は頭にはありましたが、あまり複雑にして記法に溺れても、と思い、まずはフラットに書こうと決めました。しかし、結果的にはあまり良い選択ではなかったようです。ただ、支援なしではどういうところが大変かというがわかったという意味では良かったと思います。

以上、今回は実践から得たふたつのことを書きました。ほかにもいくつかあるのですが、長くなったので今日はこのへんで。もしかしたら、来年のJaSST Tokyo 2017での発表でもう少し詳しくお話しできるかもしれません。興味がある方はぜひご参加ください。

http://jasst.jp/symposium/jasst17tokyo/details.html#D3

では、メリークリスマス

大腸内視鏡検査を受けて

大腸内視鏡検査を受けるのは大変だ。前日の朝から食事制限が始まる。食べられるのはごく一部の食品に限られる。そして前日の夜から下剤を飲まされる。当日は朝から大量の下剤。

検査そのものは病院にもよるが、自分が受診したところは無痛で検査じたいはさほど辛くない。だか、費用は自分持ちで最低8000円からだ。

もしポリープ切除となれば食事制限は一週間続く。3年前、ポリープ切除したときは食事制限のストレスから顔面に激痛が走る三叉神経痛になったほどだ。

では、なぜこんなにつらい事前準備と費用を払いながら検査を受けるのか？3年前は人間ドックで要精密検査という結果が出た。当時、自覚症状は全くなかったので「まさか、何かの間違いだろう」と思ったが念のため受けた。その結果がポリープ切除だった。今年も全く自覚症状はないが定期検診のためだ。良性のポリープもほっとくとガンの原因になる。

受けるのはつらい。でも、受けずに知らない間にもっと悪い結果になるのはもっと避けたい。

話は変わって、僕たちの仕事はどうだろうか？僕はプログラマで日々ソフトウェア開発に携わっている。

普段のプロジェクトでできていること、できていないことたくさんある。できていないところは目に付きやすい。みんな解決しようと何かとアクションがとられることも多いだろう。では、できていると思っていることはどうか？病気の自覚症状を思うと、実は気づかないだけで良くないことが進行しているかもしれない。当たり前だか、自分では気づけないものは改善できない。

では、どうすれば良いか？ひとつの手段としては他人の意見を聞くことがあるだろう。病院のときに医者の意見を聞くように。

これが意外と難しい。耳の痛いことは聞きたくないからだ。しかし、本当に良くしたいのであれば他人の意見は真摯に受け止めないといけない。「何を言っている」と言って一蹴したり遠ざけたりするのは簡単だがそれでは死あるのみだ。

以前、働いた現場でプロジェクトの問題点をいくつか指摘したことがある。こちらの言い方の問題もあったかもしれないが、最終的には受け入れられず僕はプロジェクトを外された。あとで聞いたところ、そのプロジェクトは散々だったようだ。

自分もそうならないようにしないとな、と大腸内視鏡検査を受けた日に思った。

SyncStitchを使ったAlternating bit protocol (ABP) の設計（4）〜発散をとりのぞく〜

形式手法 CSP

さて、ようやく最終回です。前回は、仕様と実装を比較して、実装が仕様を満たすことを確認したものの、実は発散が含まれているという話でした。今回はこの発散を取り除いて改めて仕様との比較を行います。

まずもう一度発散を確認しましょう。発散検査を行い、バツになったら右クリックで「explore」を選んで発散となっているtau遷移の正体を確認します。


図1. 発散の遷移列

Pathを表示すると、受信者用チャネルはRC0→RC1→RC4、送信者用チャネルはSC0→SC2→SC6と歪みによるエラーが延々と繰り返されているのが分かります。しかし、実際の通信路でエラーが起きる確率は通常何パーセント以下になっていて、このようにエラーが延々と繰り返されることはありません。そこで、モデルに連続でエラーになる最大数を入れて、無限にエラーが繰り返されないようにします。

受信用チャネルを以下のように変更します。


図2. 修正後の受信者用チャネル

各状態に n という変数が加わったのが確認できます。この n が連続でエラーを起こせる最大数となります。n を初期状態で N （ここでは 3 としました）に初期化します。エラーを起こす遷移のガード条件を 0 < n とし、エラーを送ったときには n を 1 つ減らします。正常値を送る遷移にはガード条件は設けていないので常に遷移可能です。よって、n が正のときにはエラーと正常値のどちらが送られるかは非決定的になります。エラーが続き n が 0 になるとエラーを送る遷移のガード条件が偽になり、必ず正常値が送られます。正常値を送ったときには n を N に戻すのでまたエラーが発生させることができます。

送信者、受信者それぞれのチャネルを変更したら再び検査を行います。モデルを変更したので、再びデッドロック検査から行います。デッドロックがないことが確認できたら、次に発散検査です。ともに検査が通ることが確認できます。発散がないことを確認したら、仕様と比較します。これもトレース、拒否ともに検査が通ることが確認できます。

仕様を満たすプロトコルが設計できました。最後のモデルは、https://github.com/masateruk/blog/blob/master/20130911/abp-5.ss にあります。

まとめ

以上で、ABPの設計は終わりです。今回心がけたモデリングでのポイントをまとめます。

  • シンプルなモデルから始める
  • 振る舞いを追加したり変更したりするときは、その都度検査をしながら少しずつ変更する
  • 拒否検証は発散を取り除いてから行う

参考文献

最後に参考文献を紹介してこの記事を終わります。

[1] 株式会社 PRINCIPIA『SyncStitch ユーザガイド』
今回使ったSyncStitchというツールのドキュメント。ツールの説明というより基礎となっているCSPの解説がメインになっています。CSPの概念について非常に易しく解説してあります。日本語で読めるCSPの解説書では最も易しいものだと思います。

[2] Roscoe, A. W.『The Theory and Practice of Concurrency』
CSPの解説書。[1] を読んでより形式的な解説が欲しい方にはこちらがおすすめ。操作的意味論に加え表示的意味論の解説もあります。5.3節にはCSPを使ったABPのモデリングと検証について解説があります。

[3] Gerard J. Holzmann『コンピュータプロトコルの設計法』
SPIN Model Checker の開発である、ホルツマンによるプロトコルの設計方法を解説した本です。書籍の中で使用する検証ツールはSPINですが、ツールの説明ではなくプロトコルの設計時の課題や技術について解説が豊富な良書。もちろんABPに関する解説もあります。

[4] 『Basic Spin Manual』
拙訳ながら SPIN Model Checker のマニュアルも載せておきます。「付録：検証スイートの構築」にABPのモデリングと検証についての記述があります。