コンテンツにスキップ

リード・コピー・アップデート

出典: フリー百科事典『ウィキペディア(Wikipedia)』

リード・コピー・アップデートread-copy-updateRCUと略記)とは、オペレーティングシステムにおいて一種の排他制御[note 1]を実装する同期機構であり、リーダー・ライターロック英語版の代替手段として使われることがある。参照において待ち状態が生じず、極めてオーバーヘッドが低い。しかしRCUにおけるデータ更新は、既存の参照者のために古い版のデータ構造を保持しつつ行うため、時間と空間(メモリ)をより多く必要とする。古い版のデータ構造は、既存の参照者が全てアクセスを完了した後で回収される。

概要

[編集]

RCUでは「参照側クリティカルセクション」という概念があり、通常 rcu_read_lock() と rcu_read_unlock() で挟まれた部分がそれにあたる。参照側クリティカルセクション内にない文は「不活性状態」と呼ばれ、RCUで保護されたデータ構造への参照を保持することは許されない。データを共有するスレッド間で、少なくとも1つが不活性状態にある期間を「猶予期間」と呼ぶ。定義上、任意のRCU参照側クリティカルセクションが猶予期間の始まりに存在する場合、その猶予期間の終了までにクリティカルセクションが完了しなければならず、それがRCUの提供する根本的保証の前提となっている。この保証が参照側オーバーヘッドを極めて小さくすることがわかっており、実際サーバクラスのLinuxカーネルでの参照側オーバーヘッドはゼロである[1]

RCUの基本的な考え方は、更新を「削除」と「再利用」のフェーズに分割することである。削除フェーズではデータ構造内のデータへの参照を削除する(それらの参照を別のバージョンのデータ構造への参照に切り替える)。そうすることで参照側クリティカルセクションと並行して更新可能にする。削除フェーズが参照者と並行して動作できるのは、最近のCPUの設計によって参照者が新旧いずれかの版のデータ構造だけを参照することを保証できるためである(参照側クリティカルセクション内で参照するデータ構造の版が入れ替わることがない)。猶予期間が過ぎると、旧版のデータ構造を参照している参照者がいないと断定でき、旧版のデータを構成するアイテムを再利用フェーズで解放(再利用)しても安全である[2]

更新を削除と再利用のフェーズに分割することで、更新者は削除フェーズを速やかに行い、削除フェーズに入ったときに動作していた全ての参照者が停止するまで、言い換えれば猶予期間が過ぎるまで再利用フェーズを遅らせる[note 2]

典型的なRCUにおける更新は以下のような流れとなる[3]

  1. RCUで保護されたデータ構造にアクセスする参照者は全てRCU参照側クリティカルセクション内で参照することを保証する。
  2. データ構造へのポインタを削除して、その後の参照者がそれを参照できないようにする。
  3. 猶予期間が過ぎるのを待つ。それにより(前のフェーズで削除されたデータ構造へのポインタを持っている可能性のある)全ての参照者がRCU参照側クリティカルセクションを抜けるのを待つ。
  4. この時点で更新したいデータ構造への参照を持つスレッドはいなくなるので、安全に再利用(たとえば、解放)できる[note 3]

このような手順において、更新者が削除と再利用のステップを実行するが、再利用については全く別のスレッドに任せた方が便利なことが多い。参照カウントを持たせることで、参照者が削除を行うこともできるので、更新ステップ(上記の (2))と再利用ステップ(上記の (4))が同じスレッドで行われるとしても、それらを分けて考えた方がわかりやすい。

利用

[編集]

2008年初めごろの段階で、Linuxカーネル内では、ネットワーク・プロトコルスタック[4]メモリ管理システム[5]など約2,000箇所で RCU API を利用している[6]。 2006年以降、研究者らはRCUや類似の技法をいくつかの問題に適用してきた。例えば、動的解析に使用するメタデータの管理[7]、クラスター型オブジェクトのライフタイム管理[8]、K42研究OSでのオブジェクト管理[9][10]ソフトウェアトランザクショナルメモリ実装の最適化[11][12]などである。DragonFly BSD はRCUによく似た技法を採用しており、Linuxの SRCU 実装に極めて近い。

長所と短所

[編集]

