yutopp's blog

サンドバッグになりたい

RTMPのChunkStream, MessageStreamの話

yutoppです.

今回は,RTMPのChunkStreamとMessageStreamの2種類のストリームについて書きます.

それでは,一旦ストリームの種類の概要を紹介した後,RTMPの通信が2つのストリームの種類をどのように使い分けて通信するのかという説明していきます.細かいフロー(ChunkSizeやBandwidthの設定など)は割愛します.また,RTMPは実装によってパラメータがまちまちであるため,環境によってIDの番号などが異なると思いますので,適宜読み替えてください.

※この記事の指す"RTMP"は,AdobeのRTMPの仕様(v1.0)に基づくものとします.

RTMPのデータの送受信概要 (ChunkStream)

RTMPは,1つのTCPコネクションの上に細切れにしたデータ(Chunk)を多重化して送受信します.これによって,例えば映像などの大きいデータと音声などの小さいデータを送受信する際に,大きいデータがボトルネックとなって本来先に処理を行えるはずの小さいデータが中々届かないというケースを防ぐことができます.

f:id:yutopp:20180611040426p:plain

この多重化されて送られてくるchunkは,ChunkStreamと名付けられたストリームの単位で保持されます.このchunkには実際にはChunkStreamIDと呼ばれるIDがついており,上の図のようにChunkStream毎に振り分けられた後,読み込みが終了したものからデコードが開始できます.また,上記ではAudioとVideoのみですが,実際にはRTMPで処理されるメッセージ全てが対象となります(ハンドシェイクは除く).

RTMP論理ストリーム概要 (MessageStream)

上のChunkStreamはデータの送受信に使われる概念でしたが,RTMPには更にその上のレイヤでメッセージを振り分けるMessageStreamの概念が存在します.

f:id:yutopp:20180611071830p:plain

送受信を別のChunkStreamで行っていたとしても,例えば同じ動画に対するデータを処理する場合にMessageStreamとしては同じになるようなイメージです.

詳細

それでは,上記を踏まえてRTMPの通信を例にとって実際のデータ構造について説明していきます.

その前に,2つのストリームについての細かい補足です.

まず,ChunkStreamについてです.ChunkStreamは,ChunkStreamIDと呼ばれるIDによって区別されます.
このIDは2〜65599まで使うことが可能です(計65598ストリーム).しかし,その中でもChunkStreamID 2はRTMPによって予約されているため,ユーザーが自由に使うことはできません.それを除けば,ChunkStreamは生成や削除を明示的に行わなくても使うことが出来ます.

次に,MessageStreamについてです.MessageStreamはMessageStreamIDと呼ばれるIDによって区別されます.
このIDはuint32型の範囲で指定することが可能です.RTMPは,コネクションごとにコントロールストリームと呼ばれるストリームを必ず持ちます(MessageStreamIDは0).それ以外のストリームについては,自由に使うことはできませんcreateStreamコマンド(仕様: p36, 7.2.1.3)を用いて,サーバーからMessageStreamIDを発行してもらう必要があります.

では,実際のデータの流れを見ながらデータ構造を追っていきます.
前提として,通信の流れは以下のようなコマンドで得られたデータを用いています.

ffmpeg -re -i test.mp4 -codec copy -f flv rtmp://localhost:1935/live/hogehoge

また,ChunkStreamのChunkSize(Chunkのpayloadの大きさ)はデフォルトの128Bytesと仮定し,Ackなどのメッセージは無視するものとします.

1: ハンドシェイク

割愛.後述の参考文献にハンドシェイクについてのリンクがあります.

2: クライアント → サーバー: connectコマンドの送信

クライアントは,まずサーバーにconnectコマンド(仕様: p29, 7.2.1.1)を送信します.ffmpegではMessageStreamにはID 0(コントロールストリーム),ChunkStreamにはID 3を指定するようですね.
また,このconnectコマンドを含むメッセージはpayloadが157Bytesあるようで,ChunkSizeの128Bytesを上回っているため早速Chunkに分割されて送られてきています.

TCPで送られてくるデータは以下のようになっていました.

f:id:yutopp:20180611061247p:plain

赤い部分(03とc3の部分)がChunkの切れ目です.丁度payloadの長さが128Bytes(0x80Bytes)になるところでChunkが区切れているのが分かります.
これらのChunkのHeaderを見たら取り除き,payloadの部分のみをChunkStreamとしてバッファに保持していきます.メッセージの長さの分Chunkを読み終わったら,バッファをデコードし,MessageStreamIDに紐づくMessageStreamのメッセージとしてデータを処理します.
今回はMessageStreamIDは0なので,コントロールストリームにconnectコマンドのメッセージが来たものとして処理します(接続済みのステートにコネクションを変更する).

2.1: サーバー → クライアント: _resultコマンドの送信

割愛.connectに成功したので,NetConnectionの_resultをクライアントに返します.

