読者です 読者をやめる 読者になる 読者になる

たまにゃんのメモ帳

情報系関連のメモ書きを主に載せていきます。あわよくば他の人の参考になれば...

Boosting Multi-Core Reachability Performance with Shared Hash Tables (2010)

URL : http://fmcad10.iaik.tugraz.at/Papers/papers/12Session11/033Laarman.pdf

  1. Abstract
    • この論文はモデル検査アルゴリズムとその他検証手法において重要なキーコンポーネントであるマルチコアReachabiliyのためのデータ構造について焦点を当てる。
    • 我々が提案する共有ストレージはロックレスなハッシュテーブルで実装がベースになっておりスケーラビリティもある。
    • モダンCPUのキャッシュアーキテクチャの考慮して実装された。
  2. Introduction
    • この論文ではSPINやDiVinEのようなマルチコアモデル検査器が共有の状態のストレージとしてコンカレントハッシュテーブルを扱うことで性能を改善させる。
    • Contribution
      • 効率的なコンカレント状態ストレージのデータ構造の提案をする。
      • これによって多くの探索アルゴリズムに対しReachabiliyを持ったスケール可能な並列アルゴリズムの実装を可能にする。
    • Overview
      • Section 2 : Reachability, Load Balancing, Hashing, Parallel Algorithms, Multi-Core Systems のバックグラウンドについて述べる
      • Section 3 : 共有の状態ストレージとして設計されたロックレスなハッシュテーブルについて述べる。しかし、高速な並列アルゴリズムがその上で動くという前提条件の元で評価を行う。
      • Section 4 : DiVinE や SPIN において評価を行う。例題はBEEM databaseを用いる。
  3. Preliminaries
  4. A Lockless Hash Table
    • ハッシュテーブルの要件
      • find-or-put
        • 削除とかは考えなくてよく状態を見つけるか挿入するかの2つだけを考えれば良い
        • ただマルチスレッド環境において同時のアクセスに対して保証しなくてはならない
        • find-or-putという特徴を利用することでアルゴリズムを単純化して、メモリへの負担を下げてそれぞれのコアのキャッシュライン共有を避ける
      • 基本的にはそれぞれの状態にポインタを使うことを避ける
        • 64bitマシンにおいては無視できない量になる
      • find-or-putの時間的効率性は並列実行のプロセス数によってスケールしなくてはならない
    • Hash Table Design
      • Open addressing
      • Walking-the-line
        • Double Hashingによってキャッシュライン上に Linear Probingを提供する。
      • Separated data
        • 索引づけされたデータの配列
      • Hash memoization
      • Lockless
      • Compare-and-swap
    • Hash Table Operations
    • -
  5. Experiments