More Web Proxy on the site http://driver.im/

Article

Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis

Authors:

Thomas RepsAuthors Info & Claims

CAV '08: Proceedings of the 20th international conference on Computer Aided Verification

Pages 37 - 51

https://doi.org/10.1007/978-3-540-70545-1_7

Published: 07 July 2008 Publication History

Abstract

This paper addresses the analysis of concurrent programs with shared memory. Such an analysis is undecidable in the presence of multiple procedures. One approach used in recent work obtains decidability by providing only a partial guarantee of correctness: the approach bounds the number of context switches allowed in the concurrent program, and aims to prove safety, or find bugs, under the given bound. In this paper, we show how to obtain simple and efficient algorithms for the analysis of concurrent programs with a context bound. We give a general reduction from a <em>concurrent</em>program <em>P</em>, and a given context bound <em>K</em>, to a <em>sequential</em>program $P_s^K$ such that the analysis of $P_s^K$ can be used to prove properties about <em>P</em>. We give instances of the reduction for common program models used in model checking, such as Boolean programs and pushdown systems.

References

[1]

Ball, T., Rajamani, S.: Bebop: A symbolic model checker for Boolean programs. In: SPIN (2000)

Digital Library

[2]

Berger, F., Schwoon, S., Suwimonteerabuth, D.: jMoped (2005), http://www.informatik.uni-stuttgart.de/fmi/szs/tools/moped/jmoped/

[3]

Bouajjani, A., Fratani, S., Qadeer, S.: Context-bounded analysis of multithreaded programs with dynamic linked structures. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 207-220. Springer, Heidelberg (2007)

Digital Library

[4]

Chaki, S., Clarke, E.M., Kidd, N., Reps, T.W., Touili, T.: Verifying concurrent message-passing C programs with recursive calls. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 334-349. Springer, Heidelberg (2006)

Digital Library

[5]

Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL (2002)

Digital Library

[6]

Henzinger, T.A., Jhala, R., Majumdar, R.: Race checking by context inference. In: PLDI (2004)

Digital Library

[7]

Knoop, J., Steffen, B.: The interprocedural coincidence theorem. In: CC (1992)

Digital Library

[8]

Lal, A., Reps, T.: Reducing concurrent analysis under a context bound to sequential analysis. Technical Report 1629, University of Wisconsin (2008)

[9]

Lal, A., Touili, T., Kidd, N., Reps, T.: Interprocedural analysis of concurrent programs under a context bound. TR-1598, University of Wisconsin (July 2007)

[10]

Lal, A., Touili, T., Kidd, N., Reps, T.: Interprocedural analysis of concurrent programs under a context bound. In: TACAS (2008)

Digital Library

[11]

Müller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: POPL (2004)

Digital Library

[12]

Murphy, B., Lam, M.: Program analysis with partial transfer functions. In: PEPM (2000)

Digital Library

[13]

Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: PLDI (2007)

Digital Library

[14]

Qadeer, S., Rajamani, S.: Deciding assertions in programs with references. Technical Report MSR-TR-2005-08, Microsoft Research, Redmond (January 2005)

[15]

Qadeer, S., Rajamani, S.K., Rehof, J.: Summarizing procedures in concurrent programs. In: POPL (2004)

Digital Library

[16]

Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93-107. Springer, Heidelberg (2005)

Digital Library

[17]

Qadeer, S., Wu, D.: KISS: Keep it simple and sequential. In: PLDI (2004)

Digital Library

[18]

Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. In: TOPLAS (2000)

Digital Library

[19]

Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: POPL (1995)

Digital Library

[20]

Schwoon, S.: Moped, http://www.fmi.uni-stuttgart.de/szs/tools/moped/

[21]

Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, Technical Univ. of Munich, Munich, Germany (July 2002)

[22]

Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Program Flow Analysis: Theory and Applications, Prentice-Hall, Englewood Cliffs (1981)

Digital Library

Cited By

Pick LDesai AGupta A(2023)Psym: Efficient Symbolic Exploration of Distributed SystemsProceedings of the ACM on Programming Languages10.1145/35912477:PLDI(660-685)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591247
Farzan AKlumpp DPodelski AJhala RDillig I(2022)Sound sequentialization for concurrent program verificationProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523727(506-521)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523727
Di Stefano LDe Nicola RInverso O(2022)Verification of Distributed Systems via Sequential EmulationACM Transactions on Software Engineering and Methodology10.1145/349038731:3(1-41)Online publication date: 7-Mar-2022
https://dl.acm.org/doi/10.1145/3490387
Show More Cited By