RCUでは、全参照者が参照を終えるのを待つことができ、それによって非常に軽量な同期が可能で、場合よっては同期しないで参照することができる。対照的に一般のロックを使った方式では、参照者はオーバーヘッドの大きな同期機構を使って更新者が使用中のデータ構造を削除するのを防がなければならない。これはロックを使った更新者がその場でデータを更新するためであり、従って参照する者がいないことを保証する必要がある。一方RCUでは現代的CPUでは1つのポインタの書き換えがアトミックになされるという点を利用し、参照者をわずらわせずにデータ構造のリンクをアトミックに挿入・削除・置換する。RCUの参照者は旧版のデータを同時並行的に参照し続けることができ、不可分操作メモリバリアやキャッシュミス(これらは今日のSMPコンピュータシステムではロックの衝突がなくても性能を低下させる)を排除できる[13][14]。RCUの参照側の軽量さは単に性能向上、スケーラビリティ、リアルタイム応答性に寄与するだけではない。例えば、デッドロックやライブロック状態を防ぐことにも繋がる[note 4]

RCUには当然ながら短所もある。例えば、RCUは参照が多く更新が少ない状況に最適な技法であり、更新が頻繁に行われる状況には適していない。また、RCUは参照者と更新者が同時並行的に動作できることで参照側の同期機構を軽量化しているが、参照と更新の並行性がなじまないアルゴリズムも存在する。

RCUは10年以上に渡って使われているが、その応用範囲は正確には把握されておらず、今も研究対象となっている。

特許

[編集]

この技術は米国ソフトウェア特許 5,442,758(1995年8月15日、権利者はシークエント・コンピュータ)でカバーされている(他に 5,608,893、5,727,528、6,219,690、6,886,162)。すでに権利失効している特許 4,809,168 も非常に近い技術をカバーしていた。RCU はSCOIBMの間の訴訟問題でも言及されている。

RCUインタフェースの例

[編集]

RCUはいくつかのOSで利用可能であり、Linuxカーネルには2002年10月に追加された。liburcu などのユーザーレベルの実装も利用可能である[15]

Linuxカーネル 2.6 でのRCU実装はよく知られており、以下ではそれを元に RCU API について解説する。中核となるAPIは極めて小さい[16]

  • rcu_read_lock(): RCUで保護されたデータへの参照を開始することを示す。それによってクリティカルセクション期間中に対象データが再利用されないようにする。
  • rcu_read_unlock(): 参照者が使用し、参照者が参照側クリティカルセクションから出たことを更新者に通知する。RCUの参照側クリティカルセクションはネスト可能であり、オーバーラップ可能である。
  • synchronize_rcu(): 全CPU上の既存のRCU参照側クリティカルセクションが全て完了するまでブロックされる。synchronize_rcu は後続のRCU参照側クリティカルセクションを待つ必要はない。たとえば、以下のようなイベントの流れを考えてみよう。
	         CPU 0                  CPU 1                 CPU 2
	     ----------------- ------------------------- ---------------
	 1.  rcu_read_lock()
	 2.                    enters synchronize_rcu()
	 3.                                               rcu_read_lock()
	 4.  rcu_read_unlock()
	 5.                     exits synchronize_rcu()
	 6.                                              rcu_read_unlock()
synchronize_rcu は参照者が参照を完了したことを判定するAPIであり、RCU実装の要である。RCUは特に参照が多く更新が滅多にない場合に有効であり、synchronize_rcu のオーバーヘッドは極めて小さくなければならない。
ブロックする代わりに synchronize_rcu でコールバック関数と引数を登録し、動作中のRCU参照側クリティカルセクションが完了したときにそれがコールされるようにする実装もある。Linuxカーネルでは、このコールバック型のAPIを call_rcu と呼ぶ。
  • rcu_assign_pointer(): 更新者が使用し、更新者から参照者に安全に変化を伝え、RCUに保護されたポインタを更新する。この関数は、CPUアーキテクチャ上必要なメモリバリア命令を実行し、新たな値を返す。もっと重要な点として、この関数はどのポインタがRCUによって保護されているかを保証する。
  • rcu_dereference_pointer(): RCUに保護されたポインタをフェッチするために参照者が使用し、そのポインタが指している値を安全に得る。また、CPUアーキテクチャ上必要なメモリバリア命令も実行する。rcu_dereference_pointer が返す値はRCU参照側クリティカルセクション内でのみ有効である。rcu_assign_pointer との関連で rcu_dereference_pointer の重要な機能は、どのポインタがRCUで保護されているかを示すことである。

