Blog

2016.10.8

ICFP及び関連イベント参加レポート – 併設ワークショップ3日目 –

κeenです。ICFP及び関連イベントの参加レポートもこれで最後です。

この画像はICFPで貰ったノベルティ達です。 λと副作用のTシャツ(Jane Street)はデザイン凝りすぎてて普通のTシャツに見えるとよく言われます。あとスパゲッティコードTシャツ(ahrefs)は他にもmutable stateとかバリエーションが色々ありました。

さて、ICFP周辺ワークショップ3日目、23日はHaskell Symposium (Haskell)、OCaml Users and Developers Workshop (OCaml)、Erlang Workshop (Erlang)、Commertial Users of Functional Programming Tutorials(CUPF Tutorials)が開催されています。

Revisiting Software Transactional Memory in Haskell

Workshop: Haskell
Talker: Matthew Le, Ryan Yates, Matthew Fluet
Paper: Revisiting software transactional memory in Haskell

GHCのSTMをTL2ベースの実装に置き換える実験をした、という内容。

そもそもトランザクショナルメモリというのは不可分性(Atomicity)と投機(Speculation)を組み合わせたものです。一旦実行してみて、他のスレッドの処理と競合していなかったらそのままコミット、競合していたらアボートします。

HaskellのSTMは、トランザクショナルメモリに加えてリトライによるトランザクションのブロッキングと orElse によるトランザクションの合成も提供します。

t = atomically $ do
  x <- readTVar tx
  y > when (x == y retry))
    (writeTvar ty (y+1))

t = atomically $ do

x <- readTVar tx

y > when (x == y retry))

(writeTvar ty (y+1))

TL2アルゴリズムはメタデータの持ち方に工夫があるようで、Red Black TreeやSkip Listなどのベンチマークでパフォーマンス改善があるようでした。既存の実装だと1トランザクション毎に tvar old new version を持っていますが、TL2ではReadSet WriteSetに分けてなんか色々やっているようです。

ただ、TL2にするとグローバルなボトルネックがあるのでそこが問題だな、とか。

あとはOpacityについても言及がありました。未だによく分かってないのですが、Opacityとは

Opacity (Guerraoui and Kapałka 2008) is a strong correctness property which, among other things, requires that transactions always observe a consistent state of memory.

とのことでトランザクション内で矛盾した状態が現れないことを保障したいんですかね。

TMに関連する論文は山ほどありますが頑張って色々調べて改善していきたいとのことでした。論文には細かい実装の話なんかもあるので興味のある方は是非読んでみて下さい。

因みにSimon Peyton Jonesのいる前でGHCのバグの話とかもありました。

Autobahn: Using Genetic Algorithms to Infer Strictness Annotations

Workshop: Haskell
Talker: Yisu Remy Wang, Diogenes Nunez, Kathleen Fisher
Paper: Autobahn: using genetic algorithms to infer strictness annotations

Lazyな評価は計算量を削減出来る可能性がある代わりにスペースリークの可能性もある、Strictだとその逆という特徴があります。

それらを上手く使い分けられれば良いのですがそもそも難しい上にライブラリの作者なんかはどういう使われ方をされるか想定出来ませんしましてや言語処理系のサポートなんかは徹底的に保守的になる必要があります。

そこでユーザとやりとりしつつStrictness Annotationを生成してくれるツールを作ったというもの。さらに、逆に過剰/不要なStrictness Annotationの除去もやってくれます。

ただまあ直感で分かるかと思いますがなんかつらそうでした。

あ、因みにパフォーマンスについては遅くなることはないようです。必ず速くなる。すごい。

Statistically profiling memory in OCaml

Workshop: OCaml
Talker: Jacques-Henri Jourdan

メモリプロファイラを作るお話。ワクワクしますね。

メモリプロファイラを作る実装にはいくつか可能性があります。

ランタイムのメモリ確保関数をトレースする
確保したメモリ領域にメタデータを付与する

1の方法だとヒープの使い方を上手くトレース出来ないので今回のようにOCamlに限定したやり方ならもうちょっと上手い方法があります。 2の方法ではスタックトレースをメタデータに付与なんかをしようと思うととてもじゃない量の領域をメタデータが喰うのでかなりの制限が付きます。

