品川准教授のブログ

東京大学で准教授をしています。主に研究分野（OSや仮想化などのシステムソフトウェア）に関連したことを気まぐれに書きます。

国際会議 SOSP 2019

2019年10月28日～30日にカナダで開催されたシステムソフトウェア系の最高峰の国際会議 The 27th ACM Symposium on Operating Systems Principles (SOSP 2019) で発表された論文の中で個人的に興味のあるものをリストアップしています。

※1 随時更新していますが、スローペースです。
※2 興味の程度によって分量に差があります。
※3 ざっと眺めただけですので、内容も間違っているかもしれません。

目次

概要

  • 参加者580名くらい
  • 投稿数276本、採択数38本、採択率14%
  • 査読数: 3 (1st round) + 2 or 3 (2nd round) + α
  • 査読プロセス: 投稿276本 -> (online discussion ) -> 81本 -> (1.5-day in-person PC meeting) -> 38本

Session 1: Machines, Learning

省略

Session 2: It Must Be Secure

Teechain: 非同期ブロックチェーンアクセスによる安全な決済ネットワーク
(Teechain: A Secure Payment Network with Asynchronous Blockchain Access)

Joshua Lind (Imperial College London), Oded Naor (Technion), Ittay Eyal (Technion), Florian Kelbert (Imperial College London), Emin Gun Sirer (Cornell University), Peter Pietzuch (Imperial College London) https://doi.org/10.1145/3341301.3359627doi.org https://arxiv.org/pdf/1707.05454.pdf

ビットコインなどのブロックチェーンで、Trusted Execution Environment（TEE）を使ってオフチェーンのトランザクションを非同期かつ安全に実行できるレイヤ2の決済ネットワーク Teechain を提案している。

ベースとなるブロックチェーンへのアクセスを意図的に遅延させることで資金を盗む攻撃を防ぐために、Intel SGX などの TEE で動作する「金庫」を作り、一時的に担保資金を確保しておくことで、2者間で非同期かつ安全に取引ができる。

TEE だけでは foreshadow などによって攻撃される可能性があるので、複数人の「委員会」を構成して矛盾が生じたら元の blockchain にフォールバックする。

Notary: 安全なトランザクション承認のためのデバイス
(Notary: A Device for Secure Transaction Approval)

Anish Athalye (MIT CSAIL), Adam Belay (MIT CSAIL), Frans Kaashoek (MIT CSAIL), Robert Morris (MIT CSAIL), Nickolai Zeldovich (MIT CSAIL)

https://doi.org/10.1145/3341301.3359661doi.org https://pdos.csail.mit.edu/papers/notary:sosp19.pdf

ビットコインの決済などユーザの重要な承認事項を安全に伝えるために、小さなディスプレイとボタンの付いた専用 USB スティックを使って、複数の承認エージェントを安全に動作させるリセットベースの切り替え手法（reset-based switching）を提案している。

エージェントコードとカーネルを物理的に分離した SoC 上で実行したり、ハードウェアの RTL レベルので設計及びソフトウェアの検証などをおこなうとともに、エージェント切替時にハードウェアの完全リセットをおこなってCPUやRAMなどが検証された初期状態になるようにすることで、カーネルのバグやサイドチャネル攻撃などによるエージェント間の漏洩が起きないことを保証している。ARM と RISC-V に基づく実機を実際に作って有効性を検証している。

エージェントはオフラインでインストールすることを想定→正しいアプリだけがインストールされる。 TCBは4000行→formal verificationも可能だろう。

Session 3: Systems: Still Buggy

CrashTuner: メタ情報解析によるクラウドシステムのクラッシュ回復バグの検出
(CrashTuner: Detecting Crash Recovery Bugs in Cloud Systems via Meta-info Analysis)

