Skip to content
View yuezato's full-sized avatar
26 followers · 0 following

Achievements

Achievement: Arctic Code Vault ContributorAchievement: Pull Sharkx2

Achievements

Achievement: Arctic Code Vault ContributorAchievement: Pull Sharkx2

Organizations

@frugalos

Block or report yuezato

Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse
yuezato/README.md

経歴

学会活動 / 教育等

スキル

計算機科学の理論

  • プログラム理論 / Theory of Program(ming)
  • オートマトン理論、形式言語理論 / Automata Theory, Formal Language Theory
  • ソフトウェア検証、プログラム検証、それらのための論理 / Software Verification, Program Verification, Computational Logic
  • 定理証明系、定理証明支援系 / Proof Assistant(Coq, Agda2, Isabelle/HOL, etc.)
  • 分散計算、分散システムを支える理論 / Theory & Methods for Distributed Computing and Systems.

プログラムに関する理論を駆使し、様々な分野の未解決問題を解いたり、既存手法を拡張・高速化することに興味があります。

そうした理論的解析を行う道具として、オートマトン理論や計算論理、及びプログラム理論に精通しています。
特に、博士論文はオートマトン理論に関するものです。

それぞれのトピックに対応する論文も筆頭著者で出版しています。"主な論文"のセクションをご覧ください。

プログラミング

強み

生きていると、何かが上手く行かないことを気づいていながらも、 それが誰かによって解決されるまでは、問題があったと自覚できていなかった・問題の切り口を認識できていなかったと気づくことがあります。 コロンブスの卵や、 Peers's Law: 問題の解決は問題の性質を変える("The solution to a problem changes the nature of the problem")は、そのような事柄を端的に表しています。

こうした、問題として設定さえできれば解けたかもしれないのに、そもそも問題設定すらできないということは、 上手く行かない状況を表現・形式化・記述するための道具が手許にない時に良くおこります。

上里は、何かがうまくいかない状況ならなんでも問題化できる、という程の能力はありませんが、 しかし一方で「計算機上で」何かがうまくいかない時に、それを問題として具体化する能力に長けています。

これはプログラムに関する基礎理論全般を深いレベルで修めていることと、 そして計算機に関わる問題は、多かれ少なかれ、プログラム理論の道具やプログラムに関する論理によって記述できることから可能になります。

また、深くプログラム理論に通じていると、「どこまでを」プログラムの理論に担当させれば良いかよく分かります。 これは問題を新しいレベルで解決することにも繋がります。 例えば、問題を記述できた結果、何かを最適化できれば良い類の問題だと分かったとします。 この時に問題の切り分けや分解の結果として、プログラムの理論で一般的に解決出来る部分を最大化し、そうでない部分を最小化できれば、 最小化できた「そうでない部分」が、最適化問題の正体たる部分だと同定できたことになります。

取り出された問題はもはやプログラムの問題ではなく、コンピュータサイエンス的な最適化問題や、 工学的な最適化問題、果ては数学の問題となることが多いです。 現実の問題に対して、こうした発掘されたコアとなる問題は容易ではないことが多いですが、 これは一方でコア部分を取り出せす漠然としたままでは解決が望めないことを意味します。

また、CS・工学・数学的な最適化問題になったあとに、 これをその領域を専門とする人間と協力し解決するためのコミュニケーション能力や、 そこでのやり取りを自分に取り込み他分野についての理解を深める能力も長けていると自負しています。

現在の興味 1

大規模計算・システムを実現するための技術・検証

Keywords

  • Erasure coding, Optimized File system for specific devices
  • Distributed Algorithms
  • Space-efficient Data structures

ドワンゴで分散オブジェクトストレージ Frugalos を実現するうちに、 大規模システムや分散計算という領域に興味が出てきました。

興味があるだけでなく、2021年度は、単著論文 https://dl.acm.org/doi/abs/10.1145/3458817.3476204 を書きました。

