Settingsは GET /initialize でのみsetされ，あとはgetしか行われないので，ここをDBから外す作業をしました．はじめはグローバル変数の dict に乗せていたのですが，そうするとgunicornで起動したときに /initialize を受けたプロセスでしか初期化されずFAILしていました．そのため各サーバにRedisを入れ，そこにSettingsを格納しました．

Do not use database for settings by utgwkk · Pull Request #4 · innocent-team/isucon8-final · GitHub

always get settings from Redis · innocent-team/isucon8-final@24c80be · GitHub

やらなかったこと

インデックスを貼る

今回はインデックスにはとくに手をつけませんでした．各所に重たいクエリがあるのでまずそちらをどうにかしなければなーと思っていたら競技が終了していました．

ろうそくの改善

ろうそくを出すときにかなり重たそうなクエリが投げられていることは分かっていたのですが，最後までどうにもなりませんでした． MySQL 8.0なのでwindow functionが使えるしなんとかならないか！？と思ったけれどすぐにできるものではなかった……．

SNSシェアを有効にする

終了30分前ぐらいに，SNSシェアしたらどうなるか見てみましょうということで，

res["enable_share"] = True

をやってみたところ当然failしたのですぐに差し戻しました．

懇親会で聞いたところ，appサーバのうちどれか1つだけでSNSシェアを有効にするとか，一定確率で有効にするとかの戦略を取るのが正しかったようです．巷ではこれをA/Bテストと呼びます．概念は知ってたけどそうする発想が出なかったのでめちゃくちゃ悔しい……．

サーバのリソースにはわりと余裕があったので，少しだけ有効にしてたら10000点は出ただろうなーと思っています．

ユーザのBAN

これも終了30分前ぐらいにエイヤッとやったところ当然failしたのですぐに差し戻しました．そもそもSNSシェアがかなりの割合で有効になってきてから効くようになるとのことだったので，早とちりでしたね……．

感想

テーマとしても面白く，かなり考えられた問題だなーというのが分かりました．現代のwebサービスはアプリ内部だけ完結せずに外部APIと連携するものが多く，それを踏まえたテーマとなっていたように感じます．懇親会で他のチームの方や出題者の方々とお話をしたところ目から鱗となる戦略がどんどん出てきて，やはり実力があるなーと思いました．

チームメイトの id:wass80 id:nonylene ，運営の皆様，他チームの皆様，そしていろいろなところでISUCONを支えてくださった皆様ありがとうございました．めちゃくちゃ楽しかったし勉強になりました．学生のレベルがだんだん上がっており，しかも来年から学生枠がどうなるか不明という話を耳にしてビクビクしていますが来年も出たいです．

*1:team id:18

*2:もちろん社会人枠の方々のレベルもかなり高かった．

2018-10-19

KMCの例会講座で「ラムダ計算のインタプリタを実装してみる」話をした

技術

speakerdeck.com

KMCの例会講座で，型無しラムダ計算についての軽い説明と，そのインタプリタを実装した話をしました．できた実装はこちらです．

github.com

講座の流れ

ラムダ計算について知ろう
- ラムダ項
- 束縛変数と自由変数
- 変数の置換(代入)
- α変換
- β簡約
ラムダ計算のインタプリタを実装しよう
- 仕様の決定
- データ型の定義 (syntax.ml)
- 構文解析の実装 (parser.mly)
- 字句解析の実装 (lexer.mll)
- De Bruijn indexへの変換の実装 (deBruijn.ml)
- β簡約の実装 (deBruijn.ml)
- デモ

動機

ラムダ計算を実装するという体験の共有

ラムダ計算は計算体系の1つで，

関数抽象(関数をつくること)
関数適用

2つの操作によって構成されており，これだけでチューリング完全になります．

わたしは研究分野の性質上，ずっとラムダ計算を拡張した体系の論文を読んでいます．しかし今まで，その数学的な性質を確かめていても，簡約が機械的に行われることは自分の手で確かめていませんでした．

