yodaの備忘録

エンジニアのゆるいブログ

2017年の振り返りと2018年のはなし

2017年が終わりそうなので、今年の振り返りと来年の目標(のようなもの)を設定しておこうかなと思います。

特に深い意味はなくて、雑でもいいからなんか書いておいたほうが思い出せるし、自分へのプレッシャーになって良いかなあと考えた次第です。

コンピュータ周り

仕事でScalaやりつつ、勉強会でJDKやIdrisの話をしました。それなりに本も読めたかな。

特にIdrisは個人的に今年一番の発見でしたねー。プログラミング言語はまだまだ底なし沼です。

2018年はこんな感じでいきたいなあ…

  1. IdrisとRustをもうちょっとちゃんとやる
  2. OSとかネットワークとか、ITエンジニアのベース的な知識の底上げ
  3. CPUとかコンパイラとか、コンピューティング的なところの勉強
  4. 型理論とか計算機周りの理論的なところの知識を増やしたい
  5. 久々にJJUG CCCで話がしたい

仕事に役立ちそうなものがあんまないんですけど、だいたい仕事に役立つことは仕事で身につくし、周りの人が色々調べてくれるから大丈夫なはず😇

Idrisのおかげで型理論とか計算機理論とか、CSの教科書に出てくるようなことに(ようやく)関心が湧いてきたので今のうちに勉強しておこうと思います。

OSとかネットワークとかは、関心っていうよりここまで必要に応じてやってきたので知識に穴が結構あって、その穴埋め目的です。

コンパイラとか最適化とかはようわからんな放置しとくかって感じで生きてきたのですが、CPUをちょっと勉強してみたら面白くてコンピューティング熱が高まってるのでこれも今がチャンスかなと。言語もシステムプログラミングよりのやつを1つやっておきたいのでRustやろうと。C++17でも良いのですが、オブジェクト指向より関数型プログラミングに馴染みがあるので良いかなあと思ってます。

JJUG CCC は ZGC vs Shenandoah とかで話したいです…まあCfPこれで出して票入るんかいなって感じですが。

英語

全然やらなかった😇

ただ英語力で今後のキャリアの幅は明らかに変わってくるので、ぼちぼち気合を入れてやりたいところです。

前職のときに受けたTOEICが895点だったので、なんとか900点は超えておきたいですねー。

コミュ力

振り返ってみると割と引きこもりだったかも…😞

2018年はもうちょっと人間関係を広げたいなあ。

あとLINEとかメールとかをもらったとき、なるべく早くレスポンスするようにします…😣

スポーツ

4月から近所のジムでトレーナーつけて筋トレするようになって、風邪の時以外はちゃんと週二回通い続けました。効果はばっちりなのでトレーニング丸1年になる3月までは同じやりかたでいこうかなと思ってます💪

今後の課題としては、現状パワーアップ目的で減量とか考えてないぶん体重が増えてるのと、ちゃんと見てくれるジムだとまあまあお金もかかるというところです。

普通のジム(都度利用)+区営のジム(都度利用)+月1トレーナーとかに切り替えて浮いた分を英語に回すか?と考えてます。今のジムのやり方が自分にあってるだけに、判断が難しいんですが。

テニスはぼちぼちスクールの次のレベルに上がれそうです。サーブにせよストロークにせよ一回ミスをするとミスが続くのをなんとかしたい。

趣味

ちょっとした山登りとかもできたのは良かったのだけど、いかんせん早起きが苦手なので日帰りだと大山ぐらいが限界でした。

とはいえ行けば楽しかったし、来年こそは富士山くらい登ってみたい。

あと個人的な新しい試みとしてキャンプとかフェスとか行きたいっすね…。1月から大好きなゆるキャンのテレビ放送も始まるので、もうキャンプ行きたすぎる状態になることが目に見えてます。誰か一緒に行って!

部屋

服とか本とかをだいぶ手放したのと、それによって本棚も捨てたのでかなりものが減りました。服をここから更に2/3くらいに減らせればかなりいい感じになりそうです。

細かい所を掃除しないのは家に人を呼ばないからのような気がしているので、誰か遊びにきてください😂

