yutopp's blog

サンドバッグになりたい

2018年振り返り

雑記

今年は色々変わったなあという感じがするので思い出しながら書いていく．GitHubやTwitterには断片的なログが残っており，こういうとき便利だ．

振り返り

1月

あまり記憶が無いが，VPS環境をAnsibleで全て自動で構築できるようにしていた気がする．この時期はDockerやAnsible，Consul，traefik，grafana，prometheusなど色々触っていた．今まで個人で使っていたツールを応用することもあれば初めて使うツールもあり，試行錯誤を楽しんでいたように思える．言語はGoをひたすら書いていた．

このVPS環境では自サイトであるyutopp.netがホストされている．確かHugoを使ってページを生成するようにしたので，ブログ未満ツイート以上の文章を書こうと意気込んでいたはずだが，現時点でも2記事しか書かれていない．ウケますね．
内容は，"今年こそオンラインコンパイラを作り直したい" と "Zenbook3を買った" というものだった．オンラインコンパイラは途中まで作って放置しているため，2018年の抱負はこのまま2019年に引き継ごうと思います．

振り返っていて早くも暗雲が立ち込めてきた．

以下は癒やしのツイートです．

twitter.com

2月

技術書典4へのサークル進捗大陸の参加が確定し，やっていきの月だった．この回は，@no_maddoさんや@pocketberserkerさんも参加してくださり，ワイワイといつにも増して楽しかった記憶がある．

twitter.com

言語は相変わらずGoメインで書いていたようだが，Rust齧ったりOCamlも触っていた．あとErlang VMの実装を読んで分散Erlangのフルメッシュ構造になる原因と解決策を調べていた．これは社内LTで発表した(色々手直しして公開しても良い気がしてきた)．

あと旅行(広島→岡山→神戸)に行った．

twitter.com

もう一度優勝したい．

3月

心が比較的死んでいました．ウェザーロイドAiriさんの骨折動画を見て笑いながら会社でしいたけを育てていた．

twitter.com

あとは開発合宿にお邪魔させていただいてキツネ村に行ってきた．

twitter.com

mzp.hatenablog.com

とてもよかった．ここでtraefikにPRを出したり，進捗大陸の原稿をひたすら書いていた．

最後にMLDayでLTをした．内容は自作言語である文鳥言語の，失敗したなと思う部分とその改善策についての知見です．

OCamlで作り直す 自作言語のススメ - Google スライド

4月

心が比較的死んでいました．ウェザーロイドAiriさんの骨折配信を見て笑いつつ，技術書典の最後の追い込みでひたすら煽られながら原稿を書いていた．

twitter.com

結果的に締め切りには間に合い，当日も無事頒布でき良かった．改めて感謝です．

twitter.com

(宣伝: この時の内容は 言語処理系のススメ - 進捗大陸03 - 進捗大陸 - BOOTH にて入手可能です)

イベントでは，ニコニコ超会議2018に参加した．ここでVirtualCastを実際に体験したのだが，あまりの没入感に感動しVR機器を買いたい気持ちに支配されたのであった．

あとはリズと青い鳥を観て，旅行に2回行った．

twitter.com

1回目はゆるキャンに影響されたおたくと共に富士山の麓でキャンプをした．4月だというのに夜寒すぎて眠れなかったのが良い思い出．

twitter.com

2回目は四国に行った．車で四国の左下以外(高速がないため)の部分を巡った．香川のうどんの安さと奥道後温泉が印象的だったが，全体的に四国は良い．
川に財布落としたり，空港でじゃこカツをひたすら食べた．

5月

5月，色々やった．

最初に，VR ReadyなデスクトップPCとHTC Vive一式を購入した．秋葉原のツクモで購入し，即日使いたかったので自分で運んで持ち帰った．2018年で一番重かった．

twitter.com

VirtualCastでD言語くんアバターになって配信などしていたが，やはり自分で開発したくなり，UnityとC#とBlenderをまともに触り始めた．
毎日朝5時位まで実装をしていて，5月では最終的に以下のような所まで作れることが分かった．

twitter.com

(このときモデルはウェザーロイドAiriさんのMMDデータをお借りしていました…)

UnityのMonoBehaviourのような挙動はErlangのアクターモデルっぽいなと思いつつ実装していた．労働ではひたすらErlangを書いていた時期があったので，思わぬところで知見が役に立ってよかった． 全体的に今まで触ったことがないツールや開発の対象(VR)だったので，なにもかも非常に新鮮で楽しかった．

あとはRTMP周辺のライブラリをGoで書き始めた．

規格を読みながら現実のソフトウェアの挙動と照らし合わせながら実装していくのは大変ためになった．

それ以外で言えば，プリパラを布教されたのが5月辺りだったと思います．

6月

VR開発を継続してやっていた．

twitter.com

twitter.com

自分でモデリングもしてみたくなって，Blenderの人型のモデリングにも入門した．

twitter.com

twitter.com

6月時点で出来上がったのはこれ．

6月は生活が本当に破滅しており，朝6時位までUnityやBlenderを触ったりRTMPサーバを書きつつ，プリパラを2話くらい観て寝るみたいな感じだったのを覚えている．
このあたりからGitHubの草を毎日欠かさず生やすようになってきた．

7月

引き続き毎日Blenderによるモデリングを明け方までやって，ついでにBeatSaberに自作もモデルを読み込ませてこれも明け方までやっていたら体壊した月．虚無．

twitter.com

Vive Trackerも3つ買ってしまい，沼．

プリパラは80話まで見た．

8月

