フェイスブックがRacerDをオープンソースに - Javaの競合状態を検出

フェイスブックのオープンソースの静的解析ツールであるInferが、RacerDによるJavaコード競合状態検出を追加して公開された。RacerDはロックまたは@ThreadSafeを使うクラスにあるメソッド間の競合状態を見つける。

フェイスブックはこの1年間自身の製品のコードに対してRacerDを使ってきており、1000以上のマルチスレッドの問題を見つけた。すべて本番リリース前にだ。このInferを使ってJavaコードのバグを検知しているJava開発者は並列処理のチェック機能を利用できる。

競合状態は並列処理のエラーもしくはバグの一種であり、2つのスレッドが適切な同期をせずに同じオブジェクトに対して操作すると、お互いの実行が重なり合ってしまい発生する。少なくとも1つは書き込みアクセスである。並列処理の問題はデバッグが困難で、発生した後に再現することさえ難しい。

RacerDは大規模でもすばやくそして有益な並列処理解析ができる。RacerDは並列処理の問題に対してコードベース全体をチェックしようとはしないので早い。並列に実行されると思われるコードを検査するだけである。

RacerDは明示的に@ThreadSafeアノテーションを付与されている、もしくはsynchronizedキーワードでロックを作るクラスやメソッド、インタフェースを調べて並列に実行できるコードを見つける。 クラスもしくはインタフェースが@ThreadSafeを付与されているとき、そのクラス/インタフェースの全サブクラスも検査する。RacerDでのコードカバレッジを増やす際には、オプションのアノテーションを追加するとよい。@ThreadConfinedや@Functional、@ReturnsOwnership、@VisibleForTestingだ。

RacerDの解析は通常のinferコマンドで起動する。これは同時に他のInferの解析も実行する。もしくはinfer --racerd-onlyコマンドでRacerDだけ実行する。たとえばコマンドinfer --racerd-only -- javac StockPortfolio.javaはStockPortfolio.javaに対してRacerDを実行する。

以下のサンプルコードはRacerDが検査し、競合状態を1つ警告している。

@ThreadSafe
public class StockPortfolio {
 int shares = 0;
 
 public void buy(int count) {
   if (count > 0) {
     shares += count;
   }
 }

 public int sell(int count){
   if (count >= 0 && shares - count >= 0) {
     shares -= count;
     return shares;
   } else {
     return 0;
   }
 }
}

RacerDがバグを発見

読み込み/書き込みの競合。publicメソッドint StockPortfolio.sell(int)はフィールドStockPortfolio.sharesから読み込んでいる。メソッドvoid StockPortfolio.buy(int)とint StockPortfolio.sell(int)による書き込みと競合する可能性がある。

RacerDは保護されていない書き込みか読み込み/書き込みかいずれかを含むデータ競合も警告する。RacerDは現在データ競合のチェックのみに限られる。他の並列処理の問題、デッドロックやアトミック性などはチェックしない。またRacerDは以下の原因でデータ競合を見落とす。

• エイリアス
• そのスコープの外にあるローカルに宣言されたオブジェクト
• 異なるロックで保護されたアクセス
• 所有されていないオブジェクトが入っているローカルオブジェクト
• weakメモリとJavaのvolatileキーワード

こうした限界はたとえフォールス・ネガティブとなってもフォールス・ポジティブを減らすという設計目標に起因する。

共同作成者であるSam Blackshear氏とPeter O'Hearn氏が告知にこう書いている。

Inferはフェイスブックでコードレビューにおけるバッチモードのデプロイとボット参加者の両方で使われています。コードレビューに対するデプロイでは、Inferをフェイスブックの継続的統合(CI)システムの一部として実行します。開発者が書いた各コードの変更に対して、CIはコンパイルやテストといった他のジョブと同時にInferを実行します。

RacerDはGitHubにあり、ユーザガイドにより詳しい情報がある。