Jie Lu (The Institute of Computing Technology of the Chinese Academy of Sciences), Chen Liu (The Institute of Computing Technology of the Chinese Academy of Sciences), Lian Li (The Institute of Computing Technology of the Chinese Academy of Sciences), Xiaobing Feng (The Institute of Computing Technology of the Chinese Academy of Sciences), Feng Tan (Alibaba Group), Jun Yang (Alibaba Group), Liang You (Alibaba Group)

https://doi.org/10.1145/3341301.3359645doi.org

TBA

変曲点仮説：障害の根本原因を突き止めるための原理的デバッグ手法
(The Inflection Point Hypothesis: A Principled Debugging Approach for Locating the Root Cause of a Failure)

Yongle Zhang (University of Toronto), Kirk Rodrigues (University of Toronto), Yu Luo (University of Toronto), Michael Stumm (University of Toronto), Ding Yuan (University of Toronto)

https://doi.org/10.1145/3341301.3359650doi.org

拡張可能ファジングフレームワークによるファイルシステムのセマンティックバグの発見
(Finding Semantic Bugs in File Systems with an Extensible Fuzzing Framework)

Seulbae Kim (Georgia Institute of Technology), Meng Xu (Georgia Institute of Technology), Sanidhya Kashyap (Georgia Institute of Technology), Jungyeon Yoon (Georgia Institute of Technology), Wen Xu (Georgia Institute of Technology), Taesoo Kim (Georgia Institute of Technology)

https://doi.org/10.1145/3341301.3359662doi.org

https://gts3.org/~sanidhya/pubs/2019/hydra.pdf

原理的にはファイルシステムの任意の種類のバグを発見できる拡張可能 fuzzing フレームワーク HYDRA を提案している。

HYDRA は fuzzing のための構成要素として、入力ミューテータ、フィードバックエンジン、libOSベースの実行機構、テストケースを最小化したバグ再生成器などを提供している。これにより、開発者がバグを発見するためのコアロジックの作成に集中できる。実際に、クラッシュ不整合、POSIX違反、ロジックアサーション違反、メモリエラーの4つのバグを発見するチェッカーを作って有効性を確認した。その結果、Crash Hoare logic を使ってそのようなバグは存在しないことを証明したとされていた FSCQ においてさえ1個のバグを発見したほか、4個のPOSIX違反を含むLinuxファイルシステムの新しいバグを91個発見した。

ファジングでメモリエラーだけでなく、セマンティックバグも見つけられるのがIEEE S&P論文との違い。 セマンティックはクラッシュしないので従来のファジングで見つけずらい。 チェッカーでチェックして、フィードバックする。

効率的でスケーラブルなスレッド安全性違反の検証 --- テスト中に数千個の並行バグを発見
(Efficient and Scalable Thread-Safety Violation Detection --- Finding thousands of concurrency bugs during testing)

Guangpu Li (University of Chicago), Shan Lu (University of Chicago), Madanlal Musuvathi (Microsoft Research), Suman Nath (Microsoft Research), Rohan Padhye (Berkeley)

https://doi.org/10.1145/3341301.3359638doi.org

https://www.microsoft.com/en-us/research/uploads/prod/2019/09/sosp19-final193.pdf

(Best Paper Award)

マイクロソフトで実際に使われている並行バグ発見器 TSVD を提案している。

従来手法のようにランダムに遅延を挿入するなどコストの高い同期解析を採用するのではなく、スレッドセーフでないメソッドの呼び出し行動を同期を使わずに軽量に監視して、バグが疑われるポイントを動的に特定する。その後、対応する遅延を挿入してプログラムをスレッドセーフでない動作に誘導し、その能力を学習し、次のテスト時にもその学習結果を活用する。実際にマイクロソフトの数千のプロジェクトで1000以上のスレッドセーフ違反を発見した。

Session 4: Keeping Things Private

省略

Session 5: It Must Be Correct

Serval によるシステムコードの自動検証のためのシンボリック評価の拡張
(Scaling Symbolic Evaluation for Automated Verification of Systems Code with Serval)

