RustでOSを書くプロジェクトもろもろ

2020/05/06更新：
新しい記事を書きました。こちらのほうがより新しい情報が乗っていると思います。

巷でよく聞くRustでOSないしベアメタルプログラミングの試みの備忘録。
Rustにはとても興味があってかつ大学での研究分野が低レイヤー系だったので面白そう思ったのだが、
いざやろうとしてみるといろいろなハードルがあるようで、ベストプラクティスも確立していないっぽい。
ので、とりあえず適当に漁った資料をまとめてみる

C以外でのベアメタルプログラミング

oruminさんのKernel/VM勉強会での発表のSpeaker Deck。自前のbinutilsとxargoを使ってベアメタルプログラミングしている

RustでOSを書いてみる(環境構築編) - Qiita
Introduction Rust for Creating Your Operating System - Qiita

実際にOSを書いた（書いている）人の環境設定について。両方共OS自作本をベースとしているっぽい。

GitHub - redox-os/redox: Redox: A Rust Operating System

Rustによる本格的なOS。GUIが動作している。POSIX準拠とかではなく全く新しいOSをつくろうとしているらしい。
独自のツールチェーンを用意する関係、ビルドはDockerによる方法が一番安定すると思う（ビルド周りのドキュメントはいい加減だったりする）。

rumprun-packages/rust at master · rumpkernel/rumprun-packages · GitHub

Rump Kernelを使ってRustでhello worldしている。しばらくメンテナンスされていないが、一応動くっぽい

Writing an OS in Rust

RustでOSを書いたというブログ（英語）

The Case for Writing a Kernel in Rust

今年のAPSysでの論文。RustでOSを書くときの所有権周りのデザインについて論じている。この論文ではOSそのもののパフォーマンスとかの評価はない。

Multiprogramming a 64 kB Computer Safely and Efficiently

上の論文の著者がSOSPに出した論文。この論文ではRustがどうのとかよりも単純にOSとしてのデザインについて論じているっぽい（まだちゃんと読んでない）

Tock Embedded Operating System

上２つのの論文の実際のプロダクト。OSSになっている。

System76でGalago Proを購入

使っていたノートパソコンが全く起動しないレベルで壊れたので新しいものを購入することにした。
趣味の開発で使うのが主な用途となるのだが、スペックの条件としては

  • メジャーなLinuxディストリビューションが動きそう
  • ディスク容量500GB以上（256GBだとすぐかつかつになったので）
  • そこそこ強いCPUとそこそこ大きいメモリ
  • 持ち運びを考えて重量は1.5kg以下

はじめはLet’s Noteなども検討したが、20万円を超える額が必至だったので断念。
それで友人に勧められたのがSystem76のGalago Pro

デフォルトOSとしてUbuntuが入っており、ディスク容量やCPUスペックなどもカスタマイズ可能。
なんでも10年くらいLinuxの乗るPCを販売している会社らしく、デバイスの不具合もちゃんとパッチを投げて対応しているらしい。
値段も海外の会社ゆえ送料が結構かかるのだが、それ込みでも20万円切る価格で買えた。
自分が注文した時期が良かったのか、注文から届くまで2週間かからなかった。

その他良い点としては

  • Ubuntuのバージョンとして16.04と17.04を選択できた
  • 画面の解像度がデフォルトでは細かすぎて字が小さいのだが、設定でいい感じになおせた

注意点・不満点としては

  • ACアダプタがアメリカ仕様のため変換アダプタが必要（変圧は必要なし）
  • キーボードは英字キーボードのみ（最近、英字キーボードを使う場面が増えていたのでそこまで問題ではなかった）
  • 購入の手続きでクレジットカードの利用明細に記されたコードを送信するのがちょっと面倒
    • 不正利用防止のためとして、利用明細に記されたコードを送るのだが、購入の情報がウェブの利用明細に反映されるまで3日ほどかかった
  • バッテリー持ちはそんなによくない。多分4時間位
  • Xenを入れたら起動しなくなった

あとは耐久性が気になる。以前使っていたのが1年位使って一度SSDが死んでメーカー修理に出して、その1年後今度は初期の起動エントリーすら出ないレベルで死ぬということになったので、そういうことにならないといいな。