Rustで言語処理系を作ろうとしたけれど，グラフ構造扱うのが面倒すぎて挫折した月だった．やはりOCamlは最高や．

技術書典5へのサークル進捗大陸の参加が確定したので，RTMPサーバの実装と原稿に本腰を入れ始めた．本腰を入れられることが出来たのは，この月でスプラトゥーンのウデマエXを達成したため，実装に集中できるようになったという理由(厳しい)．

あとはペンギンハイウェイを観て，富士山登ってきた(2回目)．高山病はつらい．体力をつける．
振り返って思ったが，体力以前に直近数ヶ月の生活が壊れていたのが高山病の原因だったのでは…

twitter.com

プリはパラを全191話見て，チャンを見始めました．沼．心が弱っていたのだと思う．

9月

なんかCコンパイラをフルスクラッチで書くのが流行っていたので便乗して自分も書いていた．

twitter.com

GitHub - yutopp/cc

技術書典5の原稿を書くのが最優先だったのだが，やはり現実逃避は最高や．しかし，C言語の構文は読めば読むほど実装する気が無くなってきたため途中で放置となってしまった．

月の真ん中で9連休を作り，そのうちの2日を使ってサークル進捗大陸で進捗キャンプをした．キャンプと言っているが，中身は千葉の旅館で缶詰になって原稿を書くというものであった．

twitter.com

/etc/hostsでtwitterドメインをlocalhostに向けて潰していたため，この月はツイートが少ない．プリはリズをシーズン2まで見終えた．

10月

技術書典5の原稿は無事入稿でき，ウェブサイトもリニューアルした．初めてnuxt.jsを使った．小ネタなのだが，このウェブサイトで表示されるプログレスバーは(現在の1/1からの日にちの累計/365)*100という式で計算しているため，今見るとほぼ100%になっているはず．2019年になったらまた0%になっていることでしょう．

twitter.com

twitter.com

当日も無事頒布でき良かった．こちらも改めて感謝です．
(宣伝: この時の内容も 進捗大陸04 - 進捗大陸 - BOOTH にて入手可能です)

技術書典が終わってからはひたすらRTMPサーバーのパフォーマンスチューニングをしていた気がする．
他にはクライアント側など足りない部分の実装を埋めている．たまにPRやStarを頂くのだが，初めてまともに作ろうとしたGoライブラリなので結構嬉しい．

あと旅行に2回行った．
1回目(？)は谷川岳に登山(旅行か？)をした．

twitter.com

紅葉がきれい．富士山で使ったガチ登山装備で挑んだので怪我なく楽しむことができた．

2回目は沖縄・石垣島と竹富島に行った．

twitter.com

住みたい．沖縄では時計をあまり見ないで過ごした．土地の雰囲気も相まって時間がゆったりと流れているような開放的なあの感覚が忘れられない．

感想が谷川岳と合わせてエモいしか言ってなくて笑ってしまった．

11月

iPad ProとPixel3を買ったらクレジットカードが止まった月だった．

言語処理系勉強会 Vol.1でLTもした．言語処理系開発とUnityの知見を合わせて自分ができそうなことについて話した．
デモが本当にプリミティブなものしかできなかったので，これの開発は続けていきたい．来年まだどこかで発表できたらと思う．

twitter.com

それ以外は，心が弱っていたのでプリに没頭していた．筐体に手を出してしまったので，実用的なアイテム閲覧かつ重複チェックアプリをFlutterを使って作った．

twitter.com

Flutter，非常に使いやすくて推せるなという感想を持った．Android Studioとの連携は抜群で，補完もエラーもバッチリ出る．
Hot reloadも高速で，コードを書いたらすぐ画面にUIが反映される．UIも標準でMaterial designが提供されるので見た目が良い(生の描画もできる)．

Android アプリもDartは久しぶりに書いた．スラスラなんの躓きもなく開発することができて非常に良かった．ぜひFlutterは試してみて欲しい．

12月

obeam というOCamlでErlangのBEAMフォーマットをパースするライブラリの開発が活発だった．PR本当にありがとうございます．
ただやり取りを全て英語でしているのだが，自分の英語の不自由さに厳しい気持ちになっている．OCamlより英語のほうが難しい．解決せねば...

あとは中旬あたりに職場が変わった．いまはVR関連の開発をしている．とてもありがたい．
なにもかもがとても新鮮でかなり楽しい．5月頃の経験を下地に日々足りない知識を吸収しようとしている感じ．やっていきます．

まとめ

技術書典のサークル参加やVR開発，モデリング，ライブラリ開発にLT，旅行，プリ，転と思ったより色々充実していたのかもしれない．
言語も新しくRustやC#を深く触るきっかけが作れてよかった．OCamlやGoも理解が深まったと思う．

GitHubの草も半年近く連続で生やすことが出来たのもよかったと思う．

来年

心を元気にして開発速度を取り戻していきたい．あと英語．やる気元気寝起き！

RTMPのChunkStream, MessageStreamの話

RTMP protocol

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. 型システムの健全性
      6. 符号解析
    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 にて公開されています．
また，実装はGitHubの kframework/k 上で行われているようです．

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

C言語やJava，Scheme，LLVMなどの意味論が既にK上で与えられており，実用的なように見えます．

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

実行可能というのは？

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

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

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

動く仕組みと部品の説明

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

configuration

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

computation

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

rule

Kで定義したruleはK 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 は計算の最終状態の形です．

configuration は configuration キーワードを用いて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を保持します．
このruleはdefun という構造が<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++で書き直したら幸せになった．

ワンワンワンドボックス

おわり

つらい