3: クライアント → サーバー: createStreamコマンドの送信

動画データの送信を行うために,クライアントはcreateStreamコマンドをサーバーに送信します.メッセージの内容は特にありませんが,この時点でもMessageStreamIDは0を利用します.

3.1: サーバー → クライアント: _resultコマンドの送信

connectに成功したので,NetConnectionの_resultをクライアントに返します.
ここで,新しいMessageStreamとしてStreamIDとして1(とりあえず0以外)をクライアントに返します.MessageStreamID 0は既にコントロールのために用いているので,データ用に新しいストリームを作るということです.

f:id:yutopp:20180611064641p:plain

4: クライアント → サーバー: publishコマンドの送信

クライアントは,映像の配信を行うためにサーバーにpublishコマンド(仕様: p45, 7.2.2.6)を送信します.

f:id:yutopp:20180611065613p:plain

このとき,クライアントはcreateStreamで受け取ったStreamID 1をMessageStreamIDに指定していることが分かります.これ以降のNetStream系の操作は,createStreamによって得られたMessageStreamに対して行うようになります.

4.1: サーバー→クライアント: onStatusコマンドの送信

割愛.publishに成功したので,NetStreamのonStatusをクライアントに返します.

5: それ以降

クライアントは,ChunkStreamをvideoとaudio,metadataで変更しながら,MessageStreamIDはcreateStreamで得られたIDに固定でデータを送るようになります.

最後に

RTMPの仕様に出てくる2種類のストリームについて,実際に送受信するデータを追いつつストリームの用途を確認しました.

初めてRTMPの仕様を読んだときに,ChunkStreamとMessageStreamの用語と意味を噛み砕くのに少し苦労したので,今後迷わないように残しておきます.

参考文献

おまけ

GoでRTMPサーバーを書いているので,途中の知見を書いた.そのうちコードを公開するので,そのときにもっと細かく書けたら嬉しい.

技術書典3にサークル参加した

こんにちは。先日10/22に行われた技術書典3にサークル進捗大陸で参加しました。(youxkei氏、amutake氏、ありがとうございました!)

とても楽しかったです。お疲れ様でした。手に取ってくださった方々、スタッフの方々、本当にありがとうございました。

前回の技術書典2の参加記事や気持ちをもとに今回工夫したところがあったので、この記事も何かの参考になったら良いなと思って書きます。

表紙

前回 今回
f:id:yutopp:20170402131218p:plain:h240 f:id:yutopp:20171018192426p:plain:h240

前回は"タイトルから内容がわからない"という声があったので下の方に大きく内容を箇条書きしました。 メンバーのamutake氏が入稿の日に明け方までかけて作ってくれました(感謝)。おしゃれですね。

いま落ち着いてみると、"タイトルから内容がわからない" は解決できてないですね。おわり。次はうまくやります。

タイトルと内容は同じ方向を向いていて分かりやすいものが目に止まりやすいかもな、と思いました。

持ち物

前回 今回
(手ぶら) ブックスタンド、サークルカットぶら下げるやつ、ペン、紙

前回は何も持っていかなかったので、いい感じの本の展示もできず(ダンボールに立てかけていた)、文字も書けなくて辛かったです。上記の4つは必要だと思いました。

また、"サークルスペースに引く布"も必須な気がしました。敷物があるだけで雰囲気が全然変わります。
今回も敷物を忘れたので、納品された本が包まれていた紙を敷いて使っていました。

f:id:yutopp:20171024015936j:plain:h240

次はうまくやります。

決済システム

今回は、技術書典決済システムとpixiv payに対応して向かいました。

システム 回数
技術書典決済システム 8回
pixiv pay 0回

という結果でした。アプリはどちらも使いやすかったです! 技術書典決済システムもスムーズで便利でした(途中に操作ミスがあり申し訳なさがありました… 次はうまくやります)。

アプリは個人の端末にインストールしていったので、自分が昼ご飯を食べていると決済システムで自サークルの決済が出来ない感じになってしまいました。すみません。対策をしたい。

頒布部数 (余り/持ち込み数)

前回 今回
物理 0/30部 物理 1/80部
ダウンロードカード 50/98枚 なし

前回は正午過ぎ辺りに物理本が0部になったので、今回は多めに80部を持っていきました。結果はほぼ余りなく終わることが出来ました。ありがとうございました。

ぼく「30部でよさそう」amutake氏「80くらいいけるのでは」ぼく「ボ」という感じで決めました(結果オーライ)。

内容がニッチなので不安でいっぱいでしたが、技術季報のレポートにある平均あたりくらいの部数になった気がしました。

また、今回ダウンロードカードは作れませんでした。すみません。
前回は前日に自分がgoでダウンロードサーバを作って、夜中にamutake氏がシリアルコードを印刷していたのですが、今回は体力が尽きていました。

次回があるとしたら、S3に置いて物理本にシリアルコードの紙を挟むやつでやりたいです。