そんなわけで ~~論文を読むのがダルいときに~~ 実装を進めていました．できあがったものの共有というのが講座をやった動機の1つです．

実際，じぶんの知っているラムダ計算の知識だけではうまく簡約ができず，試行錯誤する必要がありました．そういったつまずき体験を共有し，解決策についても共有する*1ことに講座のもう1つの意味があります．

プログラミング言語の処理系について意識してもらう

プログラミング言語のコンパイラやインタプリタがどのように実装されているか，というのは，普段のプログラミングではなかなか意識しないことだと思います．そこに少しだけ意識を向けてもらって，ザ・メイキングを見るときのような気持ちになってもらったり，よくわからないけどいろいろな世界があるのだなと思ってもらったりする，というのが講座の動機のもう1つです．

質問

講座のあとに出てきた質問とその回答，フィードバックを記録します．

β簡約のステップがよくわからなかった

私も最初はなぜこれでうまくいくのか全くわかりませんでした*2．簡約のステップをスライドに示しつつやっていたので，そのスライドを再掲してゆっくり追ってもらいました．

じつはスライドに示した規則はβ簡約の規則の1番目に過ぎません．項全体だけではなく，項のある一部分だけについても同様にβ簡約してよい，という規則があります．これは住井先生の「計算機ソフトウェア工学」の講義資料などにより正確な説明があります．

今回の講座ではそれを含めずにβ簡約について説明していたので，含めたほうがよかったですね*3．

実装期間はどれくらいか

2週間ぐらいで実装しました．10/7には作業をした形跡があったのでそれぐらいの時期からやっていたようです*4．

今後どこまで実装していくのか

ひとまずは「今後の課題」に挙げたものが解決できるとよいなーと思っています．

型を付けることに関しては，いちおう単純型の型推論がすでに実装されています．しかし講座でそこまで取り上げると型の説明のために時間が長くなってしまうとみて今回は割愛しました．

De Bruijn indexにおける自由変数の扱いについて，どうにかしたいと書いていましたが，諦めるしかないという結論になってきました．そもそも自由なので外部環境が変化すればindexも変化するため，外部環境が不明な状況では放っておくしかないでしょう．

その後

例会後に今更SICP読書会というSICPを読む会がありましたが，そこでチャーチ数に関する練習問題が登場し，人々が格闘していました．

ラムダ計算のインタプリタについて発表したその日，ひとびとがチャーチ数と格闘することになるとは予想だにしていなかった……
— うたがわきき🔰💊 (@utgwkk) 2018年10月18日

わたしはWikipediaをチラ見しつつ階乗を求めるラムダ式を書いていました． Y (\fn. IFTHENELSE (ISZERO n) (\fn.fn) (MULT n (f (PRED n)))) を少し簡約したのが以下の式になります．

階乗関数のλ式です．
(\g.(\x.g(xx))(\x.g(xx)))(\fn.(\pxy.pxy) ((\n.n(\x.(\yz.z))(\yz.y))n)(\fx.fx)((\mnf.m(nf))n(f((\nfx.n(\gh.h(gf))(\u.x)(\u.u))n))))
— うたがわきき🔰💊 (@utgwkk) 2018年10月18日

ところでこの階乗関数からYコンビネータを取り除いても型検査に落ちるのですが，そういうものなのでしょうか．

追記

発表原稿を公開しました．

*1:あるいは解決できなくても試行錯誤の過程を共有する

*2:今もぜんぶ分かっているかについては自信がない．

*3:実際に，スライドの参考資料[1]ではβ簡約をleast compatible relation satisfying ~というふうに定義しています．compatible というのが今回示さなかった規則にあたります．

*4:commit logはいちど消し飛ばしてしまった……．

2018-10-06

■

酒

3日連続飲酒で胃腸が荒れまくってるし，整腸剤を切らしていたことを思い出した．

2018-10-02

■

