garasubo's note

(´・ω・`)

あなたとHexo

| Comments

Octopressの動作が最近よくわからないけど不安定なのと、 どこかでHexoいいよという話を聞いたので、このブログのHexo移転を考えている。

Hexo

所要時間3分!? Github PagesとHEXOで爆速ブログ構築してみよう! | 株式会社LIG

Octopress vs Hexo

Octopressからの移行は楽で、記事のmarkdownファイルを移動してきて、configをいじってあげればよい。

Migration | Hexo

それで新しくつくったブログがこちら。 もうちょっとしたらこちらに移す。

新しいブログ

論文紹介ー”User-guided Device Driver Synthesis”

| Comments

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

UbuntuにインストールされたVMware Playerをアンインストール

| Comments

タイトルの通り。aptで入れたわけでないのでどうするのかなあと思ったら、 vmware-uninstallってコマンドあったから打ってみたところ、

The vmware-uninstall* scripts have been deprecated.  Instead, please use
the vmware-installer.

Long form:
  vmware-installer --uninstall-product PRODUCT
Short form:
  vmware-installer -u PRODUCT

とのこと。

なのでおとなしく、vmware-installer --uninstall-product vmware-playerと入れたら消えたみたい。

Android開発あれこれ

| Comments

Android開発したときのあれこれをまとめ

Android Studio

Android Studio | Android Developers

公式のSDK。IntelliJベースで、補完とかがとても優秀。 Viプラグインも結構気に入っている。 gitignoreとかもデフォルトでちゃんとしていたりと。 ビルドツールもなかなかよい。 ただし、gitプラグインの使い勝手はイマイチ。 まあ、それは別の方法で叩けばいいだけの話であって、 これなしでのAndroid開発は考えられない。

シミュレータ

実機で走らせるとデバッグ実行できなかったりと色々と不都合なので、 シミュレータを使うことになる。 しかし、とっても遅くて使い物にならないとまでは言わないが、ストレスがたまる。 WindowsとMac用にはIntell製のシミュレータが用意されていてSDKマネージャーからインストールでき、それを使えばそこそこ速いらしい。 しかし、自分はUbuntu使っているので、この方法は使えなかった。

他の方法ではGenymotionというシミュレータがあり、こちらのほうが高速との評価をちらちら見る。

Genymotion

こちらは、Virtualbox上で動作する仮想化環境。こちらはUbuntuにも対応しているが、まだ試したことはない。 Macbookでは試したが、確かに高速。 ダウンロードに個人情報要求されたりするのが癪ではある。 トラップとして謎のバグが存在しており、何回かデバッグ実行するとエラーを吐いてアプリが突然死するというものがある。 そうなった場合は再起動しなければならない。

ユニットテスト

Robolectricというのを使った。

【Android】Android Studio + Gradle + Robolectric!でテストをしよう | Yohei Blog

robolectric_deckard-gradle · GitHub

ここらへんを見ながらなんとか導入。 罠なのが、Android Studioが勝手にパッケージ宣言を補完してくるところで、これがあるとテストが動かない。 gradle checkコマンドで簡単にテストできる。ターミナルで実行するよりSDKから叩いたほうが高速(理由はよく知らないけど中間ファイルか何かを再利用していたりするのか)。 画面遷移等もチェックできるらしのだが、そこまではよく分からなかった。 しかし、Shared PreferenceとかAndroid固有の機能が絡んでくる動作もちゃんとテスト出来るのはうれしい。

ICPC2014参戦記

| Comments

ICPC2014国内予選参加しました。 結果は5完の24位でアジア地区予選には自明に進めないのでここでおしまい。

解いた問題と方針

相方にAを任している間に、C,Eの実装を考えて、 Aが終わった後、Cを通す。 疲れたので相方にBを任せている間に、Dの方針を聞いたり他の問題考えていた。 Bが終わった後、DとEを連続して実装して通す。 F、Gは歯がたちませんでした。

C問題

はじめは二部探索かな、と思ったが、判定関数考えているうちに直接求まることに気がつく。

まず、各々のx軸上の区間のビルの高さの最大値を求める。ビルが存在しなければ0とする。 i<=0となるような[i-1,i]区間ではx=iの地点がより太陽が先に見えてしまう。 i>0となるような[i-1,i]区間ではx=i-1の地点がより太陽が先に見える。 よってそれぞれの区間について、太陽が先に見えるx座標とそこの高さに円が到達する時間を求める。 そのうち最小のものが答えとわかる。

r<=20という制限により、区間中に存在するビルの高さの最大値は愚直に求まり、 到達する時間については2次方程式をさくっと解くだけ。

D問題

相方から聞いた方針を具体化しただけ。

文字数がたかだか20なので、各文字について変換されたorされないと仮定して復号化、それを暗号化してちゃんと元に戻るかを計算すれば大丈夫、 というもので実装した。 各文字について変換したかどうかをビットマスクで表現して、’z’を復号化するときだけは例外処理。 ちゃんと元に戻った文字列は記録し、最後にソートして出力。

ただ、この方針、すぐには実装できるのだが、最大で220*20*25の計算となり、500000000くらいとなり、普通のプロコンだと通用しない計算量となってしまった。 (暗号化するかしないかのパターンで220通り、暗号化で20*25の処理が入る) ただ、ICPCは制限時間が無く、手元で実行し出力ファイルを提出すればいいだけなので、 出力を待っている間、他の問題を実装していれば問題なく正解をもらえた。

もうちょい何とかするとすると、暗号化するところの処理を文字の出現位置とかをメモすることで高速化するか、 DFSとかで暗号化できないような文字列は探索しないようにすることでそもそも判定の手間を減らすとかか。 あと、ビットマスクの探索順を工夫すれば最後のソートはいらない。 まあ、いずれも実装が複雑化しそうなので、これはこれでよかったのかなあ。

E問題

自明に木構造をしているので、木DP的な何かかなと当たりをつける。 ノード数が300と少ないので、全ての点について根であると仮定した場合で回しても十分間に合いそう。 終点についてもそれぞれについて終点としてみて試せば300*300*300で間に合うんじゃないか、となったが、 擬似コード書き始める時点で、終点を固定して探索するの厄介だなあと考え、もうちょっと考えなおしてみる。

そこで、始点と終点が同じであるパターンからまず考える。 始点をAとしておく。 葉、つまりこの先に何もない島につながっている橋はわざわざ渡る必要もなく、即座に撤去すれば良い。 そうではない島(Bとおく)につながっている橋は、まず、Bより先にある橋を撤去する必要があるので、一度その橋をわたらなければならない。 Bについても、Aに戻るためには同じ橋を渡らなければならないので即座には撤去できず、Bよりも先にある橋を全て撤去してBに戻り、 Aに戻り、やっとA-B間の橋を撤去出来る。 つまり、ある島を始点とした場合、それを根にした木と考えた時、葉をつなぐ橋は即座に撤去し、そうでない橋は2回渡った後撤去することで、 全ての橋を撤去できる。始点と終点が同じならこれが最小コストのはずだ。

始点と終点が異なる場合、最後に終点まで行くとき、そのパス上にある橋を渡ることになるが、この時、戻る必要性がないので、渡った時点で即撤去できる。 つまり、始点と終点が異なる場合、始点から終点までのパス長ぶん戻るコストを節約できるという訳である。 よって、始点と終点が異なる場合の最終コストは始点を固定した場合、その始点から最も長い長さの葉ではない島を終点とした時である。

コードとしては、DFSで始点と終点が同じと仮定した場合のコストを計算しつつ、始点からその島までのコストを持つことで最も遠い島を探すようなコードになった。 最も遠い島に関してと始点と終点が同じ時のコストを計算するDFSを分けてもDFS1回の計算量が高々ノード数程度なので、十分に間に合う。

感想・反省

3度目の参戦となり、今までの反省を活かせたんじゃないかなと思っている。 1度目は個人としての能力があまりにも低すぎた&相方がガチ勢だったので、足を引っ張るだけのゴミだったのだが、 2度目は自分の能力もそれなりについて、相方もほぼ同レベルだったが、結構足を引っ張ってしまったと反省していた。 原因はちゃんと実装を細かいレベルで考えていなかったことで、 方針は立っても細かいところでつまり1台しか使えないパソコンをかなり占有してしまった。

今回は相方が実装している間に、実装の細かいところをじっくりと考えたので、実装はかなり早く終わったのではないかな、と思っている。 前回の僕であれば、Eで始点・終点それぞれ固定して探索しようで行けると思い込んで実装に詰まっているところだった。 あと、チーム全体和やかな雰囲気だったので、練習量も個人の能力もそこそこだった割にはいい成績を残せたのかなと。

ただ、今回も反省はあって、入出力パターンの確認はしっかりやるべきだった。 これで1回躓いてしまった。ロスは小さかったかもしれないが、やはり、事前に意識すべき範囲であった。

まとめ

ICPCにおいて最も重要なこと、それはパーフェクト・ハーモニー、完全調和だ!

(強い人に怒られそう)

Vimでコードリーティング

| Comments

C言語で書かれた比較的大きなプログラムを読むことになったので、 やり方をちょっと調べながら試している。

今まではVim+ctagsでタグジャンプして読み進めるで対応していたが、 大きめで呼出がアッチコッチ飛ばされたりするとなかなかつらい。 また、一度読んだところも頭に入らず、もう一度読むという事もしばしば。

ということで、この辺を参考にする
人間とウェブの未来 – GNU GLOBALとvimで巨大なコードでも快適にコードリーディング
ひらメソッド初心者奮闘記(PDF)

ひらメソッドっていうのは、コードを読みながら、 関数ごとにwikiのページをつくって、ボトムアップに読んで行きましょうというもの。 コードを読む時、GNU GLOBALとVimを連携させることで、定義にポンポン飛べる。

で、wikiなのだが、pukiwikiを使って管理しろみたいなページを結構見かけたけど、 環境構築面倒だし、pukiwikiは更新止まっているとかいう噂も聞いたしで気が進まない。 なので、Vimwikiを使うことにした。
Vimwiki : Vimエディタ上で動作するWiki環境

僕がVimwikiを導入した時、なぜかページを編集するたびエラー吐いて何かなあと思ったら、 シンタックスファイルで使われているoptionsとかいう変数が 他のプラグインと衝突していたらしく、 optionsをvimwiki_optionsとかに置換したらなおった。

まだ、手探り感あって上手くいくかわからんが、とりあえずこれで。

Eigenで疎行列を扱う

| Comments

ある方程式とかを解くときに、行列をつくるということはよくやるが、 その内の非ゼロ要素が極端に少ない場合、行列がムダにおおきくなってしまうので、 疎行列用のクラスを使ってやる必要がある。

Eigenの場合、SparseMatrixという疎行列クラスがあるので、これを使えば行列のように 簡単に扱えて便利だった。 boostとかにも疎行列用のクラスはあるのだが、どこのサイトで見たか忘れたが、各種ライブラリと速度比較してEigenはかなり優秀だそうで。

検索しても情報が少ないが、公式のチュートリアルとリファレンスが最もまともな資料だった(ともに英語)。
Tutorial page 9 – Sparse Matrix
SparseMatrix< Scalar, Options, _Index > Class Template Reference

要素のセット方法を探すのに結構手間取った。 個別に要素をセットするときはinsertメソッドを使い、 まとめてセットするならTutorialのFirst Exampleにあるみたいに、Eigen::Tripletのvectorをつくってから、setFormTripletsでやるのが楽かなって感じ。

Markdownをvimで扱う

| Comments

最近、ノーパで授業ノートを取る機会が増えてきた。 今まではプレーンテキストで何とかしていたのだが、さすがに整形しないとあれなのでmarkdown記法を使うことにした。

そのために以下のプラグインを導入。

vim用のmarkdownのシンタックスファイル。 数年前はバグがあるとか叩かれていたみたいだけど、最近も更新されているようなのでそういうことはもうないと思われる。 少なくとも、僕はまだバグに出会っていない。

編集のプログラムをその場でさっと実行するためのプラグイン。 これを使うことで、markdown記法のテキストをサッと整形してブラウザでプレビューさせることができる。

vimから指定したURLをブラウザで立ち上げるプラグイン。 quickrunと組み合わせて使った。

これらのプラグインを導入した後、vimrcに以下の記述を追加。

let g:quickrun_config = {}
let g:quickrun_config.mkd = {
            \ 'outputter' : 'browser',
            \   'command': 'pandoc',
            \   'exec': '%c --from=markdown --to=html %o %s %a',
            \ }

pandocはmarkdownのテキストをhtmlに変換するコマンド。 他にももっといいのがあるらしいのだが、aptで簡単に導入できるので今回はこれを使った。

これで<Leader>rでブラウザで仕上がりがプレビューできる。

参考:
vim-quickrunとMarkedでmarkdown編集が快適になった – Glide Note -グライドノート
Vim-users.jp – Hack #230: Markdown形式の文書を書く2 (quickrun0.5.0対応版)

本当はリアルタイムでプレビューとかする方法もあるらしいが、とりあえずこれで満足した。

VimShellを久々に使ってみたら便利だった

| Comments

以前、VimShellを使おうとして入れてみたのだが、はっきりとした理由は忘れたが、いまいちなので使わなかった。 が、久々に使ってみると普通のシェルのように使えるようになっていた。

install

ここから

導入にはvimprocが必要で、加えてunite.vimとneocomplcacheがないと、一部の拡張機能が使えない。

使い方

:VimShellでshellになる
インサートモードで入力、コマンドモードでは普通にいつものvimみたいに動いて、 ヤンクとかもできる。
インサートモードではCtrl+lでコマンドの履歴表示、tabで補完がつかえる。
:VimShellPopで画面の一部でVimshellが起動するのでちょっとしたコマンドを起動するには便利。

:VimShellInteractive [任意のインタプリタ]

はスクリプト言語を走らせるのにはかなり便利で、vimで編集しているテキストをそのインタプリタに送りつけるという事ができる。

非同期でコマンドを実行してくれるので、 コンパイルしながらちょっとコードの確認とかいうこともできる。

以前はインタプリタはiexeとかしないと動かなかったんだけど、そういうこともないみたい。

欠点

bashrcやzshrcとの連携機能は無いので、そっちで独自の設定をみっちりやっていると使いにくいかもしれない。
エイリアスくらいなら自動変換ツールくらい誰かつくっていそうなものだが。

コマンドの補完はやはり賢くない気がする。加えて、個人的にneocomlcacheの動作がイマイチだと思ったので普段は使わないのだが、 これを使わないと、ファイル名補完くらいしか効かない。

あと、gnuplot -persistでプロットしたグラフがgnuplot終了後消えてしまった。

とかまあまあ、完全なシェルとしてはさすがに使えないにしても、十分に使う価値のあるツールだとは思う。
更新も活発だし、作者はzshを目標としているらしいので、これからもどんどん良くなっていくのではないでしょうか。