ページと印刷の値段

前回 今回
52ページ30部, 16200円 (540円/1部) 68ページ80部, 27300円 (341円/1部)

頒布は、前回も今回も1部500円を設定しました。

なんと前回は紙の本を売る度に赤字になる状態でした(大草原)。ダウンロードカードによってなんとか赤字を免れることが出来ました。

今回は大丈夫でした。サークル参加費や諸経費を考えると、自分のサークルではこのあたりの価格帯がギリギリな感じがしました。

印刷所

ねこのしっぽのねこスパークというプランを利用しました。
締め切りや値段、質、部数(なんと見本用で+2冊つけてくれました)を考えると本当に最of高でした。感謝します…

まとめ

次回は締め切り1ヶ月前に分かりやすいタイトルで良い記事を書きあげるぞ!!!

とにかく、今回の技術書典も本当に楽しかったです。ありがとうございました。

技術書典3に同人誌を出す回

この広告は、90日以上更新していないブログに表示しています。を消したい。

こんにちは、yutoppです。イカ2ばかりしていたら前の記事が200日前などとなっていますね。

さて、10/22に行われる技術書典3に再びサークル進捗大陸で参加します。ので宣伝をします。

今回のサークルページです。詳細についてはこちらを参照していただけると嬉しいです。
場所はお16です。

今回出す本は進捗大陸02です。

f:id:yutopp:20171018192426p:plain

500円です。!!!pixiv payと技術書典決済システムが利用可能です!!!
後日電子版をboothで頒布します。こちらは300円です。

今回の目次です。今回は目次を作りました。


  1. 自作言語 Rill と WebAssembly (@yutopp, 12ページ)

    1. 前回の進捗大陸 01 からの自作言語の進捗
    2. WebAssembly サポート
      1. シンプルに Hello world!
      2. ランタイム移植問題: リンクとlibc
      3. ランタイムビルド
      4. 全てリンクしたバイナリを作る
      5. 実行
      6. 問題点
      7. 今後の展望
    3. まとめ
  2. 抽象解釈による,再帰を持つ関数型言語の符号解析 (@youxkei, 22ページ)

    1. はじめに
    2. 再帰を持つトイ言語
      1. 構文
      2. 型付け規則
      3. 意味論
      4. 型システムの健全性
      5. 符号解析
    3. 符号解析
      1. 抽象値
      2. 抽象環境
      3. 符号解析の定義
      4. 符号解析の well-defined 性
      5. 符号解析の健全性
    4. 符号解析の例
    5. まとめ
  3. 証明付き分散システムを作ろう! (@amutake, 26ページ)

    1. イントロダクション
      1. 本稿の流れ
    2. Coq の概要
      1. Coq のインストール方法
      2. Coq を使ってみる
      3. コード抽出(extraction)
    3. Verdi の概要
      1. Verdi の使い方
      2. ネットワーク意味論
      3. VST
      4. まとめ
    4. Verdi を使って分散システムを作る
      1. Verdi のインストール
      2. ブール値保管システム BoolServ
    5. Verdi による Raft の証明
      1. Raft の概要
      2. Verdi チームが証明した定理
      3. Verdi による Raft の実装
      4. Verdi による Raft の証明の流れ
    6. まとめ

以上の本体60ページくらいの本になります。読み応えがあります。

よろしくお願いします!!!!

技術書典2に同人誌を出す回 / Aizu Advent Calendar 2016 24日目

おはようございます。Aizu Advent Calandar 24日目の @yutopp です。
今日は、2016/12/24なので、なんの問題もありませんね………。

今回は、2017/4/9にアキバ・スクエアで開催される技術書典2に、サークルで出るので宣伝します。
サークル名は進捗大陸です。スペースは う-17 です。

今回出す本は 進捗大陸01 です。

f:id:yutopp:20170402131218p:plain

本の内容ですが、

となっています。

自作言語 Rill の実装とあれこれは、自分が書いた部分です。
自作言語Rillの紹介と実装の一部分について書きました。本当にふわっとしているので、ふわっとです。

抽象解釈による関数型言語の静的解析は、@youxkei氏が書いて下さいました。ありがとうございます。
この章では、ミニマルな言語を定義し、形式的にその言語の型付けと意味論をしたのち、符号解析を行う抽象解析を定義し、健全性を証明していきます。 抽象解析は、プログラムそのものの具体的な値を計算して解析するのは複雑すぎるので、値の性質のみを見るなどして抽象化した値を計算して解析するようなアプローチです(おそらく)。この章では、値の符号を計算する符号解析が例として用いられます。定義や健全性も証明付きで、1ステップずつ進んでいくので、とても理解しやすいです。オススメです。ぜひ最強の静的解析を目指しましょう。

