A Decision Procedure for Detecting Atomicity Violations for Communicating Processes with Locks
作者： Nicholas Kidd , Peter Lammich , Tayssir Touili , Thomas Reps
DOI: 10.1007/978-3-642-02652-2_12
关键词: Automaton 、 Thread (computing) 、 Model checking 、 Programming language 、 Context switch 、 Atomicity 、 Computer science 、 Java 、 Finite-state machine 、 Serializability
摘要: We present a new decision procedure for detecting property violations in pushdown models concurrent programs that use lock-based synchronization, where each thread's lock operations are properly nested (a la synchronized methods Java). The technique detects expressed as indexed phase automata (PAs)--a class of non-deterministic finite which the only loops self-loops. Our interest PAs stems from their ability to capture atomic-set serializability violations. (Atomic-set is relaxation atomicity user-specified set memory locations.) implemented and applied it atomic-set-serializability Java programs. Compared with prior method based on semi-decision procedure, not was 7.5X faster overall, but timed out about 68% queries versus 4% procedure.
springer.com
core.ac.uk
wisconsin.edu
researchgate.net 
sci-hub.st 参考文章(27)
Shaz Qadeer, Jakob Rehof, Context-Bounded Model Checking of Concurrent Software Tools and Algorithms for the Construction and Analysis of Systems. pp. 93- 107 ,(2005) , 10.1007/978-3-540-31980-1_7
Nicholas Kidd, Akash Lal, Thomas Reps, Language Strength Reduction Static Analysis. pp. 283- 298 ,(2008) , 10.1007/978-3-540-69166-2_19
Michael A. Harrison, Introduction to formal language theory ,(1978)
Akash Lal, Tayssir Touili, Nicholas Kidd, Thomas Reps, Interprocedural analysis of concurrent programs under a context bound tools and algorithms for construction and analysis of systems. pp. 282- 298 ,(2008) , 10.1007/978-3-540-78800-3_20
Peter Lammich, Markus Müller-Olm, Alexander Wenner, Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints Computer Aided Verification. pp. 525- 539 ,(2009) , 10.1007/978-3-642-02658-4_39
Vineet Kahlon, Franjo Ivančić, Aarti Gupta, Reasoning About Threads Communicating via Locks Computer Aided Verification. ,vol. 3576, pp. 505- 518 ,(2005) , 10.1007/11513988_49
Ahmed Bouajjani, Javier Esparza, Oded Maler, Reachability Analysis of Pushdown Automata: Application to Model-Checking international conference on concurrency theory. pp. 135- 150 ,(1997) , 10.1007/3-540-63141-0_10
Nicholas Kidd, Thomas Reps, Julian Dolby, Mandana Vaziri, Finding Concurrency-Related Bugs Using Random Isolation Lecture Notes in Computer Science. pp. 198- 213 ,(2008) , 10.1007/978-3-540-93900-9_18
Alain Finkel, Bernard Willems, Pierre Wolper, A Direct Symbolic Approach to Model Checking Pushdown Systems (extended abstract) Electronic Notes in Theoretical Computer Science. ,vol. 9, pp. 27- 37 ,(1997) , 10.1016/S1571-0661(05)80426-8
Micheal Jacob, A personal communication Health Education Journal. ,vol. 48, pp. 156- 156 ,(1989) , 10.1177/001789698904800401