この論文では、大規模システムで不可欠な問題（Erasure codingの高速化）を、プログラムの理論を用いた理論的解析をもとに大幅に最適化しました。 また、理論をもとにして、極めて高速---2022年1月時点で世界最速---なErasure codingの試験的ライブラリを実現しています。

この論文は、SCという、HPC分野のトップカンファレンスに採録されています: https://sc21.supercomputing.org/

本論文に関して、現時点（2022/01)で二件の招待講演を国内で行っています:

関連リポジトリ

  • https://github.com/yuezato/xorslp_ec
    • 概要: SC'21の論文用リポジトリ。Erasure codingの高速実装を実現。現時点ではIntelのライブラリ https://github.com/intel/isa-l より高速。
    • 使用言語: Rust
    • やっていること: 有限体の実装, 文法圧縮アルゴリズムの実装, プログラム融合変換, Pebble Gameのヒューリスティック実装, SIMD最適化
  • https://github.com/yuezato/minfs
    • 概要: 高級なPersistent KVSをサポートするための、余計なことをしないファイルシステム
      • 余計なことをしない、というのは例えばLinux Kernelのbioレイヤなどで起こるバッファのフラグメント化を最大限回避し、回避できない場合も巨大なパケット（ATAPIやSATA等のインタフェイスでのmaxとなるように）へ分割し、パケット数を減らす。これはレイテンシを上げるためにも重要。
    • 使用言語: C
    • サブリポジトリ: https://github.com/yuezato/fsprof
      • eBPFを用いてファイルシステムをデバッグするためのスクリプト群
    • モチベーション

現在の興味 2

機械学習で使われる統計や幾何的手法を用いた新たなプログラム解析

プログラムの解析や検証に学習（≠ 深層学習）を使う方法はかなり浸透してきていると言えます: https://www.usenix.org/conference/osdi21/presentation/yao

こうしたひとまず適用してみるの段階を超え、「なぜうまく行くのか・どういった構造がプログラムに隠されていたのか」を機械学習の数学的基盤をもとに明らかにする、次のステップに興味があります。

現在の興味 3

プログラムの安全性に立脚するソフトウェアやシステムの安全性検証

あいまいなcriteriaに訴える安全性検証を排し、安全か否かをエンジニアリングや計算の問題として形式化し、数理的に取り組むことに興味があります。

他の人の仕事ですが、やりたいことの一例です

主な論文

  • Accelerating XOR-based erasure coding using program optimization techniques
    • Yuya Uezato
    • SC'21: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis
    • ACM, arxiv
  • Configuration Reachability Analysis of Synchronized Recursive Timed Automata
  • Monoid-Based Approach to the Inclusion Problem on Superdeterministic Pushdown Automata
    • Yuya Uezato, Yasuhiko Minamide
    • DLT 2016: Developments in Language Theory
    • Springer
  • Synchronized Recursive Timed Automata
    • Yuya Uezato, Yasuniko Minamide
    • LPAR 2015: Logic for Programming, Artificial Intelligence, and Reasoning
    • Springer
  • Pushdown Systems with Stack Manipulation
    • Yuya Uezato, Yasuhiko Minamide
    • ATVA 2013: Automated Technology for Verification and Analysis
    • Springer
  • Implementing Monadic Total Parser Combinator on Coq

主な受賞歴 / Awards

Popular repositories Loading

  1. xorslp_ec xorslp_ec Public

    Rust 9 2

  2. cannyls cannyls Public

    Forked from frugalos/cannyls

    An embedded persistent key-value storage for Rust that optimized for random-access workload and huge-capacity HDD

    Rust 1 1

  3. frugalos frugalos Public

    Forked from frugalos/frugalos

    Frugal Object Storage

    Rust 1

  4. liberasurecode liberasurecode Public

    Forked from frugalos/liberasurecode

    A Rust wrapper for `openstack/liberasurecode`

    Rust 1

  5. minfs minfs Public

    C 1

  6. yuezato yuezato Public

    WhoAmI

    1