Aplikasi Android Facebook memiliki masalah performa. Thread UI tenggelam dalam pekerjaan, tetapi memindahkan kode ke thread latar belakang berarti race condition. Crash di produksi. Pengguna marah.

Mereka tidak menyelesaikan ini dengan code review yang lebih baik atau lebih banyak pengujian. Mereka membangun static analyzer, RacerD, yang menggunakan abstract interpretation untuk membuktikan apakah dua thread dapat menyentuh state yang sama secara bersamaan. Ini memeriksa jutaan baris Java. Menemukan ribuan race nyata sebelum dikirimkan. Dan ini dilakukan dengan sengaja salah dalam beberapa hal.

Race condition adalah masalah kardinalitas

Thread utama Android menangani menggambar, input, dan setiap mutasi View. Terlalu banyak di sana dan aplikasi Anda kehilangan frame. Perbaikannya tampak jelas: offload pekerjaan ke AsyncTask, HandlerThread, atau coroutine.

Masalahnya adalah toolkit UI Android tidak thread-safe. Memutasi TextView dari thread latar belakang melempar exception. Tetapi pembunuh sebenarnya adalah race diam-diam. Dua thread membaca dan menulis state model bersama. Interleaving yang meledak hanya terjadi pada perangkat pengguna tertentu, pada hari Selasa, dengan jaringan lambat.

Alat deteksi dinamis dapat menangkap race, tetapi hanya pada jalur eksekusi yang benar-benar Anda temui dalam pengujian. Codebase Facebook terlalu besar dan ruang state terlalu luas. Mereka perlu mengetahui race tanpa menjalankan kode.

Abstract interpretation, yang agresif disederhanakan

RacerD dibangun di atas abstract interpretation, teknik analisis program statis. Alih-alih melacak state program yang tepat (mustahil untuk codebase besar), Anda membangun domain abstrak yang lebih sederhana dan membuktikan properti tentangnya.

Contoh klasik adalah analisis interval. Anda tidak melacak nilai pasti x. Anda melacak apakah positif, negatif, atau nol. Analisisnya bersifat aproksimatif, tetapi scalable.

RacerD menerapkan ide ini pada concurrency. Ini melacak tiga hal per akses memori:

  1. Thread mana yang melakukan akses (thread UI, thread latar belakang, atau tidak diketahui)
  2. Lock mana, jika ada, yang melindunginya
  3. Jalur akses (misalnya, this.mUser.name)

Jika dua akses ke jalur yang sama dapat terjadi pada thread yang berbeda, dan setidaknya satu adalah tulisan, dan tidak satu pun dilindungi oleh lock bersama, RacerD melaporkan race.

Ini terdengar seharusnya tidak dapat ditangani untuk aplikasi multi-juta-baris. Memang begitu, jika mereka mencoba memodelkan semuanya dengan tepat.

Facebook membuat RacerD secara sengaja unsound. Ini mengabaikan generics Java, refleksi, virtual dispatch dalam beberapa kasus, dan kompleksitas aliasing yang akan membuat analisis kubik atau lebih buruk. Matematikanya brutal, jadi mereka curang. Hasilnya: kompleksitas waktu linier per metode, dan kemampuan untuk menganalisis aplikasi Facebook dalam waktu kurang dari satu jam.

Kepemilikan thread dan kontrak @ThreadSafe

Analisis berfungsi dengan menganotasi metode dengan batasan thread. Pertimbangkan cuplikan ini:

@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 melihat getUser dan setUser dianotasi dengan @AnyThread. Ini mencatat bahwa mCurrentUser diakses di bawah mLock dalam kedua kasus. Tidak ada race yang dilaporkan.

Sekarang hapus blok synchronized:

@AnyThread
public User getUser() {
    return mCurrentUser;  // baca tidak tersinkronisasi
}

@AnyThread
public void setUser(User user) {
    mCurrentUser = user;  // tulis tidak tersinkronisasi
}

RacerD menandai race pada mCurrentUser. Dua metode @AnyThread mengakses field yang sama. Satu menulis. Tidak ada lock bersama. Ini adalah laporan yang tepat dan dapat ditindaklanjuti.

Anonimasi menggerakkan analisis. @UiThread berarti metode berjalan hanya pada thread utama. @WorkerThread berarti latar belakang. Jika metode @WorkerThread dan metode @UiThread keduanya menyentuh this.mData tanpa sinkronisasi, itu hanya race jika salah satu dari mereka menulis. RacerD mengetahui ini karena melacak baca versus tulis.