ということで別の方法、統計的にメモリプロファイリングをする方法を採るというのが今回のお話。少量でありながらちゃんと全体のメモリアロケーションの特徴を掴むように上手くサンプリングしてあげます。こうすることでオーバーヘッドがなくなり、サンプリングも少量なので多くの情報を取っても問題なくなります。

アーキテクチャ的にはただのサンプリング機構で、ユーザが取得する情報を選べるようになっているそうです(OCamlの関数で書ける)。

サンプリングエンジンはユーザが指定したレートでポアソン過程に従ってアロケーションをサンプリングします（アロケーションサイズも考慮に入れます）。 E(Samples in a block) = Size of the block x Sampling rate とのこと。

サンプリングレートは自由に弄れるので勿論100%をサンプリングすることも出来ます。因みに割とパフォーマンスは良いようで、（ポアソン過程の）λを10^{-5にすると1%のオーバーヘッド、10}-4にすると10%のオーバーヘッドだったそうです。

因みに既にOCaml 4.03.0に取り込まれているようで、

opam switch install 4.03.0+statstical-memprof

1	opam switch install 4.03.0+statstical-memprof

で利用出来るようになります。

Lock-free programming for the masses

Workshop: OCaml
Talker: KC Sivaramakrishnan, Théo Laurent

論文はありませんでしたがKC Sivaramakrishnanさんのブログに関連ポストがあったので置いておきますね。 Lock-free programming for the masses · KC Sivaramakrishnan

さて、並行データ構造は1つ1つ、例えばStackなら push 、 pop などの個々の操作はスレッドセーフでもpop and pushのように複数の操作をアトミックに実行は出来ないのでロックを使う必要があります。要はコンポーザビリティに欠ける。ということでコンポーザブルでロックフリーなライブラリの作り方のお話。

ベースになっているのは PLDI 2012のReagents: Expressing and Composing Fine-grained Concurrencyで、それをOCamlに実装したようです。

雑にいうと次のようなコンビネータなんかを使うと合成が出来ますね。

type ('a,'b) t

(* channel communication *)
val swap : ('a,'b) endpoint -> ('a,'b) t

(* shared memory *)
val upd : 'a ref -> ('a -> 'b -> ('a * 'c) option) -> ('b,'c) t

(* sequential composition *)
val (>>>) : ('a,'b) t -> ('b,'c) t -> ('a,'c) t
(* conjunction *)
val () : ('a,'b) t -> ('a,'c) t -> ('a,'b * 'c) t
(* disjunction *)
val () : ('a,'b) t -> ('a,'b) t -> ('a,'b) t

val run : ('a,'b) t -> 'a -> 'b

type ('a,'b) t

(* channel communication *)

val swap : ('a,'b) endpoint -> ('a,'b) t

(* shared memory *)

val upd : 'a ref -> ('a -> 'b -> ('a * 'c) option) -> ('b,'c) t

(* sequential composition *)

val (>>>) : ('a,'b) t -> ('b,'c) t -> ('a,'c) t

(* conjunction *)

val () : ('a,'b) t -> ('a,'c) t -> ('a,'b * 'c) t

(* disjunction *)

val () : ('a,'b) t -> ('a,'b) t -> ('a,'b) t

val run : ('a,'b) t -> 'a -> 'b

気分的には ('a,'b) t はλ抽象で、 (>>>) が関数の合成、 run が適用です。こういう時にたまに型コンストラクタの中置記法が使いたくなりますね。

これを使ったサンプルコードが以下です。

module R = Reagent

module TreiberStack : sig
  type 'a t
  val create  : unit -> 'a t
  val push    : 'a t -> ('a, unit) R.t
  val pop     : 'a t -> (unit, 'a) R.t
  val try_pop : 'a t -> (unit, 'a option) R.t
end = struct
  type 'a t = 'a list R.ref

  let create () = R.ref []

  let push r =
    R.upd r (fun xs x -> Some (x::xs,()))

  let try_pop r = R.upd r (fun l () ->
    match l with
    | [] -> Some ([], None)
    | x::xs -> Some (xs, Some x))

  let pop r = Ref.upd r (fun l () ->
    match l with
    | [] -> None
    | x::xs -> Some (xs,x))
end

module R = Reagent

module TreiberStack : sig