Luke Nelson (University of Washington), James Bornholt (University of Washington), Ronghui Gu (Columbia University), Andrew Baumann (Microsoft Research), Emina Torlak (University of Washington), Xi Wang (University of Washington) https://doi.org/10.1145/3341301.3359641doi.org https://www.cs.utexas.edu/~bornholt/papers/serval-sosp19.pdf (Best Paper Award)

システムソフトウェアのためのシンボリック評価を用いた自動検証器を開発するためのフレームワーク Serval を提案している。

Serval では、まず対象となるCPUの命令セットのインタプリタを Rosette というシンボリック実行をするための専用言語で記述し、それを検証器へと格上げ（"lift"）する。実際に RISC-V や x86-32、LLVM、BPF の検証器を生成した。それらはシンプルで簡単に理解できるうえ、Rosette の特徴も利用できる。さらに検証器間での再利用や相互運用も容易になる。パス爆発の問題に対処するために、symbolic profiling の技術を用いてボトルネックとなる箇所を特定し、symbolic optimizations によってドメイン固有の知識を使ってシンボリック実行の性能を向上させる。 既存のシステムにどれだけ適用可能か検証するために、Coq で検証された x86 上で動作するセキュリティモニタ CertiKOS や、Dafny で検証された ARM の TrustZone を使ったセキュリティモニタ Komodo に対して適用して、それらが Serval の対象となりうることを確認した。

Perennial による並行でクラッシュセーフなシステムの検証
(Verifying Concurrent, Crash-safe Systems with Perennial)

Tej Chajed (MIT CSAIL), Joseph Tassarotti (MIT CSAIL), Frans Kaashoek (MIT CSAIL), Nickolai Zeldovich (MIT CSAIL) https://doi.org/10.1145/3341301.3359632doi.org https://people.csail.mit.edu/nickolai/papers/chajed-perennial.pdf

並行かつクラッシュセーフなシステムを検証するフレームワーク Perennial を提案している。

並行実行するシステムを検証する既存のフレームワーク Iris をベースにして、回復リース、回復補助、バージョン化メモリの3つの技術を導入して拡張した。開発と導入を容易にするために、Go言語のサブセット Goose を作って、Go スレッドやデータ構造、POSIXファイルシステムのAPI を Perennial のモデルに変換できるようにした。実際に、Perennial と Goose を使って、クラッシュセーフで並行実行可能なメールサーバを実装した。

AtomFS ファイルシステムを検証するためのヘルパを用いた並行関係論理の使用
(Using Concurrent Relational Logic with Helpers for Verifying the AtomFS File System)

Mo Zou (Shanghai Jiao Tong University), Haoran Ding (Shanghai Jiao Tong University), Dong Du (Shanghai Jiao Tong University), Ming Fu (Huawei Technologies Co. Ltd), Ronghui Gu (Columbia University), Haibo Chen (Shanghai Jiao Tong University) https://doi.org/10.1145/3341301.3359644doi.org https://www.cs.columbia.edu/~rgu/publications/sosp19-zou.pdf

アプリケーションに線形化されたインターフェースを提供する、形式検証され細粒度で並行な初めてのファイルシステムAtomFS を提案している。

著者らの観測によると、線形性の証明に際して最も難しいのはパス間依存性である。パス間依存性は、rename のようなたった一つの操作でも他の操作のパス一貫性を損なうものであり、扱いが非常に難しい。この論文では、ヘルパ付き並行関係論理（Concurrent Relational Logic with Helpers: CRL-H）という検証された並行ファイルシステムを構築するためのフレームワークを提案している。

検証の専門知識を使わないソフトウェアネットワーク機能の検証
(Verifying Software Network Functions with No Verification Expertise)

Arseniy Zaostrovnykh (EPFL), Solal Pirelli (EPFL), Rishabh Iyer (EPFL), Matteo Rizzo (EPFL), Luis Pedrosa (EPFL), Katerina Argyraki (EPFL), George Candea (EPFL) https://doi.org/10.1145/3341301.3359647doi.org https://dslab.epfl.ch/pubs/vigor.pdf