Index Terms

Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Concurrent programming languages
2. Theory of computation
  1. Logic

Index terms have been assigned to the content through auto-classification.

Recommendations

Reducing concurrent analysis under a context bound to sequential analysis

This paper addresses the analysis of concurrent programs with shared memory. Such an analysis is undecidable in the presence of multiple procedures. One approach used in recent work obtains decidability by providing only a partial guarantee of ...
Rely-guarantee bound analysis of parameterized concurrent shared-memory programs: With an application to proving that non-blocking algorithms are bounded lock-free
Abstract
We present a thread-modular proof method for complexity and resource bound analysis of concurrent, shared-memory programs. To this end, we lift Jones’ rely-guarantee reasoning to assumptions and commitments capable of expressing bounds. The ...
Context-Bounded Analysis for Concurrent Programs with Dynamic Creation of Threads
TACAS '09: Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems: Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009,

Context-bounded analysis has been shown to be both efficient and effective at finding bugs in concurrent programs. According to its original definition, context-bounded analysis explores all behaviors of a concurrent program up to some fixed number of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

CAV '08: Proceedings of the 20th international conference on Computer Aided Verification

July 2008

555 pages

ISBN:9783540705437

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 07 July 2008

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

36
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Pick LDesai AGupta A(2023)Psym: Efficient Symbolic Exploration of Distributed SystemsProceedings of the ACM on Programming Languages10.1145/35912477:PLDI(660-685)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591247
Farzan AKlumpp DPodelski AJhala RDillig I(2022)Sound sequentialization for concurrent program verificationProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523727(506-521)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523727
Di Stefano LDe Nicola RInverso O(2022)Verification of Distributed Systems via Sequential EmulationACM Transactions on Software Engineering and Methodology10.1145/349038731:3(1-41)Online publication date: 7-Mar-2022
https://dl.acm.org/doi/10.1145/3490387
Harmim DMarcin VSvobodová LVojnar T(2022)Static Deadlock Detection in Low-Level C CodeComputer Aided Systems Theory – EUROCAST 202210.1007/978-3-031-25312-6_31(267-276)Online publication date: 20-Feb-2022
https://dl.acm.org/doi/10.1007/978-3-031-25312-6_31
Kragl BEnea CHenzinger TMutluergil SQadeer SDonaldson ATorlak E(2020)Inductive sequentialization of asynchronous programsProceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3385412.3385980(227-242)Online publication date: 11-Jun-2020
https://dl.acm.org/doi/10.1145/3385412.3385980
Bak SChaki S(2016)Verifying cyber-physical systems by combining software model checking with hybrid systems reachabilityProceedings of the 13th International Conference on Embedded Software10.1145/2968478.2968490(1-10)Online publication date: 1-Oct-2016
https://dl.acm.org/doi/10.1145/2968478.2968490
Ahn SMalik SGupta ANicolescu GGerstlauer A(2015)Completeness bounds and sequentialization for model checking of interacting firmware and hardwareProceedings of the 10th International Conference on Hardware/Software Codesign and System Synthesis10.5555/2830840.2830862(202-211)Online publication date: 4-Oct-2015
https://dl.acm.org/doi/10.5555/2830840.2830862
Deligiannis PDonaldson ARakamarić ZCohen MGrunske LWhalen M(2015)Fast and precise symbolic analysis of concurrency bugs in device driversProceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE.2015.30(166-177)Online publication date: 9-Nov-2015
https://dl.acm.org/doi/10.1109/ASE.2015.30
Chaki SGurfinkel ASinha NJobstmann B(2014)Efficient Verification of Periodic Programs using Sequential Consistency and SnapshotsProceedings of the 14th Conference on Formal Methods in Computer-Aided Design10.5555/2682923.2682939(51-58)Online publication date: 21-Oct-2014
https://dl.acm.org/doi/10.5555/2682923.2682939
Ahn SMalik SMarculescu RNicolescu G(2014)Automated firmware testing using firmware-hardware interaction patternsProceedings of the 2014 International Conference on Hardware/Software Codesign and System Synthesis10.1145/2656075.2656080(1-10)Online publication date: 12-Oct-2014
https://dl.acm.org/doi/10.1145/2656075.2656080
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents