Facebook의 Android 앱에는 성능 문제가 있었다. UI 스레드가 작업에 압도당했지만, 코드를 백그라운드 스레드로 이동하면 race condition이 발생했다. 프로덕션의 크래시. 화난 사용자.

그들은 더 나은 코드 리뷰나 더 많은 테스트로 이를 해결하지 않았다. 그들은 RacerD라는 정적 분석기를 구축했다. 이는 abstract interpretation을 사용하여 두 스레드가 동시에 동일한 가변 상태에 접근할 수 있는지 증명한다. 수백만 줄의 Java를 검증했다. 수천 개의 실제 경쟁을 출하 전에 발견했다. 그리고 이는 일부러 몇 가지에서 틀림으로써 이루어졌다.

race condition은 기수 문제이다

Android의 메인 스레드는 그리기, 입력 및 모든 View 변경을 처리한다. 거기서 너무 많은 작업을 하면 앱이 프레임을 드롭한다. 해결책은 명백해 보인다: 작업을 AsyncTask, HandlerThread 또는 코루틴으로 오프로드한다.

문제는 Android의 UI 툴킷이 스레드 세이프하지 않다는 것이다. 백그라운드 스레드에서 TextView를 변경하면 예외가 발생한다. 하지만 진정한 킬러는 조용한 race condition다. 두 스레드가 공유 모델 상태를 읽고 쓴다. 폭발하는 인터리빙은 특정 사용자의 기기에서, 화요일에, 느린 네트워크에서만 발생한다.

동적 탐지 도구는 경쟁을 잡을 수 있지만, 테스트 중에 실제로 도달한 실행 경로에서만 가능하다. Facebook의 코드베이스는 너무 컸고 상태 공간이 너무 넓었다. 그들은 코드를 실행하지 않고 경쟁에 대해 알 필요가 있었다.

공격적으로 단순화된 abstract interpretation

RacerD는 정적 프로그램 분석 기법인 abstract interpretation을 기반으로 한다. 정확한 프로그램 상태를 추적하는 대신(대규모 코드베이스에서는 불가능), 더 단순한 추상 영역을 구축하고 그에 대한 속성을 증명한다.

고전적인 예는 구간 분석이다. x의 정확한 값을 추적하지 않는다. 양수인지, 음수인지, 또는 0인지 추적한다. 분석은 근사적이지만 확장된다.

RacerD는 이 아이디어를 동시성에 적용한다. memory access마다 세 가지를 추적한다:

  1. 어떤 스레드가 접근을 수행하는가 (UI 스레드, 백그라운드 스레드, 또는 알 수 없음)
  2. 어떤 락이, 있다면, 이를 보호하는가
  3. 접근 경로 (예: this.mUser.name)

동일한 경로에 대한 두 접근이 서로 다른 스레드에서 발생할 수 있고, 적어도 하나가 쓰기이며, 둘 다 공통 락에 의해 보호되지 않는 경우, RacerD는 경쟁을 보고한다.

이는 수백만 줄 규모의 앱에서 다룰 수 없어야 할 것처럼 들린다. 모든 것을 정확하게 모델링하려고 한다면 그럴 것이다.

Facebook은 RacerD를 의도적으로 unsound하게 만들었다. Java 제네릭, 리플렉션, 일부 경우의 가상 디스패치, 그리고 분석을 3차 이상으로 만들 복잡한 에일리어싱을 무시한다. 수학이 잔인하므로 그들은 속임수를 썼다. 결과: 메서드당 선형 시간 복잡도, 그리고 Facebook의 앱을 1시간 이내에 분석할 수 있는 능력.

스레드 소유권과 @ThreadSafe 계약

분석은 메서드에 스레드 제약 조건을 주석으로 다는 방식으로 작동한다. 다음 코드 조각을 고려하라:

@ThreadSafe
public class UserRepository {
    private User mCurrentUser;
    private final Object mLock = new Object();

    @AnyThread
    public User getUser() {
        synchronized (mLock) {
            return mCurrentUser;
        }
    }

    @AnyThread
    public void setUser(User user) {
        synchronized (mLock) {
            mCurrentUser = user;
        }
    }
}

RacerD는 getUser와 setUser가 @AnyThread로 주석 처리된 것을 본다. 두 경우 모두 mCurrentUser가 mLock 아래에서 접근된다는 점을 주목한다. 경쟁은 보고되지 않는다.

이제 synchronized 블록을 제거하라:

@AnyThread
public User getUser() {
    return mCurrentUser;  // 동기화되지 않은 읽기
}

@AnyThread
public void setUser(User user) {
    mCurrentUser = user;  // 동기화되지 않은 쓰기
}

RacerD는 mCurrentUser에서 경쟁을 플래그한다. 두 개의 @AnyThread 메서드가 동일한 필드에 접근한다. 하나는 쓴다. 공통 락이 없다. 이는 정확하고 실행 가능한 보고서다.

주석이 분석을 주도한다. @UiThread는 해당 메서드가 메인 스레드에서만 실행됨을 의미한다. @WorkerThread는 백그라운드를 의미한다. @WorkerThread 메서드와 @UiThread 메서드가 둘 다 동기화 없이 this.mData를 접근하면, 그중 하나가 쓰는 경우에만 경쟁이다. RacerD는 읽기 대 쓰기를 추적하므로 이를 알고 있다.

트레이드오프: 도입과의 교환으로서의 unsoundness

RacerD는 경쟁의 부재를 증명하지 않는다. 가능한 경쟁의 존재를 증명한다. 이 구분은 중요하다.

sound한 분석기는 경쟁이 보고되지 않으면 경쟁이 존재하지 않음을 보장할 것이다. 동시 Java에서 soundness를 달성하려면 메모리 모델, 모든 가능한 스레드 인터리빙, 그리고 정확한 포인터 에일리어싱을 모델링해야 한다. Facebook의 규모에서 합리적인 시간 내에 이를 수행하는 도구는 없다.

unsoundness를 선택함으로써 RacerD는 거짓 음성을 받아들인다. 일부 실제 경쟁이 누락된다. 내기는 매일 밤, 모든 diff에서 자동으로 90%의 경쟁을 찾는 것이 결코 100%를 찾지 못하는 것보다 가치 있다는 것이었다.

false positive률은 낮게 유지되어야 했다. 세 메서드마다 거짓 경보를 울리는 도구는 비활성화된다. RacerD는 보수적으로 보고하여 거짓 긍성을 10% 미만으로 유지했다. 스레드 세이프한 불변형을 포함하는 경쟁은 플래그하지 않는다. final 필드는 생성 후 안전하다는 것을 이해한다. 일반적인 동기화 패턴을 모델링한다.

Facebook이 어떻게 배포했는가

RacerD는 코드가 배포되기 전의 모든 코드 diff에서 실행되었다. 이는 Infer(그들의 오픈소스 정적 분석 프레임워크)의 일부였다. 엔지니어는 유닛 테스트 결과와 함께 코드 리뷰 도구인 Phabricator에서 경쟁 보고서를 보았다.

워크플로는 다음과 같았다:

  1. 엔지니어가 공유 상태에 대한 백그라운드 스레드 접근을 추가하는 diff를 제출한다.
  2. Infer가 수정된 메서드에서 RacerD를 실행한다.
  3. 경쟁이 발견되면 diff는 블로킹 신호를 받는다. 엔지니어는 이를 수정하거나 명시적으로 억제해야 한다.

이것은 부담을 왼쪽으로 이동시켰다. race condition은 프로덕션 크래시가 아닌 리뷰 중에 포착되었다.

Facebook은 2015년에 RacerD를 포함한 Infer를 오픈소스화했다. 오늘날 Java, C, C++, Objective-C에서 실행할 수 있다.

자체 Android 코드에서 Infer 실행하기

이것을 시도하려면 Infer는 단일 바이너리다. Homebrew를 통해 설치하거나 릴리스를 다운로드하라:

brew install infer

Gradle 프로젝트에서 실행하라:

infer run -- ./gradlew build

Infer는 프로젝트를 컴파일하고 바이트코드를 분석할 것이다. 경쟁 탐지를 위해 코드에 스레드 주석을 추가하라. Infer는 com.facebook.infer.annotation에 주석을 포함한다:

import com.facebook.infer.annotation.ThreadSafe;
import com.facebook.infer.annotation.AnyThread;
import com.facebook.infer.annotation.UiThread;

@ThreadSafe
public class SessionManager {
    private String mToken;

    @AnyThread
    public void setToken(String token) {
        mToken = token;  // Infer 보고: mToken에서 경쟁
    }
}

보고서는 파일, 줄 및 충돌하는 접근을 알려준다. 동기화, 원자적 참조, 또는 스레드 제한 모델로 상태를 이동하여 수정하라.

어디서 무너지는가

RacerD는 은탄이 아니다. 비명백한 별칭을 통한 경쟁, 네이티브 코드의 경쟁, 그리고 모델링하지 않는 프레임워크를 통해 중재되는 경쟁에 어려움을 겪는다. RxJava나 복잡한 스레드 홉핑이 있는 코루틴을 사용하는 경우, 스레드 주석이 실제 실행 컨텍스트를 포착하지 못할 수 있다.

또한 규율이 필요하다. 주석에서 거짓말을 하면 분석도 거짓말을 한다. 메서드가 실제로는 백그라운드 스레드에서 호출되는데 @UiThread로 표시하면 목적이 무산된다.

진정한 교훈

Facebook의 통찰은 abstract interpretation이 마법적이라는 것이 아니었다. 지속적으로 모든 변경에서 실행되는 약간 잘못된 분석이 결코 실행되지 않는 완벽한 분석을 이긴다는 것이었다.

오늘날 동시 Android 코드를 구축하고 있다면 RacerD를 직접 구축할 필요는 없다. Infer를 채택하거나, 동일한 원칙을 적용할 수 있다: 어떤 스레드가 어떤 상태에 접근하는지 모델링하고, 정적 분석으로 이를 강제하며, 스레드 안전성을 프로덕션 디버깅이 아닌 컴파일 타임 문제로 다루라.

사용자는 당신이 방지한 경쟁에 대해 감사하지 않을 것이다. 그들은 단순히 앱을 제거하지 않을 것이다.