性能と生産性を維持しつつ、正しいことが保証されているソフトウェアネットワークミドルボックスを構築・実行するためのソフトウェアスタックおよびツールチェーンである Vigor を提案している。

Session 7: The Revolution Will Be Distributed

分散ストレージのバックエンドとしてのファイルシステムの不適合: 10年に渡るCephの進化からのレッスン
(File Systems Unfit as Distributed Storage Backends: Lessons from 10 Years of Ceph Evolution)

Abutalib Aghayev (Carnegie Mellon University), Sage Weil (Red Hat Inc.), Michael Kuchnik (Carnegie Mellon University), Mark Nelson (Red Hat Inc.), Gregory R. Ganger (Carnegie Mellon University), George Amvrosiadis (Carnegie Mellon University) https://doi.org/10.1145/3341301.3359656doi.org https://www.pdl.cmu.edu/PDL-FTP/Storage/ceph-exp-sosp19.pdf

分散ファイルシステム Ceph の経験から新しく作り直したバックエンドストレージ BlueStore を提案している。

従来のファイルシステムの問題点としては、(1) ゼロオーバーヘッドのトランザクション機構を作ることが困難、(2) ローカルレベルでのメタデータの性能が分散レベルでの性能にも大きく影響を与える点、(3) 新しいストレージハードウェアをサポートするのが苦痛なほど遅い点、がある。BluStore はユーザ空間で動作してI/Oスタックを完全にコントロールすることで、空間効率の良いメタデータやデータチェックサム、イレイジャーコード化されたデータの高速な更新、インライン圧縮、性能のばらつきの低減、ローカルファイルシステムの性能上の欠点の回避などを実現している。

Session 8: Net Work

Snap: ホストネットワーキングへのマイクロカーネルアプローチ
(Snap: a Microkernel Approach to Host Networking)

Michael Marty (Google), Marc de Kruijf (Google), Jacob Adriaens (Google), Christopher Alfeld (Google), Sean Bauer (Google), Carlo Contavalli (Google), Michael Dalton (Google), Nandita Dukkipati (Google), William C. Evans (Google), Steve Gribble (Google), Nicholas Kidd (Google), Roman Kokonov (Google), Gautam Kumar (Google), Carl Mauer (Google), Emily Musick (Google), Lena Olson (Google), Erik Rubow (Google), Michael Ryan (Google), Kevin Springborn (Google), Paul Turner (Google), Valas Valancius (Google), Xi Wang (Google), Amin Vahdat (Google) https://doi.org/10.1145/3341301.3359657doi.org

TBA

Taiji: エッジにおける大規模インターネットサービスのためのグローバルユーザトラフィックの管理
(Taiji: Managing Global User Traffic for Large-Scale Internet Services at the Edge)

David Chou (Facebook), Tianyin Xu (UIUC), Kaushik Veeraraghavan (Facebook), Andrew Newell (Facebook), Sonia Margulis (Facebook), Lin Xiao (Facebook), Pol Mauri Ruiz (Facebook), Justin Meza (Facebook), Kiryong Ha (Facebook), Shruti Padmanabha (Facebook), Kevin Cole (Facebook), Dmitri Perelman (Facebook) https://doi.org/10.1145/3341301.3359655doi.org

TBA

Session 9: The Persistence Of Memory

KVell: 高速な永続キーバリューストアの設計と実装
(KVell: the Design and Implementation of a Fast Persistent Key-Value Store)

Baptiste Lepers (University of Sydney), Oana Balmau (University of Sydney), Karan Gupta (Nutanix Inc.), Willy Zwaenepoel (University of Sydney and EPFL) https://doi.org/10.1145/3341301.3359628doi.org

TBA

RECIPE: 並行DRAMインデックスの永続メモリインデックスへの変換
(RECIPE: Converting Concurrent DRAM Indexes to Persistent-Memory Indexes)