Idrisのどん語を解読する

Idrisは超ざっくり言うと文法はHaskellそっくりで機能的にはCoqに近い、依存型を使う言語です。Idris自体の簡単な紹介は前に書いたスライドがあるので、興味がある方はそっちを読んでみてください。

yoda-jp.hatenablog.com

今回は Type Driven Development with Idris に出てくる練習問題の中で、ちょっとシュールなものを紹介しようと思います。 

問題

以下のシグネチャを持つ関数 same_lists を実装してみましょう。

--- 関数のシグネチャ
same_lists : {xs : List a} -> {ys : List a} -> x = y -> xs = ys -> x :: xs = y :: ys
--- ここに実装を書く

シグネチャが既に実装みたいになってますが、シグネチャでしかありません。 x = yxs = ys の2つが関数の受け取る値の型で、 x::xs = y::ys が返り値の型です。

{} で囲まれているのは暗黙的な引数で、呼び出し時に渡す必要はありません。 今回は xs = ys が(明示的な)引数にあるので、わざわざ xsys を個別に渡す必要はないということです。

この関数のやっていることを言葉で説明すると List a 型の値xsと List a 型の値 ysについて、x = y かつ xs = ys が成り立っていれば、x::xs = y::ys が成り立つ ということになります。

同じもの同士をくっつけているので同じになるのはわかるんですが、プログラムとして書けと言われるとウッとなりますね。

解答

実装はこんな感じになります。

same_lists : {xs : List a} -> {ys : List a} -> x = y -> xs = ys -> x :: xs = y :: ys
same_lists Refl Refl = Refl

Refl

f:id:yoda_jp:20171216233934j:plain

この実装は「関数の引数が ReflRefl であれば Refl を返す」としか言ってません。

もう一度言うと、この関数が指しているのは List a 型の値xsと List a 型の値 ysについて、x = y かつ xs = ys が成り立っていれば、x::xs = y::ys が成り立つ ということです。

これじゃ どんでんの「そらそうよ」 か田舎のおばちゃんの会話レベルで色々すっ飛ばされているので、ちゃんと順を追って見てみようと思います。

解説

前提知識

まず x = y について考えてみます。これは2つの値をとる型を中置で書いたものという風に見てください。一般的なプログラミング言語でも型に対して型をパラメータで渡す( List String など)ことは多いと思いますが、Idris では型に値を含めることができます(これが依存型)。たとえば 1 = 1 という型が存在するわけです。そして Reflx = x という型の値を作ることのできる、ただひとつのコンストラクタです。Reflx をパラメータとしてとるわけではなく、型推論で必要なxを判定して自動的に x = x 型の値を作ります。

ではこの知識を元に、答えの Refl 連発まで導いてみましょう。

導出

Atom + Idris プラグインの人は各行程をショートカットキーで行えるので、それも一緒に書いておきます。

シグネチャの暗黙的な引数は無視して、とりあえず1つ目のパラメータ(x=y 型の値)と2つ目のパラメータ(xs=ys 型の値)に対応する変数 prfprf1 を置きます。答えはまだわからないので ?result としています(ホールといいます)。ショートカットは Ctrl+Alt+a です。

same_lists : {xs : List a} -> {ys : List a} -> x = y -> xs = ys -> x :: xs = y :: ys
same_lists prf prf1 = ?result

次に prfprf1Refl に置き換えます。Maybe a のパラメータを Just aNothing と書けるように、x = yxs = ys もコンストラクタの Refl として表すことができます。ショートカットはCtrl+Alt+c (を2回)です。

same_lists : {xs : List a} -> {ys : List a} -> x = y -> xs = ys -> x :: xs = y :: ys
same_lists Refl Refl = ?result

値を Refl で書くことは非常に重要です。なぜなら、x = y 型の値ではなく、Refl と書くことで Idris の型チェッカーから以下の推論が可能になるからです。

  • 関数が受け取る値の型は x = y である
  • x = y 型の値はコンストラクタ Refl によって作られている
  • Refl で作られた値の型は x = x である
  • したがって x = yx = x と表すことができるはずであり、 yx に置き換えることができる