最近ずっとGoogle Homeのアラームを設定して，設定した時間よりちょっと早く目が覚めるというのをやっている．試しにちょっと早めに目が覚めたらそのまま二度寝したら，アラームで起きたときめちゃくちゃ目覚めが悪かった．文明を逆手に取って生活リズムが形成されているみたいな形になっている．

2018-09-28

突発和歌山旅行

旅行

夜中に，旅行したいなーという気持ちが高まってきて，Googleマップを眺めていたところ，京都から和歌山まで安価で行けることが分かったので，友だちのオタクを連れてやっていきました．

松尾酒店

www.instagram.com

ホテルに荷物を預けてからまず真っ先に松尾酒店に行きました．ここには高垣酒造の高垣という日本酒があり，まあ上の写真で分かるように分かりやすいスポットとなっています．お酒がいっぱいあります．

写真撮影を快諾していただき，いろいろなお酒を眺めたのち高垣を購入し，ついでに枡も買いました．

和歌山城

城です．この日は雨が強くなかなか大変でしたが，展示を見てまわりました．順路に日本全国の城の写真が展示されていたのですが，首里城から五稜郭まで揃っており，城ですね～～となっていました．

🍺🍺🍺

tabelog.com

城を見たのち，ちょうどよく雨が弱まったので目星をつけていたビールのお店に行きました．ここは醸造所とパブが一緒になっており，できたてのビールを飲むことができます．

www.instagram.com

やっていきました．はーおいしかった．

🍶

tabelog.com

ホテル近くのお店で日本酒を飲みまくりました．写真で分かるかは不明ですが，湯呑みみたいな容器に日本酒がなみなみ注がれています．店員のおばちゃんが，私たちが日本酒を飲み干したらすぐに注いでこようとし，実際そのようになったので，めちゃくちゃな感じで面白かったです．

このような様子で4杯飲んだところ横のオタクのテンションがおかしくなりましたが生きています．

🐱

和歌山電鉄の電車に乗りました．地方ローカルの単線電車に久しぶりに乗ったような気がします．

I'm at 貴志駅 in 紀の川市, 和歌山県 https://t.co/MzmSj9oZRY
— うたがわきき🔰💊 (@utgwkk) 2018年9月27日

貴志駅では猫の駅長を見ました．猫の駅長は週休がちゃんとあり，我々より環境がよいのかもしれません．

総評

和歌山は想像以上に行きやすいので，行きましょう．京都からだと京阪+在来線普通車で1500円ちょっともあれば行けます．くろしおに乗るにしても+1kぐらい．

2018-09-18

ISUCON8 :thinking_face: 学生枠で予選通過した #isucon

技術 ISUCON

:thinking_face: *1というチームで参加しました．チーム名がかぶっているのには気づかなかったです．なんとか学生枠で予選を通過することができました．

チームはid:utgwkkと@wass80とid:nonyleneの学生3人です．使用言語はPythonです．3人ともそこそこ読み書きできるしコードの振る舞いが予想しやすいから，みたいな理由で選択した気がします．

github.com

やったこと

N+1クエリの撲滅

まず明らかに get_event() の処理が重いということが分かるのでN+1クエリを気合でエイヤッとした．ここがバグってなかなか前に進めなかったのが悔しい．なんとか解決できたのはよかったけど時間をかけすぎた． get_events() も含めるとN²クエリになっていたのをなんとかしたかった気もするけど時間が足りなかったね……．

`get_event()` を極力呼ばないようにする

イベントに関する情報をいろいろなところで get_event() を使って取得していたけど，そもそも存在確認ぐらいしかしていないところがあったので，そこは個別でSELECT文を発行するようにした．ブール演算ができなくて何度もバグった……．

その他

validate_rank() で座席のランクの存在を確認していたが，そもそも座席は増減しないのでDBに問い合わせないようにした．以下はおもしろコードです．

def validate_rank(rank):
    return rank in set('SABC')

なんかいろいろやった気がするけど忘れてしまった．他のふたりが記事を書いてくれると思うので待ってます．