Se Kwon Lee (University of Texas at Austin), Jayashree Mohan (University of Texas at Austin), Sanidhya Kashyap (Georgia Tech), Taesoo Kim (Georgia Tech), Vijay Chidambaram (University of Texas at Austin and VMware Research) https://doi.org/10.1145/3341301.3359635doi.org

並行DRAMインデックスを永続メモリのためのクラッシュ整合性のあるインデックスに変換する原理的なアプローチである RECIPE を提案している。

ユーザ空間NVMファイルシステム ZoFS における性能と保護
(Performance and Protection in the ZoFS User-space NVM File System)

Mingkai Dong (Shanghai Jiao Tong University), Heng Bu (Shanghai Jiao Tong University), Jifei Yi (Shanghai Jiao Tong University), Benchao Dong (Shanghai Jiao Tong University), Haibo Chen (Shanghai Jiao Tong University)
https://dl.acm.org/authorize?N695045
https://www.cs.utexas.edu/~vijay/papers/sosp19-recipe.pdf

ユーザ空間からでも安全に管理できる不揮発メモリ(NVM)上のファイルシステム ZoFS を提案している。

NVM上のファイルシステムをユーザレベルで管理すると、カーネルアクセスのオーバーヘッドを削減できるため高速化出来るが、従来のNVM向けファイルシステムでは、ファイルシステムを保護するためにメタデータの管理はカーネルレベルで行わなければいけなかった。

ZoFSでは、ファイルのパーミッションはめったに変わらないことに着目して、ファイルのパーミッションが同じファイルをまとめて置いておくNVMページの集まりである coffer という新しい抽象化を導入し、coffer 単位でプロセスに割り当てることでユーザ空間からメタデータの操作をおこなえるようにする。coffer のプロセスへの割当自体はカーネルが管理することでセキュリティは担保しつつ、一旦割り当てたらメタデータを含むファイルシステムの操作をユーザレベルで完結できるようにする。プロセスのバグによってファイルシステムが破損する stray write が発生する可能性を減らすために、Intel MPK を用いてメタデータを変更する瞬間だけページの書き込み権限を与えることで、通常動作時にメタデータが破壊される可能性を減らす。

実験の結果、ZoFS は LevelDB のレイテンシを最大82%削減し、SQLite のスループットを最大31%向上させることが出来た。

SplitFS: 永続メモリのためのファイルシステムにおけるソフトウェアオーバーヘッドの削減
(SplitFS: Reducing Software Overhead in File Systems for Persistent Memory)

Rohan Kadekodi (University of Texas at Austin), Se Kwon Lee (University of Texas at Austin), Sanidhya Kashyap (Georgia Tech), Taesoo Kim (Georgia Tech), Aasheesh Kolli (Penn State University and VMware Research), Vijay Chidambaram (University of Texas at Austin and VMware Research) https://arxiv.org/pdf/1909.10123.pdf

最先端のシステムと比べてもソフトウェアオーバーヘッドを大幅に削減した永続メモリ（Persistent Memory: PM）のためのファイルシステム SplitFS を提案している。

SplitFS はユーザ空間のライブラリファイルシステムと既存のカーネルのPMファイルシステムの間の責任をうまく分割している。ユーザ空間のファイルシステムは、データ操作を処理するために、POSIXファイルシステムを横取りし、ファイルをメモリマップし、読み込みや更新をプロセッサのロード・ストア命令で処理する。メタデータ操作はカーネルのPMファイルシステム（ext4 DAX）でおこなう。SplitFS は relink という、ファイルのある領域を別のファイルの領域へ物理的なデータ移動なしに行う機能を追加して、ファイルの追加やアトミックなデータ操作をサポートする。さらに、SplitFS は3つの一貫性モデル（POSIX, sync, strict）を提供する。SplitFS は NOVA と比べてソフトウェアのオーバーヘッドを最大4倍、ext4 DAX と比べて17倍削減できた。LevelDB で YCSB を走らせたベンチマークなどで、アプリケーションの性能が ext4 DAX や NOVA と比べて最大2倍向上した。