Idris はこのように型レベルで同じと判定できる値を見つけると、内部的に型の値を書き換えていきます(この様子はステップの前後で Ctrl+Alt+t をすると確認できます)。

つまり、Idris からは関数のシグネチャは以下のように見えています。

same_lists : {xs : List a} -> x = x -> xs = xs -> x :: xs = x :: xs
same_lists Refl Refl = ?result

最終的に返したい値の型は x :: xs = x :: xs になりました。これは左辺と右辺が同じなので、返したい値のところに Refl と書くだけで推論して x::xs = x::xs 型の値を作ることができます。ショートカットは Ctrl+Alt+s です。

same_lists : {xs : List a} -> x = x -> xs = xs -> x :: xs = x :: xs
same_lists Refl Refl = Refl

無事ゴールまでたどり着けましたね。

パターンマッチはプログラミング言語の標準的な機能となりつつありますが、ただ値を分解してくれるだけではなくて、そこから値同士の関係性を導き出して関数全体を簡単にしていくというのは依存型ならではかなと思います。依存型すごい(書けるとは言っていない)。

そら(x=yxs=ys なら)そう(x::xs=y:ys)よ。

そら、そうよ ~勝つ理由、負ける理由

そら、そうよ ~勝つ理由、負ける理由

Type-Driven Development with Idris

Type-Driven Development with Idris

Idrisの勉強会をやりました

プログラミング言語Idrisの勉強会をやりました。

テーマを勢いよく選んだあとConnpassのイベントページを作りながら「これ参加してくれる人いるのだろうか…?」と不安になっていたのですが、定員いっぱいまで申し込みがあり、更に参加率も非常に高く、非常に良い方々に参加していただけてとても楽しかったです。ありがとうございました。

勉強会の内容としては、「Type Driven Development with Idris」に載っている例を使いながらIdrisの基本や特徴について話しました。あまり話されないテーマだとネタをひねらなくて良いのがありがたいところです。資料にどこか間違ってるところがあるんじゃないかと怖いところもあるのですが、依存型を使うことでプログラミングがどのように変わるのか、ちょっとでも興味を持ってもらえたら嬉しいです。

個人的には「オブジェクトを作るもの」くらいの認識だったコンストラクタが、「ある型に対する値が存在しうる条件を規定するもの」として使うことができるのを知ったのが一番の驚きでしたね…。今すぐ役に立つ言語ではないのですが、もうちょっと勉強してみようと思います。

 

gitpitch.com

JJUG CCC に Shenandoah で登壇しました

 JJUG CCC 2016 Fall に ShenandoahGC ネタで登壇させてもらいました。いかんせん人も技術も知名度がない上に実用性も皆無というトピックだったので誰もいない部屋で話すことになったらどうしようと不安だったのですが、なんとか無事に終えることができました。セッションにご来場いただいたみなさま、スタッフのみなさま、本当にありがとうございました。

 

 

前職でたまーにオンラインセミナーをやったり人の発表を手伝ったりはしたのですが、こういう公の場にスピーカーとして登壇したのははじめてだったので、やってみての感想を書いておきます。

 

  • ものすごく勉強になる

今回はあまり情報がないテーマだったこともあり、説明を考えているとちょっとした疑問が湧いてきてソースコードを調べて…というのを繰り返していました。自分だけが知っていればよいのであれば「まーそのへんはいい感じに実装してくれてるでしょ」ですませるようなことでもセッションとなればそうはいかないので、私のような怠け者にとっては良い意味でのプレッシャーになりました。

 

  • しゃべり大事

採択してもらえている、セッションに来てもらえているという時点ででそれなりにテーマに興味を持ってもらえているはずなので、実はセッションの満足度ってかなりの部分でプレゼンに依存しているのではないかと感じました。調べ物とか資料作りに時間を使いたくなるのですが、喋るのもちゃんと練習しておいた方が良いです。今回はそれなりに練習をしており、ペースも把握できていたので、まずまず落ち着いてちゃんと喋れたような気がします(それでも言い忘れたこととかちょいちょいありました)。あと短めの時間を選択したのも正解でしたね。時間が半分になれば同じ練習時間で倍の回数をこなせますから、あまり話すのに自信がないという方はショートセッションがおすすめです。

 

  • 感想大事

