caa a22 4500 445835338 CHVBK 20180317145328.0 cr unu---uuuuu 170323e20111201xx s 000 0 eng 10.1007/s10515-011-0085-0 doi (NATIONALLICENCE)springer-10.1007/s10515-011-0085-0 Symbolic modular deadlock analysis [Elektronische Daten] [Jyotirmoy Deshmukh, E. Emerson, Sriram Sankaranarayanan] Methods in object-oriented concurrent libraries often encapsulate internal synchronization details. As a result of information hiding, clients calling the library methods may cause thread safety violations by invoking methods in an unsafe manner. This is frequently a cause of deadlocks. Given a concurrent library, we present a technique for inferring interface contracts that specify permissible concurrent method calls and patterns of aliasing among method arguments. In this work, we focus on deriving contracts that guarantee deadlock-free execution for the methods in the library. The contracts also help client developers by documenting required assumptions about the library methods. Alternatively, the contracts can be statically enforced in the client code to detect potential deadlocks in the client. Our technique combines static analysis with a symbolic encoding scheme for tracking lock dependencies, allowing us to synthesize contracts using a SMT solver. Additionally, we investigate extensions of our technique to reason about deadlocks in libraries that employ signaling primitives such as wait-notify for cooperative synchronization. Our prototype tool analyzes over a million lines of code for some widely-used Java libraries within an hour, thus demonstrating its scalability and efficiency. Furthermore, the contracts inferred by our approach have been able to pinpoint real deadlocks in clients, i.e. deadlocks that have been a part of bug-reports filed by users and developers of client code. Springer Science+Business Media, LLC, 2011 Deadlock prediction nationallicence Static analysis nationallicence Concurrent libraries nationallicence Deshmukh Jyotirmoy Department of Computer and Information Science, University of Pennsylvania, 19104, Philadelphia, PA, USA aut Emerson E. Department of Computer Science, The University of Texas at Austin, 78712, Austin, TX, USA aut Sankaranarayanan Sriram Department of Computer Science, University of Colorado Boulder, 80309-0430, Boulder, CO, USA aut Automated Software Engineering Springer US; http://www.springer-ny.com 18/3-4(2011-12-01), 325-362 0928-8910 18:3-4<325 2011 18 10515 https://doi.org/10.1007/s10515-011-0085-0 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1007/s10515-011-0085-0 text/html Onlinezugriff via DOI NATIONALLICENCE 700 1- Deshmukh Jyotirmoy Department of Computer and Information Science, University of Pennsylvania, 19104, Philadelphia, PA, USA aut NATIONALLICENCE 700 1- Emerson E. Department of Computer Science, The University of Texas at Austin, 78712, Austin, TX, USA aut NATIONALLICENCE 700 1- Sankaranarayanan Sriram Department of Computer Science, University of Colorado Boulder, 80309-0430, Boulder, CO, USA aut NATIONALLICENCE 773 0- Automated Software Engineering Springer US; http://www.springer-ny.com 18/3-4(2011-12-01), 325-362 0928-8910 18:3-4<325 2011 18 10515 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer