メソッドに線形化点がないことを確実に証明できる場合、それは必ずしもそのメソッドが線形化できないことを意味しますか? また、サブ質問として、メソッドに線形化ポイントがないことをどのように証明できますか?
3 に答える
上記の答えに基づいて構築するために、メソッドは線形化可能であると記述できます。ジョーカーが言及した本で参照されているように:http://www.amazon.com/dp/0123705916/?tag=stackoverfl08-20
69 ページの練習問題 32 を見てください。
enq() は実際にはメソッドであり、線形化可能/線形化可能ではない可能性があると説明されていることに注意してください。
線形化可能な点があることを証明することは、線形化可能性を壊す可能性のある例があるかどうかを見つけることになります。メソッド内のさまざまな読み取り/書き込みメモリ操作が線形化可能であると仮定し、そのような仮定の結果として線形化不可能な状況が存在することを矛盾によって証明する場合、前述の読み取り/書き込み操作は線形化できないと宣言できます。有効な線形化ポイント。
たとえば、次の enq()/deq() メソッドを取り上げます。これらのメソッドは、ヘッド/テール ポインターとバッキング配列 "arr" を備えた標準的なキュー実装の一部であると想定しています。
public terribleQueue(){
arr = new T[10];
tail = 0;
head = 0;
}
void enq(T x){
int slot = tail;
arr[slot] = x;
tail = tail + 1;
}
T deq(){
if( head == tail ) throw new EmptyQueueException();
T temp = arr[head];
head = head + 1;
return temp;
}
このひどい実装では、たとえば、enq の最初の行が有効な線形化ポイントではないことを簡単に証明できます。これは、それが線形化ポイントであると想定し、次に示すように、そうでないことを示す例を見つけることによって行われます。
A と B の 2 つのスレッドの例と、履歴の例を見てみましょう。
A: enq( 1 )
A: slot = 0
B: enq( 2 )
B: slot = 0
(A と B は現在、線形化ポイントを過ぎているため、履歴に合わせて並べ替えることができません)
A: arr[0] = 1
B: arr[0] = 2
A: tail = 1
B: tail = 2
C: deq()
C: temp = arr[0] = 2
C: head = 1
C: return 2
ここで、線形化ポイント (A と B の順序を固定する) を選択したため、C の deq をどこに置いても 1 を返すようにすることができないため、この実行を線形化することは不可能であることがわかります。
ちょっと長ったらしい回答ですが、参考になれば幸いです
メソッドに線形化ポイントがないことを確実に証明できる場合、それは必ずしもそうですか? そのメソッドは線形化できないということですか?
まず、線形化可能性はメソッドのプロパティではなく、実行シーケンスのプロパティです。
メソッドに線形化ポイントがないことをどのように証明できますか?
メソッドの線形化ポイントを見つけることができるかどうかは、実行シーケンスに依存します。
たとえば、FIFO キューのスレッド A のシーケンスは次のとおりです。t1、t2、t3 は時間間隔です。
A.enq(1) A.enq(2) A.deq(1)
t1 t2 t3
最初の 2 つの enq メソッドの線形化ポイント (lp) は、それぞれ時間間隔 t1 と t2 の任意のポイントとして選択でき、deq の場合は t3 の任意のポイントを選択できます。これらの方法で選択するポイントは lp です。
さて、不完全な実装を考えてみましょう
A.enq(1) A.enq(2) A.deq(2)
t1 t2 t3
線形化可能性により、lp はリアルタイムの順序付けを尊重できます。したがって、メソッドの lp は時間の順序、つまり t1 < t2 < t3 に従う必要があります。ただし、実装が正しくないため、これを明確に行うことはできません。したがって、メソッド A.deq(2) の線形化ポイントを見つけることができません。あまりにも線形化できません。
詳細を知る必要がある場合は、この本を読むことができます: http://www.amazon.com/Art-Multiprocessor-Programming-Maurice-Herlihy/dp/0123705916
この回答は、私がウィキペディアで線形化可能性について初めて読んだことに基づいており、それを事前発生関係を通じてメモリの一貫性に関する私の既存の理解にマッピングしようとしています。だから私は概念を誤解しているかもしれません。
メソッドに線形化点がないことを確実に証明できる場合、それは必ずしもそのメソッドが線形化できないことを意味しますか?
共有された変更可能な状態が、同期や可視化支援なしで複数のスレッドによって同時に操作され、破損のリスクなしにすべての不変条件を維持するシナリオを持つことができます。
ただし、そのようなケースは非常にまれです。
メソッドに線形化ポイントがないことをどのように証明できますか?
私は線形化ポイントを理解しているので、ここで間違っているかもしれませんが、それらはスレッド間で事前発生関係が確立される場所です。メソッドが(順番に呼び出すすべてのメソッドを再帰的に)そのような関係を確立しない場合、線形化ポイントがないと断言します。