Facebook製Java並行性バグ解析ツール「RacerD」を試してみた

Facebookがオープンソースとして公開しているJava並行性バグ解析ツール「RacerD」を試してみました。本稿では以下の二点について共有します。

- RacerDのインストール手順（Dockerを使用）
- JCIP（Java Concurrency in Practice）とCC/CERTに掲載されている代表的なJava並行性バグの検出結果

## 「RacerD」とは

「RacerD」はFacebookがオープンソースとして公開しているJava並行性バグの静的コード解析ツールです。2015年にオープンソースとして公開された **静的コード解析ツール「Infer」の機能の一部** として使用します。（2018年2月現在、BSDライセンス）

![](https://encrypted-tbn1.gstatic.com/images?q=tbn:ANd9GcQNnjEvzSGsqz5lrV3mFRgH13FcuDo3KoJx8IF30pf_XAauFWGSgF5yzsfw0Q)

2018年3月現在、厳選されたJavaツールのみが掲載されている[Awesome Java](https://github.com/akullpp/awesome-java/blob/master/README.md#code-analysis) にも、inferが紹介されています。

Facebookでは既にCI（継続的インテグレーション）としてRacerDを組み込んでおり、同社のAndroid版アプリでは1000件以上の並行性バグを検出しています。

---
- [Infer : RacerD | Infer](http://fbinfer.com/docs/racerd.html)
- [Facebook、競合状態検出ツール「RacerD」を公開 - Computerworldニュース：Computerworld](http://tech.nikkeibp.co.jp/it/atcl/idg/14/481542/102300429/)
- [Infer：人工知能を使った静的コードチェック](https://www.slideshare.net/mobile/f-hasegawa/infer-78986112)
- [Open-sourcing RacerD: Fast static race detection at scale | Engineering Blog | Facebook Code | Facebook](https://code.facebook.com/posts/293371094514305)
- [Facebook、マルチスレッドのコードを静的解析してデータ競合を検出する「RacerD」、オープンソースで公開。同社Androidアプリのリリース前に1000以上の問題を検出 - Publickey Smart Editionβ3](http://www.publickey1.jp/m/blog/17/facebookracerdandroid1000.html)
- [infer/LICENSE at master · facebook/infer · GitHub](https://github.com/facebook/infer/blob/master/LICENSE)

## Inferをインストールする

まずは静的コード解析ツール「Infer」をインストールします（本稿執筆時点のバージョンは0.13.1）。

### gitリポジトリをクローンする

任意のディレクトリで以下のコマンドを入力します。

```
$ git clone https://github.com/facebook/infer.git
```

### Dockerfileを書き換える

InferはJavaだけでなく、C, C++, Objective-Cにも対応しています（ただし、RacerDはJavaのみ）。本稿ではJavaの静的コード解析に必要な環境があれば十分であるため、Dockerfileを書き換えます。

Dockerイメージをインストールするためのファイルが格納されているディレクトリに移動します。

```
$ cd infer/docker
```

ディレクトリ構成は以下の通りです。

```
$ tree
.
├── Dockerfile
├── README.md
└── run.sh
```

Dockerfileを以下のように書き換えます。

**Dockerfile.origin（修正前）とDockerfile（修正後）の差分**

```
$ diff -u Dockerfile.origin Dockerfile
--- Dockerfile.origin	2018-02-22 09:47:10.504984404 +0000
+++ Dockerfile	2018-02-22 09:47:46.533118963 +0000
@@ -31,17 +31,8 @@

 # Compile Infer
 RUN OCAML_VERSION=4.05.0+flambda; \
-    cd /infer && ./build-infer.sh --opam-switch $OCAML_VERSION && rm -rf /root/.opam
+    cd /infer && ./build-infer.sh java --yes --opam-switch $OCAML_VERSION && rm -rf /root/.opam

 # Install Infer
 ENV INFER_HOME /infer/infer
 ENV PATH ${INFER_HOME}/bin:${PATH}
-
-ENV ANDROID_HOME /opt/android-sdk-linux
-WORKDIR $ANDROID_HOME
-RUN curl -o sdk-tools-linux.zip \
-      https://dl.google.com/android/repository/sdk-tools-linux-3859397.zip && \
-    unzip sdk-tools-linux.zip && \
-    rm sdk-tools-linux.zip
-ENV PATH ${ANDROID_HOME}/tools/bin:${PATH}
-RUN echo "sdk.dir=${ANDROID_HOME}" > /infer/examples/android_hello/local.properties
```

### Dockerイメージをインストールする

以下のシェルを実行し、Dockerイメージをインストールします。

```
./run.sh
```

本稿で使用した環境では **インストールに20分ほどかかりました。**

### Inferの動作確認をする

以下のコマンドを入力して、InferのDockerイメージからコンテナを生成します。

```
$ docker run -v /home/user/project:/mnt --rm -it infer
```

[Running Infer in Docker · facebook/infer Wiki · GitHub](https://github.com/facebook/infer/wiki/Running-Infer-in-Docker)

マウントした以下のディレクトリに移動します。

```
# cd mnt
```

Inferのウェブページ（[Hello, World! | Infer](http://fbinfer.com/docs/hello-world.html)）に掲載されている`Hello.java`を`mnt`ディレクトリに作成します。

以下のコマンドを入力することで`Hello.java`の静的コード解析が可能となります。

```
# infer run -- javac Hello.java
Capturing in javac mode...
Found 1 source file to analyze in /mnt/infer-out
Starting analysis...

legend:
  "F" analyzing a file
  "." analyzing a procedure

F..

Found 1 issue

Hello.java:5: error: NULL_DEREFERENCE
  object `s` last assigned on line 4 could be null and is dereferenced at line 5.
  3.       int test() {
  4.           String s = null;
  5. >         return s.length();
  6.       }
  7.   }


Summary of the reports

  NULL_DEREFERENCE: 1
```

## 並行性バグのコードでRacerDを試してみる

それでは本題である並行性バグの解析を始めてみたいと思います。

RacerDは**「ロック」または「@ThreadSafeアノテーション」** を用いたJavaコードを対象に静的解析をします。@ThreadSafeアノテーションのjarファイルはJCIPのウェブサイト（[Java Concurrency in Practice](http://jcip.net/)）からダウンロードできます。

本稿では、`mnt`ディレクトリに以下のサンプルコードを作成しました。

```
.
|-- Hello.java
|-- LongContainer.java
|-- UnsafeSequence.java
|-- jcip-annotations.jar
```

### 例題1. スレッドセーフでない順序数生成メソッド

まずはJCIPに掲載されている違反コードを使ってRacerDを試してみます。

#### 違反コード

[Java Concurrency in Practice - Code Listings](http://jcip.net/listings.html)

```
package net.jcip.examples;

import net.jcip.annotations.*;

/**
 * UnsafeSequence
 *
 * @author Brian Goetz and Tim Peierls
 */

@ThreadSafe
public class UnsafeSequence {
    private int value;

    /**
     * Returns a unique value.
     */
    public int getNext() {
        return value++;
    }
}
```

 上記コードの問題点は、タイミングが悪ければgetNextを呼んだ二つのスレッドが **同じ値** を受け取ってしまうことです。`nextValue++`のようなインクリメントの記述は一つの操作のように見えますが、実際は以下の三つの操作を行なっています。

1. 値を読む
2. 1を加える
3. 新しい値を書き出す

そのため、複数のスレッドのタイミングによっては
二つのスレッドが同時に同じ値を読み、同じように1を加えることで、二つのスレッドが同じ値を返してしまう可能性があります。

#### 解析結果：「THREAD_SAFETY_VIOLATION」を検出

```
infer --racerd-only -- javac -classpath jcip-annotations.jar UnsafeSequence.java
Capturing in javac mode...
Found 1 source file to analyze in /mnt/infer-out
Starting analysis...

legend:
  "F" analyzing a file
  "." analyzing a procedure

F..

Found 1 issue

UnsafeSequence.java:19: error: THREAD_SAFETY_VIOLATION
  Unprotected write. Non-private method `net.jcip.examples.UnsafeSequence.getNext` writes to field `&this.net.jcip.examples.UnsafeSequence.value` outside of synchronization.
 Reporting because the current class is annotated `@ThreadSafe`, so we assume that this method can run in parallel with other non-private methods in the class (incuding itself).
  17.        */
  18.       public int getNext() {
  19. >         return value++;
  20.       }
  21.   }


Summary of the reports

  THREAD_SAFETY_VIOLATION: 1
```

### 例題2. 64ビット値の読み書き

[VNA05-J. 64ビット値の読み書きはアトミックに行う](https://www.jpcert.or.jp/java-rules/vna05-j.html)

> プログラミング言語Javaメモリモデルでは、 **volatileでないlong値やdouble値への単一の書込みは、それぞれ32ビットずつの二つの書込みとして扱われる。** 結果的に、ある64ビット値の書込みの最初の32ビットと、他の書込みによる次の32ビットの組み合わせをスレッドが参照しうる。

> この動作が原因で、スレッドセーフであることが要求されるコードにおいて、未確定の値が読み取られてしまうかもしれない。それゆえ、マルチスレッドプログラムでは、64ビット値の読み書きがアトミックに行われることを保証しなくてはならない。

#### 違反コード

> 以下の違反コードで、あるスレッドがassignValue()メソッドを繰り返し呼び出し、別のスレッドがprintLong()メソッドを繰り返し呼び出す場合、 **printLong()メソッドは0でも引数jの値でもないiの値を出力することがある。**

```
import net.jcip.annotations.*;

@ThreadSafe
class LongContainer {
  private long i = 0;

  void assignValue(long j) {
    i = j;
  }

  void printLong() {
    System.out.println("i = " + i);
  }
}
```

#### 解析結果：「THREAD_SAFETY_VIOLATION」を検出
```
infer --racerd-only -- javac -classpath jcip-annotations.jar LongContainer.java
Capturing in javac mode...
Found 1 source file to analyze in /mnt/infer-out
Starting analysis...

legend:
  "F" analyzing a file
  "." analyzing a procedure

F...

Found 2 issues

LongContainer.java:9: error: THREAD_SAFETY_VIOLATION
  Unprotected write. Non-private method `LongContainer.assignValue` writes to field `&this.LongContainer.i` outside of synchronization.
 Reporting because the current class is annotated `@ThreadSafe`, so we assume that this method can run in parallel with other non-private methods in the class (incuding itself).
  7.   
  8.     void assignValue(long j) {
  9. >     i = j;
  10.     }
  11.   

LongContainer.java:13: error: THREAD_SAFETY_VIOLATION
  Read/Write race. Non-private method `LongContainer.printLong` reads without synchronization from `&this.LongContainer.i`. Potentially races with writes in method `void LongContainer.assignValue(long)`.
 Reporting because the current class is annotated `@ThreadSafe`, so we assume that this method can run in parallel with other non-private methods in the class (incuding itself).
  11.   
  12.     void printLong() {
  13. >     System.out.println("i = " + i);
  14.     }
  15.   }


Summary of the reports

  THREAD_SAFETY_VIOLATION: 2
```

## まとめ

スレッドセーフに使いたいクラスは明示的に`@ThreadSafe`アノテーションを付与する必要がありますが、RacerDによる並行性バグの解析はかなり効果的だと感じました。