type 'a t

val create : unit -> 'a t

val push : 'a t -> ('a, unit) R.t

val pop : 'a t -> (unit, 'a) R.t

val try_pop : 'a t -> (unit, 'a option) R.t

end = struct

type 'a t = 'a list R.ref

let create () = R.ref []

let push r =

R.upd r (fun xs x -> Some (x::xs,()))

let try_pop r = R.upd r (fun l () ->

match l with

| [] -> Some ([], None)

| x::xs -> Some (xs, Some x))

let pop r = Ref.upd r (fun l () ->

match l with

| [] -> None

| x::xs -> Some (xs,x))

end

CASやバックオフ、リトライなんかは陽には現れませんし、スレッド、wait、notifyなんかも使っていません。

で、実装なんですが2フェーズに分かれていて、フェーズ1でCASを集めてフェーズ2でk-CASを行うようです。k-CAS…？ 2フェーズに分かれる理由は、まあよくある計算の合成と実行の分離以外にもエラーの種類の分類もあるようです。フェーズ1でのエラーはそもそも無理な計算なので他のスレッドによる干渉を待ってからリトライしますが、フェーズ2でのエラーはただのトランザクションの失敗なのですぐさまリトライします。あとは今回はocamllabs/ocaml-multicore上に実装されているのですが、HTMをアクセラレータに使ったりするそうです。

STMとの比較もあり、

Reagents = STM + 同期コミュニケーションですが、制約が強いために pop s1 >>> push s1 が必ず失敗したりします。
Reagents はパフォーマンス側に倒していて、ロックフリーであったりHTMとの対応が綺麗だったりします。

とのこと。

因みにMonadでない理由はパフォーマンスが理由だそうです。

val (>>=): 'a Monad.t -> ('a -> ' Monad.t) -> 'b Monad.t
val (>>>): ('a, 'b) Arrow.t -> ('b, 'c) Arrow.t -> ('a, 'c) Arrow.t

1 2	val (>>=): 'a Monad.t -> ('a -> ' Monad.t) -> 'b Monad.t val (>>>): ('a, 'b) Arrow.t -> ('b, 'c) Arrow.t -> ('a, 'c) Arrow.t

'a     'b       'c        'd       'e     'f
--[R1] -- [R2]   --   [R3] --  [R4] -- [R5] --
  no cas    |  can cas  immly?  | no cas

'a 'b 'c 'd 'e 'f

--[R1] -- [R2] -- [R3] -- [R4] -- [R5] --

no cas | can cas immly? | no cas

Reagent気になりますね。因みにReagentの元論文はScalaなので興味のある方は是非読んでみて下さい。

Profiling Actor Utilization and Communication in Akka

Workshop: Erlang
Talker: Andrea Rosà, Lydia Y. Chen, Walter Binder
Paper: Profiling actor utilization and communication in Akka

Akkaの話があるということでErlangワークショップに足を伸ばしました。

Akka Profilerのようにメールボックスのサイズだとかメッセージを処理する時間とかではなくてアクター毎の初期化の時間だとか実行計算だとかメッセージやりとり数だとかを見たいのでそういうプロファイラを作ったというお話。

bytecodeベースのプロファイラなので抜け漏れがない他、既存のアプリケーションにアタッチすることが出来ます。

何やら難しそうな気がしますが、要は akka.actor.Actor のサブクラスのコンストラクタ、 tell 、 ask 、 receive なんかを追えば済みます。

さて、これを追うことで過負荷なActorや遊んでいるActorを追えるのでパラメータ調整なんかがしやすくなります。

で、実際のアプリケーション(Savina, Signal/Collect, Spark)を調べたレポートがありました。

まあ、バイトコードベースというのはJITが絡んだりとかを考えると色々辛そうですが頑張っているようです。因みにツールは公開してなさそう。残念。

The Nifty Way to Call Hell from Heaven

Workshop: Erlang
Talker: Andreas Löscher, Kostis Sagonas
Paper: The Nifty way to call hell from heaven

Erlangの世界をHeaven、Cの世界をHellに例えてC FFIのお話。

ErlangからCを呼ぶにはPort-Driverを使ってstdio経由でやりとりする、C Nodesを使ってSocket経由でやりとりする、そしてNative Implementation Function (NIF)を使って直接呼ぶ方式がありますが、 NIFは高速ですが危険です。

