SMP/マルチコアに対応した 型付きアセンブリ言語 前田俊行 東京大学大学院情報理工学系研究科

型付きアセンブリ言語 (TAL) とは 「強く型付けされた」アセンブリ言語 型検査により以下の安全性を保証できる メモリ安全性 制御フロー安全性 型が付いていること以外は 普通のアセンブリ言語と変わらない Type-preserving compilation の分野で研究がはじまった[Morrisett et al. 1999]

TAL のフレームワークの概観: バイナリの生成 型情報 TAL で書かれた ソース プログラム TAL の アセンブラ バイナリ プログラム

TAL のフレームワークの概観: バイナリの検査 安全 型情報 TAL の 型検査器 バイナリ プログラム 危険

TALK: TAL for Kernel OS カーネルを書くために 型システムを強化した TAL メモリ管理機構やスレッド管理機構 そのものを記述可能 従来の TAL では不可能だった 外部のメモリ管理機構 (= GC) に依存していたため SMP/マルチコア環境や割込みにも対応している [前田,米澤 DSW2007,DSW2008]

TALK の特徴 Strong update を実現している

メモリ管理と strong update の関係 メモリの再利用の例 int* の領域を int として再利用する int* reuse(int** o) { int* p = (int*)o; *p = 42; return p; }

メモリ管理と strong update の関係 メモリの再利用の例 int* の領域を int として再利用する 型 int** int* reuse(int** o) { int* p = (int*)o; *p = 42; return p; } 型 int* このメモリを 再利用する 型 int

メモリ管理と strong update の関係 メモリの再利用の例 int* の領域を int として再利用する 型 int* int* reuse(int** o) { int* p = (int*)o; *p = 42; return p; } 型 42 int Strong update 型 int

メモリ管理と strong update の関係 メモリの再利用の例 int* の領域を int として再利用する 型 int* int* reuse(int** o) { int* p = (int*)o; *p = 42; return p; } 型 42 int Strong update 型 ポインタ o が他の場所で 使われていないことは 型システムで保証する int

SMP/マルチコア環境における メモリ管理と strong update の関係 難しいところ 複数スレッド間での ポインタのエイリアス関係を追跡しなければだめ 複数スレッドに関する 情報が型に含まれていない int* reuse(int** o) { int* p = (int*)o; *p = 42; return p; } 危険!!! : 他のスレッドが まだポインタ o を 使っているかも

SMP/マルチコア環境において 安全な strong update を実現する 従来の TALK の型付け手法 メモリの型を 2 種類に分ける: ローカルメモリ 1つのスレッドからしか アクセスされないメモリ 共有メモリ 複数スレッド間で 共有されるメモリ ローカル メモリ ローカル メモリ ローカル メモリ スレッド スレッド スレッド 共有 メモリ

SMP/マルチコア環境において 安全な strong update を実現する 従来の TALK の型付け手法 他のスレッドは アクセスできないので 共有メモリには (基本的には) strong update を許さない ただし、条件付きで許す ローカル メモリ ローカル メモリ ローカル メモリ スレッド スレッド スレッド 共有 メモリ

共有メモリに対する strong update を許す条件 共有メモリの型が 実際の命令実行の前後 (右図の マーク) で変わらないこと Strong update は 1 CPU命令 + pseudo 命令の間 (右図の マークの間) なら実行できる Pseudo 命令 = 型のみを操作する、 実行時に影響のない命令 こうすると他のスレッドからは 型が不変であるかのように「見える」 CPU 命令 CPU 命令 Pseudo 命令 CPU 命令 Pseudo 命令 CPU 命令 CPU 命令 CPU 命令 命令実行の流れ

ロックの獲得の例 {p∃i.{qdata if [i==0]}. (i, q)} (r1 : p) lock: mov r2  1 unpack r1 xchg [r1], r2 pack r1 bne r2, 0, lock …

