【11月度】社内勉強会を開催しました。

ジオロジックでは、毎月月末に「ジオロジックカンファレンス」という勉強会を行っています。今回は、11月分のエンジニア勉強会、ジオロジックカンファレンスの様子を紹介します。

今回の勉強会は、SmartNewsとの合同で行いました。
参加してくださった２名の方、ありがとうございました！

Glimping Agda @sarashino

「型による証明をAgdaというによって行う」というテーマで、sarashinoさんが発表してくれました。
型による証明が開発者にとって有益であることはHaskellやScalaの産業での応用から明かだそうです。
一方でそれらの型システムは不完全で，プログラムに完全な証明を提供することはできないそう。
そこで，プログラムの証明をより良く学ぶために，定理証明を提供するAgdaについて調べたところ、AgdaはHaskellとの相互利用が可能であり、つまり産業レベルのライブラリと共存することができるそうです。

内容がかなり高度で、その後の質疑応答も大変盛り上がりました。

Intel CPUの50年 @aramaki

aramaki （from SmartNews）さんが「ビジネス要求によってアーキテクチャ構造が変わる」というテーマで、IntelのCPUの歴史を振り返ってくれました。

Intel CPUの50年の歴史を紹介しながら、要求の変化について解説してくださいました。歴史を追っていくと「開発リソースがない」「とにかく高速化したい」「様々なユースケースに対応したい」などのリソース面の事情や、ビジネス要求、社会の構造を反映したCPU構造になることが分かるということでした。

組織構造がソフトウェアアーキテクチャに反映される「コンウェイの法則」は聞いたことがありましたが、ハードウェアにも当てはまる、ということを知りました。

普段のジオロジックカンファレンスではあまり取り上げられないようなテーマだったので、とても興味深かったです。

Apache Spark 入門@haru

私、haruは「Apache Spark」について、今回は特にSpark SQLを中心に発表しました。Sparkでデータを扱うためのAPIや、実行プランの最適化について紹介しました。

最適化の方法には、読み込むデータを減らすなど様々ありますが、業務をしていてJoinアルゴリズムの影響は大きいと感じます。実際に、アルゴリズムをBroad Hash Joinに変更するだけで、クエリの実行時間が大幅に短縮されたことがありました。

次回は、今回発表できなかったSparkのストリーミング処理や機械学習について紹介したいと思います。

LXDを触ってみる @ishikawa

ishikawa（from SmartNews）さんが「Docker以外のコンテナ技術、LXD」というテーマで発表してくれました。

Dockerが「アプリケーションコンテナ」であるのに対して、LXDはマシンをコンテナとして立ち上げる「システムコンテナ」です。実際に発表内でデモをしながらわかりやすく説明してくださいました。
家でたくさんの仮想マシンを建てている場合は、LXDを使ってみるのも面白いかもしれません。

sarashinoさん、aramakiさん、ishikawaさん、ありがとうございました！