やらなかったこと

MariaDBを捨てる

みんな大好きMySQLのほうが設定しやすいと思ったけど，MySQLだとなぜかデータの整合性が取れなくてMariaDBだと正常になるということがあって結局捨てなかった．あれ何だったんですか？？？？

デッドロックへの対処

複数台構成に切り替えたあたりからMariaDBのデッドロックが発生してスコアが安定しなくなった．これどうすればよかったんでしょうね……．最後はスコアが13000点代に乗ったらフィニッシュですねとひたすらベンチを回していて，点数が上下した末に13621点でフィニッシュした．下がりっぱなしではなくてよかった．

総評

gyazo.com

今回の問題は，「1台でそこそこ動くようになってきたし，とりあえず複数台にしたらもっとスコア上がるでしょ」という学生気分な希望的観測をへし折ってくれたという点でとてもよい問題だったと思います．高得点を目指すためにはDBのロックのことをちゃんと考えたり，もっと貪欲に重い処理を切り出していったりしないといけなく，なんとか本戦出場ラインに乗ったという感じでした．

15時ぐらいに，ぜんぜんスコアが上がらなくてもうだめだとなっていたのにいきなり19000点代が出て一瞬だけ大盛り上がりしました．そのあと実装もサーバ構成も整えたけどその点数には届かなかった．あれは何だったのでしょう……．

追記:他の2人がやったことがここに書いてあることを思い出しました．やったこと · Issue #1 · innocent-team/isucon8 · GitHub

運営の皆様ありがとうございました．ダッシュボードがとにかく使いやすくベンチも快適でした． @wass80 ありがとうございました．アプリの実装を先読みして改善点を洗い出しつつペアプロでバグを解消してくれて大変やりやすかったです． id:nonylene ありがとうございました．インフラ関係のところを全部任せていましたが高速に設定を変えていってくれたので実装に専念できました．

本戦楽しみ！！！！！名札欲しい！！！！！！！！

*1:team id: 18

2018-08-29

8月振り返り

めでたい報告はだいたい行ったので，それ以外の雑多な振り返りです．

utgwkk.hateblo.jp

言語処理系

多相 let と let rec が実装できたので優勝といっても差し支えないのではないだろうか．

Coq

ぜんぜんできなかった証明を友だちに診てもらったらできてしまったので、見てもらうの大事そう
— うたがわきき🔰💊 (@utgwkk) 2018年8月29日

「無限ループは停止しない」ということを証明できずに詰まっていたが，見てもらいながら証明を書いていたら数分でできた．

アルバイト

最近ちゃんと労働できてない気がするのでもうちょっと整えてやっていきたい*1 *2．

総括

いろいろ終わって落ち着いてたら無限に寝たいと思うことが増え，人間ぽい活動をするのが億劫になってしまった．

*1:心の底から労働がやりたいというわけではなく，文化的な生活をキープするために続けなければならないのである．

*2:コミュニケーションが発生してだるいなーという気持ちが出てきたり出てこなかったりしているというのもあり……．

やったこと

N+1クエリの解消

_get_latest_trade() に LIMIT 1 を付ける

SettingsをRedisから取ってくる

やらなかったこと

インデックスを貼る

ろうそくの改善

SNSシェアを有効にする

ユーザのBAN

感想

講座の流れ

動機

ラムダ計算を実装するという体験の共有

プログラミング言語の処理系について意識してもらう

質問

β簡約のステップがよくわからなかった

実装期間はどれくらいか

今後どこまで実装していくのか

その後

追記

松尾酒店

🍺🍺🍺

🍶

🐱

総評

やったこと

N+1クエリの撲滅

get_event() を極力呼ばないようにする

その他

やらなかったこと

MariaDBを捨てる

デッドロックへの対処

総評

言語処理系

Coq

アルバイト

総括

`_get_latest_trade()` に `LIMIT 1` を付ける

`get_event()` を極力呼ばないようにする