品川研究室のブログ

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

国際会議 SOSP 2019

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

※1 随時更新するかもしれません。
※2 PDFはまだ正式版のものではありません。
※3 ざっと眺めただけですので、概要も間違っているかもしれません。

目次


Session 2: It Must Be Secure

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

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)

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

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

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

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

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

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


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)

TBA

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

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)

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

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

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

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

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

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


Session 5: It Must Be Correct

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

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)

システムソフトウェアのためのシンボリック評価を用いた自動検証器を開発するためのフレームワーク 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) [PDF]

Tej Chajed (MIT CSAIL), Joseph Tassarotti (MIT CSAIL), Frans Kaashoek (MIT CSAIL), Nickolai Zeldovich (MIT CSAIL)

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

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

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

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)

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

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

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

Arseniy Zaostrovnykh (EPFL), Solal Pirelli (EPFL), Rishabh Iyer (EPFL), Matteo Rizzo (EPFL), Luis Pedrosa (EPFL), Katerina Argyraki (EPFL), George Candea (EPFL)

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


Session 7: The Revolution Will Be Distributed

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

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)

分散ファイルシステム 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)

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)

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)

TBA

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

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)

並行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)

TBA

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

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)

最先端のシステムと比べてもソフトウェアオーバーヘッドを大幅に削減した永続メモリ(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)

TBA

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

Xianzheng Dou (University of Michigan), Peter M. Chen (University of Michigan), Jason Flinn (University of Michigan)

TBA

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

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)

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

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