以下の図は各APIが参照者、更新者、再利用者の間でどう関係しているかを示している。

            rcu_assign_pointer()
                                    +--------+
            +---------------------->| 参照者 |---------+
            |                       +--------+         |
            |                           |              |
            |                           |              | 保護:
            |                           |              | rcu_read_lock()
            |                           |              | rcu_read_unlock()
            |        rcu_dereference()  |              |
       +---------+                      |              |
       | 更新者  |<---------------------+              |
       +---------+                                     V
            |                                    +-----------+
            +----------------------------------->| 再利用者  |
                                                 +-----------+
              遅延:
              synchronize_rcu() & call_rcu()

RCUの内部機構は rcu_read_lock, rcu_read_unlock, synchronize_rcu, call_rcu が呼び出された順番を記憶し、(1) synchronize_rcu がそれらの呼び出し側への戻りを設定するか、(2) call_rcu のコールバックが呼び出される順番を決定する。効果的な実装としては、各APIのオーバヘッドを減らして、背後でバッチ的に処理するほうがよい。

RCUの単純な実装

[編集]

RCUのおもちゃ的な実装を考えるとRCUを理解しやすいだろう。ここではそのような簡単な実装を説明する。この実装はプリエンプション不可な環境でのみ動作することに注意[17]

	void rcu_read_lock(void) { }

	void rcu_read_unlock(void) { }

	void call_rcu(void (*callback) (void *), void *arg)
	{
		// add callback/arg pair to a list
	}

	void synchronize_rcu(void)
	{
		int cpu, ncpus = 0;

		for_each_cpu(cpu)
                        schedule_current_task_to(cpu);

                for each entry in the call_rcu list
                        entry->callback (entry->arg);
	}

rcu_assign_pointerrcu_dereference_pointer を無視しても大勢に影響はないが、いずれにしろ、以下のようになる。

	#define rcu_assign_pointer(p, v)	({ \
							smp_wmb(); \
							(p) = (v); \
						})

	#define rcu_dereference_pointer(p)      ({ \
					        	typeof(p) _value = (p); \
					        	smp_rmb(); /* not needed on all architectures */ \
					        	(_value); \
					        })

rcu_read_lockrcu_read_unlock は全く何もしない。プリエンプション不可な古いカーネルでは、このように参照側のオーバヘッドは全く無い(メモリバリアが必要となるのは DEC Alpha だけである[18])。したがって rcu_read_lock がデッドロック状態になることもなく、リアルタイムプロセスがスケジューリングのデッドラインに陥ることもなく、優先順位の逆転が発生することもなく、ロックの衝突が激しく発生することもない。

synchronize_rcu の実装は、synchronize_cpu を呼び出した者を各CPUに移動させ、全CPUでコンテキストスイッチ可能となるまでブロックさせる。プリエンプション不可なのでRCU参照側クリティカルセクション内でプリエンプションは発生せず、あるCPUで(他のプロセスをスケジュールする)コンテキストスイッチが起きたときにはそれ以前のRCU参照側クリティカルセクションは完了しているはずである。全CPUでコンテキストスイッチが起きたら、既存のRCU参照側クリティカルセクションが全て完了していることを保証できる。

リーダー・ライターロックとの比較

[編集]