ロックの獲得の例 {p∃i.{qdata if [i==0]}. (i, q)} (r1 : p) lock: mov r2  1 unpack r1 xchg [r1], r2 pack r1 bne r2, 0, lock … アドレス p: (0, q) 共有 メモリ q: data スレッド ローカル メモリ

ロックの獲得の例 {p∃i.{qdata if [i==0]}. (i, q)} (r1 : p) lock: mov r2  1 unpack r1 xchg [r1], r2 pack r1 bne r2, 0, lock … アドレス p: (0, q) 共有 メモリ スレッド q: data ローカル メモリ

ロックの獲得の例 {p∃i.{qdata if [i==0]}. (i, q)} (r1 : p) lock: mov r2  1 unpack r1 xchg [r1], r2 pack r1 bne r2, 0, lock … アドレス p: (1, q) 共有 メモリ スレッド q: data ローカル メモリ

ロックの獲得の型検査の例 {p∃i.{qdata if [i==0]}. (i, q)} (r1 : p) lock: mov r2  1 unpack r1 xchg [r1], r2 pack r1 bne r2, 0, lock … 型検査器の状態 {p  ∃i.….(i, q)} (r1 : p, r2 : ??)

ロックの獲得の型検査の例 {p∃i.{qdata if [i==0]}. (i, q)} (r1 : p) lock: mov r2  1 unpack r1 xchg [r1], r2 pack r1 bne r2, 0, lock … 型検査器の状態 {p  ∃i.….(i, q)} (r1 : p, r2 : 1)

ロックの獲得の型検査の例 {p∃i.{qdata if [i==0]}. (i, q)} (r1 : p) lock: mov r2  1 unpack r1 xchg [r1], r2 pack r1 bne r2, 0, lock … 型検査器の状態 {p  (i, q)} [q  data if [i == 0]] (r1 : p, r2 : 1)

ロックの獲得の型検査の例 {p∃i.{qdata if [i==0]}. (i, q)} (r1 : p) lock: mov r2  1 unpack r1 xchg [r1], r2 pack r1 bne r2, 0, lock … 型検査器の状態 {p  (i, q)} [q  data if [i == 0]] (r1 : p, r2 : 1) Strong update: 次の次のCPU命令までに 型を元に戻さなくてはならない

ロックの獲得の型検査の例 {p∃i.{qdata if [i==0]}. (i, q)} (r1 : p) lock: mov r2  1 unpack r1 xchg [r1], r2 pack r1 bne r2, 0, lock … 型検査器の状態 {p  (1, q)} [q  data if [i == 0]] (r1 : p, r2 : i)

ロックの獲得の型検査の例 {p∃i.{qdata if [i==0]}. (i, q)} (r1 : p) lock: mov r2  1 unpack r1 xchg [r1], r2 pack r1 bne r2, 0, lock … 型検査器の状態 {p  ∃i.….(i, q)} [q  data if [i == 0]] (r1 : p, r2 : i)

ロックの獲得の型検査の例 {p∃i.{qdata if [i==0]}. (i, q)} (r1 : p) lock: mov r2  1 unpack r1 xchg [r1], r2 pack r1 bne r2, 0, lock … 型検査器の状態 {p  ∃i.….(i, q)} [q  data if [i == 0]] (r1 : p, r2 : i) 型が元に戻ったのでOK

ロックの獲得の型検査の例 {p∃i.{qdata if [i==0]}. (i, q)} (r1 : p) lock: mov r2  1 unpack r1 xchg [r1], r2 pack r1 bne r2, 0, lock … 型検査器の状態 {p  ∃i.….(i, q)} [q  data if [i == 0]] (r1 : p, r2 : i)

ロックの獲得の型検査の例 {p∃i.{qdata if [i==0]}. (i, q)} (r1 : p) lock: mov r2  1 unpack r1 xchg [r1], r2 pack r1 bne r2, 0, lock … 型検査器の状態 {p  ∃i.….(i, q)} [q  data] (r1 : p, r2 : i)