静的に型がつく Erlang を目指しては、@amutake氏が書いて下さいました。ありがとうございます。
この章では、Erlangの静的型チェッカであるdialyzerが用いている型システムsuccess typingsの解説とその問題点、Erlangの型システムを設計する難しさ、問題解決の鍵になるかもしれない型システムMLsubの解説とその拡張について考察していきます。
日々Erlangで大きめのプログラムを書いていると、dialyzerの便利さに救われることも多いのですが、一方で型チェックやリソース食いすぎ問題に困ることも多々あり、もっと良い型チェッカはないものかと考えてしまいます。この章は、それらの問題に立ち向かったとある型プロの考察です。現行の型システムsuccess typingsや、新たな希望のMLsubの解説が詳しく載っています。オススメです。ぜひ最強の型システムを作りましょう。

以上の47ページくらいの本です。500円です。ぜひよろしくお願いします!!!エイプリルフールではないです

K-frameworkの紹介 #1 - Aizu AdC 2015 / 20日目

おはようございます.Aizu Advent Calandar 20日目の @yutopp です.
前の人は @GUCC1_sp1ritu4l,次の人は @ishi_kuro です.

今回はK-frameworkというプログラミング言語の意味付けをサポートするフレームワークの紹介をしたいと思います.
日本語の資料がほとんど無い(英語もない)ので,どんどん使っていきましょう!!

間違えなど含んでいると思われます.ご指摘いただけると嬉しいです.

K-framework is 何

概要やチュートリアル,論文などは K-framework にて公開されています.
また,実装はGitHubkframework/k 上で行われているようです.

何が出来るかというと,K-framework上で configurationcomputation, rule を用いて,実行可能なプログラミング言語や型システム,解析ツールを定義できます. 加えて読みやすいドキュメントの自動生成もしてくれます.便利ですね.

C言語JavaSchemeLLVMなどの意味論が既にK上で与えられており,実用的なように見えます.

Kで用いられている項書換えの形式的な定義などは解説出来る気がしない(ボ!w)ので,この記事では実際に簡単な言語を定義して使用例を示したいと思います.

実行可能というのは?

K-tools というものがあり,これを用いることでKで定義した意味論を実際に動かすことができます.
今回のサンプルを動かす場合は,GitHubkframework/k から Version 3.6 のビルド済みパッケージ落としてくるか,私が作ったDocker imageを使うと楽に試せると思います.
ちなみにmasterはK-framework 4.0のSNAPSHOTになっており,挙動が不安定なため使用を見送りました.

言語はどう定義するのか??

冒頭で述べたように,意味論に関しては configurationcomputation, rule をK-framework上の記法に従って定義します. 加えて,syntax として言語の構文も定義し,それらを組み合わせて言語の定義とします.

動く仕組みと部品の説明

形式的ではないざっくりした説明ですが,
まず,K-frameworkは定義したsyntaxに従って文字列の入力をパースして構造に変換します.
次に,定義したruleに従ってconfigurationのマッチした構造を書き換えていき,それの繰り返しで入力の実行を行います.

configuration

configurationcellと呼ばれる値の集まりです.
ざっくり説明すると,プログラムのコードやシンボルテーブル,データのストレージなどを保持しておくような所です.

computation

computationは計算の順序です. \curvearrowright という記号で区切られたデータ列で,左から右へと評価されます.
Kでは構文などの構造をcomputationに落として計算の順序のようなものを作ります.

rule

Kで定義したruleK rulesと呼ばれ,これは項書換え規則に変換された後,それに従ってconfigurationが書き換えられていきます.
rulesは構造をcomputationに書き換えるstructural ruleと,実際に計算を進めるcomputational ruleに区別されます.

その他

Sort

型みたいなやつ.

Attributes

syntaxの項で指定できるもの.結合規則や評価順序などの指示を与えられます.

KResult

計算の最終状態のSortを指定します.

オンラインチュートリアル

Run K Online - kweb というものがあり,実際のK-framework上で用いる記法や,意味論の定義の仕方などをステップごとに試すことが出来ます.

面白いな,と思ったものは

  • SIMPLE言語 (場所:tutorial/2_languages/1_simple)
    • 並列計算もできる手続き言語のSIMPLE(震え声)言語.Static semantics(Typedと書かれた型付け規則)と,Dynamic semantics(実行時)の両方の定義があるので,静的型付けの言語の意味付けの参考になります.
  • 型システムチュートリアル (場所:tutorial/1_k/5_types)
  • Brainf*ck (場所:samples/bf/bf.k)
    • Bfの意味論が定義されていた… 単純なので読みやすいです.

実際に作成された定義など

試してみる

プログラミング言語 Hammon Lisp の定義

複雑な言語はK-MetaMLで力尽きたので,ここではステップバイステップで簡単なLisp風言語を定義してみます!
この章を読んだ後に公式チュートリアルを読むとスラスラ理解できるようになっていれば嬉しいです.

K-frameworkにハマりすぎて研究室を破門されないように頑張っていきましょう!

