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:

• protecting mode shows no junk and no confusion.
• extending mode is to allow junk, but to rule out confusion.
• including mode is to allow junk and/or confusion.

References

• http://maude.lcc.uma.es/manual271/maude-manualch6.html

誰?

• 大学では経済学を専攻していたが、大学院では情報科学の分野で研究をしたい人
• 社会人
• プログラミング歴は約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)) = L

Proof 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 hypothesis
rev(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があります。

参考

• https://www.tcpdump.org/papers/bpf-usenix93.pdf
• Linux Observability with BPF
• Berkeley Packet Filter（BPF）入門
• https://github.com/iovisor/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はよりクライアントに近いので考慮が漏れた際、ユーザに直接的な影響をもたらしてしまいます。

参考

• Microservices Patterns
• https://philcalcado.com/2015/09/18/the_back_end_for_front_end_pattern_bff.html
• https://microservices.io/patterns/apigateway.html