Automatically Verifying and Reproducing Event-Based Races in ...

Automatically Verifying and Reproducing Event-Based Races in ...

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

Recently Viewed Presentations

  • Philosophical Research: - University of Idaho

    Philosophical Research: - University of Idaho

    Philosophical Research: "What is this mumbo, jumbo stuff?" What most people think: Poorly understood and not highly valued…. Why? Rise in empirical science onset of related doubts about reflective, reason-based procedures lack of consensus among contemporary philosophers about proper research...
  • Periodic Relationships Among the Elements

    Periodic Relationships Among the Elements

    Periodic Relationships Among the Elements Chapter 7 Periodic Relationships Among the Elements Chapter 7 When the Elements Were Discovered ns1 ns2 ns2np1 ns2np2 ns2np3 ns2np4 ns2np5 ns2np6 d1 d5 d10 4f 5f Ground State Electron Configurations of the Elements Classification...
  • Cybersecurity as a Business Differentiator February 28, 2017

    Cybersecurity as a Business Differentiator February 28, 2017

    CybersecurityA critical part of a company's business strategy. Board level engagement, business driven strategy. Risk based approach is key — threats vary according to industry, but all industries are vulnerable
  • Chapter 10 - Protein Synthesis: Transcription and Translation

    Chapter 10 - Protein Synthesis: Transcription and Translation

    RNA . polymerase. recognizes a specific base sequence in the DNA called a . promoter. and binds to it. The promoter identifies the start of a gene, which strand is to be copied, and the direction that it is to...
  • MAps - GitHub Pages

    MAps - GitHub Pages

    Maps. Maps allow for the possibility of keys in a key-value to appear only once in a collection. In syntax, creating a map is similar to how we create lists and sets. With maps though, the Key is the value...
  • Primary Helpers   Thank you for downloading this product.

    Primary Helpers Thank you for downloading this product.

    Thank you for downloading this product. If you should have any questions please email me at the following address: [email protected]
  • CSE 590ST Statistical Methods in Computer Science

    CSE 590ST Statistical Methods in Computer Science

    Probability: Calculus for dealing with nondeterminism and uncertainty Cf. Logic Probabilistic model: Says how often we expect different things to occur Cf. Function What's in It for Computer Scientists? Logic is not enough The world is full of uncertainty and...
  • Branston Junior Academy Topic Planning Topic: Extreme Earth

    Branston Junior Academy Topic Planning Topic: Extreme Earth

    compare and group together a variety of everyday materials on the basis of whether they are attracted to a magnet, and identify some magnetic materials. ... pulleys and gears, allow a smaller force to have a greater effect. Computing: National...