RCUはいろいろな使い方があるが、一般的な使い方はリーダー・ライターロックに近い。以下のふたつのコードはリーダー・ライターロック(左側)とRCU(右側)を同じ処理で使ったものである[19]

 1 struct el {                           1 struct el {
 2   struct list_head lp;                2   struct list_head lp;
 3   long key;                           3   long key;
 4   spinlock_t mutex;                   4   spinlock_t mutex;
 5   int data;                           5   int data;
 6   /* Other data fields */             6   /* Other data fields */
 7 };                                    7 };
 8 DEFINE_RWLOCK(listmutex);             8 DEFINE_SPINLOCK(listmutex);
 9 LIST_HEAD(head);                      9 LIST_HEAD(head);

 1 int search(long key, int *result)     1 int search(long key, int *result)
 2 {                                     2 {
 3   struct el *p;                       3   struct el *p;
 4                                       4
 5   read_lock(&listmutex);              5   rcu_read_lock();
 6   list_for_each_entry(p, &head, lp) { 6   list_for_each_entry_rcu(p, &head, lp) {
 7     if (p->key == key) {              7     if (p->key == key) {
 8       *result = p->data;              8       *result = p->data;
 9       read_unlock(&listmutex);        9       rcu_read_unlock();
10       return 1;                      10       return 1;
11     }                                11     }
12   }                                  12   }
13   read_unlock(&listmutex);           13   rcu_read_unlock();
14   return 0;                          14   return 0;
15 }                                    15 }

 1 int delete(long key)                  1 int delete(long key)
 2 {                                     2 {
 3   struct el *p;                       3   struct el *p;
 4                                       4
 5   write_lock(&listmutex);             5   spin_lock(&listmutex);
 6   list_for_each_entry(p, &head, lp) { 6   list_for_each_entry(p, &head, lp) {
 7     if (p->key == key) {              7     if (p->key == key) {
 8       list_del(&p->lp);               8       list_del_rcu(&p->lp);
 9       write_unlock(&listmutex);       9       spin_unlock(&listmutex);
                                        10       synchronize_rcu();
10       kfree(p);                      11       kfree(p);
11       return 1;                      12       return 1;
12     }                                13     }
13   }                                  14   }
14   write_unlock(&listmutex);          15   spin_unlock(&listmutex);
15   return 0;                          16   return 0;
16 }                                    17 }

両者の違いは非常に小さい。参照側のロックは rcu_read_lock() と rcu_read_unlock() になり、更新側のロックはリーダー・ライターロックから単純なスピンロックに変更され、kfree()を実行するまえに synchronize_rcu() が呼び出される。

しかし、この場合参照側と更新側が同時に動作する可能性が出てくる。多くの場合はこれは問題とはならないが、使われ方を十分注意する必要がある。たとえば、複数の独立したリストをアトミックに更新しなければならない場合、これをRCUに置き換えるには注意が必要である。

synchronize_rcu() があるということはRCUでは delete() がブロックされる可能性があることを示す。 それが問題となる場合は代わりに call_rcu() を call_rcu (kfree, p) のように使用すればよい。これは参照カウントと組合わせる場合に特に便利である。

リード・コピー・アップデートと呼ばれる理由

[編集]

この名称はRCUがリンクリストをその場で更新するのに使われていたことに由来する。 この場合、以下のような処理の流れとなる。

  • 新しい構造体を作成する。
  • データを古い構造体からコピーし、古いデータ構造へのポインタをセーブする。
  • 新しいデータ構造に更新(変更)を加える。
  • グローバルなポインタが新しいデータ構造の方を指すよう変更する。
  • カーネルが古いデータ構造の参照者がいないと判断するまでスリープする(Linuxなら synchronize_rcu() を使用する)。

更新を行ったスレッドがカーネルによって起こされたら、安全に古いデータ構造を解放できる。

そのため、参照 (read) スレッドは、更新 (update) スレッドがコピー (copy) している間も並行して動作できる。以上から、「リード・コピー・アップデート(read-copy update)」と呼ばれたのである。これを RCU という略称で呼ぶようになったのはLinuxコミュニティである。類似の技術は、例えばVM/XA英語版では passive serialization あるいは MP defer と呼ばれ、K42英語版Tornadoでは generations と呼ばれている。

歴史

[編集]

RCUと類似する技法や機構は、歴史上何度も独自に発明されてきた[20]

  1. H. T. Kung と Q. Lehman は、2分探索木へのRCU風アクセスの実装にガベージコレクタを使った方式を提案している[21]
  2. Udi Manber と Richard Ladner は Kung と Lehman の業績をガベージコレクションを行わない環境で機能するよう発展させ、削除時点で動作していた全スレッドが完了するまで再利用を遅らせる方式を考案した。これは長命なスレッドが存在しない環境で機能する[22]
  3. リチャード・ラシッドらは、全CPUがTLBをフラッシュするまで仮想アドレス空間の再利用を遅らせるTLB実装方式を提案。基本概念はRCUの実装と共通している[23]
  4. J. Hennessy、D. Osisek、J. Seigh は1989年、米国特許 4,809,168 を取得(既に失効)。この特許はIBMメインフレーム上のVM/XA英語版で使われているRCU風機構に関するものである[24]
  5. William Pugh は参照者が明示的にフラグを設定するRCU風機構を提案した[25]
  6. Aju John は、更新者が単にある一定時間待つというRCU風機構を提案。これは、参照者が一定時間以内に完了することを前提としたもので、純粋なリアルタイムシステムに向いている[26]バン・ジェイコブソンも1993年に同様の方式を口頭のみだが提案している。
  7. J. Slingwine と P. E. McKenney は1995年8月、米国特許 5,442,758 を取得。後にLinuxカーネルに採用された DYNIX/ptx でのRCU実装を記述した特許である[27]
  8. B. Gamsa、O. Krieger、J. Appavoo、M. Stumm は、トロント大学Tornado research operating system でRCU風機構を使用している。これは、IBMの研究用OS K42英語版 と密接な関係がある[28]
  9. ラスティ・ラッセルと Phil Rumpf は、Linuxのカーネルモジュールのアンロードを行う技法としてRCU的な技法を提案[29][30]
  10. D. Sarma は2002年10月、RCUをLinuxカーネル 2.5.43 に導入した[31]
  11. Robert Colvin らはRCUに似たリストベース集合の遅延並行アルゴリズムを形式的に検証している[32]

