research-article

Parameterized verification of transactional memories

Authors:

Rupak Majumdar,

Roman ManevichAuthors Info & Claims

PLDI '10: Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 134 - 145

https://doi.org/10.1145/1806596.1806613

Published: 05 June 2010 Publication History

Abstract

We describe an automatic verification method to check whether transactional memories ensure strict serializability a key property assumed of the transactional interface. Our main contribution is a technique for effectively verifying parameterized systems. The technique merges ideas from parameterized hardware and protocol verification--verification by invisible invariants and symmetry reduction--with ideas from software verification--template-based invariant generation and satisfiability checking for quantified formulæ (modulo theories). The combination enables us to precisely model and analyze unbounded systems while taming state explosion.

Our technique enables automated proofs that two-phase locking (TPL), dynamic software transactional memory (DSTM), and transactional locking II (TL2) systems ensure strict serializability. The verification is challenging since the systems are unbounded in several dimensions: the number and length of concurrently executing transactions, and the size of the shared memory they access, have no finite limit. In contrast, state-of-the-art software model checking tools such as BLAST and TVLA are unable to validate either system, due to inherent expressiveness limitations or state explosion.

References

[1]

K. R. Apt and D. Kozen. Limits for automatic verification of finite-state concurrent systems. Inf. Process. Lett., 22 (6): 307--309, 1986.

Digital Library

[2]

T. Arons, A. Pnueli, S. Ruah, J. Xu, and L. D. Zuck. Parameterized verification with automatically computed inductive assertions. In CAV, pages 221--234, 2001.

Digital Library

[3]

T. Ball and S. K. Rajamani. The SLAM project: debugging system software via static analysis. In POPL, pages 1--3, 2002.

Digital Library

[4]

J. Berdine, T. Lev-Ami, R. Manevich, G. Ramalingam, and S. Sagiv. Thread quantification for concurrent shape analysis. In CAV, pages 399--413, 2008.

Digital Library

[5]

D. Beyer, T. A. Henzinger, R. Majumdar, and A. Rybalchenko. Invariant synthesis for combined theories. In VMCAI, pages 378--394, 2007.

Digital Library

[6]

A. Cohen, J. W. O'Leary, A. Pnueli, M. R. Tuttle, and L. D. Zuck. Verifying correctness of transactional memories. In FMCAD, pages 37--44, 2007.

Digital Library

[7]

A. Cohen, A. Pnueli, and L. D. Zuck. Mechanical verification of transactional memories with non-transactional memory accesses. In CAV, pages 121--134, 2008.

Digital Library

[8]

S. Sankaranarayanan, and H. Sipma. Linear invariant generation using non-linear constraint solving. In CAV, pages 420--432, 2003.

[9]

L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, pages 337--340, 2008.

Digital Library

[10]

D. Dice, O. Shalev, and N. Shavit. Transactional locking II. In DISC, pages 194--208, 2006.

Digital Library

[11]

D. L. Dill, A. J. Hu, and H. Wong-Toi. Checking for language inclusion using simulation preorders. In CAV, pages 255--265, 1991.

Digital Library

[12]

R. Guerraouić, and M. Kapalka. Dividing transactional memories by zero. In TRANSACT, 2008.

[13]

B. Dutertre and L. de Moura. The YICES SMT solver. http://yices.csl.sri.com.

[14]

M. D. Ernst, J. H. Perkins, P. J. Guo, S. McCamant, C. Pacheco, M. S. Tschantz, and C. Xiao. The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program., 69 (1--3): 35--45, 2007.

Digital Library

[15]

R. Guerraoui, T. A. Henzinger, B. Jobstmann, and V. Singh. Model checking transactional memories. In PLDI, pages 372--382, 2008.

Digital Library

[16]

R. Guerraoui, T. A. Henzinger, and V. Singh. Completeness and nondeterminism in model checking transactional memories. In CONCUR, pages 21--35, 2008.

Digital Library

[17]

R. Guerraoui, T. A. Henzinger, and V. Singh. Software transactional memory on relaxed memory models. In CAV, pages 321--336, 2009.

Digital Library

[18]

T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL, pages 58--70, 2002.

Digital Library

[19]

M. Herlihy and J. E. B. Moss. Transactional memory: Architectural support for lock-free data structures. In ISCA, pages 289--300, 1993.

Digital Library

[20]

M. Herlihy, V. Luchangco, M. Moir, and W. N. S. III. Software transactional memory for dynamic-sized data structures. In PODC, pages 92--101, 2003.

Digital Library

[21]

S. Kleene. Introduction to Metamathematics. North Holland, 1980.

[22]

L. Lamport. Specifying concurrent program modules. ACM Trans. Program. Lang. Syst., 5 (2): 190--222, 1983.

Digital Library

[23]

J. R. Larus and R. Rajwar. Transactional Memory. Morgan & Claypool Publishers, 2006.

[24]

T. Lev-Ami and S. Sagiv. TVLA: A system for implementing static analyses. In SAS, pages 280--301, 2000.

Digital Library

[25]

Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.

Digital Library

[26]

K. L. McMillan. Verification of infinite state systems by compositional model checking. In CHARME, pages 219--234, 1999.

Digital Library

[27]

C. H. Papadimitriou. The serializability of concurrent database updates. J. ACM, 26 (4): 631--653, 1979.

Digital Library

[28]

A. Pnueli, S. Ruah, and L. D. Zuck. Automatic deductive verification with invisible invariants. In TACAS, pages 82--97, 2001.

Digital Library

[29]

J. Reineke. Shape analysis of sets. Master's thesis, Universität des Saarlandes, Germany, June 2005.

[30]

J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS, pages 55--74, 2002.

Digital Library

[31]