Session 11: The Final Session

Linuxのコア操作の性能進化の分析
(An Analysis of Performance Evolution of Linux's Core Operations)

Xiang (Jenny) Ren (The University of Toronto), Kirk Rodrigues (The University of Toronto), Luyuan Chen (The University of Toronto), Camilo Vega (The University of Toronto), Michael Stumm (The University of Toronto), Ding Yuan (The University of Toronto) https://doi.org/10.1145/3341301.3359640doi.org

Linux カーネルは過去7年で基本性能がどんどん遅くなって。select() は2年前と比べて最大100%の性能低下。要因はセキュリティ強化、新機能、設定ミス。

セキュリティ対策による性能低下は、Meltdown 対策の KPTI で recv() が最大63%、Spectre v2 対策の Retpoline でpoll() が最大89%、SLAB freelist dandomization で epoll() が最大41%、usercopy の強化で select() が最大18%。

新機能による性能低下は、fault around（page fault 発生時に周辺ページもついでにマップする）で page fault が最大54%、cgroup で munmap が最大81%、transparent huge table デフォルト無効化で read() が最大83%、userspace page fault handling でfork()が4%。

設定ミスによる性能低下は、forced context tracking（reduced scheduling-clock ticks 開発のためのデバック機能）無効化し忘れで最大100%、TLB layout change で munmap() が最大50%。CPU idle power-state support はHaswell上の select() で31%の性能向上があるが、LTS に backport されていない。

上記の11個の要因中8つはカーネルの reconfiguration で、残り3つは簡単なパッチで回避可能。その結果、Redis, Apache, Nginx benchmark の性能がそれぞれ 56%, 33%, 34% まで改善した。

パッチ1: Spectre 対策の retpoline は indirect jump を予測不能にするので、indirect jump をよく使う select や poll が著しく性能低下する。対策は、セキュリティに問題のない if文＋ direct jump への置き換え。

パッチ2: KPTI は TLB flush のコストが重い。PCID を使って最適化可能だが、それでも切り替えに 400-500 サイクルはかかる。PCID は CR3 に格納されており、CR3 の書き込み自体 200 サイクルかかる。

ShortCut: ほとんど決定的なコード領域の高速化
(ShortCut: Accelerating Mostly-Deterministic Code Regions)

Xianzheng Dou (University of Michigan), Peter M. Chen (University of Michigan), Jason Flinn (University of Michigan) https://doi.org/10.1145/3341301.3359659doi.org

TBA

Shuffling によるスケーラブルで実用的なロッキング
(Scalable and Practical Locking with Shuffling)

Sanidhya Kashyap (Georgia Tech), Irina Calciu (VMware Research Group), Xiaohe Cheng (Hong Kong University of Science and Technology), Changwoo Min (Virginia Tech), Taesoo Kim (Georgia Institute of Technology) https://doi.org/10.1145/3341301.3359629doi.org https://gts3.org/~sanidhya/pubs/2019/shfllock.pdf

この論文では、ロックアルゴリズムの性能に影響を与える4つの支配的要素を特定し、ロックのクリティカルパスを遅くすることなく、それらの要素を動的に調節する手法 shuffling を提案している。

ロックは高性能マルチコアシステムソフトウェアにおける重要な構成要素だが、環境が異なるとうまく性能が出ない。例えば、spinlock を NUMA で使うとキャッシュラインが頻繁に行き来することになり、一方NUMA-awareなロックはシングルスレッドの性能が出ない。この論文では、ロックの性能を与える4つの要素として、1) 異なるキャッシュ間のキャッシュライン移動、2) スレッド競合のレベル、3) コアのオーバーサブスクリプション、4) メモリフットプリントを挙げている。これに対して、shuffling ではロックの取得／開放のフェーズをロックの順番のポリシーから切り離し、クリティカルパスではない所でポリシーに基づくロック待ちのスレッドの順番入れ替えをおこなう。