checker-framework - 副作用の保証が弱いメソッドを呼び出すにはどうすればよいですか?

Question

ロックチェッカーからこれを取得しました：

Error:(52, 30) java: [method.guarantee.violated] @ReleasesNoLocks method proc() calls method unfree() with a weaker @MayReleaseLocks side effect guarantee

コードを投稿できますが、問題ありません。副作用メソッドの呼び出しに関するドキュメントがわかりません。

Answer 1

コードは次のようになります。

@ReleasesNoLocks
void proc() {
  ...
  unfree();  // line 52
  ...
}

void unfree() {
  // arbitrary code that might include someLock.unlock();
}

のドキュメントに @ReleasesNoLocksは次のように書かれています：

メソッドとそれが呼び出すすべてのメソッドは、厳密に非減少のロック保持カウントを維持します

メソッドの@ReleasesNoLocks注釈は、メソッドがロックを解放しないprocことを約束します。procただし、メソッドunfreeは一部のロックを解放する場合があります (注釈が付けられていないため@ReleasesNoLocks)。unfreeロックを解除すると、その仕様に違反procします。それが、Lock Checker のメッセージが (簡潔に) 言っていることです。

実行時の動作には、次の 3 つの可能性があります。

1. unfree本当にロックを解除します。この場合、コードにバグがあり、ロック チェッカーがそのことを知らせています! の注釈@ReleasesNoLocksはprocfalse です。その注釈を削除するunfreeか、ロックを解放しないように変更する必要があります。
2. unfreeロックを解放することはありません。この場合、 として注釈を付ける必要がありunfreeます@ReleasesNoLocks。その時点で、ロック チェッカーはprocの実装がその仕様を満たしていることを確認できるため、警告は発行されなくなります。
3. unfreeロックを解除する場合と解除しない場合があります。の本体内の特定の呼び出しがprocロックを解除しないことはわかっています。この場合、@SuppressWarnings("method.guarantee.violated")ソース コードの 52 行目に注釈を記述する必要があります。キー「method.guarantee.violated」がエラー メッセージに表示されます。@SuppressWarningsこの事実をどのように知っているかを説明するコメントを追加することをお勧めします。これにより、将来、注釈を書いた理由がわかるようになります。