いろいろ準備を頑張っただけに、感想をもらえると本当にうれしかったです。ありがとうございました。自分も良いセッションを聞かせてもらったら直接でもSNSでもスピーカーの人に感想を伝えようと思いました。

 

今後も機会があればまた登壇したいと思いますので、そのときはよろしくお願いします(良いネタが見当たらないですが…)。

Shenandoahの話をしました

少し前のことになりますが会社の勉強会で1時間ほどGCの話をする機会があり、普通のGCの話ばかりしてもつまらないので後半はShenandoahをテーマにしてみました。以下そのときの話の備忘録です。

 

はじめに

早速ですがShenadoahの資料はプロジェクトメンバーのRoman Kennkeさんが公開してくれているので、英語が苦ではない方、ちゃんとした資料が見たい方はそちらを参照した方が幸せになれます。

https://rkennke.files.wordpress.com/2014/02/shenandoahtake4.pdf

また以下の文章には、自分の勘違いや記憶違い、開発が進んで変更されるところもあると思います。もしそういうところに気付かれた方はやさしく教えていただけるとありがたいです。

 

Shenadoahとは 

ShenandoahはOpenJDKのプロジェクトの一つで、"ultra-low pause time garbage collector"の開発プロジェクトであり、(少なくとも現時点では)GCの名前そのものでもあります。現在HotSpotに実装されているCMSでは、回収フェイズがミューテータと並行で動作するものの、スイープしか行わないため断片化を招いてしまいます。一方G1GCではコピーGCを行うことで断片化を防いでいますが、コピーしている間ミューテータは停止しています。ということでShenandoahではミューテータを動かしつつコピーをするといういいとこ取りを目指しています。

 

Shenandoahは一見G1GCにとてもよく似ています。例えばヒープをリージョンに分け、回収効率の良いリージョンをコピーGC(退避)により回収する、というところはそっくりです。Humongousリージョン等も相変わらず出てきます。そのくせ違う所はガラッと違うというところが面白いところです。

 

Concurrent Evacuation を実現するために 

では一番の特徴である並行退避(Concurrent Evacuation)を実現するための仕組みを見ていきましょう。あるオブジェクトを別のリージョンに退避させる場合、そのオブジェクトを指すポインタも退避先を指すように更新する必要があります。stop the worldしている間に全てのポインタをチェックして更新できればいいのですが、ミューテータの動作を止めない場合、どうしてもポインタの更新を始めてから全てのポインタを更新し終わるまでにタイムラグができてしまいます。そのラグの間はプログラマが同じオブジェクトだと思っているものが実は別のオブジェクトだということが発生してしまい、フィールドの更新が発生すると大事故になります。

 

この問題へのアプローチには2つ候補があります。

  • From領域のメモリ空間をプロテクトして、アクセスがきたらTo領域にリダイレクトする。
  • 間接参照を導入して、一箇所更新すれば全てのアクセスが更新されるようにする。

パフォーマンスを考えれば余計なステップを踏まないぶんどう考えても前者の方がベターで、無停止コレクタとして有名なC4はこの方法を使っています。Shenandoahは後者の方法を採用していますが、これはできるだけJVMのレイヤーで実装してポーティングしやすいようにしたいためなどの理由があるそうです。ということで、Shenandoahではオブジェクトごとに対になるポインタが一つ用意され*1オブジェクトへのアクセスはそのポインタを経由して行うことになります(リードバリア)*2。ちなみにこのポインタのことはBrooksPointerと呼びます。

 

通常BrooksPointerは対になるオブジェクトを指していますが、GCによりそのオブジェクトが退避させられると、退避先のオブジェクトのアドレスを指すように変更されます。From領域のオブジェクトにアクセスした場合でもBrooksPointerを経由してTo領域のオブジェクトにアクセスすることになるので、参照の経路によってFrom領域のオブジェクトにアクセスしたり、To領域のオブジェクトにアクセスしたりということはなくなります。

 

