Automatically Verifying and Reproducing Event-Based Races in Android Apps Yongjian Hu Iulian Neamtiu Arash Alavi Rise of Event-Driven Systems Mobile apps Web apps Event-based races are prevalent and may cause harmful result: crash, incorrect results, etc. 2 Outline Motivation of Event-Based Race Most prevalent concurrency errors in Android [Maya et al., PLDI14, etc.] Prior Work of Event-Based Race Detectors Imprecise: mostly false positives & benign races Not able to reproduce the race
Our Approach: ERVA Replay based approach to verify race Event flipping to alternate schedule Filter benign races by state comparison Experiment Result 3% true positive harmful races in out work Example of Event-Based Race Done! Syncing Back Example of Event-Based Race Syncing
! h s a Cr Back State-of-art Race Detectors for Event Driven Systems Web Applications WebRacer, PLDI12 EventRacer for JavaScript, OOPSLA13 Mobile Applications(Android) DroidRacer, PLDI14 CAFA, PLDI14 EventRacer for Android, OOPSLA15 Instrumented Framework App Execution
Happens Before Graph Building Race Detection Report Filtering and Generation Limitation of State-of-art Race Detector False positives DroidRacer: FP rate is 63% CAFA: FP rate is 21.7%, benign rate 27.8% EventRacer reduces FP by race coverage, but still have FPs in our experiment Cannot distinguish between harmful &benign races Manual efforts to check the race report Cannot reproducing races
False Positive Type 1: Imprecise Android Model EventRacer reports a harmful race in AnyMemos RecentListFragment onCreateView() { mHandler = new Handler(); mAdapter = new ArrayAdapter(); } onResume() { Thread thrd = new Thread() { public void run() { // query database operation mHandler.post(new Runnable() { public void run() { mAdapter.clear(); for (RecentItem ri : database) mAdapter.insert(ri); } }); } } thrd.start(); } Looper
Looper Thread Thread onCreate View onResume Runnable Thread Thread False Positive Type 2: Implicit Happens-Before Relation One race reported in CoolReader apps CoolReaderActivity Looper Looper Thread Thread At om ici t
y [CoolReaderActivity.java] onStart() { Delayed post time = 0 waitForCRDService(new Runnable() { public void run() { post(Runnable r) Service.getHistory().loadFromDB(); new CRRootView(); post(Runnable r) } Delayed post time = 0 }); } [History.java] onRecentBookListLoaded(List list) { mBooks = list; } [History.java] getOrLoadRecentBooks() {
if (mBooks != null && mBooks.size() > 0) // update mBooks. } onStart onRecentBookListLoaded getOrLoadRecentBooks Benign Race Type 1: Ad-hoc Synchronization One race reported in Volley HTTP library public class ImageLoader { private Handler mHandler = new Handler(); private Runnable mRunnable; private void batchResponse() { if (mRunnable == null) { mRunnable = new Runnable() { public void run() { // deliver batched request mRunnable = null; }
} mHandler.post(mRunnable); } } } Looper Looper Thread Thread batchResponse Runnable.run() batchResponse Benign race: read/write access protected by the control flow Benign Race Type 2: No External Visible State Difference One race reported in AnyMemo apps QACardActivity startLoading() {
for (Loader loader : mLoaders) { loaderManager.initLoader(loader); nRunningLoader++; } } checkAllLoaderCompleted() { nRunningLoader--; if (nRunningLoader <= 0) { onAllLoaderComplete(); } } checkAllLoaderCompleted() { nRunningLoader--; if (nRunningLoader <= 0) { onAllLoaderComplete(); } } Thread-1 Thread-1 Thread-2 Thread-2
onLoadFinished onLoadFinished Benign race: no state difference Our Approach ERVA: Eventrace Reproducer and Verifier for Android Race detection phase Race verification phase Race Report False positive Input log Event Racer Input
capture Event capture Benign race Harmful race App state comparison Input replay EDG Event flipping Replay platform (emulator or phone)
Instrumented platform (emulator) on s xecuti e le p multi single ex ecution App ERVA Details Input Capture and Replay Input, sensors, IPC, threading events are captured by VALERA(OOPSLA15) Event Dependency Graph(EDG) Causal relationship between events (strong HB relations)
Event Flipping Leverage VALERAs deterministic schedule replay User defined order of event execution which is allowed by EDG State Recording and Comparison Externally visible state(EVS) EVS = All GUI states(layout & contents) + shared preference data EVS is extensible to dump customized state Race Verification Race Verification: FP Race Type 1 onCreateView() { mHandler = new Handler(); mAdapter = new ArrayAdapter(); } onResume() { Thread thrd = new Thread() { public void run() { // query database operation mHandler.post(new Runnable() { public void run() { mAdapter.clear();
for (RecentItem ri : database) mAdapter.insert(ri); } }); } } thrd.start(); } Looper Looper Thread Thread Thread Thread onCreate View Dead lock!!! onResume Runnable
Race Verification: FP Type 2 Analyze the trace [CoolReaderActivity.java] onStart() { waitForCRDService(new Runnable() { public void run() { post1(Runnable r1, delay1=0) Service.getHistory().loadFromDB(); new CRRootView(); post2(Runnable r2, delay2=0) } }); } [History.java] onRecentBookListLoaded(List list) { mBooks = list; } [History.java] getOrLoadRecentBooks() { if (mBooks != null && mBooks.size() > 0) // update mBooks. }
Looper Looper Thread Thread onStart onRecentBookListLoaded getOrLoadRecentBooks post1 < post2 && delay1 == delay2 Race Verification: Benign Type 1 One race reported in Volley HTTP library public class ImageLoader { private Handler mHandler = new Handler(); private Runnable mRunnable; private void batchResponse() { if (mRunnable == null) { mRunnable = new Runnable() { public void run() {
// deliver batched request mRunnable = null; } } mHandler.post(mRunnable); } } Looper Looper Thread Thread batchResponse Runnable.run() Flippable batchResponse } Different branch condition executed in flipped schedule Racy read write disappear in new schedule
Race Verification: Benign Type 2 One race reported in AnyMemo apps QACardActivity startLoading() { for (Loader loader : mLoaders) { loaderManager.initLoader(loader); nRunningLoader++; } } checkAllLoaderCompleted() { nRunningLoader--; if (nRunningLoader <= 0) { onAllLoaderComplete(); } } Thread-1 Thread-1 Thread-2 Thread-2 onLoadFinished
Flippable checkAllLoaderCompleted() { nRunningLoader--; if (nRunningLoader <= 0) { onAllLoaderComplete(); } } onLoadFinished Benign race: no state difference External visible state dumping and comparison Experimental Result High priority: races in app code Normal priority: races in framework but invoked from app Related Work Race Detection Multi-threaded races Various works: static, dynamic or hybrid approaches
Event-based races Web apps: WebRacer, EventRacer Mobile apps: DroidRacer, CAFA, EventRacer Android Race Classification Multi-threaded races Instruction-level replay, Narayanasamy et al., PLDI07 Symbolic execution, Kasikci et al., ASPLOS12 Related Work Model checking for event driven systems Systematically explore all schedules for find concurrency errors R4: OOPSLA16, for web applications Dynamic partial order reduction + bounded conflict reversal AsyncDroid: CAV15, for Android applications Delay-bounded prioritized systematic exploration Model checking may have scalability problems Huge number of events, exponential schedules EVRA can help model checkers Use EDG to filter unreachable schedules Use EVS to verify harmful and benign races
Conclusions Event-based races Most prevalent concurrency errors Prior works on event-based race detectors Imprecise, mostly false positives & benign races Not able to reproduce races Our approach: ERVA Replay based approach to verify race Event flipping to alternate schedule Filter benign races by state comparison Experiment result 3% true positive harmful races Thanks! Android Event Handling Thread Handler UI Thread
Looper Message Queue msg evt Thread msg Handler Hardware Events Deterministic Event Schedule: Recording UI Thread Message Queue Event Log
Looper A B C D 1 2 3 4 Deterministic Event Schedule: Replaying Reconciling different event orders between record and replay Controller = UI Thread 1243 Message Queue Event Log Looper
B D C A Pending Queue A B C D 1 2 3 4