全体のソースコードのリポジトリはここになります.動作確認はK-framework revision(a7673ca)で行いました.多分ver 3.6でも動くと思います.

全体の定義は上のリポジトリを見て頂いて,ここでは重要な点の説明をしていきます.

Step 1. 構文の定義

まず,構文の定義からいきます.ファイル名hammon-lisp.kの中に,HAMMON-LISP-SYNTAXというmoduleを作って,構文を定義していきます.

module HAMMON-LISP-SYNTAX
  syntax Expr ::= SId | Int | "nil" | "t"
                | "(" SList ")"

  syntax SList ::= List{Expr, ""}

  syntax SOp ::= "+" | "-" | "*"
               | "="
  syntax SId ::= Id | SOp
               | "defun"
               | "progn"
               | "lambda"
               | "if"
               | "print"

endmodule

アトムとS式の構文の定義です.
syntaxキーワードを使って,構文を定義します.まんまBNFですね.多少拡張されており,attributeを加えたり,優先順位を変更できます.

Step 2. Configuration の定義と下準備

HAMMON-LISPというmoduleを作って,その中に本体の定義を書いていきます.

module HAMMON-LISP
  imports HAMMON-LISP-SYNTAX

  syntax KItem ::= "%t" | "%nil"
  syntax KResult ::= Int | SId | "%t" | "%nil"
  syntax KItem ::= "%toplevel"

  configuration <k> %toplevel $PGM:SList </k>
                <venv> .Map </venv>
                <fenv> .Map </fenv>
                <store> .Map </store>
                <nextLoc> 0 </nextLoc>
                <results> .List </results>
                <out stream="stdout"> .List </out>
                
  // rewrite parentheses to << >>
  // it is needed to avoid confusion of K parsers...
  syntax Expr ::= "<<" SList ">>"
  rule ( E:SList ):Expr => << E >>  [macro]
endmodule

まずimportsを用いて構文の定義を読み込みます.
KItem というのはKの構造の項みたいなもので,ここに加えた構文はどこでも使えるようになります.
KResult は計算の最終状態の形です.

configurationconfiguration キーワードを用いてXMLで定義します.今回の定義のCell内訳は,

  • <k> : プログラム本体.$PGMの部分にパースされた構造が入ります.
  • <venv> : 変数とLocationの対応を保存します..Mapというのは空のマップ構造を指します.
  • <fenv> : 関数とLocationの対応を保存します.
  • <store> : Locationとデータの対応を保存します.
  • <nextLoc> : LocationのFreshIdを保存します.
  • <results> : おまけ.トップレベルのS式を評価したときの結果を保存します.デバッグ用.
  • <out> : 標準出力です.

となります.変数と関数の名前空間は分割しました.

最後に,S式のカッコを<< >>に変換するマクロを定義しています.式の結合を変えるカッコとS式のカッコで,K-frameworkのパーサが混乱するようなので…

Step 3. Rules の定義

残るは書き換え規則をガンガン入れていくだけです!

Step 3.1 変数のルックアップ

  // Variables
  rule <k> X:Id => Val ... </k>
       <venv> ... X |-> Loc ... </venv>
       <store> ... Loc |-> Val </store>

このルールは以下のように読むと意味を汲みやすいです.

  • <k>の先頭にあるIdというSortを持った項をXと置いて,
  • <venv>Xに対応するLocが存在して,
  • <store>Locに対応するValが存在したときに,
  • Xと置いた項をValに書き換える

また,=> は左辺を右辺に書き換えることを示します.
... は0個以上の何かしらの値がある,ということを示します.

Step 3.2 値

  // special value
  rule <k> nil => %nil ... </k>
  rule <k> << .SList >> => %nil ... </k>
  rule <k> t => %t ... </k>

nilリテラル空リスト真偽値の変換を定義します.

Step 3.3 defun

  // defun
  syntax KItem ::= func(SId, SList, SList, Map, Map, Int)

  syntax KItem ::= midDefunCheckParam(SList)
  rule <k> << defun:SId Sym:SId << Params:SList >>:Expr Exprs:SList >> => midDefunCheckParam(Params) ~> Sym ... </k>
       <venv> VEnv </venv>
       <fenv> FEnv => FEnv[Sym <- N +Int 1] </fenv>
       <store> Sto => Sto[ N +Int 1 <- func(Sym, Params, Exprs, VEnv, FEnv, N +Int 1)] </store>
       <nextLoc> N => N +Int 1 </nextLoc>

  rule midDefunCheckParam(P:Id Ps:SList) => midDefunCheckParam(Ps)      [structural]
  rule midDefunCheckParam(.SList) => .K                                 [structural]

まず,funcという構造を定義しておきます.先頭から,関数名,パラメータ,関数本体,定義時の変数環境,定義時の関数環境,この関数のLocationを保持します.
このruledefun という構造が<k>の先頭にあったとき,それをmidDefunCheckParam(Params) ~> Sym という computation に書き換えます.
 \curvearrowright で区切られるcomputationは,K-frameworkの記法では~> で区切られます.これで,midDefunCheckParam(Params) が評価されてから Symが評価されることになります.
加えて,<fenv><store>nextLocの値も書き換えます.
<fenv>を例に説明すると,まず現時点の<fenv>の内容をFEnvと置き,それにSymというキー を N +Int 1 という値に関連つけたものに書き換えます.

midDefunCheckParam再帰的に,パラメータが全てIdというSortになっているかを確かめています.(パラメータに数字などを置かれると困りますからね…)
パラメータの名前の重複判定は省いてしまったので,気になる場合は追加してみてください.

Step 3.4 if

  // if
  syntax KItem ::= midCond(Expr, Expr)
  rule <k> << if:SId Cond:Expr Then:Expr Else:Expr >> => Cond ~> midCond(Then, Else) ... </k>
       [structural]
  rule <k> CV:KResult ~> midCond(Then, Else) => Then ... </k>
       when CV =/=K %nil
       [structural]
  rule <k> %nil ~> midCond(_, Else) => Else ... </k>
       [structural]

みんな大好きifです.ここでは,まずif条件式を最初にcomputationに乗せて評価させ,Then節Else節は構造のまま保っておきます.
そして,条件式の結果によってThen節Else節の構造をcomputationに乗せて評価させます.
これによって,Then節Else節の片方のみが評価されます.

ruleにはwhen節を付けることができて,ここで細かいruleの切り替えを行えます.

Step 3.5 呼び出し

大物になってしまいました…

  // ===
  // call
  // ===
  syntax KItem ::= midFApply(SList) | midBeginApply(K, SList)
  rule <k> << E:Expr Args:SList >> => E ~> midFApply(Args) ... </k>
       when notBool isSpecialFormOrBuiltin(E)
       [structural]

  rule <k> Sym:Id ~> midFApply(Args) => midBeginApply(Func, Args) ... </k>
       <fenv> ... Sym |-> Loc ... </fenv>
       <store> ... Loc |-> Func ... </store>
       [structural]

  // (ref 1)
  syntax KItem ::= midConv(SList, SList, Map, Map) | midEndApply(Map, Map)
  rule <k> midBeginApply(func(Sym, Params, Body, FVEnv, FFEnv, N), Args) =>
                midConv(Params, Args, FVEnv, FFEnv[Sym <- N])
                ~> << progn Body >>
                ~> midEndApply(VEnv, FEnv) ...
       </k>
       <venv> VEnv </venv>
       <fenv> FEnv </fenv>
       [structural]

  // (ref 3)
  rule <k> V:KResult ~> midEndApply(VEnv, FEnv) => V ... </k>
       <venv> _ => VEnv </venv>
       <fenv> _ => FEnv </fenv>
       [structural]

  // (ref 2.1)
  syntax KItem ::= midBind(Id)
  rule <k> midConv(P:Id Ps:SList, A:Expr As:SList, VEnv, FEnv) => A ~> midBind(P) ~> midConv(Ps, As, VEnv, FEnv) ... </k>
       [structural]
  rule <k> Val:Expr ~> midBind(P) ~> midConv(Ps, As, VEnv, FEnv) => midConv(Ps, As, VEnv[P <- N +Int 1], FEnv) ... </k>
       <store> Sto => Sto[N +Int 1 <- Val] </store>
       <nextLoc> N => N +Int 1 </nextLoc>
       [structural]

  // (ref 2.2)
  rule <k> midConv(.SList, .SList, VEnv, FEnv) => .K ... </k>
       <venv> _ => VEnv </venv>
       <fenv> _ => FEnv </fenv>
       [structural]

最初の3つのルールは今までの説明で読み取れると思います.今度は<venv>ではなく<fenv>から値を取ってきています.

面倒なのが残りのルールで,これは変数環境と関数環境をstatic scopeかつ再帰呼出し可能に設定しているところです(より効率よくできるかもしれません…).
ざっくり説明すると,現在の変数/関数環境を保存した後(ref 1)に,呼び出す関数のパラメータと引数の対応を作りつつ(ref 2.1)新しい変数/関数環境に切り替えて(ref 2.2)関数本体をprognで包んで評価を行い(ref 1のcomputation),評価が終わったら呼び出す前の変数/関数環境に戻す(ref 3),という事をしています.
このあたりはK-frameworkのテクニックというよりは,この本の内容に近いです.

サンプルコード

これでコア部分の説明は終わりました.では,実際にどんなコードをHammon Lispで書けるのかというと,

(defun zoi (x y) 10)
(zoi 10 20)
(+ 10 20)
((lambda (x y) (+ x y)) 20 30)
(defun zero () 0)
(zero)
(if () 114 514)
(if nil 114 514)
(if (+ 10) 114 514)
(- 10 2)
(- 10 2 3)
(= 10 20)
(= 10 10)
(defun f1 (x)
  (print (= x 0))
  (if (= x 0) 100 200))
(f1 0)
(f1 1)
(defun fact (x)
  (if (= x 0) 1 (* x (fact (- x 1)))))
(print (fact 4))

このくらいなら実行することができます. コレを実行すると,最終状態のconfiguration<results>Cellから

<results>
    ListItem ( zoi )
    ListItem ( 10 )
    ListItem ( 30 )
    ListItem ( 50 )
    ListItem ( zero )
    ListItem ( 0 )
    ListItem ( 514 )
    ListItem ( 514 )
    ListItem ( 114 )
    ListItem ( 8 )
    ListItem ( 5 )
    ListItem ( %nil )
    ListItem ( %t )
    ListItem ( f1 )
    ListItem ( %t )
    ListItem ( 100 )
    ListItem ( %nil )
    ListItem ( 200 )
    ListItem ( fact )
    ListItem ( 24 )
</results>

という結果が得られます.特に最後のfactではしっかり24という値が得られていますね!

まとめ

高級な言語の意味論を定義でき,形式的な検証を行うことの出来るK-frameworkくんの紹介でした.
LLVM-IRくんの意味も定義されていることだし,Translatorの定義ができたらコンパイラになるんちゃうか?とか考えたりしています.
形式的な定義については教えて下さいお願いします,なんでもしますから!

〜おわり〜

鳥小屋のシンチョク#2

9月に入ってしまうので,鳥小屋のここまでのシンチョクのまとめ.
もう前のシンチョクから1年経ってしまったのか…

相変わらずWandboxがつよくてつらい.

鳥小屋 is 何

いわゆるオンラインコンパイラです.アドレスが変わりました.
ProcGarden(仮)
まだUIが未完成だけれど,ひとまず動く.

昔の方は,データを吸い出し次第止めようかな.

シンチョク

まとめ

Rubyでゴチャゴチャ書いていた部分をGoで書き直したら幸せになった.
Goでゴチャゴチャ書いていた部分をC++で書き直したら幸せになった.

ワンワンワンドボックス

おわり

つらい

Boost.Spirit.X3のご紹介 - C++ Advent Calendar 2014(16日目)

この記事はC++ Advent Calendar 2014 16日目の記事です.
おはようございます,@yutoppです.

去年のC++ Advent Calendar 2013ではBoost.Spirit.QiのTipsを書きました.今年は,Boost.Spirit.X3の紹介をしたいと思います!

環境は,Antergos Linux(x64) / Clang 3.5.0 / Boost 1.56.0 です.
また,Boost.Spirit.X3はexperimentalとのことなので,この記事の内容はすぐに古くなる可能性があります.

Boost.Spirit.X3とは?

Spirit X3
boostorg/sprit

C++11やC++14の機能を用いて再設計されたBoost.Spirit.Qiの次のexperimentalな実装です.
Classic Spiritのようなシンプルさを取り戻すことを目標にしているとのことです.

spirit/include/boost/spirit/home/x3がお目当てのX3の内容になります.

X3を使ったコードには以下のものがありました.

X3の利点

コンパイルが速い

試しにサンプルをビルドして計測してみました.
Qi Calc1 / Qi Calc2 / Qi Calc4
X3 Calc1 / X3 Calc2 / X3 Calc4

以下の表は,
clang++ -ftime-report -std=c++14 -I /usr/include/boost/ -c 各サンプル名
を10回繰り返し計測したClang front-end timerUser Timeの値(sec)の平均です.

calc1 calc2 calc4
Qi 4.283 4.409 4.96335
X3 1.87333 1.89767 2.34934

大体今までの2倍の速さでコンパイル出来るようになっているようです.体感でわかる程度に速いので良いですね.

エラーがわかりやすい(Qi比)

内部実装がシンプルになったことによって,エラーも分かりやすくなった気がします.

宣言と定義を同時に書けるようになる(?)

X3からruleの内容を先に定義してから,rule自体を定義するようなスタイルになったので,謎マクロを噛ますことで同時に宣言できます(後述します).

C++14を使いまくれる

ライブラリ自体が最低でもC++14を要求するので,このライブラリをincludeした時点でC++14の機能を使わないともったいないという気持ちになれます.

X3の現状の問題点

undocumented

ドキュメントが無いのでつらいです…が,X3の実装がとても読みやすいので,コードを読みながら何とか使えます.
特に変わったのはruleの定義とセマンティックアクションの記述,attrvalの扱いかな,と思います.

定義済みパーサが少ない

仕方がないので自分で書きます.

Tips

X3では,以下のようにruleを定義します.(サンプルより抜粋)

x3::rule<class expression, ast::program> const expression("expression");

auto const expression_def =
            term
            >> *(   ('+' >> term)
                |   ('-' >> term)
                )
            ;

