HIW 2019で発表された、Copilotという内部DSLについて

~HIW 2019参加レポート その4~

Posted by Yuji Yamamoto(@igrep) on October 1, 2019Tags: Haskell Implementors' Workshop

前回から引き続き、Haskell ImplementorsWorkshop 2019への参加レポートとして、私の印象に残った発表を紹介します。
今回は、Copilotという、C言語のコードを生成するHaskell製内部DSLについての発表です。

Link to
here
Copilot 3.0: a Haskell runtime verification framework for UAVs

発表者: Frank Dedden Royal Netherlands Aerospace Center, Alwyn Goodloe NASA Langley Research Center, Ivan Perez NIA / NASA Formal Methods

Haskell製の内部DSLからC言語のソースコードを生成する、Copilotの紹介です。
似た謳い文句の内部DSLとしてivoryがありますが、Copilotは、ハードウェアの実行時検証を行うC言語のコードを生成することに、より特化しています。
「センサーから信号を受け取って、一定の条件を満たした場合に何らかの処理を実行する」という処理をHaskellで宣言的に記述すると、メモリの消費量・実行時間において常に一定なC言語のコードを生成することが出来ます。

メモリが限られていて、リアルタイムな処理が必要なハードウェアにとって「邪魔にならない監視」を実現するための必須条件なのでしょう。
現状HaskellGCが必要であるといった制約もあり、リアルタイムな処理や厳格なメモリー管理が必要な機器での採用は難しいですが、Ivoryや今回発表されたCopilotはあくまでも「C言語のコードを生成するだけ」なので、生成するHaskellではメモリー管理をする必要がありません。
にっくきスペースリークに悩まされる心配もないのです。
こういったHaskell製内部DSLは、Haskellの持つ強い型付けによるメリットを享受しながら、変換した言語の実行時におけるパフォーマンスを出しやすい、といういいとこ取りなメリットがあるので、もっと広まってほしいユースケースですね。

Link to
here
Copilotを試してみる

  • ℹ️ 実際に使用したコードはHaskell-jp BlogGitHubのリポジトリーにあります。
  • ℹ️ 使用したcopilotパッケージのバージョンは、3.0.1です。
  • ℹ️ サンプルコードの解説については、notogawaさんのアドバイスも参考になりましたHaskell-jpslack-logではこのあたり。執筆時点でCSSが当たってないため読みづらいですが一応)。ありがとうございます!

せっかくなんでCopilotを試してみましょう。
公式サイトにあったサンプルコードそのまんまですが、生成されるCのコードを眺めてみます。

👇のコマンドでサンプルコードが入ったリポジトリーをgit cloneした後、

👇のコマンドでビルド・C言語によるコードの生成できるはずです。

こちらが生成元のHaskellのコードです。

まず、tempctempという識別子に定義した式が、センサーが発信する、連続的に変化する値を表しています。
Copilotの言葉はこれをStreamと呼んでいます。

specという識別子で定義している式が、「どのセンサーから信号を受け取って、どんな条件を満たした場合にどの処理を実行するか」規定しているようです。
👆の場合、ctempというStream18.0を下回ったらheatonというイベントを発火し、21.0を超えたらheatoffというイベントを発火する、と定めているわけですね。
そしてmain関数で実行しているreify spec >>= compile "heater"という箇所で、.hファイルと.cファイルを書き込んでいます。

そして、生成されたヘッダーファイルheater.hがこう👇

で、肝心のCのコード本体heater.cがこちらです。

先ほどStreamとして定義した値のうち、tempは、temperatureというグローバル変数と、それを一時的に保存するtemperature_cpyという二つの変数に翻訳されました。
specにおいてtriggerという関数で列挙した「どのセンサーから信号を受け取って、どんな条件を満たした場合にどの処理を実行するか」というルールは、stepという関数に現れたようです。
この関数を利用する側では、heaton関数とheatoff関数を別途定義した上で、temperatureにセンサーから受け取った値を代入してstepを呼ぶことによって、temperatureの値が条件に一致したとき、heaton関数とheatoff関数を実行してハードウェアの制御ができるのでしょう。
Haskell側で定義したもう一つのStreamctempは、heaton_guardheaton_arg0heatoff_guardheatoff_arg0、それぞれの関数に書かれた、temperature_cpyの値を変換する式に現れているようです。

正直なところこの程度であれば、直接Cで書いた方が余計なカッコもないし読みやすそうではあります。
tempctempに変換する式(150.0 / 255.0) - 50.0が変換後のソースコードでは冗長に適用されていることから、もっと最適化できそうですし。
とはいえ、わざわざDSLを作ったからには、より複雑で、Haskellでなければ書いてられないようなケースが、Copilotの開発者の現場ではあるのでしょう(なんせNASAの方も関わっているぐらいですから!)
詳しいユースケースや、ビルド時のフローといった運用方法を聞きたいところですね。