ロックの獲得の型検査の例 {p∃i.{qdata if [i==0]}. (i, q)} (r1 : p) lock: mov r2  1 unpack r1 xchg [r1], r2 pack r1 bne r2, 0, lock … 型検査器の状態 {p  ∃i.….(i, q)} [q  data] (r1 : p, r2 : i) ロックで保護されていた メモリ領域 q を共有メモリから 取り出せた

ここまでの型付け手法の問題点 SMP/マルチコア環境における 「メモリコンシステンシモデル」 を考慮していない 「緩い」メモリコンシステンシの 共有メモリ上では メモリ安全性が破られる可能性がある

「緩い」メモリコンシステンシとは あるスレッド (CPU) で実行されたメモリ操作が 他のスレッド (CPU) から観測可能となる順序が 元のメモリ操作の順序と異なるような メモリコンシステンシのこと

「緩い」メモリコンシステンシの例 以下の 2 つのスレッドの実行結果が 「r1 = 1 かつ r2 = 0」 となり得る x: y: アドレス x: 共有メモリの 初期状態 y: Thread1: st [x]  1 st [y]  1 Thread2: ld r1  [y] ld r2  [x]

「緩い」メモリコンシステンシの例 以下の 2 つのスレッドの実行結果が 「r1 = 1 かつ r2 = 0」 となり得る x: y: アドレス この 2 つの st 命令が 他のスレッドから「見える」順番が入れ替わるかも x: この 2 つの ld 命令が 他のスレッドから「見える」順番が入れ替わるかも y: Thread1: st [x]  1 st [y]  1 Thread2: ld r1  [y] ld r2  [x]

他のスレッドから「見える」順番が入れ替わるかも 「緩い」メモリコンシステンシの例 以下の 2 つのスレッドの実行結果が 「r1 = 1 かつ r2 = 0」 となり得る アドレス この 2 つの st 命令が 他のスレッドから「見える」順番が入れ替わるかも x: y: Thread1: st [x]  1 st [y]  1 Thread2: ld r1  [y] ld r2  [x] 4 2 1 3

他のスレッドから「見える」順番が入れ替わるかも 「緩い」メモリコンシステンシの例 以下の 2 つのスレッドの実行結果が 「r1 = 1 かつ r2 = 0」 となり得る アドレス x: この 2 つの ld 命令が 他のスレッドから「見える」順番が入れ替わるかも y: Thread1: st [x]  1 st [y]  1 Thread2: ld r1  [y] ld r2  [x] 2 4 3 1

「緩い」メモリコンシステンシ上で メモリ操作の「見え方」を制御する方法 今日の多くの CPU は 以下の 2 つの機能を提供する アトミック命令実行機能 メモリ操作反映順序制御機能

アトミック命令実行機能 命令の行うメモリ操作の結果が 他のスレッドから 「全て見えない」か「全て見える」か のどちらかになる 中途半端なメモリ状態が 他のスレッドから見えなくなる

メモリ操作反映順序制御機能 Acquire メモリ操作 Release 操作 この操作より後のどのメモリ操作よりも先に 他のスレッドから観測可能となる操作 Release 操作 この操作より前のどのメモリ操作よりも後に 他のスレッドから観測可能となる操作

メモリ操作反映順序制御機能の例 以下の 2 つのスレッドの実行結果が 「r1 = 1 かつ r2 = 0」 となり得ない x: y: アドレス x: 共有メモリの 初期状態 y: Thread1: st [x]  1 release st [y]  1 Thread2: ld r1  [y] acquire ld r2  [x]

メモリ操作反映順序制御機能の例 以下の 2 つのスレッドの実行結果が 「r1 = 1 かつ r2 = 0」 となり得ない x: y: アドレス x: 共有メモリの 初期状態 y: Thread1: st [x]  1 release st [y]  1 Thread2: ld r1  [y] acquire ld r2  [x] 必ず x より後に y に書き込まれるように「見える」 必ず x より前に y が読み込まれるように「見える」