脚注

[編集]

注釈

[編集]
  1. RCU は一般的な意味での排他制御の実装ではない。通常の排他制御機構が時間的に排他するのに対して、RCUではデータを更新中もデータの古いバージョンへの参照を同時に行えるようにすることで、空間的な排他を行う。
  2. 削除フェーズ中に動作中の参照者のみを考慮する必要がある。削除フェーズ後に動作開始した参照者は削除された旧版のデータへの参照が不可能なためであり、再利用フェーズに影響されることがない。
  3. 可能ならばこのステップでガベージコレクションを行うこともある。
  4. RCUでもデッドロックは発生しうる。例えばRCU参照側クリティカルセクション内で猶予期間が完了するまでブロックする操作を行った場合などである。

出典

[編集]
  1. Guniguntala, Dinakar; McKenney, Paul E.; Triplett, Joshua; Walpole, Jonathan (2008). “The read-copy-update mechanism for supporting real-time applications on shared-memory multiprocessor systems with Linux”. IBM Systems Journal 47 (2): 221–236. doi:10.1147/sj.472.0221.
  2. McKenney, Paul E. (2007年12月17日). What is RCU, Fundamentally?”. Linux Weekly News. 2010年9月24日閲覧。
  3. McKenney, Paul E.; Slingwine, John D. (October 1998). Read-Copy Update: Using Execution History to Solve Concurrency Problems (PDF). Parallel and Distributed Computing and Systems. pp. 509–518.
  4. Olsson, Robert; Nilsson, Stefan (May 2007). TRASH: A dynamic LC-trie and hash table structure. Workshop on High Performance Switching and Routing (HPSR'07).
  5. Piggin, Nick (July 2006). A Lockless Pagecache in Linux---Introduction, Progress, Performance (PDF). Ottawa Linux Symposium.
  6. McKenney, Paul E.; Walpole, Jonathan (July 2008). “Introducing technology into the Linux kernel: a case study”. SIGOPS Oper. Syst. Rev. 42 (5): 4–17. doi:10.1145/1400097.1400099.
  7. Kannan, Hari (2009). Ordering decoupled metadata accesses in multiprocessors. MICRO 42: Proceedings of the 42nd Annual IEEE/ACM International Symposium on Microarchitecture. New York, NY, USA. pp. 381–390. doi:10.1145/1669112.1669161. ISBN 978-1-60558-798-1.
  8. Matthews, Chris; Coady, Yvonne; Appavoo, Jonathan (2009). Portability events: a programming model for scalable system infrastructures. PLOS '06: Proceedings of the 3rd workshop on Programming languages and operating systems. San Jose, CA, USA. doi:10.1145/1215995.1216006. ISBN 1-59593-577-0.
  9. Da Silva, Dilma; Krieger, Orran; Wisniewski, Robert W.; Waterland, Amos; Tam, David; Baumann, Andrew (April 2006). “K42: an infrastructure for operating system research”. SIGOPS Oper. Syst. Rev. 40 (2): 34–42. doi:10.1145/1131322.1131333.
  10. Appavoo, Jonathan; Da Silva, Dilma; Krieger, Orran; Auslander, Mark; Ostrowski, Michal; Rosenburg, Bryan; Waterland, Amos; Wisniewski, Robert W. et al. (August 2007). “Experience distributing objects in an SMMP OS”. ACM Trans. Comput. Syst. 25 (3): 6/1–6/52. doi:10.1145/1275517.1275518.
  11. Fraser, Keir; Harris, Tim (2007). “Concurrent programming without locks”. ACM Trans. Comput. Syst. (ACM) 25 (2): 34–42. doi:10.1145/1233307.1233309.
  12. Porter, Donale E.; Hofmann, Owen S.; Rossbach, Christopher J.; Benn, Alexander; Witchel, Emmett (2009). Operating systems transactions infrastructures. SOSP '09: Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles. Big Sky, MT, USA: ACM. doi:10.1145/1629575.1629591. ISBN 978-1-60558-752-3.
  13. Hart, Thomas E.; McKenney, Paul E.; Demke Brown, Angela; Walpole, Jonathan (December 2007). “Performance of memory reclamation for lockless synchronization”. J. Parallel Distrib. Comput. 67: 1270–1285.
  14. McKenney, Paul E. (2008年1月4日). RCU part 2: Usage”. Linux Weekly News. 2010年9月24日閲覧。
  15. Desnoyers, Mathieu (December 2009). “Low-Impact Operating System Tracing”. Ecole Polytechnique de Montreal.
  16. McKenney, Paul E. (2008年1月17日). RCU part 3: the RCU API”. Linux Weekly News. 2010年9月24日閲覧。
  17. McKenney, Paul E.; Appavoo, Jonathan; Kleen, Andi; Krieger, Orran; Russell, Rusty; Sarma, Dipankar; Soni, Maneesh (July 2001). Read-Copy Update (PDF). Ottawa Linux Symposium.
  18. Wizard, The (2001年8月). Shared Memory, Threads, Interprocess Communication”. Hewlett-Packard. 2010年12月26日閲覧。
  19. McKenney, Paul E. (2003年10月). Using {RCU} in the {Linux} 2.5 Kernel”. Linux Journal. 2010年9月24日閲覧。
  20. McKenney, Paul E. (July 2004). “Exploiting Deferred Destruction: An Analysis of Read-Copy-Update Techniques”. OGI School of Science and Engineering at Oregon Health and Sciences University.
  21. Kung, H. T.; Lehman, Q. (September 1980). “Concurrent Maintenance of Binary Search Trees”. ACM Transactions on Database Systems 5 (3): 354. doi:10.1145/320613.320619.
  22. Manber, Udi; Ladner, Richard E. (September 1984). “Concurrency Control in a Dynamic Search Structure”. ACM Transactions on Database Systems 9 (3).
  23. Rashid, Richard; Tevanian, Avadis; Young, Michael; Golub, David; Baron, Robert; Bolosky, William; Chew, Jonathan (January 1995). Machine-Independent Virtual Memory Management for Paged Uniprocessor and Multiprocessor Architectures (PDF). Second Symposium on Architectural Support for Programming Languages and Operating Systems. Association for Computing Machinery.
  24. 4,809,168, "Passive Serialization in a Multitasking Environment"
  25. Pugh, William (June 1990). Concurrent Maintenance of Skip Lists (Technical report). Institute of Advanced Computer Science Studies, Department of Computer Science, University of Maryland. CS-TR-2222.1.
  26. John, Aju (January 1995). Dynamic vnodes design and implementation. USENIX Winter 1995.
  27. 5,442,758, "Apparatus and Method for Achieving Reduced Overhead Mutual Exclusion and Maintaining Coherency in a Multiprocessor System"
  28. Gamsa, Ben; Krieger, Orran; Appavoo, Jonathan; Stumm, Michael (February 1999). Tornado: Maximizing Locality and Concurrency in a Shared Memory Multiprocessor Operating System (PDF). Proceedings of the Third Symposium on Operating System Design and Implementation.
  29. Russell, Rusty (2000年6月). Re: modular net drivers”. 2012年3月28日閲覧。
  30. Russell, Rusty (2000年6月). Re: modular net drivers”. 2012年3月28日閲覧。
  31. Summary of changes from v2.5.42 to v2.5.43
  32. Colvin, Robert; Groves, Lindsay; Luchangco, Victor; Moir, Mark (August 2006). Formal Verification of a Lazy Concurrent List-Based Set Algorithm (PDF). Computer Aided Verification (CAV 2006).

関連項目

[編集]

外部リンク

[編集]