Popular in Course
Popular in ComputerScienence
This 5 page Class Notes was uploaded by Roman McCullough on Friday October 30, 2015. The Class Notes belongs to CMPSCI 691 at University of Massachusetts taught by Staff in Fall. Since its upload, it has received 7 views. For similar materials see /class/232273/cmpsci-691-university-of-massachusetts in ComputerScienence at University of Massachusetts.
Reviews for S
Report this Material
What is Karma?
Karma is the currency of StudySoup.
Date Created: 10/30/15
CMPSCI 691W Parallel and Concurrent Programming Spring 2006 Lecture 9 March 8 Lecturer Emery Berger Scribe Heather Conboy 91 Overview Atomicity is a correctness property of multithreaded programs that guarantees that concurrent threads do not interfere with atomic methods andor blocks This means that the atomic methods andor blocks can be reasoned about in a sequential manner without having to consider all possible thread interleavings This makes it easier to reason about the behavior and correctness of these programs which simpli es code inspection testing and veri cation It is possible to check for atomicity using techniques such as static analysis dynamic analysis and nite state veri cation 92 Correctness properties of multithreaded programs Data race freedom A race condition occurs when two threads simultaneously access the same data variable and at least one of the accesses is a write 7 As a correctness property the above is not sufficient nor necessary Atomicity A method or block is atomic if for every arbitrarily interleaved program execution there exists an equivalent execution with the same overall behavior where the method or block is executed serially l Linearizability A concurrent program is linearizable if each object is linearizable This correctness property is nonblocking and local 4 Serializability ln databases A concurrent schedule is serializable if it is equivalent to one in which trans actions appear to execute using a sequential schedule This correctness property is blocking and global As correctness properties the above three provide stronger guarantees than data race freedom and still allow a great deal of parallelism 93 Atomizer Atomizer is a dynamic atomicity checker that for all methods andor blocks speci ed as atomic by either 0 The user as annotations o A heuristic de ned as 7 All methods that are public or package except for main and run methods 7 All synchronized blocks 92 Lecture 9 March 8 detects and reports any atomicity violationsr More speci cally7 the tool inputs a multithreaded Java program7 generates the corresponding instrumented multithreaded Java program that uses dynamic analysis to 0 Identify race conditions based on Eraserls lockset algorithm 7 0 Check atomicity based on Lipton s reduction theory 5 and outputs any atomicity violations With program executions that display the undesired behaviors 931 Lockset algorithm The Lockset algorithm is used for data race detectionr For each allocated object7 for each eld track to What degree it has been shared among threads rst thread rw second thread rw second thread rw Thread Local 2 Thread Local other thread w other thread r Shared Read Shared Modified any thread w any thread r any thread rw Figure 91 Thread sharing degree Figure 91 If a eld is thread local7 thread local 27 or shared read7 then any access is considered not racyr But if a eld is shared modi ed then its protecting lock set must be inferred Version 1 Each eld has a protecting lock set inferred If an access occurs When the lock set is empty then the access is considered racyr Lecture 9 March 8 93 For writeprotected data7 the above categorization is too restrictive Version 2 Each eld now has an accessprotecting lock set and a writeprotecting lock set inferred If a read occurs when the the writeprotecting lock set is empty then the read is considered racy If a write occurs when the accessprotecting lock set is empty then the write is considered racy 932 Reduction algorithm The Reduction algorithm is used for atomicity Violation detection It makes use of the data race information Version 1 o Rightmover R lock acquire o Leftmomver L lock release 0 Bothmover B nonracy eld access 0 Nonmover N racy eld access An atomic section must always conform to R l B 96 N l L L l B For locks7 the above categorization is often too restrictive For a general lock7 a lock acquire is a rightmover and a lock release is a leftmove But for a special lock as de ned below its acquire and release can be considered a bothmover o The lock is thread local 0 The lock is protected by another lock 0 The lock is reentrant and this is not the rst last acquire release Version 2 o Rightmover R lock acquire not special case 0 Leftmomver L lock release not special case 0 Bothmover B 7 lock acquire special case 7 lock release special case 7 nonracy eld access 0 Nonmover N racy eld access The atomic sections can now be larger since more actions are categorized as bothmovers 94 Lecture 9 March 8 94 Evaluation The Atomizer was evaluated on 12 multithreaded Java programs gathered from various benchmarks It used the heuristic to specify methods andor blocks as atomic Generally it appears that programmers often do code to this style of concurrency The benchmarks for the most part used it In summary 0 There were very few false alarms 0 There were actual bugs found 0 There was a performance penalty 15x 40X 95 Related Work 951 Static type systems A static type system takes as input a multithreaded program where the programmer must specify o For each object allocated for each eld the protecting locks o For each method andor block the atomicity and outputs whether or not the atomicity is violated Evaluation of the static type systems 0 The programmer must provide the annotations 0 Since it is a static analysis it provides better coverage and soundness guarantees then the dynamic analysis 0 But is has a more restrictive domain 0 In theory the static analysis is NPcomplete 0 In practice they often are applicable o The static analysis results may be used to restrict the dynamic analyses See 2 952 Finite state veri ers A nite state veri er takes as input a multithreaded program and perhaps the corresponding sequential program and outputs whether or not the atomicity is violated Evaluation of the nite state veri ers Lecture 9 March 8 o The programmer may have to provide annotations o It provides better coverage and soundness guarentees then the dynamic analysis o For integration testing it must deal With the state explosion probleml o For unit testing it is applicable See References 1 Ci Flanagan and SiNl Freundl Atomizer A dynamic atomicity checker for multithreaded programs In Proc of the ACM Symposium on Principles of Programming Languages POPL ACM Press 2004 2 Ci Flanagan and Si Qadeerl A type and effect system for atomicityl In Proc of the ACM Conference on Programming Language Design and Implementation pages 3387349 2003 3 Jr Hatcliff Robby and MiBl DWyerl Verifying atomicity speci cations for concurrent objectoriented software using modelchecking In Proc of the International Conference on Veri cation Model Checking and Abstract Interpretation 2004i 4 MiPl Herlihy and JiMl Wing Linearizability A correctness condition for concurrent objects ACM Transactions on Programming Languages and Systems 1234637492 1990 5 El Liptonl Reduction A method of proving properties of parallel programs Communications of the ACM18127177721 1975i 6 Ci Papadimitrioul The theory of database concurrency control Computer Science Press 1986 7 Si Savage Ml Burrows Gr Nelson Pi Sobalvarro and TE Andersonl Eraser A dynamic data race detector for multithreaded programsl ACM Transactions on Computer Systems 154917411 1997