「緩い」メモリコンシステンシ に対応するための型付け手法 以下の 2 つの制約を型システムで検査する 共有メモリに対するメモリ操作には 常に「アトミック命令実行機能」を用いること 共有メモリとローカルメモリの間で メモリ領域を移動する場合は 「メモリ操作反映順序制御機能」を用いること 共有メモリ  ローカルメモリ : acquire ローカルメモリ  共有メモリ : release

「緩い」メモリコンシステンシに対応した ロックの獲得の例 {p∃i.{qdata if [i==0]}. (i, q)} (r1 : p) lock: mov r2  1 unpack r1 atomic xchg [r1], r2 acquire pack r1 bne r2, 0, lock …

「緩い」メモリコンシステンシに対応した ロックの獲得の型検査の例 {p∃i.{qdata if [i==0]}. (i, q)} (r1 : p) lock: mov r2  1 unpack r1 atomic xchg [r1], r2 acquire pack r1 bne r2, 0, lock … 型検査器の状態 {p  ∃i.….(i, q)} (r1 : p, r2 : ??)

「緩い」メモリコンシステンシに対応した ロックの獲得の型検査の例 {p∃i.{qdata if [i==0]}. (i, q)} (r1 : p) lock: mov r2  1 unpack r1 atomic xchg [r1], r2 acquire pack r1 bne r2, 0, lock … 型検査器の状態 {p  ∃i.….(i, q)} (r1 : p, r2 : 1)

「緩い」メモリコンシステンシに対応した ロックの獲得の型検査の例 {p∃i.{qdata if [i==0]}. (i, q)} (r1 : p) lock: mov r2  1 unpack r1 atomic xchg [r1], r2 acquire pack r1 bne r2, 0, lock … 型検査器の状態 {p  (i, q)} [q  data if [i == 0]] (r1 : p, r2 : 1)

「緩い」メモリコンシステンシに対応した ロックの獲得の型検査の例 {p∃i.{qdata if [i==0]}. (i, q)} (r1 : p) lock: mov r2  1 unpack r1 atomic xchg [r1], r2 acquire pack r1 bne r2, 0, lock … 型検査器の状態 {p  (i, q)} [q  data if [i == 0]] (r1 : p, r2 : 1) まだ acquire していないので アドレス q はアクセス不可

「緩い」メモリコンシステンシに対応した ロックの獲得の型検査の例 {p∃i.{qdata if [i==0]}. (i, q)} (r1 : p) lock: mov r2  1 unpack r1 atomic xchg [r1], r2 acquire pack r1 bne r2, 0, lock … 型検査器の状態 {p  (1, q)} [q  data if [i == 0]] (r1 : p, r2 : i)

「緩い」メモリコンシステンシに対応した ロックの獲得の型検査の例 {p∃i.{qdata if [i==0]}. (i, q)} (r1 : p) lock: mov r2  1 unpack r1 atomic xchg [r1], r2 acquire pack r1 bne r2, 0, lock … 型検査器の状態 {p  (1, q)} [q  data if [i == 0]] (r1 : p, r2 : i) アトミックにメモリ操作 しているのでOK

「緩い」メモリコンシステンシに対応した ロックの獲得の型検査の例 {p∃i.{qdata if [i==0]}. (i, q)} (r1 : p) lock: mov r2  1 unpack r1 atomic xchg [r1], r2 acquire pack r1 bne r2, 0, lock … 型検査器の状態 {p  (1, q)} [q  data if [i == 0]] (r1 : p, r2 : i)

