論文紹介ー"User-guided device driver synthesis"

システム系論文紹介 Advent Calendar 2014の7日目の記事です。

論文概要

デバイスドライバをユーザーが指示を出しつつ半自動でデバイスドライバを合成するツールTermiteというものを提案しています。
この著者はこのTermiteというツールをAutomatic Device Driver Synthesis with Termiteという論文で
その2つのやり取りをオートマトンとしてみて、その上で行なわれるゲームの必勝法としてデバイスドライバの合成をしてやろうというものです。

当初は完全自動だったのですが、現代の科学では完全自動だと厳しいものがあると悟った著者らがユーザーの入力補助をうまく取り入れるという
方針に変えてこのような形になったようです。
この論文は今までやってきたことのまとめ、という形になっているようです。

Specificationの書き方

このTermiteへの入力として必要なのはdriver, device, OSそれぞれのmodelのspecificationです。
これはTermite Specification Language（TSL）によって与えられます。

TSLの具体例は論文にあります。

Device model

デバイスの動作についてのモデルです。
デバイスがどのように動くかは
デバイスのデザイナーが持っているはずのtransaction-level models（TLM）から簡単にわかります。
ただし、ベンダーが非公開にしている場合も多く、TLM to TSLのコンパイラも開発中とのこと。

デバイスモデルを仕様書から書き起こす方法についてはSOSPの論文の方に詳しく議論されていましたが、この論文ではされていませんでした。

OS model

OSがドライバに向けて発行するAPIを構築するためのモデルです。
イーサーネットならパケットを送るとか受け取るとかそんな感じです。

DeviceとOSモデルをつなげる

このデバイスとOSの定義の関係する状態を結びつける必要があるのですが、
この2つの定義をできるだけ独立に保ちたいという要請もあります。

そこで、virtual interfaceというものを導入しています。
これはデバイスモデルの重要なイベントをOSに通知するコールバックみたいなものです。
これは実際に合成されるデバイスドライバの動作というわけではなく、
これで定義を与えてやろうというものです。

また、ドライバの動きを制限するassertや、ドライバがどこに向かっていくのかを定義するgoalというものも定めることができます。

ドライバテンプレート

OSが実際に呼び出す関数を定めるテンプレートです。

User-guided code generation

コードの合成はIDEで編集するという感じでおこなわれます。
このIDEの機能としてgeneratorとverifierがあります。
generatorが自動補完のように現在の入力位置にモデルから合成したコードを埋め込むことができます。
もちろん、合成したコードに対しての変更も可能です。
verifierが書かれたコードが定義に合っているかどうかをチェックします。

Synthesis

モデル間の合成なのですが、これはデバイス・OSとドライバ間でおこなわれるゲームと見立てることでおこなわれます。
ゲームの状態を有限オートマトンとして、状態遷移はコントロール可能なものとドライバやOSが勝手に行うコントロール不可能なものの2つです。
このゲームに勝つ戦略、すなわちなってはならない状態に陥らないように行動するのがドライバで、これを合成するというわけです。
このゲームに勝つ戦略がそもそも存在しない場合、合成は失敗となります。

この合成は下手に行うと状態数爆発を起こしたりと厄介なのですが、
それを起こさないため、筆者は様々な工夫をしています。

詳しいことを書いているとキリが無いので、ここでは省略します。
また、この論文より他の関連する論文のほうが詳しく書かれているようです。
（私は読んでいません）

Debugging with counterexamples

このゲームベースの合成に失敗した時のデバッグ支援方法もTermiteは備えています。
ゲームに勝つ戦略を妨げている環境の振る舞い、counterexample strategiesを探します。
これはこのゲームの双対ゲームを解くことで得られます。
このcounterexample strategyをステップ実行することで、デバッグを支援します。

Limitations of Termite

  • DMAを扱えない
    • 状態数が爆発する
  • デバイスコントロールとは本質的に関係ないところは他の手法を使うことで簡単に合成できるが、現在のところでは手動で埋め込むしかない
  • 並列処理への対応ができない
  • リアルタイム性の保障はできないので、ハードリアルタイムなドライバはつくれない

Implementation and evaluation

このTermite、Haskellのコードおよそ3万行で10人年かかっているとのこと。
USBのwebカメラ、UARTのシリアルコントローラなどを実際に実装して評価しています。
各デバイスドライバに実装するのに1週間ほど（ドキュメントを読んでデバイスの仕様を調べる時間も含まれている）とのこと。

合成アルゴリズムも、提案している手法と従来手法を比べ、従来手法だと2時間以内に終わらなかったものが、1分〜10分ほどで終わっていることが示されています。
verificationはまだ最適化されていないため、合成より時間はかかっていますが、それでも最大でも13分ほどしかかかっていません。

実際に出来上がるドライバはどうしても手動での最適化や変更が必要なのですが、60%〜90%は自動で合成できたようです。

また、できあがったコードサイズなのですが、これも全体的に小さくなっています。
これは、このドライバがデバイス動かすロジックに集中していること、
普通のデバイスドライバはコードの再利用などを考えて冗長になっていることなどが挙げられるようです。

この方法では定義の再利用が可能というのが1つの売りなのですが、これについてもOSを変えたることで試しています。
これも定義をほとんど変えることなく再利用できたとしています。

パフォーマンスもほぼ同等とのことです。

まとめと私見

Termiteというデバイスドライバ合成ツールについての論文でした。
形式的手法を用いて定義からドライバを合成し、さらにそのデバッグについても形式的手法を用いて支援しているというのはおもしろいと思い、今回この論文を紹介しました。
私自身、デバイスドライバを書いたことは一切なく、専門分野でもなく少々準備が甘くなりつたない文章となってしまいましたが、
ご指摘・マサカリ等ありましたら、コメントお願いします。