ただし、このアプローチによって発生する問題もあります。次のような順番で処理が行われた時のことを考えてみましょう。

  1. GCスレッドがFrom領域にあるオブジェクトをTo領域にコピーする
  2. ミューテータがBrooksPointerを見て、From領域にあるオブジェクトを更新する
  3. GCスレッドがBrooksPointerの指す先をFrom領域からTo領域に更新する

このとき2番目の操作で更新した内容は消えてしまいます。

 

ということでFromリージョンにあるオブジェクト(かつBrooksPointerもFromリージョンを指している)を更新する場合はこんな感じで動くよう、ライトバリアが必要です。

  •  ミューテータは更新を行う前にToリージョンへオブジェクトをコピーする
  •  ミューテータもGCスレッドも、BrooksPointerの更新はCAS命令で行う

 CAS命令を使うことで、コピーしてからBrooksPointerを更新するまでの間に別のスレッドがBrooksPointerを更新してしまっていた場合はBrooksPointerを更新できないようにしています*3。競合した場合は既にToリージョンにコピーが作られているはずなのでそちらに対して更新を行えばよいだけですし、その際にできてしまう無駄なコピーはもったいないですがそのうち回収されるでしょうからあまり気にしないことにします。

 

ここまでShenandoahの大きな特徴である退避関連の動作について説明してきました。もちろんこれだけでGCはできないので、今度は全体像について見ていきます。

 

Shenandoahのサイクル

Shenandoahのサイクルは3つのフェイズに分けると把握しやすいと思います。

 

  • マークフェイズ
  • 準備フェイズ
  • 退避フェイズ

 

マークフェイズのメインの仕事は、文字通り生存オブジェクトのマークです。動作としてはG1GCのConcurrent Markのようなものですが、主目的が異なる点は抑えておきましょう。G1GCのConcurrentMarkの主目的はリージョンごとのオブジェクトの生存状況を確認し、効率的な退避を行えるようにすることです。退避時には別途生存オブジェクトの確認を行うため、ConcurrentMarkと退避は一対一で行われるわけではありません。一方ShenandoahのConcurrentMarkは退避フェイズにおけるオブジェクトの生死判定を主目的とします。従ってShenandoahではConcurrentMark一回の直後に退避フェイズが一回走ります*4。このフェイズは基本的にはミューテータと並行に実施されますが、最初のルートセットのスキャンからルートオブジェクトのマークまで(initial mark)と、最後に行うフェイズ中の変更分の集計(final mark)はstop the worldの処理です。

 

ここまででヒープ全体の生存オブジェクトをマークすることが出来ました。早速退避フェイズに入る…前に準備が必要です。退避対象となるリージョン、つまりCollectionSetの選択をします。Shenandoahでは退避フェイズの停止時間はないので、ゴミの量が基準を超えているリージョンは全てCollectionSetに含めることができます*5。このフェイズもstop the worldの処理です*6

 

準備が完了したら退避フェイズの開始です。CollectionSetに含まれたリージョン内の生存オブジェクトを順次空きリージョンに退避していきます。既に説明したように、退避はGCスレッドだけでなく、回収対象リージョンのオブジェクトを更新しようとしたミューテータによっても行われます。

 

退避フェイズ終了時点では退避対象リージョンへのポインタがそのまま残っていることに注意してください。退避前のオブジェクトをA、退避先にコピーされたオブジェクトをA’とした場合、A’への参照はAのBrooksPointerを経由します。従ってAの存在するリージョンを回収してしまうとA’への参照経路も絶たれてしまいます。次に行うべきは退避対象リージョンのオブジェクトへのポインタを退避先へと更新していくことです。

 

この作業を完了するためには、全ての有効なポインタをチェックする必要があります。ポインタのチェックは既にやっていますよね。そう、マークフェイズです。マークフェイズでは、生存オブジェクトを確認すると同時に、前回の退避フェイズでCollectionSetに含まれたリージョンへのポインタを、退避先リージョンへのポインタに更新していきます。マークフェイズが終了すると全てのポインタの更新が完了するので、準備の段階でCollectionSetに含まれたリージョンを解放することができます。

 