BOOST_SPIRIT_DEFINE(
    expression = expression_def
    );

しかし,個人的にはruleとdefを同時に書きたいわけです. そこで,マクロを噛まします.
実際のコード

#define RULES_BEGIN( struct_name, entrypoint_name )         \
    struct struct_name                                      \
    {                                                       \
    using self_type = struct_name;                          \
                                                            \
    static auto instance()                                  \
        -> struct_name const&                               \
    {                                                       \
        static struct_name self;                            \
        return self;                                        \
    }                                                       \
                                                            \
    static auto entrypoint()                                \
    {                                                       \
        return instance().entrypoint_name;                  \
    }                                                       \

#define RULES_END                          \
    };

#define ANNOTATOR_COL() :

#define ANNOTAROR_BASE_SPEC( r, _unused, index, elem )      \
    BOOST_PP_IIF( BOOST_PP_EQUAL(index, 0),                 \
                  ANNOTATOR_COL,                            \
                  BOOST_PP_COMMA                            \
        )() public elem

#define RULE( name, type, ... )                    \
    RULE_WITH_ANNOTATOR( name, type, BOOST_PP_SEQ_NIL, __VA_ARGS__ )

#define RULE_WITH_ANNOTATOR( name, type, bases, ... )                   \
    class name                                                          \
        BOOST_PP_SEQ_FOR_EACH_I( ANNOTAROR_BASE_SPEC, _, bases )        \
    {};                                                                 \
    struct PP_ ## name {                                                \
        using rule_type = x3::rule<name, type>;                         \
        static auto def( self_type const& t ) {                         \
            return __VA_ARGS__;                                         \
        }                                                               \
        auto operator()() const -> rule_type                            \
        {                                                               \
            return rule_type( #name );                                  \
        }                                                               \
    };                                                                  \
    decltype(( std::declval<PP_ ## name>()) ()) name                    \
        = PP_ ## name()();                                              \
    template <typename Iterator, typename Context, typename Attribute>  \
    friend inline bool parse_rule(                                      \
        decltype(( std::declval<PP_ ## name>()) ()) rule_,              \
        Iterator& first, Iterator const& last,                          \
        Context const& context, Attribute& attr                         \
        )                                                               \
    {                                                                   \
        using boost::spirit::x3::unused;                                \
        auto const& ri = self_type::instance();                         \
        auto const& raw_def = PP_ ## name :: def( ri );                 \
        auto const& def_ = ( ri.name = raw_def );                       \
        return def_.parse(first, last, context, unused, attr);          \
    }

classの中であれば前方参照できるので,ruleは全体的にclassの中で定義するようにします.
ruleの中身はstruct PP_ ## namedefで定義します.引数のtがキモで,ruleを定義する際は,tのメンバ変数として参照するようにします.
また,parse_ruleが呼べればX3から使えるようなので,BOOST_SPIRIT_DEFINEの定義から抜き出してfriendとして定義しておきます.

実際の使い方はこのような感じになります.
実際のコード

RULES_BEGIN( rules, program )

RULE_WITH_ANNOTATOR( program, ast::module_ptr,
    ( on_error_annotator_base ),
    t.module > ( x3::eol | x3::eoi )
    )

RULES_END

RULES_BEGINでは,rulesというクラスを定義して,programから始まるrule群を定義しています.
RULE_WITH_ANNOTATORでは,on_error_annotator_baseに従ってアノテーションを行い,ast::module_ptr型の属性を持つ,programというruleを定義しています.
t.moduleというrule(ここでは定義していませんが…)を参照しています.残りはQiのときと同じですね.

あとはこのように使うだけです.

このマクロを用いると,ruleの定義を1箇所で行えるようになります.X3自体の効果でコンパイル時間も短くなりますし,良さがありますね.

実際に使ってみた

去年の記事にも書いた文鳥言語で,実際にX3を使ってみました.
(文鳥言語はC++14とBoost.Spirit.X3,LLVMを用いて,C++とDlangライクな言語を目指して開発している言語です)

yutopp/rill

Boost.Spirit.X3を使ってみて大きいのは,コンパイル時間が短くなったこと,それとコンパイル時間が短くなったこと,後はコンパイル時間が短くなったことが挙げられます.
エラーメッセージが分かりやすくなったこと,マクロで定義を1箇所に書けるようになったのも大きいかもしれません.
C++14のgeneric lambdaと組み合わせると,セマンティックアクションがとても書きやすいのも魅力でした.

Spirit.Qiでコンパイル時間がBoostするのがつらい皆様,ぜひX3を使ってみませんか.
そしてついでに文鳥言語も開発しませんか?とてもアットホームな鳥小屋です.

おわり

experimentalだけど現段階でも十分魅力的なBoost.Spirit.X3の紹介でした.
後日もう少し書き足します…

イヌヌ
@Linda_ppさんの今年気になった C++ ライブラリとかフレームワークを紹介する記事