NIFはまあ便利ではあるんですがちょっとバインディングを書くだけで圧倒的な量のコードを書く必要があってとても面倒です。実際に必要な情報は関数のプロトタイプの情報があれば十分です。なのでそれを使ってバインディングを生成するツール、Niftyのお話です。

デモがありました。ヘッダファイルをとソースファイルを食わせてあげるとerlang側からコンパイルして、リンクまでします。

eshell
1> nihty:compile("demo.h", demo, nifty_utils:add_sources(["demo.c"], [])).
generating...
==> demo (compil)
Compiled src/demo_remote.erl
Compiled src/demo.erl
Compiled c_src/demo_nif.c
Compiled /home/kostis/nara_demo/demo.c
ok
2> demo:heaven(0).
42

eshell

1> nihty:compile("demo.h", demo, nifty_utils:add_sources(["demo.c"], [])).

generating...

==> demo (compil)

Compiled src/demo_remote.erl

Compiled src/demo.erl

Compiled c_src/demo_nif.c

Compiled /home/kostis/nara_demo/demo.c

2> demo:heaven(0).

で、実装の話ですが大きく分けてパーサ、ジェネレータ、コンパイラから成ります。

Cヘッダのパーサ部分はLibClangに移譲していいます。TypeTableやSymbolTableなんかにアクセス出来るそう。

コードジェネレータはASTを組み立ててるのかと思いましたが、まさかのErlangのDjangoテンプレートライブラリのErlyDTLを使って生成しているようです。テンプレートで十分なのかぁ。

なんかコンパイラの話は飛ばされてました。

で、これでNIFが簡単に使えるようになったのですが、それでもまだ問題があります。CのコードでSEGVなんかを引いたらErlangのBEAM VM全体が死んでしまいます。折角堅牢なErlangを使っているのに残念ですね。この危険性上手く扱う方法としてVM isolation、NIFを動かす別ノードを立ててremote nodeとの通信という形で関数を呼び出す方法があります。 Niftyはなんとこれ用のコードも生成してくれます。

あとはスケジューリングの話だとか無名共用体/構造体はまだ扱えないなんかの話もありました。

因みにZeroMQのヘッダを食わせてみたら全てのデモコードが動いたそうです。すごいですね。

niftyはこちらにあります。

Semantics of the Lambda intermediate language

Workshop: OCaml
Talker: Pierre Chambart

OCamlの中間言語のLambdaのセマンティクスを考える話。

LambdaはOCamlの中間言語として使われている型無ラムダ計算をベースとした言語で、byte codeとnative codeの分岐点でもあります。つまりバックエンドに依らない一番低レベルな部分であり、最適化を行なうのに適していたり他の言語からターゲットにされたりの他にも静的解析やら他のバックエンドの開発、Coqなど色々に使われるのでセマンティクス大事だよね、というモチベーション。

「型無しって本当に型ねーからな」みたいな話もありました。

一応既にcamlrun、native backend, JavaScriptなど色々なバックエンドはありますが、どれも形式的には扱いづらく、また、バージョンによって変わるので非常につらいです。

ということで独立なセマンティクスを考えますが、色々考えていくとブロックや整数を扱わないとメモリを参照出来なかったりとLambdaを拡張するのも必要なようです。

==の問題だとかコンパイラのフロントエンドがセマンティクスではなくコードの形に依存しているとか色々問題があるようです。割と熱く説明していたのですがよく分かりませんでした。

最後に、これだけは覚えておいて欲しいのは Obj.magic は思っている以上に危険です。普通は使わないようにしましょう。

最後に

ICFPから大分時間が掛かってしまいましたがこれでICFP及び併設イベントの参加レポート全てが終わりです。併設ワークショップ自体は24日まで続きますが、私は参加しませんでした。また、25日に有志で証明の勉強会、Proof Summitが行われ、参加してきましたがそろそろ疲れてきたのでレポートはやめておきます。Coqで機械学習する話とかがありました。

最後まで読んで下さった方に耳寄り情報を出すと、ほとんどのセッションのビデオがYou Tubeで公開されています。ICFP Video – YouTube

それではお疲れ様でした。

Author

admin