ARM向け自作ハイパーバイザーT-Visorを公開しました

修士の研究としてつくったARM用ハイパーバイザ「T-Visor」を公開しました。
https://github.com/garasubo/T-Visor

(2016/05/24 ちょっと加筆しました）

背景

組み込みの世界でもLinuxのような汎用システム向けOSが使われるようになる一方、
リアルタイム性の保障やセキュリティ等の観点からリアルタイムOSの需要も高い。
そこで、ハイパーバイザを使って汎用OSとリアルタイムOSを同時に動かす、というような研究や製品が結構あります。
具体例を上げれば、ロボットの姿勢制御などをリアルタイムOSできっちりとやる一方、
画像処理やネットワーク機能とかを使ってクールな機能だけど最悪バグっても安全には支障がないといったものをLinux側で、といった感じです。
実際にARMの一部シリーズではIntel VT-xのような仮想化支援のハードウェア機構が備わっていて、
KVMやXenはこれらに対応してARM上でも動くようになっています。

しかし、XenやKVMはLinuxをベースにしていてシステム全体が重い、リアルタイムでないなどの問題点があります。
Linuxなどのスケジューラは短い一定周期ごとに確実にこれこれをしなければいけない、といったような要請（ハードリアルタイム）を満たしにくいことが知られています。
リアルタイム性や組み込み用途というものを重視しようということで開発したのがT-Visorです。
このT-Visorは動作にLinuxやその他標準ライブラリを要さず、Cortex-A7/A15での動作が可能です。
方式としてはハードウェア上で直接動くType-1型で、仮想マシン上で動くOSをに対して変更がいらない完全仮想化をおこなっています。

ざっくりとした技術的な説明

このT-VisorはARMv7-Aの拡張のひとつであるVirtualization Extensionsを利用することで、
完全仮想化Type-1型のハイパーバイザを実現しています。
この拡張でHypモードというプロセッサモードが追加され、プロセッサ全体に影響を与えるような命令に対してトラップをかけてこのHypモードにさせる、ということが可能です。

メモリアクセスですが、通常のMMUに加えてStage-2のMMUというものがあり、これは仮想マシン上での物理アドレスを中間物理アドレスとして受け取り、
実物理アドレスに変換させたうえでメモリアクセスをさせると言うものです。
これにより、仮想マシンは自由にMMUを使うことができる一方、ハイパーバイザ側でアクセスできるメモリ領域を制限することができます。

仮想デバイスドライバは基本的には実装していません。ARMのIOはすべてMMIOなので、アクセスできるメモリ領域を制限することで、
仮想マシンから触れるデバイスは制限されています。
また、外部からの割り込みも一度ハイパーバイザにトラップされるので、割り込みについてもどの仮想マシンが受け取るかを制御できます。

割り込みに関してはGICという割り込みコントローラで管理されています。
ゲストOSもこのGICを使って割り込みをコントロールするので、競合が起きないよう対応が必要です。
このGICはある程度の部分が仮想化対応されているのですが、ある程度の部分に関してはなされていないので、
先述のStage-2 MMUを使うことで、アクセスをコントロールすることで仮想割り込みコントローラを実装して対応します。

リアルタイム性を保障するためスケジューリング方式が重要になってきますが、ユーザーが設定しやすいようにということを意識してフレームワークが設計されています。
具体的には実装すべき関数をいくつか定め、その中ではあくまでスケジューリングに関することのみを行い、
仮想マシン内部などには干渉する必要がないようにされています。
サンプルとして固定優先度式とEDF方式のスケジューラが実装されていますが、設定により静的にひとつのスケジューラのみが組み込まれるようになっています。

仮想マシンの数やそのメモリ割当等の設定はコンパイル時に決定されます。
現状はソースコードにベタ書きしていく感じになっているので、まともなconfigureについてはfuture workのひとつです。

起動に関してですが、ブートローダはU-Bootを使って動作させていました。
ただし、U-Boot固有の機能に何か依存していたわけではなく、メモリ上に外部からハイパーバイザとゲストOSが展開できるようなものならなんでもよいです。

動作確認として無修正のLinuxを動かし、各種ベンチマークの動作を確認しました。
また、複数のリアルタイムOSを動かして、OS間通信ができることも確認しています。
Xen4.4とも比較実験をおこなっていて、詳細は省きますが、基本的にポジティブな結果が出ました。
ただし、Xen4.5で割り込みに関して性能改善がなされたらしく、そちらとはまだ比べられていません。

主要なソースコードの中身

ソースコード読みたい人向けに簡単に説明しておきます。

  • vcpu.c
    • 仮想CPUの状態管理を行う
  • hyp_call.c
    • 仮想マシンからのhyp例外を管理する
  • virtual_gic.c
    • 割り込みコントローラについての仮想化を担っている
  • schedulers/
    • 各種スケジューラの実装
  • users/
    • この以下のディレクトリのうちひとつを選択することで、ハイパーバイザ上でどのようなアプリケーションを使うかを決定する
  • boards/
    • ハードウェア依存部分を置くところ。

課題と今後やりたいこと

まず第一に、複数OSは動かせることは確認しているものの、ひとつのVMに対して仮想CPUを複数提供することには失敗しています。
また、このハイパーバイザはコアをひとつしか使うことができません。
前者に対してはPSCIというコアを管理するためのインターフェースがARM側では定義されているので、
それに乗っ取り、仮想CPUを操作するインターフェースを実装済みではあるのですが、いざLinuxを動かしてみると起動途中で止まってしまいます。
どうも２つのコアとも処理できるスレッドがなくなってスリープしているようなのですが、はっきりとした原因がわかっていません。
原因として考えられるのは

  • 割り込みコントローラの仮想化部分がバグっていてハードウェアからの信号待ちのようになってしまって動かなくなっている
  • コア間の状態保存・復帰がバグっている
  • キャッシュ・TLBなどが適切にcleanできていない
    などなのですが、未だにはっきりとつかめていません。

また、仮想マシンの管理のconfigがよくない感じなのは前述のとおりなのですが、それ以外にもコードの構造がひどいことは重々承知していて、
そこをまず叩き直さなければならないという話もあります。
そもそも一人で書いているはずなのに気分でコード規約が変わって名前の付け方が色々おかしいとか、もしかしたらインデントも統一されていない部分もあるかも…
あとは今のところ全部C言語とアセンブラで書かれているのですが、C++で書くともっとすっきりするかもしれませんね。

OSや組み込み開発に対してほとんど知識がない状態ではじめたため、かなり拙い部分もありますが、まあなんとか動作することができたのはよかったかなっと

補足

現在、動作確認はCubieboard 2で行っています。
Raspberry Pi2だと割り込みコントローラの関係上、動かすのに大変な労力が必要となります。

あと、課題とかいろいろ書きましたが、現在は基本的に開発止まっています。
私の能力では解決が難しいというのがひとつ、つくったとしてもそれを使ったアプリケーションをつくる機会がないといったモチベーションの問題がひとつです。
ただ、興味ある人がいれば連絡くれると幸いです。ある程度協力できると思います。

ちなみにこのタイミングで公開したのは、ソースコードを多少はマシにしたかったというのもそうなのですが、
これについて書いた論文がリジェクトされたからです。
評価が甘かったりアプリケーションが見えにくかったというのが主な原因なのだろうか、アカデミアの道は厳しいですね。
この手の分野はクローズドソースなものが多すぎたり、ハードウェア依存な部分が多かったりで、実装までこぎつけても評価が…ってなるのは悲しい

論文紹介ー"Jitsu: Just-In-Time Summoning of Unikernels"

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

論文概要

Jitsuという、Unikernelを使う組込みプロセッサでWebサービスを提供するためのツールをつくりましたというお話。
著者はMirageOSを開発でお馴染みの方々が並んでいますね。
会議は今年のNSDIで、USENIX系の会議なので論文も著者のスライドも無料で手に入るので、
こんなブログを読まずともそちらを読んでしまえば全て完了するのではという気がしますが…

予備知識

最近ちょくちょく話題になりこの論文のキーともなるUnikernelについて簡単に説明しておこうと思います。

Unikernelとは、動かすプロセスを1つに限定することで様々なOSの抽象化を簡略化してライブラリのようにすることで、
アプリケーション単体でプロセッサで動くイメージとしたもの、といったとこでしょうか。
代表的なのはMirageOSとかOSvとかですね。
Unikernelの詳しい説明については、
Unikernels: Library Operating Systems for the Cloud
がよいでしょう。
英語版Wikipediaにも記事があります。
Unikernel - Wikipedia, the free encyclopedia
もう少し体系的でざっくりとした話だと、このスライドとかわかりやすいかもしれません。
An Introduction to Drawbridge(ja) // Speaker Deck

今回使うUnikernelはMirageOSなのですが、これはOCamlで書かれており、
OCamlにはARM用のコンパイラがあること、MirageOSが動作する環境であるXenがARM向けに対応していることなどが幸いしてか、
一部のARMボード上（CubieBoard2など）で動作するようです。
私も試してみようとCubieBoard2を購入したのですが、コンパイルでこけてしまいましたが。

論文の中身

研究背景

クラウド環境からサービスを提供することが流行っているが、クラウド環境への通信のオーバーヘッドが厄介。
また、IoTのデバイスはセキュリティの脆弱性が問題になる。
そこで、組込みハードウェア上でXenなどのハイパーバイザを動かしサービスを提供できれば、
ユーザーに近い位置でのサービス提供が可能となるため通信のレイテンシが緩和される。
また、ハイパーバイザを使うことで各サービスを独立で動かせる。

実現したこと

組込みデバイスで動くネットワークアプリケーションをセキュアに管理するためのツールを、Xenのツールスタックとして実装した。
VMとしてUnikernelを使うことでより低いlatencyでネットワークリクエストに応答する。

実装

XenのツールスタックをXenStoreを拡張し実装。
目標としては、サービスがネットワークに対してきちんと応答するようにするが、必要のないときはリソースがもったいないのでサービスを停止させましょうというもの。
そのために

  • Unikernelのブート時間の最適化
  • VM間コミュニケーションプロトコル”Conduits”の実装
  • 外部クライアントからのアクセスに対して、起動時間のレイテンシを隠蔽するためのディレクトリサービス”Synjitsu”の実装
    を行っている。
    Xen上でVMの設定値を管理・保存するためのツールスタック
    XenStoreを拡張することによって行なわれる。

ブート時間最適化

起動時の仮想デバイスの割りあてを並列処理したことと、
OCamlによるXenStoreトランザクションを利用することで高速化。
また、Unikernelを用いるたので、そもそものバイナリサイズが小さいためそれも高速化に寄与している。

Conduits

vchanという共有メモリを用いたデータパスを利用し、OCamlでvchanのプロトコルを実装。
ランデブーのためのインターフェースがvchanにはないので、XenStoreの名前空間を拡張してランデブーインターフェースを提供。

Directory Service

DNSのリクエストをどのUnikernelに割り当てるかをマップしているもの。
DNSのリクエストによりUnikernelが起動し、その後外部クライアントからTCPのリクエストが送られてくるのだが、
起動が完了していないとリクエストに応答できない。
そこで、起動前の場合、ひとまずリクエストをXenStoreに保存しておき、Unikernelとの間に割り込んでいるSynJitsuがTCPのACKを返しておく。
その後、Unikernelが起動すると溜まったリクエストへの応答を開始し、Synjitsuを介さずにクライアントとUnikernelが直接やり取りを開始する。
このようなことをしないと起動前のTCPパケットがタイムアウトして再送までの時間がかかってしまうため、
サービスのレスポンスが下がってしまう。
わかりやすい図が論文にあるので、そちらを参照されたい。

評価

いろいろなパフォーマンスを計測するための実験を行っているが、
そもそもARMボード上でこのようなことをやるというのがなく、
比較ができていないといった印象を受けた。
セキュリティに関しては、CVEのリストにある脆弱性のうち、どれがJitsuでは影響があるか調べている。
Unikernelを用いているため、
基本的にはLinuxのデバイスドライバ部分やカーネルそのものバグとXenに関するものしか受けず、
SSH overflowのようなアプリケーションよりのものは影響を受けない。

関連研究・議論

コンテナ型仮想化であるDockerやDrawbridgeなどが紹介されている。
UnikernelがよりOSの各種抽象化を省略しアプリケーション特化の構成になっている。

この研究はXenのABIを変えたりなどはしていないため、他のツールと併用することも可能。
ConduitsもMirageOSに特化したものではないため、プロトコルを実装すれば他のunikernelでも利用可能。

まとめ・私見・愚痴

Unikernelを使うことでARMボード上でWebサービスを素早く提供できるJitsuというXenのツールスタックを実装した、というものでした。
全体的に雑な説明になってしまいましたが、まあ、細かい話は論文を直接読んだほうがいろいろ手っ取り早くわかるでしょう。

最近ではDockerでUnikernelを動かすとかよくわからない話も上がってきたりして、
段々と注目度が上がっているようなので、このようなUnikernelを活用したシステムがこれからもいろいろと出てくるのでしょうか。

12日目といってもまだ2人目ですね。
システム系やっている人ってやっぱり少ないなあと思うし、
成果を出すのに時間がかかることが多かったりするせいか評価されることも少ないし、
いろいろとつらいなあと思う今日このごろ。

LaVie Z750にWindows 8.1+Arch Linuxのデュアルブート環境構築

今使っているLet’s noteがパーティション分けミスってLinuxの容量がかつかつになってしまったっていのと、ハードウェア的にポツポツと不具合が出てきていたので、新しいパソコンを買った。
LaVie Z750を選んだのは軽いのと、SSD 256GBにOffice付きのわりに安かったから。

今までUbuntuに甘えてきたが、思い切ってArch Linuxにすることにした。
Gentooも考えたが以前挫折したこと、資料がArchのほうが充実している感じだったことを考慮してArchを選んだ。
Archのバージョンは2015.01.01のを使った（以前ダウンロードしていたので）。

基本的には公式wikiのBeginner’s guideに従うだけ。
英語と日本語があるが、英語のほうがinstallまでの説明が詳しい一方、日本語はinstall後の作業の説明がついている。
Beginners’ guide - ArchWiki.html
Beginners’ Guide (日本語) - ArchWiki

躓いたのはまずパーティション分け。
今回取った方法は

  1. Windowsのコントロールパネルから「管理ツール」→「ハードディスク パーティションの作成とフォーマット」でWindowsパーティションを縮小
  2. Archのブートメディアからgdiskで空領域にパーティションを作って、mkfs.ext4で初期化
    というもの。

あとはインストール中の/bootにどこをマウントするか。
/dev/sda2をマウントすればいいのだが、はじめはこれをスキップしてしまい、後々面倒なことになった。

日本語環境化はここが参考になった。
Arch Linuxに日本語環境を構築する

Xenで使っているディスクイメージの容量拡張

Ubuntu 14.04にXenを入れてその上でArch Linux(2015-01版）を動かしている。
ディスク容量が足りなくなったので増やそうと思ったのだが、virt-managerあたりからはいけそうな雰囲気がなかったので、
適当に調べた方法を試したら上手くいった。

念の為、ディスクイメージのバックアップをとっておくことを推薦

  1. Ubuntu上でディスクイメージの後ろにほしい長さ分だけ追加
    ディスクイメージは/var/lib/libvirt/imagesの中とかにある。

    1
    dd if=/dev/zero bs=512M count=20 >> arch.img

  2. ゲストOS上でパーティションを再構築fdiskとかで一番後ろのパーティションを一度dで破壊して、nでもう1回つくるとき後ろまで最大限まで伸ばす。
    その後wで保存。自分の場合、マウントされているパーティションを伸ばしているので、認識させるには一度再起動する必要がある。

  3. 再起動後、resize2fsでパーティションを拡張、df -hでパーティションが拡張されていることを確認。

参考：Xenで使用しているディスクイメージを拡張する | misty-magic.h

あなたとHexo

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

Hexo

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

Octopress vs Hexo

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

Migration | Hexo

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

新しいブログ

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

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

タイトルの通り。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開発あれこれ

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固有の機能が絡んでくる動作もちゃんとテスト出来るのはうれしい。