pi calclusを学ぶにあたって参照したドキュメントとその紹介その一
動機
ぼくはgopherなのでgorutine/channelを用いたプログラミングが好きだ。
ついでに非同期、並行プログラミングも好ましいもので、haskellやrustなんかの手法を知ってにやにやしている。
それらにともなって背景とされるhoareのCSPとその拡張のpi calclusについて調べて遊んでいる。
なんか寄り道をしてタネンバウムの分散システム本をなめたりTaPL再読なんかもしているが、
それはそれとして様々なドキュメントを参照した。
それぞれを紹介することで自分への理解度を試したいと思う。
言ってしまえば、ぼくの愚痴であり、自習ノートである。
ついては、ぼくの紹介が不十分であったり間違っていたりした場合には、
ブクマコメやツイッターなどでdisっていただけるとぼくの勉強の一助となってありがたい。
ついでに、間違った情報を界隈に広めずに済む利点がある。ご協力いただける方々には感謝を捧げたい。
以下紹介
初歩の理解のために
和訳版TaPL監修やmini-camlのsumii先生(たぶん)のところのWebにあるπ計算の紹介記事。
true/falseの定義や再帰的な処理に関しての記述を簡単に書いてある。
十全な学習にはならないが導入としてわかりやすい。
encoding: ISO-2022-JPじゃないと読めないため要注意
大学の諸先生方には口を酸っぱくして「wikipediaは参考にするな」と教えられたが
それはそれとして和訳本が見つからず、一単語しか知らない時にwikipediaのreferenceとlinkを参考にするのは大変手っ取り早い。
後に述べるMilnerの原論文のsummary的なものに仕上がっている。また、応用についてのrefをたやすく得ることができる。
spi calculus, ambient calclus, Calculi of Sequential Process, Algebra of Sequential System などだ。
pi calculusはCSPの拡張だからprocess algebraの歴史をさらっておくと理解が進むような気がする。
process algebraのサーベイ論文を読むことにした。
意味論の登場からbetri netにつながり、CCSやCSP、ASPへの経緯。またpi calclusへの拡張のモチベーションが分かるような気がする。
大本命、pi calculusの原論文。この後何回かの拡張(チャネルの可変引数とか)がされているため、後発の資料に書いてある定義と異なる部分が多々ある。
あと、記法に関しても多くの方言が存在するようだ。
part 1とpart 2で構成されていてpart 1は最小のにgrammer(と僅かなsyntax sugar)と等価性、双模倣性に関する簡単な記述と数多くの具体例(encoding to lambda calculus, tupple etcetc)、
part 2は等価性と双模倣性の関係や、強い双模倣性と弱い双模倣性に関する詳しい記述がある。
双模倣性は余再帰を用いてよしなにするらしいという点とTaPL21章に詳しいと聴くがちゃんと読んでいない。
大学の図書館にあったので借りて読んでみた。日本語で書いてあり、大変わかりやすく、前提なしでも程度理解できる。
食事する哲学者の例えを用いていたりJCSPを用いて実装からCSPを用いた並列と検証について記述している。
Javaが読めなかったので半分くらいしか読んでないが、実用における用途は大体書いてあってちょっと知りたいだけなら
これよんでおしまいで十分のようだ。
next step
可変長の引数を取るプロセスへの拡張。
Milnerの原論文でプロセスに多変数を束縛する構文が備えられていた。
複数の経路を受け取ることもできるわけだし、この構文がそのまま可変長引数に当たると思うので何故わざわざ拡張しなくてはいけないか。
自分の理解は
間違っている事に気がついたのであとで書き直す
単純な型付きpi calculusについてのスライド。形式的定義が書いてあるので、どのような定義が与えられるのか参考にした。 このあたりで一度TaPLを読み返し単純型付きラムダ計算との比較などをすると面白い。
conclusion
pi calculus、ひいてはCSPさらにはプロセス代数にまつわるドキュメントを参照として並べた。大変お粗末なものである。
形式的な定義を理解しその意味を知ることはより良い並行性、非同期性の手法を考えるのに意味があるんじゃないかなと思う。
pi calculus特有の型システムの存在しているのかだとかASPやspi calculusにanbient calculus
あまり関係ないがbetri netやactor modelなどの比較ドキュメントなども知りたいので探していきたいと思う。
プロセス間の通信経路を持つ(そのような抽象化がされている)言語でregion infferenceは使えるのかとかgorutineのGC実装にどれくらいCSPの影響あるのかなども気になるところだ。
multithread programmingにおけるGCが使えるような気がするからgorutineでのGCはそんなにプロセス代数を背景にしていないような気もする。
グリーンスレッドに関する研究開発はそれは昔からあったであろうし。
線形型をpi calculusに落としこんだらメモリ開放もよしなにできるとかないだろうか。
こんなアホなことやってないで、留年生らしく単位とって進級しろと怒る学友の姿が目に浮かびすぎてつらい。
だいがくおもんないなぁ
appendix
コレも読んどけ
* Type and Programming language
邦訳"型システム入門" 通称TaPL
ある程度の予備知識として単純型付きラムダ計算についての理解があるとpi calculusの動機についてインフォーマルな理解ができると思う。
5,6章辺りまで、深く追いかけたとしても10章まで読めばpi calculusへの導入としては十分に思える。
- Advanced Topic in Type and Programming language
上記"型システム入門"の発展版 多分通称はATTaPL
ただし僕の周りにこれを読んだことがある人がいないのでなんて呼ばれているかは分からない。
rust1.7.0のTcpStreamに関する所見
tl;dr;
rust 不慣れな感じがバリバリ出ている僕のための覚え書きエントリ
intro
今後様々なプロトコルを様座な言語で実装する遊びを行うに当たってはじめにrustでなんか実装することにしたから、rust 1.7.0のstd::net::TcpStreamに
関する取り回しを考えてみた。
おそらく僕はそれらを忘れると思うので、念の為にまとめてみたいと思う。
rustに関する説明は
https://www.rust-lang.org/www.rust-lang.org
またソースコードは
github.com
手始めに覚えたい人は
このtutorialを見ると良い。
最後のtutorial。tutorialとか言いつつ結構色々あって一週間くらい毎日読まないと全部読み終わらないっぽいのが強い。
ハマったコード
HTTP/1.1を叩くだけの簡単なプログラムを書いた
use std::io::prelude::*; use std::vec::Vec; use std::net::TcpStream; use std::string::String; fn main() { { let url = String::from("google.com:80"); let mut stream = TcpStream::connect(url.as_str()).unwrap(); let _ = stream.write(b"GET / HTTP/1.1\nHost: google.com\n\n"); let mut s : Vec<u8> = Vec::new(); let _ = stream.read_to_end(&mut s); println!("{}", String::from_utf8_lossy(s.as_slice())); } }
このコードはgoogle.comの80番ポートにあるHTTP1.1サーバにGETを要求するだけの簡単なプログラムだが、
ずっとblockingしてstdoutへの出力が一向に出てこない。
tcp timeout
この時点での問題は std::net::TcpStreamのdocumentにnoticeとして書いてある。
TcpStreamにはreadとwriteのtimeoutがあり、これを設定せずにNoneのままにしておくとobj.readが無限にブロックする。 つまりstream.read_to_endが現状ではblockしてprintln!まで出てこない。 よって obj.set_read_timeoutを設定すれば良い。
use std::net::Duration; //中略 let _ = stream.set_write_timeout(Some(Duration(10,0))); let _ = stream.read_to_end(&mut s); println!("{}", String::from_utf8_lossy(s.as_slice())); } }
timeout目一杯まで待ってしまう
先ほどの変更を加えるとresponseを受け取れる様になった。が、timeout時間目一杯までresponseがblockした。
shutdownを呼び出す
使い終わったstreamに対しshutdownを呼び出す事によって、timeoutまで待たない処理を書けるようになる。 shutdown関数はstreamの処理を直ちに終了しその時点で適切な返り値を設定する。例えば、Result型におけるOkを返すようにするなどする。 これを呼び出すと望み通り動く
use std::net::Shutdown; //中略 let _ = stream.write(b"GET / HTTP/1.1\nHost: google.com\n\n"); let _ = stream.flush(); let _ = stream.shutdown(Write); let mut s = String::new(); let _ = stream.read_to_string(&mut s); println!("{}", s); } }
shutdownはShutdown型をうけつけShutdown型はBoth, Write, Readのenumだ。 でもコレ以降TcpStreamを受け取れなくなるからナンセンスな感じがすごいする。 try_cloneして複数オブジェクトからTcpStreamを共有したときにこの方法は使えない
※追記
Connection: closedを明示するとちゃんと動く。これはHTTP/1.1の仕様に基づくものでrust lang側の問題ではない。 僕の過失である。ざんねん。
結果
ほんまどうにもなんねぇな
ここから所見
ust langは並列並行処理を強くサポートしメモリ管理を厳しく行う言語である。
そのため、標準ライブラリのAPI設計も強くメモリ管理を意識した設計になっていて、
更に問題を並列化で解決させようとするきらいがある。
ひとつのTCPコネクションを取り回して設計したりするとき、rustが求める使い方は
TcpStream::connectでstreamを取得したら、ブロックでスコープを分けて、try_cloneでオブジェクトを複製して
スコープが閉じるタイミングあたりでオブジェクトの寿命が来るように書いて、複製したメモリは
region infferenceで回収させるといったかんじにするべきなのだと思う。
しかしどうあがいてもtimeout目一杯までのまつ問題は解決できなかったためこれどうなってのまじで。
おしまい
pixiv 2016 SPRING BOOT CAMP に行ってバックエンド(の一部)を触ってきた
inb4, tl;dr
の感想エントリです。
- github面接で受かった
- 技術職と総合職(一般職)が半々で二十人弱来てた
- やることは運用されているコードの改善
- ミドルウェア/処理サーバ実装を好むインフラ系技術職は(おそらく)僕だけだった
- グループ開発だったが僕は一人チーム
- 書いた言語はC++
- やったことはオレオレプロトコルサーバの冗長化実装
- 普通に時間足りなくて終了
- 面白かったよ
- 今回の課題方針だと、技術職インターン生の割合はどうしてもPHP/Railsエンジニアが多めになる傾向を感じる
- でも課題によってはセキュリティ系が多かったり僕みたいなのが多かったりまちまちっぽい
以下、詳細に説明していきます。
対象読者とまえがき
当エントリは、Pixivの学生インターンに興味のある技術職向けに書きます。
また、僕の主観はインフラ/ミドルウェア開発に寄っているので、
Pixivを志す学生の多くを占めるだろうPHP/RailsやHTML/CSS/JSによるWebアプリケーション開発者や
Andoroid/iOS開発者としては不満の残る記事になるかもしれません。
さらに、総合職の人とはあまり話してないので、彼らひいてはこの記事を読むであろう
総合職志望のあなたが持つの関心にそうことができないと思います。
幸いなことに、同期のインターン生のかれらもまた彼らのエントリを書くことになるので、
Pixivの広報ブログなり何なりから探してみてください。
多くの技術職インターン生はPHP/Railsに詳しい学生でしたし、データ解析やデザイナーの学生もいました。
参加のきっかけ
github面接って応募するコストがまったくないので、締め切り2時間前くらいにぽいっと投げました。
知ってたけどgithub面接って応募するのは楽でも採用するのはエンジニアの時間を持ってくのでけっこう大変らしいですね。
理由は自社ホスティングのWebサービスを主にして回っている企業の中身を見てみたかったというのが強いです。 あと金。
採用まで
github面接なので書類はほぼなし、「面接しよ?」ってメールが来たのでSkype面接をお願いして
日程合わせて、お昼から30分弱くらいおしゃべりしました。
RailsもPHPもわからんって話とmrubyのC ext ライブラリを書くのが趣味だからruby自体はそれなりにわかるみたいな話をしました。
あと、Go言語が好きでconcurrencyを用いてリクエストを捌くのが面白そうって話はしたようなしてないような気がします。
そしたらなんか受かってたので楽しい東京旅行が決定しました。
環境
オフィスは商業ビルのワンフロア。フリードリンクでコーヒー、緑茶、紅茶、みそしるから好き勝手持ってってよし。
椅子はいい感じに座りやすい。最寄りの駅からは5分くらい。
パソコンは持ち込み可、僕はZenbookにArchのっけて使っていますが、技術職はほぼMac稀にubuntu/debian、総合職の人たちは
Mac or Windowsでした。
インターン生は、来月新卒が来るらしい空きスペースに陣取って、わいわい開発をしているみたいでした。
遠方からのインターン生にはビジネスホテルの部屋が割り当てられて徒歩30分くらいの場所です。
僕はカフェイン中毒者なのでオコーチャとコーヒーを交互にかっぱかっぱ開けて飲んでいました。
勤務時間は10時から19時まで(8時間+1時間休憩)。
真面目に考え事していると18時くらいには眠くなってしまうのと定時帰宅するという強い意志をもって臨んでいたので大体とっととホテルに帰ってゆゆ式見ていました。
課題の割当
みんなの話
そもそものインターンのコンセプトにとしてPixivの裏側を見れるってのがあり
それにで釣られて来た学生なので、それぞれPixivのサービスの改善の提案と
実装を5日間で試してみるっていう話だったと思います。
二,三人のチームに技術メンターさんと総合職メンターさんに統括の人がついて
下手な会社の研修より人員が投入されてそうな気配すらありました。
おそらく、解析とかマーケとかに興味のある総合職さんの提案を、技術職やデザイナーが
吟味して実装に落とし込む見たいなフローだったんじゃないかなぁと思ってます。たぶんね。
ところで、僕の話をしますと
まずインフラチームのところに連れてってもらって、インフラチームの技術職の人にメンターをしてもらいました。
そしてやや中規模くらいのC++のソースコードを渡されて、コードリーディングをしてもらって内容の把握と設計の方針を教えてもらった後、一人ひたすら拡張の実装を行いました。
冗長化実装を主にやってたのは、僕の中で洗い出された方針の中で調査に時間がかからなそうだったと、メンターさんのおすすめと、改善に必要な情報が守秘義務項目にかかりそうでいらん守秘義務を持つのが嫌だったからです。
他のチームがユーザから見える部分に重きをおいた課題だったのに対して
僕はサーバの改善というひたすらに技術的な課題を与えられました。
githubにはミドルウェアの拡張とかshared librayの言語clientだとか
言語 to 言語のFFIみたいなのばっかおいているので
なんかそういうのが向いていると思われたらしいです。
慧眼だと思います。
そもそもインフラがメインっぽい人たちは僕以外そんなにいない上に、
当初の予定では、今回はインフラっぽい人が来ることは想定してなかったらしいので
TODOではあるけれどASAPでもMUSTでもないタスクを割り振られた感じがしました。
万が一改善したら御の字みたいなやつ。触りやすくてGoodでした。
想定外の方向性をついてインターンに参加するとほぼ実務みたいなのが出てきて面白いので
インフラのみんなもPixivをつついて遊んでみましょ?
結果
課題の結果と、割当の結果についてお話します。
課題の結果について
技術的調査と仕様の拡張の策定に3日かかりました。ちなみに、全体的な方針はともかくとして個人的にはとりあえず実装してみるという方針で行い、多少悪筋でも動くものを提出するようにしました。 だいたい午前と午後の始まりと終わりにメンターさんに方針を相談して、方針の問題点を洗い出して、 次の調査を行って相談して洗い出してを繰り返していました。必要上、現行の運用方針とかも聞いたりするのは楽しかったです。 C++も書いたことがなくて主にblocking pararrelの調査に時間を割きました。
仕様を提案してレスポンスが返ってくる実装はしたのですが、プロトコルを拡張しただけでサーバとして動く実装が終わらなかったのが心残りです。
プロトコル拡張も仕様としての整合性がいまいち取れてない点に気がついちゃってその対応も半ばという状態です。
ぶっちゃけて言うと時間が足りないのが悪いんじゃい。
最終報告の際、粛々と手堅くエンジニアリングしている的なことを言われたのは喜ばしいことでした。
総合職インターン生やフロントエンド側のインターン生の反応とかいまいちで(喋ってる側としても思ってたけど正直反応に困るってのが普通だと思います)、まあインターン生の中では一番地味な成果だったと思います。
割当の結果について
他のチームは数人の学生に技術メンターと統括メンターがついておりまして、
また、統括メンターさんは複数のチームを文字通り統括していらしたので、かなり大変だったと思います。
さらにまた面白い話で、僕はインフラチームに連れてかれた後、そのままインフラチームのテーブルで、他の学生と離れて作業していました。
なので統括メンターさんがこっち来ることはあまりなくて、技術メンターの人の隣で作業していたことも相まって 半分OJT状態です。
この状態は個人的には、プログラミングのあれからこれまでを相談する相手ってのに恵まれたことがなかったので好ましいものでした。
(プログラマーの先生ってソースコードだよね。仕様がわからんかったら公式ドキュメントか最悪コンパイラ読めよそこにはすべてを置いてあるっていう勉強の仕方してる人です)
元のコードの設計も手堅いように見えましたし、メンターさんの受け答えも明快だったので捗りました。
その状態に問題がなかったかってっとそうでもなく、一番の問題は、他のインターン生とやりとりが一切なくて、最終日の打ち上げでおまえ誰だ感がなかったようななかったようなあったようなって感じです。
KPTも初日しかしてなかったし。
コミュニケーションコストを支払ってチーム開発するのと、一人設計をし続けるのではやはり色々と違うものがあるので、その辺を体験できなかったのは痛手かもしれません。
そういえば、なぜかインフラチームの朝会に混ざって聞いていたのであれはとてもおもしろかったです。途中からなぜか自分もしゃべるようなったので、さらに面白くなりました。
お昼も社員さんに混じってばっかでしたし(おごってもらったありがたい)、水曜日にあった全社員によるランダムマッチお弁当大会(席を完全ランダムに決めてお弁当を食べる)も系列会社だかなんだかの人を他のインターン生が質問攻めにしているのをのんびり聞いてました。
まとめ
ほかにもいくつかありましたが、僕が書くべきことはこれくらいかと思います。
自社ホスティングのWebサービス企業において、最も良い環境をエンジニアに提供している企業のひとつであるかと見受けられるPixivさんを見ることができたのは僥倖でした。
しかし、実装がおわらんかったのはすごく痛いなぁ。
僕は技術と嫌いなことをやらないことと遊ぶことの次にお金のことを考えているので、今回のインターンにかけられたマンパワーと経費を脳内で換算しながら説明とかを聞いていたのですが、
おおーってずっと思いながら聞いていました。ここに書くのもなんなのでリアルで会える知り合いは僕に話題を振ってみてください。守秘義務に反しない程度にお教えします。
インターン終了の次の日、立川シネマシティでガルパンの極爆上映を見た後、博多への新幹線に乗りお家へかえりました。
thnx for reading.
libvmod_mrubyなるものを作り始めた
概略
HTTPアクセラレータVarnish Cacheの設定言語VCL。そのVCLにmrubyのコードを呼び出せるようにした。
今後はRubyでVCLの設定をスクリプティングできるようにして、C言語ライクなVCLより柔軟性が高いであろうRubyのDSLで設定をいじれるようにしたい。ので、作り始めた。
詳細
例
requrement
Varnish Cache 4.0.0 or later(開発ではHEADを使っている)
root権限
git clone http://github.com/KeizoBookman/libvmod_mruby.git cd libvmod_mruby/src git clone http://github.com/mruby/mruby.git cd mruby make cd ../.. ./autogen.sh ./configure make make install
そしてdefault.vclなどのVarnishの設定ファイルに以下のように記述します。(Archでは/etc/varnish/default.vcl)
import mruby; sub vcl_deliver { set resp.http.mruby = mruby.exec(" 'hello world' "); }
と設定してVarnish Cacheを起動させ、VarnishCacheの立っているポートにアクセスすると
ヘッダにmrubyと言う名前のものが追加されておりhello worldという値が入っているはずです。
今できるのはこれだけであとはintegerかvoidのRubyスクリプトをVCLから呼び出せます。
今後
今のところ出来ることはほとんどないけど、RubyからVCLを呼び出せるようにするところまではちゃんと実装するつもりです。
masterは一応make出来る状況を維持しておくけれどもちゃんと動く保証はありません。github.com
余談
ネタ自体は一年位前に人にもらって何度か作ろうとしてたけどやっと実装を始められたのでちょっとワクワクしている。
とあるvim宣教師の手記
vim advent calendar
Vim Advent Calendar 2013 : ATNDの131日目です。
昨日はsupermomonga さんのジャズだって聴ける。そう、Vimならね。 - かなりすごいブログでした。
jazzradio.vimよいですね。
vimテクニックバイブルに対して戦いていた友達に教えて、味のある顔をしてもらおうと思います。
前振り
諸事情でOS = windows くらいの情報リテラシーの人たちにvim を教える
機会に巡り合いました。「よーし、お兄さん張り切っちゃうぞー!」と
頑張っていたのですが、そこはそこ。
ちゃんと偉い人に「自重するべし」とくぎを刺され、
vimtutor ja をやってもらったところでお開きとすることに相成りました。
しかし、ゴーストがスライドを書けと囁いたので
vim ネタスライドを書いて自分の熱意をお焚きあげしようと思います。
ちなみにVACをやっているコミュニティvim-jpですが、
活動の一つに
vimrc読書会が毎週土曜日23時から行われております。
またvim plugin 読書会その前の21時からたまに開催されているそうです。
つぎは今週でvital.vimをやるとか。
自分は半年くらいROM専やってますが面白いです。だめじゃん
というわけで以下リンクよりネタスライドをどうぞ
reveal.jsを使ったmdで書きました。
あとがき
この前、クトゥルフ神話TRPGを初めてやってキャラロストしてきたので
なんとなくこんなタイトルになりました。