私は2020年の10月に北陸先端科学技術大学院大学（Japan Advanced Institute of Science and Technology）先端情報科学 博士前期課程の東京社会人コースに入学しました。緒方研究室に所属しています。形式検証が主な研究テーマです。
修了するためには研究以外で20単位以上必要なので、この半年は講義の受講がメインでした。受講した講義は以下のとおりです。
- システム最適化
- オペレーティングシステム特論
- データサイエンス論
- 機械学習工学
- 高機能コンピュータネットワーク
- 遠隔教育システム工学
- 人間力イノベーション論
- 創出力イノベーション論
優が7つ、良が1つでした。良があったのはとても残念でした。自習と比べると、必死に勉強しようと自然と思える点、テストやレポートを通して理解度が明確になる点、先生から興味深い話を聞ける点が良かったです。未経験のことを短期間で習得しようとすることも楽しいです。
個人の将来的な目標は技術で未解決の問題を解決することです。人の役に立ち、かつ普遍的な知見となるようなことを目指したいです。博士前期課程では研究をとおして専門性を深めていくための準備をしたいと考えていたので、まだやりたいことはできていません。
よくある質問
いつ勉強していますか？
平日の朝と夜、休日です。
仕事と大学院を両立するのは大変ですか？
まだ、それほど大変だとは感じていません。自分の意志で自由に使える時間が多いことが関係していると思います。ただ、大学院で勉強や研究をしている状態と大学院に入学せず、何もしない状態を比較すれば、前者はやることが単純に増えているので、より大変だと言えるでしょう。また、どれだけ成果を出したいかは人それぞれですし、同様の事象に直面した際に大変だと捉えるかどうかも人それぞれです。
大学は文系学部だったのに、数学は大丈夫ですか？
今のところは大丈夫です。理解できていない箇所を明確にして、予め自習していたからです。ただ、ユーザーとして数学を使っているだけなので、数学自体を研究対象にするレベルのことはわかりません。
In Maude, a module can be imported as a submodule of another in three different modes: protecting, extending, including. This is done with the syntax declarations
protecting ⟨ModuleExpression⟩ .
extending ⟨ModuleExpression⟩ .
including ⟨ModuleExpression⟩ .which can be abbreviated, respectively, to
pr ⟨ModuleExpression⟩ .
ex ⟨ModuleExpression⟩ .
inc ⟨ModuleExpression⟩ .The different modes of importation can be understood as promises by the user, which would need to be proved by him/herself. Before explaining each difference, I clarify no junk and no confusion. No junk is that extra values should not be added. No confusion is that different values should not be made equal.
The different modes of importation is as follows:
protectingmode shows no junk and no confusion.extendingmode is to allow junk, but to rule out confusion.includingmode is to allow junk and/or confusion.
References
誰?
- 大学では経済学を専攻していたが、大学院では情報科学の分野で研究をしたい人
- 社会人
- プログラミング歴は約5年
受験の流れ
2020-04-19
オンラインでJapan Advanced Institute of Science and Technology(JAIST)の東京社会人コース説明会に参加した。
2020–04–22
関心のある研究室に受け入れが可能かを問うメールを送った。COVID-19のため、対面でなく、メールでやり取りすることになった。教授が発表した論文や担当している講義の資料のリンクが送られてきた。講義の単位を取得できそうとかなどについて確認するため課題を出していただくことになった。講義の資料はi217 Functional Programmingという講義のものだった。
2020–04–27
講義資料の指定された箇所を読み終わったという旨のメールを送った。1つ目の課題を出していただいた。
2020–04–28
1つ目の課題が完了した。課題をメールで送付した。
2020–04–29
2つ目の課題を出していただいた。
2020–05–02
2つ目の課題が完了した。課題をメールで送付した。短期間で2つの課題を完成させることができたので、該当の講義に関しては単位を取得できるレベルであるという評価を受けた。大学院や研究について改めて説明を受けた。どのような研究をしたいかと問われた。
2020–05–03
分散システムを形式検証したいという内容（実際には具体的な内容）のメールを送信した。そのメールに対する返信内容から自分のしたい研究を行うことができそうだとわかった。
出身大学に成績証明書と卒業証明書を発行する手続きをした。
2020–05–16
研究計画書の書き方を問うメールを送り、アドバイスをいただいた。
2020–05–22
研究計画書のドラフトを送付した。内容はよいという返信をいただいた。
2020–06
研究に関係する論文を読んでまとめたり、情報科学や数学の基礎的な内容を改めて勉強したりし始めた。職歴調書、エントリーシート、研究計画書を作成した。
2020–07–08
博士前期課程の社会人コース特別選抜に出願した。
2020–07–19
口頭試問で使用する資料を作成し始めた。
2020–08–06
受験票が届いた。
2020–08–21
有給を取得して、口頭試問でのプレゼンテーションの練習をひたすら行った。
2020–08–22
品川で口頭試問を受けた。会場に向かう最中にスマートフォンを無くして少し焦ったが、早めに出発していたので試験に間に合った。
2020–08–29
合格通知が届いた。
その他
- COVID-19のため出願期間と入試の日程が一度延期になった。
- 課題は関数型プログラミングと証明に関する内容だった。関数型プログラミング言語を用いて簡単な関数型プログラミング言語を実装した経験、数理論理学の基礎的な内容が書かれた本を読んだ経験、高校数学の知見などが役立ったと思う。
- 私が学部で文系科目専攻だったことが関係するのか(?)、面接では情報科学や数学に関する基礎的な質問があった。こちらも趣味で色々やっていたことが役立ったと思う。
Let R@ be {(@1),(@2),(r1),(r2)} such that
nil @ L2 = L2 (@1)
(E | L1) @ L2 = E | (L1 @ L2) (@2)
rev(nil) = nil (r1)
rev(E | L) = rev(L) @ (E | nil) (r2)Theorem1
rev(rev(L)) = LProof of Theorem1 by structural induction on L.
Let e be a fresh constant of Elt.E , l be a fresh constant of List.
I. Base case
What to show is rev(rev(nil)) = nil .
rev(rev(nil))
-> rev(nil) by(r1)
-> nil by(r1)II. Induction case
What to show is rev(rev(e | l)) = e | l.
assuming the induction hypothesisrev(rev(l) = l -- (1H)
…RustでBFSを練習するために、AtCoder AGC 033 A — Darker and Darker を解きました。
問題概要
「白」「黒」に塗られているH × Wのマスがあります。1 秒ごとに、各黒マスに対し、その上下左右に隣接したマスが存在するならば、そのマスを黒で塗りつぶします。全マスを黒で塗りつぶすのに何秒必要かを求めます。HとWには 1≤H,W≤1000 という制約があります。
解法
「各白マスに対して最も近い黒マスまでの距離」の中で最大の値を求めます。キューを使いたかったので、Rustでの標準ライブラリのstd::collections::VecDeque を使いました。std::collections::VecDeque にはpop_frontとpush_back があり、FIFOできます。
コードは以下のような感じで書きました。入力のマクロに関してはhttps://qiita.com/tanakh/items/0ba42c7ca36cd29d0ac8 を参照ください。
The aim of this blog post is to examine type-driven development with Rust. Type-driven development is an approach to develop robust and verified software, using a type system. The first section gives a brief overview of a type system.
What is a type system?
A type system is defined in the “Types and Programming Languages” as follows.
A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kinds of values they compute.
It allows early detection of some programing errors and helps us to build robust software.
What is a Type-driven development?
Dr. Edwin Brady used the term…
In Layered Architecture (e.g., Clean Architecture, or Hexagonal architecture), the key idea is to use the dependency inversion principle. This blog post provides the dependency inversion principle in Rust, skipping the details of Layered Architecture.
The sample in this blog post is a news app which gets news asynchronously. I will illustrate the dependency inversion principle with three layers: Use case, Gateway, and Port.
- Use case: app-specific business rules
- Gateway: adapter between a data format (e.g., JSON or ORM ) and a particular Domain object
- Port: abstraction depended by details (concrete implementations)
The diagram below shows dependency relationships.
Now lets’…
まず、Berkeley Packet FilterとBPF Compiler Collectionについて簡単に説明していきます。(以下ではそれぞれをBPFとBCCと略します。)
BPFとは
BPFは独自の命令セットを持つVMです。ユーザーランドのコードをカーネル内で安全に実行することができます。”The BSD Packet Filter: A New Architecture for User-Level Packet Captur”によると、1992年時点ではパケットフィルタリングのためのものだったようです。現在はセキュリティやトレーシングのためにも使用されています。
BCCとは
BPFでカーネルのトレーシングやフィルダリングなどを行うためのツール郡です。Python用のバインディングもあり、BPFを容易に扱うことができます。(実際にはC言語も書くことになりますが…)
インストール方法はこちらをご覧ください。
BCCを使用しない場合、BPFアセンブラを直接書いたり、ClangでC言語をBPFにコンパイルしたりすることでBPFを利用できます。(LLVM 3.7からLLVMのバックエンドにBPFが追加されています。)
トレース
BPFを利用すれば、下の図のようにカーネルの多くの部分にアタッチすることができます。
今回はすでに用意されているbpf/tools/tcptracer.py を利用して、TCPのコネクションをトレースしていきます。以下のようにPythonのファイルを実行します。(-t はタイムスタンプを表示するためのオプションです。)
$ sudo ./tcptracer.py -t
Tracing TCP established connections. Ctrl-C to end.
TIME(s) T PID COMM IP SADDR DADDR SPORT DPORT
0.000 C 7672 curl 4 127.0.0.1 127.0.0.1 59394 16004
0.006 X 7672 curl 4 127.0.0.1 127.0.0.1 59394 16004
0.006 X 7405 http-nio-16004- 6 [::] [0:ffff:7f00:1::] 0 65535
2.061 C 7682 curl 4 10.202.210.1 172.217.161.68 60036 443
2.177 X 7682 curl 4 10.202.210.1 172.217.161.68 60036 443
2.948 A 9565 java 4 127.0.0.1 127.0.0.1 42641 55980プロセスごとのTCPコネクションの状態を確認することができました。T列のC,A,Xはそれぞれはシステムコールのconnect(), accept(), close()を示しています。
まとめ
BPFはプログラマブルでかつ、Linuxのさまざまな箇所にアタッチすることができるため、カーネルの動作を柔軟にトレースできます。また、BPFを容易に扱う手段としてBCCがあります。
参考
Backends For Frontendsの概要
Backends For Frontends(以下BFF)とは、デスクトップやモバイルなどのクライアントごとに実装されたAPI Gatewayのことです。まずはAPI Gatewayについて説明していきます。
API Gateway
API Gatewayには以下のような役割があります。
- リクエストのルーティング
- APIコンポジション（バックエンドのAPIを複数呼び出して、その結果を集約する）
- プロトコルの変換
- 認証・認可
- リクエストの制限
- キャッシュ
- メトリックの収集
- リクエストログの出力
かなり多くの役割がありますが、これらすべてを１つのサーバで実装するという訳ではありません。認証・認可を共通基盤として切り出したり、リクエストのルーティングはクラウドサービスのロードバランサを使用したりすることがあると思います。API Gatewayはクライアントとバックエンドのマイクロサービスの間に存在するレイヤだと考えた方がよいでしょう。
API Gatewayが存在しない場合、問題がいくつか発生します。主な問題はパフォーマンスの低下でしょう。クライアントがAPIコンポジションを行う場合、大量のリクエストがインターネットを経由することになります。LANとモバイルネットワークでは100倍ほどの差があると考えられます。クライアントが並列にリクエストすればよいという考えもあるかもしれませんが、モダンなブラウザでもTCP同時接続数は６なので、HTTP/1.1での通信だと並列にリクエストしてもパフォーマンスの改善が難しいケースがあります。また、API Gatewayが存在しないのであれば、クライアントがバックエンドのサービスそれぞれの位置を知る必要があります。そのため、クライアントはService Discoveryし、その後で必要なデータ取得のためのリクエストをすることになります。
BFFの文脈だと、API Gatewayの役割の中で焦点が当たるのは主にAPIコンポジションだと思います。BFFが返すべきAPIコンポジションの結果はクライアントごとに大きく異なるからです。次はBFFがどのような考えに基づいて開発されたのかについて説明します。
BFFの歴史的背景
Microservices Patterns によると、BFFは当時SoundCloud社に所属していたPhil Calçadoたちによって考案されました。（BFFという命名はNick Fisherが行ったようです。）SoundCloud社ではデスクトップのWebとモバイルで１つAPI Gatewayを共有していました。API Gatewayがあるものの、デスクトップのWebとモバイルの両方で使える汎用的な作りだったこともあり、クライアントは大量にリクエストする必要があり、パフォーマンスの問題がありました。その問題を解決するため、クライアントごとに専用のAPI Gateway（BFF）を用意することを考案しました。BFFはクライアントが必要とするデータを返すため、クライアントはリクエスト数が減り、コードがシンプルになったようです。
SoundCloud社の事例の詳細は Phil Calçadoの”The Back-end for Front-end Pattern (BFF)”という記事を参照ください。
BFFのメリット
BFFを採用することでいくつかメリットがあります。上に書いたように、クライアントのリクエスト数を減らすことできます。また、それぞれのBFFを独立してスケールさせることもできます。例えば、デスクトップのWebとモバイルのアクセス数に大きな乖離がある場合でも、柔軟に対応できます。
BFFは対象のクライアントが必要とする形式のデータを返すため、クライアントでAPIコンポジションする必要はなくなります。そのため、クライアントのコードはシンプルになるでしょう。
BFFのデメリット
各クライアントが必要とするデータの中に共通している箇所がある場合、BFFごとに処理が重複してしまうというデメリットがあります。これはBFFというよりマイクロサービスを開発していると発生する事象だと思います。
APIコンポジションを実装する上の注意点
外部からのリクエストはBFFを経由することになります。バックエンドのマイクロサービスの処理がいくら速くてもBFFの処理が遅ければ、クライアントのユーザビリティを低下させます。そのため、BFFはマイクロサービスに対して非同期で並列にリクエストした方がよいです。
また、一部のレスポンスが長時間返ってこないケースや、リトライしても一部のリクエストが失敗するケースを考慮する必要があります。「マイクロサービスAがn秒以内にレスポンスを返さなかったら、マイクロサービスA以外のレスポンスを組み合わせてクライアントに返す」などの仕様を決めておくとよいでしょう。このようなケースを考慮すべきなのはBFFに限った話ではありませんが、BFFはよりクライアントに近いので考慮が漏れた際、ユーザに直接的な影響をもたらしてしまいます。
参考
Uzabase, Inc. のブログで書きました。
https://tech.uzabase.com/entry/2019/08/05/183629
