DroidRacer: A Dynamic Tool for Race Detection in Android Applications

1. Race Detection for Android Applications Pallavi Maiya , Aditya Kanade (Indian Institute of Science) Rupak Majumdar (Max Planck Institute for Software Systems) PLDI 2014

2. Popularity of Android Applications 2 Million+ Android apps in the market Billions of downloads

3. Our Contributions Formalizing concurrency semantics of Android applications Encoding happens-before relation for them Algorithm to detect and categorize data races Environment modeling to reduce false positives A dynamic tool to detect data races ( DroidRacer ) Performs systematic testing Identified potential races in popular applications like 3

4. Android Concurrency Model Multithreading constructs: threads, synchronization Dynamic thread creation (fork) Lock unlock, join, notify wait Asynchrony constructs: task queues, posting asynchronous tasks Threads may be associated with task queues Any thread can post an asynchronous task to a task queue Tasks may be associated with timeouts or posted to front-of-queue Tasks executed in FIFO order Atomic execution of asynchronous tasks 4

5. public class MainActivity extends Activity { int X; protected void onCreate( ){ Runnable r = new Runnable( ){ public void run( ){ X = 2; runOnUiThread(new Runnable( ){ public void run( ){ System.out.println(X); } }); } }; Thread t = new Thread(r); t.start( ); X = 1; } protected void onDestroy( ){ X = -1; } } 5 Main thread (mt) begin(mt,onCreate) fork(mt,t) write(mt,X) end(mt,onCreate) t write(t,X) post(t,run,mt) begin(mt,run) read(mt,X) end(mt,run) begin(mt,onDestroy) write(mt,X) end(mt,onDestroy) System process DESTROY ACTIVITY onCreate run onDestroy Application process Concurrency Semantics binder thread (bt) post(bt,onCreate,mt) LAUNCH ACTIVITY post(bt,onDestroy,mt) Task Queue

6. Single-threaded Race 6 Main thread (mt) begin(mt,onCreate) fork(mt,t) write(mt,X) end(mt,onCreate) t write(t,X) post(t,run,mt) begin(mt,run) read(mt,X) end(mt,run) begin(mt,onDestroy) write(mt,X) end(mt,onDestroy) binder thread (bt) post(bt,onCreate,mt) post(bt,onDestroy,mt) Unordered conflicting memory operations on the same thread Non-deterministic ordering of asynchronous tasks Sources of non-determinism Thread interleaving Re-ordering of asynchronous tasks

7. Race Detection : Happens-before Reasoning Thread-local ordering Total order between all operations on a thread (program order) Total order only between operations on a thread with no task queue Total order between all operations in the same asynchronous task Inter-thread ordering FORK happens-before init of newly forked thread Thread exits before JOINing to another thread UNLOCK happens-before a subsequent LOCK on the same monitor 7 without Asynchrony Multi-threading with Asynchrony ( e.g. Android ) (+ additional rules) (+ additional rules)

8. Happens-before Relation for Android Applications 8 POST FORK JOIN ASYNC-PO NO-Q-PO Main thread (mt) begin(mt,onCreate) fork(mt,t) write(mt,X) end(mt,onCreate) t write(t,X) post(t,run,mt) begin(mt,run) read(mt,X) end(mt,run) begin(mt,onDestroy) write(mt,X) end(mt,onDestroy) binder thread (bt) post(bt,onCreate,mt) post(bt,onDestroy,mt) FIFO NO-PRE LOCK TRANSITIVITY

9. Environment Modeling 9 Main thread (mt) begin(mt,onCreate) fork(mt,t) write(mt,X) end(mt,onCreate) t write(t,X) post(t,run,mt) begin(mt,run) read(mt,X) end(mt,run) begin(mt,onDestroy) write(mt,X) end(mt,onDestroy) System process DESTROY ACTIVITY Application process binder thread (bt) post(bt,onCreate,mt) LAUNCH ACTIVITY post(bt,onDestroy,mt) ? Track system process and IPC Model the effect of the environment in ordering of operations

10. Environment Modeling 10 Main thread (mt) begin(mt,onCreate) fork(mt,t) write(mt,X) end(mt,onCreate) t write(t,X) post(t,run,mt) begin(mt,run) read(mt,X) end(mt,run) begin(mt,onDestroy) write(mt,X) end(mt,onDestroy) System process DESTROY ACTIVITY Application process binder thread (bt) post(bt,onCreate,mt) LAUNCH ACTIVITY post(bt,onDestroy,mt) enable(_, m) HB post (_, m) Ordering due to environment modeled using enable operation enable(mt,onDestroy)

11. DroidRacer Algorithm Acyclic graph representation of happens-before constraints Nodes: operations in trace Edges: happens-before relation Saturate the graph with happens-before rules Report conflicting memory operations with no happens-before relation as race Debugging assistance Method stack, high level events Classification of reported data races 11

12. Classification of Data Races Type of data race Sources of non-determinism Multi-threaded race Thread interleaving Single- threaded race Co-enabled High level events causing the conflicting operations are unordered Cross-posted Non-deterministic interleaving of two threads posting tasks to the same target thread Delayed At least one of the conflicting operations is due to a task with timeout . This breaks FIFO . 12

