João Lourenço Bruno Teixeira Ricardo Dias Ricardo Pinto Diogo Sousa Vasco Pessanha Center for Informatics and Information Technologies Computer Science Department New University of Lisboa, Portugal [email protected] Haifa Verification Conference, October 4, 2010 / 1 Agenda 1. Software Transactional Memory: what, why and how? 2. Detection of dataraces in Transactional Memory 3. Visualization of Transactional Memory computations 4. Final notes Haifa Verification Conference, October 4, 2010 / 2 The problem Multicores are here to stay Moore’s law Power consumption Home computers are multicore now Soon will be manycore Haifa Verification Conference, October 4, 2010 / 3 The problem Computers are data processing tools Data may be scattered among different computing units A set of data manipulations may be inter-related and inter-dependent The isolated change of a data item may leave the overall system in an inconsistent state Haifa Verification Conference, October 4, 2010 / 4 The problem Parallel programming is hard Multiple (asynchronous) control flows Concurrency control Synchronization Contention management Haifa Verification Conference, October 4, 2010 / 5 The problem For developing parallel code we need Parallel programming skills Programming languages constructs System / run-time support Techniques and tools for (parallel) program development Haifa Verification Conference, October 4, 2010 / 6 Programming Constructs / / System Support Blocking methodologies Locks Condition variables Semaphores Non-blocking algorithms e.g., java.util.concurrency Haifa Verification Conference, October 4, 2010 / 7 Locks: Insert in a Double Linked List Succ Succ Succ Succ Succ Pred Pred Pred Pred Pred Haifa Verification Conference, October 4, 2010 / 8 Locks: Insert in a Double Linked List Succ Succ Succ Succ Pred Pred Pred Pred Coarse grain locks public synchronized void insertNode (node, precedingNode) { node.prec = precedingNode; node.succ = precedingNode.succ; precedingNode.succ.prec = node; precedingNode.succ = node; } Haifa Verification Conference, October 4, 2010 / 9 Locks: Insert in a Double Linked List Succ Succ Succ Succ Pred Pred Pred Pred Fine grain locks public void insertNode (node, precedingNode) { synchronized (precedingNode) { synchronized (precedingNode.succ) { node.prec = precedingNode; node.succ = precedingNode.succ; precedingNode.succ.prec = node; precedingNode.succ = node; }}} Haifa Verification Conference, October 4, 2010 / 10 Fine grain locks lead to deadlocks Fine grain locks synchronized (precedingNode) { synchronized (precedingNode.succ) { … } } Deadlock synchronized (precedingNode.succ) { synchronized (precedingNode) { … } } Haifa Verification Conference, October 4, 2010 / 11 Problem: locking granularity Coarse grain locks Threads lock each other out Lower concurrency Fine grain locks Higher overhead Risk of deadlocks Lower maintainability Haifa Verification Conference, October 4, 2010 / 12 Example: bank account transfer Transfer 50! from account A to account B 1. read (A); 2. A = A – 50; 3. write (A); 4. Read (B); 5. B = B + 50; 6. write (B); Fault Haifa Verification Conference, October 4, 2010 / 13 Example — Atomicity Transfer 50! from account A to account B 1. read (A); 2. A = A – 50; 3. write (A); 4. Read (B); 5. B = B + 50; 6. write (B); Atomicity requirement — if the transaction fails after step 3 and before step 6, the system must ensure that that updates are not reflected in the database Haifa Verification Conference, October 4, 2010 / 14 Example — Consistency Transfer 50! from account A to account B 1. read (A); 2. A = A – 50; 3. write (A); 4. Read (B); 5. B = B + 50; 6. write (B); Consistency requirement — the sum of A and B is unchanged by the execution of the transaction Haifa Verification Conference, October 4, 2010 / 15 Example — Isolation Transfer 50! from account A to account B 1. read (A); 2. A = A – 50; 3. write (A); 4. Read (B); 5. B = B + 50; 6. write (B); Isolation requirement — no other successful transaction can see an intermediate state of this transaction (where the temporary sum of the accounts is less than it should) Haifa Verification Conference, October 4, 2010 / 16 Example — Durability Transfer 50! from account A to account B 1. read (A); 2. A = A – 50; 3. write (A); 4. Read (B); 5. B = B + 50; 6. write (B); Durability requirement — once the user has been notified that the transaction has completed (i.e., the transfer of the 50! has taken place), the updates to the database by the transaction must persist despite failures Haifa Verification Conference, October 4, 2010 / 17 Properties Consistency — the transaction must obey legal protocols Atomicity — it either happens or it does not; either all are bound by the contract or none are Isolation — transactions must behave as if executed alone in the system Durability — once a transaction is committed, it cannot be abrogated Haifa Verification Conference, October 4, 2010 / 18 Locks: Insert in a Double Linked List Succ Succ Succ Succ Pred Pred Pred Pred Fine grain locks public void insertNode (node, precedingNode) { synchronized (precedingNode) { synchronized (precedingNode.succ) { node.prec = precedingNode; node.succ = precedingNode.succ; precedingNode.succ.prec = node; precedingNode.succ = node; }}} Haifa Verification Conference, October 4, 2010 / 20 Transactional memory A possible solution !"#$%&&'&(")$()"*+,-'&.+$/"#+*01(*#+-'1+2'"%$#3%".' )&*+,'1(#4*$'1$(*#+&'56#4%('7899-'Shavit & Touitou 1995, Herlihy et al. 2003: Transactional memory public void insertNode (node, precedingNode) { atomic { //means “transaction” node.prec = precedingNode; node.succ = precedingNode.succ; precedingNode.succ.prec = node; precedingNode.succ = node; } } Haifa Verification Conference, October 4, 2010 / 21 Transactional memory Transactional operations Transaction Established in the domain of databases Easy to understand Series of read and write operations Executed at least atomically and isolated (AI from ACID properties) Performance is an issue On conflict Transaction is repeated Haifa Verification Conference, October 4, 2010 / 22 Transactional memory Advantages Developer worries less about parallelism Code is marked as atomic/isolated Code is generated and run-time ensure the properties Disadvantages Not always ideal Successive collisions repetitive rollbacks Memory transactions can not contain certain operations (e.g., I/O operations) Haifa Verification Conference, October 4, 2010 / 24 Expectations Preserving real-time ordering The conceptual point in time a transaction appear to execute lies within its lifespan i.e., transactions do no execute “in the past” neither “in the future” Precluding inconsistent views Assumption 1: transactions that access an inconsistent memory state will generate an exception Assumption 2: transactions that generate exceptions are aborted Haifa Verification Conference, October 4, 2010 / 25 Types of Actions in STM Non-transactional operations: Action whose effects are observed by an entity external to the system Killing a process user seeing a printf Irreversible and cannot be undone Haifa Verification Conference, October 4, 2010 / 31 Types of Actions in STM Transactional operations: Pure transactional Storing a value in memory Execute a gettimeofday() system call Revertible / Compensable Memory management operations Execute a lseek() system call Appending data to a file Execute the creat() system call Haifa Verification Conference, October 4, 2010 / 32 Non-Transactional Operations in STM Possible approaches: Don’t care Leave to the programmer the responsibility to avoid or manage its use in TM blocks Common approach for library-based TM frameworks Do not allow The programming language type system do not allow its use inside TM blocks Approach in Concurrent Haskell IO operations are typified and statically verified by the compiler e.g., putChar :: Char -> IO() Haifa Verification Conference, October 4, 2010 / 33 Non-Transactional Operations in STM Possible approaches: Enter a non-speculative mode Enforce that transactions execution NTO will never abort May use an optimistic approach, assuming transactions will not execute NTO, otherwise… Wait for all other concurrent transactions to finish Restart and run the transaction that will execute NTOs as the only transaction in the system Once finished, resume the normal operation Haifa Verification Conference, October 4, 2010 / 34 Revertible / Compensable Operations in STM Possible approaches: Defer Some operations may/must be postponed to the end of the atomic block Compensate Some operations are not revertible, but may be compensated later without compromising the application semantics Haifa Verification Conference, October 4, 2010 / 35 Handling Revertible Operations in STM Deferred operations can be supported by transaction handlers Handlers extend the transaction life cycle with new states Example for memory transactions in next slide Haifa Verification Conference, October 4, 2010 / 36 Memory Transaction States partially committed BEGIN committed active Transaction States aborted END Haifa Verification Conference, October 4, 2010 / 38 Memory Transaction States void *my_malloc(...) { void *m = malloc (...); register_pre_abort(free, m); } partially committed #define my_free (m) \ register_pos_commit (free, m); preparecommit precommit postponed free() BEGIN active free local malloc() Postpone d committed poscommit free() Transaction States pre-abort aborted pos-abort END Handler System States Haifa Verification Conference, October 4, 2010 / 39 An Handler System prepare-commit pre-abort pre-commit pos-commit pos-abort Haifa Verification Conference, October 4, 2010 / 40 Unifying Memory and DB Transactions void TxDBStart(...) { TxStart(); register_pre_abort(...); register_prepare_commit(...); register_pre_commit(...); } partially committed BEGIN active Transaction States Database Transaction COMMIT preparecommit DB Tx ABORT Mem Tx ABORT pre-abort aborted precommit Mem Tx COMMIT committed poscommit pos-abort END Handler System States Haifa Verification Conference, October 4, 2010 / 41 A Static Approach for Detecting Concurrency Anomalies in Transactional Memory Haifa Verification Conference, October 4, 2010 / 42 Problem Statement Concurrency errors have always been a problem Dataraces Deadlocks Priority inversion Convoying ... There are still errors observed in TM Low-level dataraces High-level dataraces No tools for TM Our goal is to statically detect these errors Haifa Verification Conference, October 4, 2010 / 43 Low-level Dataraces (LLDR) private boolean hasSpaceLeft() { return (list.size() < MAX_SIZE); } private void store(Object obj) { list.add(obj); } public void attemptToStore(Object obj) { if (hasSpaceLeft()) { store(obj); } } Haifa Verification Conference, October 4, 2010 / 44 Low-level Dataraces (LLDR) private boolean hasSpaceLeft() { return (list.size() < MAX_SIZE); } private void store(Object obj) { list.add(obj); } public void attemptToStore(Object obj) { if (hasSpaceLeft()) { store(obj); Low-level datarace: list is read and concurrently updated } } Haifa Verification Conference, October 4, 2010 / 45 Low-level Dataraces (LLDR) private boolean hasSpaceLeft() { synchronized { return (list.size() < MAX_SIZE); } } private void store(Object obj) { synchronized { list.add(obj); } } public void attemptToStore(Object obj) { if (hasSpaceLeft()) { store(obj); } } Haifa Verification Conference, October 4, 2010 / 46 High-level Dataraces (HLDR) private boolean hasSpaceLeft() { synchronized { return (list.size() < MAX_SIZE); } } private void store(Object obj) { synchronized { list.add(obj); } } public void attemptToStore(Object obj) { if (hasSpaceLeft()) { // list may become full store(obj); } } Haifa Verification Conference, October 4, 2010 / 47 High-level Dataraces (HLDR) private boolean hasSpaceLeft() { synchronized { return (list.size() < MAX_SIZE); } } private void store(Object obj) { synchronized { list.add(obj); } } public void attemptToStore(Object obj) { if (hasSpaceLeft()) { // list may become full store(obj); } } High-level datarace: accesses are synchronized but list can overflow Haifa Verification Conference, October 4, 2010 / 48 LLDR Detection Automatically convert TM to lock based programs New program is processed by a datarace detector Detected dataraces are also present in TM program Control with TM Ø T Ø T Ø Ø T T DR DR DR Control with Locks Ø L1 Ø L1 L1 Ø Ø L1 L2 L1 DR DR DR DR Ø : Unprotected access L : Lock-guarded access T : Transactional access Haifa Verification Conference, October 4, 2010 / 49 LLDR Detection TMbased Program Datarace Report LLDR Detector Automatic Transformer (Polyglot based tool) Lock-based (single lock) Program Datarace Detector (JChord) Haifa Verification Conference, October 4, 2010 / 50 Example private boolean hasSpaceLeft() { atomic { return (list.size() < MAX_SIZE); } } private void store(Object obj) { atomic { list.add(obj); } } public static Object GLOCK; private boolean hasSpaceLeft() { synchronized (GLOCK) { return (list.size() < MAX_SIZE); } } private void store(Object obj) { synchronized (GLOCK) { list.add(obj); } } Haifa Verification Conference, October 4, 2010 / 51 Validation: Lee-TM Renowed benchmark 2 versions (lock- and TM-based) Ran JChord in lock version 52 dataraces – nolocks and wrong-locks Ran LLDR detector in TM version 48 dataraces – accesses outside transactional blocks Haifa Verification Conference, October 4, 2010 / 52 High-level Dataraces (HLDR) private boolean hasSpaceLeft() { synchronized { return (list.size() < MAX_SIZE); } } private void store(Object obj) { synchronized { list.add(obj); } } High-level public void attemptToStore(Object obj) { Anomaly: if (hasSpaceLeft()) { list could overflow, // list may become full although accesses store(obj); are synchronized } } Haifa Verification Conference, October 4, 2010 / 53 HLDR Detection TMbased Program Anomaly Reports HLDR Detector AST AJEX Parser (Polyglot extension) Traces Symbolic Executor/ /Tracer Pattern Matcher Haifa Verification Conference, October 4, 2010 / 54 HLDR Detection (Example) private boolean hasSpaceLeft() { atomic { return (list.size() < MAX_SIZE); } } private void store(Object obj) { atomic { list.add(obj); } } public void attemptToStore(Object obj) { if (hasSpaceLeft()) store(obj); } public void run() { attemptToStore("I’m a misbehaving program."); } Haifa Verification Conference, October 4, 2010 / 55 Tracer (Example) hasSpaceLeft() ATOMIC R: list R: MAX_SIZE store() ATOMIC R: list W: list attemptToStore() run() CALL: hasSpaceLeft () CALL: attemptToStore () IF CALL: store () - END Haifa Verification Conference, October 4, 2010 / 56 Tracer (Example) hasSpaceLeft() ATOMIC R: list R: MAX_SIZE store() ATOMIC R: list W: list run() CALL: hasSpaceLeft () CALL: attemptToStore () IF CALL: store () - END Haifa Verification Conference, October 4, 2010 / 57 Tracer (Example) store() ATOMIC R: list R: MAX_SIZE ATOMIC R: list W: list run() CALL: hasSpaceLeft () IF CALL: store () - END Haifa Verification Conference, October 4, 2010 / 58 Tracer (Example) ATOMIC R: list W: list run() ATOMIC R: list R: MAX_SIZE IF CALL: store () - END Haifa Verification Conference, October 4, 2010 / 59 Tracer (Example) run() ATOMIC R: list R: MAX_SIZE IF ATOMIC R: list W: list END Haifa Verification Conference, October 4, 2010 / 60 Tracer (Example) Trace 1 Trace 2 START START ATOMIC R: list R: MAX_SIZE ATOMIC R: list W: list run() R: list ATOMIC R: MAX_SIZE R: list ATOMIC R: MAX_SIZE IF END ATOMIC END R: list W: list END Haifa Verification Conference, October 4, 2010 / 61 Tracing: Calls and Flow Control Method calls If statement Both branches are considered, but independently Loops Target method is expanded (inlined) 0, 1, and 2 iterations are considered Recursive calls Method is expanded twice, avoid infinite expansions but yield all possible anomalies Haifa Verification Conference, October 4, 2010 / 62 HLDR Detection TMbased Program Anomaly Reports HLDR Detector AST AJEX Parser (Polyglot extension) Traces Symbolic Executor/ /Tracer Pattern Matcher Haifa Verification Conference, October 4, 2010 / 63 Anomaly Patterns Relation between transactions may be inferred by data access patterns Certain access patterns may indicate anomalies Haifa Verification Conference, October 4, 2010 / 64 Anomaly Patterns Thread 1 Transaction3 Transaction1 Read(y) Read(x) Anomaly Write(x,y) Thread 2 RwR Transaction2 Thread 1 Transaction1 Transaction3 Write(y) Write(x) Anomaly Read(x,y) Thread 2 WrW Transaction2 Thread 1 Thread 2 Transaction1 Transaction3 Write(x) Read(x) Write(x) RwW Anomaly Transaction2 Haifa Verification Conference, October 4, 2010 / 65 Pattern Matcher (Example) 1 Trace 1’ Trace 2 START START START ATOMIC ATOMIC R: R: list list R: R: MAX_SIZE MAX_SIZE ATOMIC R: list ATOMIC ATOMIC R: R: list list W: W: list list W: list R: list R: MAX_SIZE Anomaly Pattern: RwW END list is retrieved, and updated in another transaction END END Haifa Verification Conference, October 4, 2010 / 66 Validation Well-known Lockbased Buggy Programs Hand Rewritting Anomaly Reports TM-based Buggy Programs TM HLDR Detection (Polyglot) Haifa Verification Conference, October 4, 2010 / 67 Coordinates’03 //Thread 3 public void run() { double x = c.getX(); double y = c.getY(); // use x and y... } //atomic //atomic //Thread 1 public void run() { c.setXY(...); //atomic } //Thread 4 public void run() { Coord d4 = c.getXY(); double x4 = d4.getX(); double y4 = d4.getY(); } Anomaly: RwR Coordinates could be from different states False Positives pointer analysis required Haifa Verification Conference, October 4, 2010 / 68 Counter public class Counter { int i; int inc(int a) { atomic { i = i + a; return i; } } } // Thread code public void run() { int i = c.inc(0); //get i // value could have changed c.inc(i); //increment by i } Anomaly: RwW Updates could be lost No False Positives Haifa Verification Conference, October 4, 2010 / 69 Results Test Total Anomalies Total Warnings Correct Warnings False Warnings Missed Anomalies $,/5- !*/2,/2- !,/2- ,/2- !*/3,/3- &!,/3- +,/3- #!&!,/3- &#,'/2- "(,'/2- '!+! !#,'/2- !+! !#,'/2- #!,- #'" 1 0 0 0 0 / / 0 0 0 / 0 0 0 1 3 1 0 3 4 1 / 0 1 1 0 1 2 0 0 0 0 0 / / / 0 0 / 0 0 0 0 2 0 / 2 4 1 / / 0 1 / 0 1 0 / / / / / / 0 / / / / / / Haifa Verification Conference, October 4, 2010 / 70 Results Summary for 14 tests performed 2 RwR 3 WrW 5 RwW Total Anomalies Total Warnings Correct Warnings False Warnings Missed Anomalies 12 33 10 23 2 3 RwR 3 WrW 6 RwW 70% of total results 5 redundand reads 6 pointer analysis 10 pattern refinement 2 permanent Due to Unavailable source-code 1 RwR 1 RwW Haifa Verification Conference, October 4, 2010 / 71 Monitoring and Visualizing Transactional Memory Programs InForum 2010 Haifa Verification Conference, October 4, 2010 / 72 Message Passing… “how did we used to do? ” Haifa Verification Conference, October 4, 2010 / 73 Shared Memory… “how did we used to do? ” Clear lack of tools Haifa Verification Conference, October 4, 2010 / 74 Transactional Memory… “how did we used to do? ” Total lack of tools Haifa Verification Conference, October 4, 2010 / 75 Transactional Memory… “how do we do now? ” !"#$%$#&'()*+'",'-.$/")01+-1".'21, !"#$%(%'&) !"#$%&%*+) !"#$%'%*+) !"#$%& !"#$%' !"#$%( !"#$%#&'()$*+,'"-*+#', !' !' !& #.,"#/,*)0*$123,"*)0*",'"(,% !% !$ !# !" !! !* ) ( ' &+''& & % $ # # # " ! *+#"$ * "## Haifa Verification Conference, October 4, 2010 / 76 Requirements for Tracing in JTraceView Keep hardware requirements Log only well defined time-slots Different hardware may mask some behaviors and trigger new ones When to start to collect events and for how long Huge log files Keep the global application behavior Same behavior pattern Low and constant overhead No additional synchronizations Haifa Verification Conference, October 4, 2010 / 77 Our Proposal for Tracing in JTraceView Keep events in separate buffers One buffer per thread Avoids additional synchronizations Use RDTSC (or similar) registers as a global clock Clock drifting can be a problem In many cases it is not Provides info on real execution time for transactions Keep global application behavior Haifa Verification Conference, October 4, 2010 / 78 Behavior of Memory Transactions Specification: Tx_Start (Tx_Read | Tx_Write)* (Tx_Abort | Tx_Commit) Run-time: Tx_Start (Tx_Read | Tx_Write)* (Tx_Abort_Read | Tx_Abort_Write | Tx_Abort_Commit | Tx_Abort_User | Tx_Commit) Haifa Verification Conference, October 4, 2010 / 79 Events for TM Tracing All Events timestamp eventID threadID transID • When? • What? • Where? • Whom? Tx_Read | Tx_Write Tx_Abort varID evType • Memory location • Why? [?] Haifa Verification Conference, October 4, 2010 / 80 Keeping App Behavior Linked List Red-Black Tree Red-Black 1000 nodes 300 6000 250 5000 200 Unmonitored 150 100 50 1000x Operations/second 1000x Operations/second List 1000 nodes 4000 3000 2000 1000 5% insert, 5% remove, 90% lookup 45% insert, 45% remove, 10% lookup 0 1 2 4 Number of threads 5% insert, 5% remove, 90% lookup 45% insert, 45% remove, 10% lookup 0 8 1 8 Red-Black / RDTSC Counter / 1000 nodes List / RDTSC Counter / 1000 nodes 2500 100 JTraceView tracing 80 60 40 20 1000x Operations/second 120 1000x Operations/second 2 4 Number of threads 2000 1500 1000 500 5% insert, 5% remove, 90% lookup 45% insert, 45% remove, 10% lookup 0 1 2 4 5% insert, 5% remove, 90% lookup 45% insert, 45% remove, 10% lookup 0 1 8 2 4 8 Number of threads Number of threads List / Atomic Counter / 1000 nodes Red-Black / Atomic Counter / 1000 nodes 25 350 15 Naïve tracing 10 5 1 2 4 Number of threads 250 200 150 100 50 5% insert, 5% remove, 90% lookup 45% insert, 45% remove, 10% lookup 0 1000x Operations/second 1000x Operations/second 300 20 5% insert, 5% remove, 90% lookup 45% insert, 45% remove, 10% lookup 0 8 1 2 4 Number of threads 8 Haifa Verification Conference, October 4, 2010 / 81 Tracing System Output RB-Tree in CTL generates 0.5 KB per processor per milisecond Unmanageable by common mortals Haifa Verification Conference, October 4, 2010 / 82 JTraceView: Visualization Tool for TM Trace file processor Trace file analyzers Monitoring Layer Visualization plugins JTraceView Haifa Verification Conference, October 4, 2010 / 83 JTraceView: Visualization Tool for TM Trace file processor Trace file analyzers Monitoring Layer Visualization plugins JTraceView Haifa Verification Conference, October 4, 2010 / 84 Visualization Plugins !"#$"%%& +'1''' *.1,'' *,1''' *)1,'' ).1,'' ),1''' ))1,'' !"##$%&'()"*%&+),+)"%-+%-.+/-*.01& )'1''' (.1,'' 6534 !"#$%#&'()$%*+#%',-*+)".*/,"&,$'#0,% (,1''' 6432 6/34 ()1,'' !"#$%&'()"*+'#,-#.)(/,*!#)"- ('1''' .1,'' -06101 5, .16121 '#%()*+,-. ' ' (' )' *' +' ,' -' .' 4,/' 0' ('' ((' '(#" 3, !"#$"%%& 2, 23#).*+"4+5"##$%& )1,'' 6232 /534 -,, ,1''' 4 )*#+",-./-0.##('& *'1''' /432 //34 /232 .534 .432 ./34 .232 1, 534 !"#$%&+//. 0, 416011 3060/1 -,, 432 /34 /, 232 232 ., /34 , 534 .232 ./34 .432 .534 /232 //34 /432 /534 6232 %$#. -, !"#$%& 432 !"##$%&'()*+,-. '#%()* )*$"+, )*$"+- !"##$%&'()*+,-/ 01"*%&'()*+,-. 01"*%&'()*+,-/ )*$"+. 0,$(1($2#3*+'#,-#.)(/,!"#$ %&'(" Haifa Verification Conference, October 4, 2010 / 85 Example !"#$%#&'()$*+,'"-*+#', !"#$%#&'()$*+,'"-*+#', 52 LL, 8, 20%, 20%, 60%, 50 540 #0,"#3,*)4*$156,"*)4*",'"(,% 430 300 .4 .4 020 210 1/0 /. /- LL, 8, 20%, 20%, 60%, 10000 .3 .2 #0,"#3,*)4*$156,"*)4*",'"(,% 50 .0 .1 .0 ./ .. .6 5 4 37443 3 2 1 0 0 .16574 0 -60/5 )*+#,- . -6/// )*+#,. -70/1 )*+#,- )*+#,. !"#$%&# '%( .6 6 RB, 8, 45%, 45%, 10%, 50 5 4 3 2 1 0 0 / . / /0-- / RB, 8, 45%, 45%, 10%, 10000 .021 #0,"#3,*)4*$156,"*)4*",'"(,% #0,"#3,*)4*$156,"*)4*",'"(,% .. '%( !"#$%#&'()$*+,'"-*+#', .0 ./ )*+#,/ .$/(0(/1#2*!"#$%#&'()$% !"#$%#&'()$*+,'"-*+#', .0 -7/00 )*+#,/ .$/(0(/1#2*!"#$%#&'()$% !"#$%&# 0 / 3 .01- .0/1 . .0-- -021 -01- -0/1 -7256 -72/ -7.13 -0-- )*+#,- )*+#,. .$/(0(/1#2*!"#$%#&'()$% !"#$%&# '%( )*+#,/ -0--3 -0--3 )*+#,- -0--/ )*+#,. )*+#,/ .$/(0(/1#2*!"#$%#&'()$% !"#$%&# '%( Haifa Verification Conference, October 4, 2010 / 86 STAMP Stanford Transactional Applications for MultiProcessing Collection of applications for TM benchmarking Includes both sequential and parallel code sections Eight different applications Six were ported to Java (DeuceSTM framework) http://stamp.stanford.edu Haifa Verification Conference, October 4, 2010 / 87 STAMP: Intruder Signature-based network intrusion detection systems (NIDS) scan network packets for matches against a known set of intrusion signatures Properties: Short transactions length Medium read/write sets High contention Medium transaction time Haifa Verification Conference, October 4, 2010 / 88 Trace Data Collected in a Sun Fire x4600 8 x AMD Opteron Model 8220 dual-core processor @ 2.8GHz 32 GB DDR2-667 memory Linux Debian lenny Test Conditions TM algorithm: TL2 Run time: 20 secs Trace File Size: 37MB Total transactions: 20814 Total commit: 14254 Total abort: 6560 Haifa Verification Conference, October 4, 2010 / 89 STAMP: Intruder Includes three transactional code blocks Code 0 — atomicGetPacket (streamPtr); Pop data from a queue Code 1 — atomicProcess (decoderPtr, packetPtr); Assemble packet segments and decode them Code 2 — atomicGetComplete (decoderPtr, decodedFlowId); Get decoded data of the packet Haifa Verification Conference, October 4, 2010 / 90 Transactional Code Blocks Haifa Verification Conference, October 4, 2010 / 91 Read / Write Rates Haifa Verification Conference, October 4, 2010 / 92 Abort Rate Haifa Verification Conference, October 4, 2010 / 93 Abort Types Haifa Verification Conference, October 4, 2010 / 94 Abort — False Conflicts Haifa Verification Conference, October 4, 2010 / 95 Haifa Verification Conference, October 4, 2010 / 96 Transaction Abort / Retry Haifa Verification Conference, October 4, 2010 / 97 Haifa Verification Conference, October 4, 2010 / 98 Duration of Transactions Haifa Verification Conference, October 4, 2010 / 99 Thread timeline Haifa Verification Conference, October 4, 2010 / 100 Thread timeline Haifa Verification Conference, October 4, 2010 / 101 Concluding Remarks Transactional Memory is an appealing paradigm for specifying concurrent programs We need software development tools specifically targeting TM Traditional tools do not apply to TM Transactional Memory programs may also exhibit dataraces Low-level dataraces: only in weak-isolation High-level dataraces: always Haifa Verification Conference, October 4, 2010 / 102 Concluding Remarks It is possible to detect LLDR’s in TM by analyzing “equivalent” lock-based programs Most HLDR’s occur when a transaction runs between two consecutive transactions of another thread The three patterns identified capture most of the anomalies referenced in the literature Good detection rates for a set of well known examples from different sources Haifa Verification Conference, October 4, 2010 / 103 Concluding Remarks JTraceView includes a low intrusion monitoring layer Deals with the very high frequency of events and huge logs The huge logs can be visually synthesized Statistical charts Time-space diagram Time-space view may also help in debugging Haifa Verification Conference, October 4, 2010 / 104 Want to try it yourself? Get: TM framework instrumented to generate logs (tracing data) JTraceView to visualize tracing data From: http://asc.di.fct.unl.pt/trxsys Check the prototypes page When: From October 16th Haifa Verification Conference, October 4, 2010 / 105 The End… Have fun! Haifa Verification Conference, October 4, 2010 / 106