まとめると、以下の様なサイクルでGCは進みます。

マークフェイズ

  1. ルートセットから到達可能な全てのポインタをスキャンし、生存オブジェクトを確定する。
  2. スキャンしたポインタのアドレスが、前回のConcurrent Evacuation PhaseのCollectionSet内だった場合、退避先オブジェクトを指すようポインタを更新する。

準備フェイズ

  1. 前回のGCでCollectionSetに含まれていたリージョンを解放する。
  2. 到達不能になったHumongousリージョンを解放する。
  3. リージョンごとのごみの量をチェックし、基準を超えたリージョンをCollectionSetに含める。

退避フェイズ

  1. CollectionSetに含まれたリージョンのオブジェクトを順次空きリージョンへコピーする。コピーしたオブジェクトのBrooksPointerを更新し、コピー先のオブジェクトが参照されるようにする。
  2. GCスレッドが退避させる前にオブジェクトをミューテータが更新しようとした場合は、ミューテータは空きリージョンへのオブジェクトのコピーとBrooksPointerの更新を行い、退避先のオブジェクトを更新する。

 

世代

ここまでYoungやOldのような世代の話はしてきませんでした。なぜでしょう?Shenandoahは世代別GCではないのです。世代別GCは(ちょっと乱暴に説明すると)弱い世代別仮説に基づいてヒープを分割し、回収効率が良いと期待されるオブジェクト群だけを回収することで効率を上げる方法です。Shenandoahは退避前に全てのリージョンのごみの量を確認してリージョンを選択するので、特定の仮定に基づく必要はなく、アプリケーションの動作が弱い世代別仮説にあてはまらない場合でも効率を落とすことがありません。

 

また、Shenandoahは毎回ヒープ全体の生存オブジェクトをマークしてから一部のリージョンだけを解放します。G1は毎回ヒープ全体をマークするわけではないので、そのほうが効率が良さそうです。しかし、そのためにG1ではRememberedSetが必要になります。これはリージョン間をまたぐ参照を管理しておくことで、ヒープ全体をスキャンせずともリージョンの生存オブジェクトを確定できるようにするためのものです。G1はヒープを数千のリージョンに分けるので、その分のRemenbered Setを管理しておく必要があり*7、RemenberedSetをちゃんとアップデートしていくためのコストはG1GCを選択した場合にスループットの悪化として現れてしまいます*8。Shenandoahは毎回ヒープ全体をスキャンすることでRememberedSetを不要にしてオーバーヘッドを削減しています。

 

将来の話

まだShenandoahは開発中なので、Productionで使えるようになるまではだいぶ時間がかかると思われます。ただ現在開発中のShenandoahはShenandoah1.0と位置づけられており、Shenandoah2.0ではstop the worldの処理が取り除かれて完全にConcurrentなGCになる*9ことを目指しているそうなので、楽しみに待ちましょう*10

*1:instanceOopに追加されるわけではない

*2:もちろんポインタを配置する分メモリを余分に使い、リードバリアの分CPUも余計に使う

*3:要するに楽観的ロックを行っている

*4:G1GCはコピーGCだがShenandoahはマークコピーGCであるという言い方もできる

*5:100%ごみしかなかったリージョンはCollectionSetに含まずこの時点で回収される

*6:「これもstop the world」というよりは、実装を踏まえるとfinal markから退避開始までをひと固まりの処理であるとみなすのが妥当なのですが、じゃあこいつはマークなのか退避なのかと言われるとつらいので、今回は説明しやすいように一つの固まりとして切り出しています

*7:実際にはYoungのリージョンは必ずCollectionSetに含まれるためYoungからOldへの参照を管理しておく必要はない

*8:GCの停止時間が長いという話ではなく、ライトバリアによってGCしていないときのミューテータの処理が遅くなるということ

*9:一度にスレッドを止めずに順次止めながらスキャンする仕組みなどが必要。Pauselessのマークの仕組みがよくわからないので誰か教えて下さい…

*10:待てない方はZing使いましょう