13. DroidRacer Dynamic Data Race Detection Tool UI Explorer Systematic Testing Depth first traversal with backtracking Supports click, long press, data input, rotate screen . Trace Generator Logs concurrency constructs and read-writes Logs debug information Race Detector Happens-before graph constructed on generated trace Categorization of data races Android core library and Dalvik virtual machine of Android 4.0 instrumented. 13

14. Experimental Evaluation Trace Statistics* Applications Trace length Fields Threads (w/o Q) Threads (w/ Q) Async. tasks Aard Dictionary Music Player My Tracks Messenger Tomdroid Notes FBReader Browser OpenSudoku K-9 Mail SGTPuzzles 1k 5k 7k 10k 10k 10k 19k 25k 30k 39k 189 521 573 845 413 322 963 334 1296 566 2 3 11 11 3 14 13 5 7 4 1 2 7 4 1 1 4 1 2 1 58 62 164 99 348 119 103 45 689 80 Remind Me Twitter Adobe Reader Facebook Flipkart 10k 17k 34k 52k 157k 348 1362 1267 801 2065 3 21 17 16 36 1 5 4 3 3 176 97 226 16 105 14 * Representative trace for each of the tested application

15. Experimental Evaluation Data Races in given Trace Applications Multi-threaded Cross-posted Co-enabled Delayed Aard Dictionary Music Player My Tracks Messenger Tomdroid Notes FBReader Browser OpenSudoku K-9 Mail SGTPuzzles TOTAL 1 ( 1 ) 0 1 ( 0 ) 1 ( 1 ) 0 1 ( 0 ) 2 ( 1 ) 1 ( 0 ) 9 ( 2 ) 11 ( 10 ) 27 ( 15 ) 0 17 ( 4 ) 2 ( 1 ) 15 ( 5 ) 5 ( 2 ) 22 ( 22 ) 64 ( 2 ) 1 ( 0 ) 0 21 ( 8 ) 147 ( 44 ) 0 11 ( 10 ) 1 ( 0 ) 4 ( 3 ) 1 ( 0 ) 14 ( 4 ) 0 0 1 ( 0 ) 0 32 ( 17 ) 0 4 ( 0 ) 0 2 ( 2 ) 0 0 0 0 0 0 6 ( 2 ) Remind Me Twitter Adobe Reader Facebook Flipkart 0 0 34 12 12 21 20 73 10 152 33 7 0 0 84 0 4 9 0 30 15 X ( Y ) : Races reported ( True Positives ) True positives: 37% Bad behaviour

16. Related Work 16 Race detection for multi-threaded programs Savage et al., TOCS 97 (locksets) FastTrack by Flanagan and Freund, PLDI 09 (vector-clocks) Pozniansky and Schuster, Concurr. Comput.: Pract. Exper. 07 (hybrid technique) Race detection for single-threaded event-driven programs Petrov et al., PLDI 12 Raychev et al., OOPSLA 13 Zheng et al., WWW 11 Race detection for multi-threaded and asynchronous programs Kahlon et al., FSE 09 (for C programs only reports multithreaded races) Hsio et al., PLDI 14 (for Android applications)

17. Conclusions Formalization of Android concurrency model and happens-before rules to capture causality in this model. Implemented DroidRacer, a dynamic data race detection tool for Android applications. Future Work Transitive closure slows down on long traces device faster algorithms to infer happens-before relation (e.g., vector clocks) Reduce false positives : ad-hoc synchronization, concurrency operations by native threads, better environment model 17

18. DroidRacer webpage http://www.iisc-seal.net/droidracer

19.

20. Backup Slides

21. Happens-before Relation for Android Applications Thread-local rules (HB-S): ordering between operations on the same thread. t : thread m1, m2 : asynchronous tasks [NO-Q-PO] Total order between all operations only on threads without task queues. [ASYNC-PO] Total order between all operations in asynchronous task. [POST-ST] post(t, m1, t) HB-S begin(t, m1) [FIFO] If post(_, m1, t) HB-S post(_, m2, t) then task m1 is executed before task m2. [NO-PRE] a : an operation in task m1 If a HB-S begin(t, m2) then end(t, m1) HB-S begin(t, m2) 21 Transitive closure

22. Happens-before Relation for Android Applications Inter-thread rules (HB-M): ordering between operations on different threads. t1, t2 : thread m : asynchronous task [FORK] Fork operation HB-M init of newly forked thread. [JOIN] A thread completes execution before joining to another thread. [LOCK] Unlock HB-M subsequent lock on the same monitor. [POST-MT] post(t1, m, t2) HB-M begin(t2, m) 22 Transitive closure (using both HB-M and HB-S)

23. Nave transitive closure misses races! 23 Main thread (mt) begin(mt,onE1) lock(mt,l) write(mt,X) end(mt,onE1) event e1 unlock(mt,l) Worker thread (wt) begin(wt,task1) lock(wt,l) write(wt,Y) end(wt,task1) unlock(wt,l) begin(mt,onE2) lock(mt,l) read(mt,X) end(mt,onE2) unlock(mt,l) event e2

24. Environment Modeling - Activity 24 Launched onCreate() onStart() onResume() onPause() Running onStop() onDestroy() Destroyed onRestart()