S. Sagiv, T. W. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst., 24 (3): 217--298, 2002.

Digital Library

[32]

S. Srivastava and S. Gulwani. Program verification using templates over predicate abstraction. In PLDI, pages 223--234, 2009.

Digital Library

[33]

S. Tasiran. A compositional method for verifying software transactional memory implementations. Technical Report MSR-TR-2008-56, Microsoft Research, April 2008.

[34]

C. Weidenbach, D. Dimova, A. Fietzke, R. Kumar, M. Suda, and P. Wischnewski. SPASS version 3.5. In CADE, pages 140--145, 2009.

Digital Library

[35]

H. Yang, O. Lee, J. Berdine, C. Calcagno, B. Cook, D. Distefano, and P. W. O'Hearn. Scalable shape analysis for systems code. In CAV, pages 385--398, 2008.

Digital Library

[36]

K. Zee, V. Kuncak, and M. C. Rinard. Full functional verification of linked data structures. In PLDI, pages 349--361, 2008.

Digital Library

Cited By

Farzan AKlumpp DPodelski A(2024)Commutativity Simplifies Proofs of Parameterized ProgramsProceedings of the ACM on Programming Languages10.1145/36329258:POPL(2485-2513)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632925
König JWehrheim H(2021)On the Correctness Problem for SerializabilityTheoretical Aspects of Computing – ICTAC 202110.1007/978-3-030-85315-0_4(47-64)Online publication date: 20-Aug-2021
https://doi.org/10.1007/978-3-030-85315-0_4
Biswas REmmi MEnea C(2019)On the Complexity of Checking Consistency for Replicated Data TypesComputer Aided Verification10.1007/978-3-030-25543-5_19(324-343)Online publication date: 12-Jul-2019
https://doi.org/10.1007/978-3-030-25543-5_19
Show More Cited By

Index Terms

Recommendations

Parameterized verification of transactional memories
PLDI '10

We describe an automatic verification method to check whether transactional memories ensure strict serializability a key property assumed of the transactional interface. Our main contribution is a technique for effectively verifying parameterized ...
Grasping the gap between blocking and non-blocking transactional memories

Transactional memory (TM) is an inherently optimistic abstraction: it allows concurrent processes to execute sequences of shared-data accesses (transactions) speculatively, with an option of aborting them in the future. Early TM designs avoided using ...
Verification of transactional memories and recursive programs

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI '10: Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2010

514 pages

ISBN:9781450300193

DOI:10.1145/1806596

General Chair:
Ben Zorn
Microsoft Research
,
Program Chair:
Alex Aiken
Stanford University

ACM SIGPLAN Notices Volume 45, Issue 6
PLDI '10
June 2010
496 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1809028
Issue’s Table of Contents

Copyright © 2010 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 June 2010

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

PLDI '10

Sponsor:

SIGPLAN

PLDI '10: ACM SIGPLAN Conference on Programming Language Design and Implementation

June 5 - 10, 2010

Ontario, Toronto, Canada

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

17
Total Citations
View Citations
368
Total Downloads

Downloads (Last 12 months)8
Downloads (Last 6 weeks)1

Reflects downloads up to 21 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Farzan AKlumpp DPodelski A(2024)Commutativity Simplifies Proofs of Parameterized ProgramsProceedings of the ACM on Programming Languages10.1145/36329258:POPL(2485-2513)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632925
König JWehrheim H(2021)On the Correctness Problem for SerializabilityTheoretical Aspects of Computing – ICTAC 202110.1007/978-3-030-85315-0_4(47-64)Online publication date: 20-Aug-2021
https://doi.org/10.1007/978-3-030-85315-0_4
Biswas REmmi MEnea C(2019)On the Complexity of Checking Consistency for Replicated Data TypesComputer Aided Verification10.1007/978-3-030-25543-5_19(324-343)Online publication date: 12-Jul-2019
https://doi.org/10.1007/978-3-030-25543-5_19
Peterson CDechev D(2017)A Transactional Correctness Tool for Abstract Data TypesACM Transactions on Architecture and Code Optimization10.1145/314896414:4(1-24)Online publication date: 14-Nov-2017
https://dl.acm.org/doi/10.1145/3148964
Kordic BPopovic MGhilezan SBasicevic I(2017)An approach to formal verification of python software transactional memoryProceedings of the Fifth European Conference on the Engineering of Computer-Based Systems10.1145/3123779.3123788(1-10)Online publication date: 31-Aug-2017
https://dl.acm.org/doi/10.1145/3123779.3123788
Hoenicke JMajumdar RPodelski A(2017)Thread modularity at many levels: a pearl in compositional verificationACM SIGPLAN Notices10.1145/3093333.300989352:1(473-485)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009893
Hoenicke JMajumdar RPodelski ACastagna GGordon A(2017)Thread modularity at many levels: a pearl in compositional verificationProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009893(473-485)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3009837.3009893
Lesani MPalsberg J(2014)Decomposing OpacityDistributed Computing10.1007/978-3-662-45174-8_27(391-405)Online publication date: 2014
https://doi.org/10.1007/978-3-662-45174-8_27
Johnson TMitra S(2013)Invariant Synthesis for Verification of Parameterized Cyber-Physical Systems with Applications to Aerospace SystemsAIAA Infotech@Aerospace (I@A) Conference10.2514/6.2013-4811Online publication date: 15-Aug-2013
https://doi.org/10.2514/6.2013-4811
Conchon SGoel AKrstic SMebsout AZaidi F(2013)Invariants for finite instances and beyond2013 Formal Methods in Computer-Aided Design10.1109/FMCAD.2013.6679392(61-68)Online publication date: Oct-2013
https://doi.org/10.1109/FMCAD.2013.6679392
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents