Language Strength Reduction
作者： Nicholas Kidd , Akash Lal , Thomas Reps
DOI: 10.1007/978-3-540-69166-2_19
关键词: Language primitive 、 Record locking 、 Programming language 、 Data control language 、 Low-level programming language 、 High-level programming language 、 Programming language implementation 、 Context-sensitive language 、 Specification language 、 Computer science
摘要: This paper concerns methods to check for atomic-set serializability violations in concurrent Java programs. The straightforward way encode a reentrant lock is model it with context-free language track the number of successive acquisitions. We present construction that replaces describes by regular non-reentrant lock. call this replacement strength reduction. Language reduction produces an average speedup (geometric mean) 3.4. Moreover, 2 programs previously exhausted available space, tool now able run completion.
springer.com
springerlink.com参考文章(19)
Swarat Chaudhuri, Rajeev Alur, Instrumenting C Programs with Nested Word Monitors Model Checking Software. ,vol. 4595, pp. 279- 283 ,(2007) , 10.1007/978-3-540-73370-6_20
Akash Lal, Thomas Reps, Gogul Balakrishnan, Extended Weighted Pushdown Systems Computer Aided Verification. pp. 434- 448 ,(2005) , 10.1007/11513988_44
Rajeev Alur, Kousha Etessami, P. Madhusudan, A Temporal Logic of Nested Calls and Returns tools and algorithms for construction and analysis of systems. ,vol. 2988, pp. 467- 481 ,(2004) , 10.1007/978-3-540-24730-2_35
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
Stefan Schwoon, Model-Checking Pushdown Systems ,(2002)
Rajeev Alur, P. Madhusudan, Adding nesting structure to words Journal of the ACM. ,vol. 56, pp. 1- 43 ,(2009) , 10.1145/1516512.1516518
Christian Hammer, Julian Dolby, Mandana Vaziri, Frank Tip, Dynamic detection of atomic-set-serializability violations international conference on software engineering. pp. 231- 240 ,(2008) , 10.1145/1368088.1368120
Mohamed Nassim Seghir, Andreas Podelski, ACSAR: Software Model Checking with Transfinite Refinement Model Checking Software. pp. 274- 278 ,(2007) , 10.1007/978-3-540-73370-6_19
Mandana Vaziri, Frank Tip, Julian Dolby, Associating synchronization constraints with data in an object-oriented language symposium on principles of programming languages. ,vol. 41, pp. 334- 345 ,(2006) , 10.1145/1111037.1111067
Yaniv Eytani, Klaus Havelund, Scott D. Stoller, Shmuel Ur, Towards a framework and a benchmark for testing tools for multi‐threaded programs Concurrency and Computation: Practice and Experience. ,vol. 19, pp. 267- 279 ,(2007) , 10.1002/CPE.1068