Trade-off: unsoundness sebagai imbalan adopsi

RacerD tidak membuktikan tidak adanya race. Ia membuktikan adanya race yang mungkin terjadi. Perbedaan ini penting.

Sebuah analyzer yang sound akan menjamin bahwa jika tidak ada race yang dilaporkan, tidak ada race yang ada. Mencapai soundness untuk Java yang concurrent memerlukan pemodelan memory model, semua kemungkinan interleaving thread, dan aliasing pointer dengan tepat. Tidak ada tool yang melakukan ini pada skala Facebook dalam waktu yang wajar.

Dengan memilih unsoundness, RacerD menerima false negative. Beberapa race nyata lolos. Taruhannya adalah menemukan 90% race secara otomatis, setiap malam, di setiap diff, lebih berharga daripada menemukan 100% race yang tidak pernah.

Tingkat false positive harus tetap rendah. Tool yang menangis serigala pada setiap metode ketiga dinonaktifkan. RacerD menjaga false positive di bawah 10% dengan bersikap konservatif tentang apa yang dilaporkan. Ini tidak menandai race yang melibatkan tipe immutable yang thread-safe. Ini memahami bahwa field final aman setelah konstruksi. Ini memodelkan pola sinkronisasi umum.

Bagaimana Facebook men-deploy-nya

RacerD berjalan pada setiap diff kode sebelum mendarat. Ini adalah bagian dari Infer, framework analisis statis open source mereka. Insinyur melihat laporan race di Phabricator (tool code review mereka) bersama hasil unit test.

Alur kerjanya terlihat seperti ini:

  1. Insinyur mengirimkan diff yang menambahkan akses thread latar belakang ke state bersama.
  2. Infer menjalankan RacerD pada metode yang dimodifikasi.
  3. Jika race ditemukan, diff mendapat sinyal pemblokiran. Insinyur harus memperbaikinya atau secara eksplisit menekannya.

Ini menggeser beban ke kiri. Race condition tertangkap selama peninjauan, bukan dalam crash produksi.

Facebook open-sourced Infer, termasuk RacerD, pada tahun 2015. Anda dapat menjalankannya hari ini di Java, C, C++, dan Objective-C.

Menjalankan Infer pada kode Android Anda sendiri

Jika Anda ingin mencoba ini, Infer adalah satu binary. Instal melalui Homebrew atau unduh release:

brew install infer

Jalankan pada proyek Gradle Anda:

infer run -- ./gradlew build

Infer akan mengompilasi proyek Anda dan menganalisis bytecode. Untuk deteksi race secara khusus, tambahkan anonimasi thread ke kode Anda. Infer mengirimkan anonimasi dalam 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 melaporkan: race pada mToken
    }
}

Laporan memberi tahu Anda file, baris, dan akses yang bertentangan. Perbaiki dengan sinkronisasi, referensi atomic, atau dengan memindahkan state ke model yang terbatas pada thread.

Di mana ini runtuh

RacerD bukanlah peluru perak. Ia kesulitan dengan race melalui alias yang tidak jelas, race dalam kode native, dan race yang diperantarai oleh framework yang tidak ia modelkan. Jika Anda menggunakan RxJava atau coroutine dengan thread hopping yang kompleks, anonimasi thread mungkin tidak menangkap konteks eksekusi yang sebenarnya.

Ini juga memerlukan disiplin. Jika Anda berbohong dalam anonimasi Anda, analisis berbohong kembali. Menandai metode @UiThread ketika sebenarnya dipanggil dari thread latar belakang mengalahkan tujuannya.

Pelajaran sebenarnya

Wawasan Facebook bukan bahwa abstract interpretation itu ajaib. Melainkan bahwa analisis yang sedikit salah, yang dijalankan secara berkelanjutan pada setiap perubahan, mengalahkan analisis sempurna yang tidak pernah dijalankan.

Jika Anda membangun kode Android yang concurrent saat ini, Anda tidak perlu membangun RacerD sendiri. Anda dapat mengadopsi Infer, atau Anda dapat menerapkan prinsip yang sama: modelkan thread mana yang menyentuh state mana, berlakukan dengan analisis statis, dan perlakukan thread safety sebagai masalah compile-time, bukan debugging produksi.

Pengguna Anda tidak akan berterima kasih atas race yang Anda cegah. Mereka hanya tidak akan menghapus aplikasi Anda.