「緩い」メモリコンシステンシに対応した ロックの獲得の型検査の例 {p∃i.{qdata if [i==0]}. (i, q)} (r1 : p) lock: mov r2  1 unpack r1 atomic xchg [r1], r2 acquire pack r1 bne r2, 0, lock … 型検査器の状態 {p  (1, q)} [q  data if [i == 0]] (r1 : p, r2 : i) acquire 操作の結果 アドレス q に アクセス可能になった

「緩い」メモリコンシステンシに対応した ロックの獲得の型検査の例 {p∃i.{qdata if [i==0]}. (i, q)} (r1 : p) lock: mov r2  1 unpack r1 atomic xchg [r1], r2 acquire pack r1 bne r2, 0, lock … 型検査器の状態 {p  ∃i.….(i, q)} [q  data if [i == 0]] (r1 : p, r2 : i)

「緩い」メモリコンシステンシに対応した ロックの獲得の型検査の例 {p∃i.{qdata if [i==0]}. (i, q)} (r1 : p) lock: mov r2  1 unpack r1 atomic xchg [r1], r2 acquire pack r1 bne r2, 0, lock … 型検査器の状態 {p  ∃i.….(i, q)} [q  data if [i == 0]] (r1 : p, r2 : i)

「緩い」メモリコンシステンシに対応した ロックの獲得の型検査の例 {p∃i.{qdata if [i==0]}. (i, q)} (r1 : p) lock: mov r2  1 unpack r1 atomic xchg [r1], r2 acquire pack r1 bne r2, 0, lock … 型検査器の状態 {p  ∃i.….(i, q)} [q  data] (r1 : p, r2 : i)

「緩い」メモリコンシステンシに対応した ロックの獲得の型検査の例 {p∃i.{qdata if [i==0]}. (i, q)} (r1 : p) lock: mov r2  1 unpack r1 atomic xchg [r1], r2 acquire pack r1 bne r2, 0, lock … 型検査器の状態 {p  ∃i.….(i, q)} [q  data] (r1 : p, r2 : i) 既に acquire 済みなので アドレス q はアクセス可

関連研究 マルチスレッドに対応した型付きアセンブリ言語 [Vasconcelos et al. 2006] 同期機構やスレッド機構そのものを記述することはできない Lock や unlock 、スレッド機構はプリミティブとして提供されている その他、型でロックの整合性を 保証する研究[Flanagan et al. 1999, 2007, Iwama et al. 2002, Grossman 2003, etc.] レースコンディションやデッドロック等を防ぐことを 主な目的としている 一方我々の手法はメモリ安全性等のみを目的としている

関連研究 「緩い」メモリコンシステンシモデルに関する検証 SMP/マルチコア環境におけるプログラム検証 [Ghughal et al. 2000, Chatterjee et al. 2002] 「緩い」メモリコンシステンシの「実装」の検証 [Burckhardt et al. 2008] TSO 上のプログラムが SC を満たすことをチェックする [Boudol et al. 2009, Atig et al. 2010] 「緩い」メモリコンシステンシの共有メモリを持つシステムの 操作的意味論を定義してプログラム検証に使う SMP/マルチコア環境におけるプログラム検証 [Dinsdale-Young et al. 2010] 共有メモリに対する不変条件を扱えるように separation logic を拡張している ただし「緩い」メモリコンシステンシモデルを考慮していない

まとめ SMPやマルチコア環境に対応した 型付きアセンブリ言語を提案した ロック等の同期機構そのものを記述できる 複数スレッド間で共有されるメモリに対しては strong update を 1CPU命令 + pseudo命令のみで許可することで実現した 「緩い」メモリコンシステンシモデルにもとづく 共有メモリのもとでも メモリ安全性を保証できる 型付けによって以下の 2 つの制約を検査する 共有メモリに対する操作は 「アトミック命令実行機能」を用いること 共有メモリとローカルメモリの間で メモリ領域を移動するときには 「メモリ操作反映順序制御機能」を用いること 共有メモリ  ローカルメモリ: acquire ローカルメモリ  共有メモリ: release