research-article

Optimal context-sensitive dynamic partial order reduction with observers

Authors:

Maria Garcia de la Banda,

Miguel Gómez-Zamalloa,

Peter J. StuckeyAuthors Info & Claims

ISSTA 2019: Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis

Pages 352 - 362

https://doi.org/10.1145/3293882.3330565

Published: 10 July 2019 Publication History

Abstract

Dynamic Partial Order Reduction (DPOR) algorithms are used in stateless model checking to avoid the exploration of equivalent execution sequences. DPOR relies on the notion of independence between execution steps to detect equivalence. Recent progress in the area has introduced more accurate ways to detect independence: Context-Sensitive DPOR considers two steps p and t independent in the current state if the states obtained by executing p · t and t · p are the same; Optimal DPOR with Observers makes their dependency conditional to the existence of future events that observe their operations. We introduce a new algorithm, Optimal Context-Sensitive DPOR with Observers, that combines these two notions of conditional independence, and goes beyond them by exploiting their synergies. Experimental evaluation shows that our gains increase exponentially with the size of the considered inputs.

References

[1]

Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. Source sets: A foundation for optimal dynamic partial order reduction. J. ACM, 64(4):25:1–25:49, 2017.

Digital Library

[2]

Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos F. Sagonas. Optimal Dynamic Partial Order Reduction. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’14, San Diego, CA, USA, January 20-21, 2014, pages 373–384. ACM, 2014.

Digital Library

[3]

Elvira Albert, Puri Arenas, María García de la Banda, Miguel Gómez-Zamalloa, and Peter Stuckey. Context Sensitive Dynamic Partial Order Reduction. In Victor Kuncak and Rupak Majumdar, editors, 29th International Conference on Computer Aided Verification (CAV 2017), volume 10426 of Lecture Notes in Computer Science, pages 526–543. Springer, 2017.

[4]

Elvira Albert, Miguel Gómez-Zamalloa, and Miguel Isabel. Syco: A Systematic Testing Tool for Concurrent Objects. In Ayal Zaks and Manuel V. Hermenegildo, editors, Proceedings of the 25th International Conference on Compiler Construction, CC 2016, Barcelona, Spain, March 12-18, 2016, pages 269–270. ACM, 2016.

Digital Library

[5]

Elvira Albert, Miguel Gómez-Zamalloa, Miguel Isabel, and Albert Rubio. Constrained Dynamic Partial Order Reduction. In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II, volume 10982 of Lecture Notes in Computer Science, pages 392–410. Springer, 2018.

[6]

Elvira Albert, Miguel Gómez-Zamalloa, Albert Rubio, Matteo Sammartino, and Alexandra Silva. Sdn-actors: Modeling and verification of SDN programs. In Formal Methods - 22nd International Symposium, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 15-17, 2018, Proceedings, pages 550–567, 2018.

[7]

Stavros Aronis, Bengt Jonsson, Magnus Lång, and Konstantinos Sagonas. Optimal dynamic partial order reduction with observers. In Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II, pages 229–248, 2018.

[8]

Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya. Data-centric dynamic partial order reduction. PACMPL, 2(POPL):31:1–31:30, 2018.

Digital Library

[9]

Edmund M. Clarke, Orna Grumberg, Marius Minea, and Doron A. Peled. State space reduction using partial order techniques. STTT, 2(3):279–287, 1999.

[10]

Cormac Flanagan and Patrice Godefroid. Dynamic Partial-Order Reduction for Model Checking Software. In Jens Palsberg and Martín Abadi, editors, Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005, pages 110–121. ACM, 2005.

Digital Library

[11]

Optimal Context-Sensitive DPOR with Observers ISSTA ’19, July 15–19, 2019, Beijing, China

[12]

Patrice Godefroid. Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem, volume 1032 of LNCS. Springer, 1996.

Digital Library

[13]

Patrice Godefroid and Didier Pirottin. Refining dependencies improves partialorder verification methods (extended abstract). In CAV, pages 438–449, 1993.

Digital Library

[14]

Einar Broch Johnsen, Reiner Hähnle, Jan Schäfer, Rudolf Schlatte, and Martin Steffen. ABS: A Core Language for Abstract Behavioral Specification. In Bernhard K. Aichernig, Frank S. de Boer, and Marcello M. Bonsangue, editors, Formal Methods for Components and Objects - 9th International Symposium, FMCO 2010, Graz, Austria, November 29 - December 1, 2010. Revised Papers, volume 6957 of Lecture Notes in Computer Science, pages 142–164. Springer, 2012.

Digital Library

[15]

Vineet Kahlon, Chao Wang, and Aarti Gupta. Monotonic partial order reduction: An optimal symbolic partial order reduction technique. In CAV, pages 398–413, 2009.

Digital Library

[16]

Shmuel Katz and Doron A. Peled. Defining conditional independence using collapses. TCS, 101(2):337–359, 1992.

Digital Library

[17]

Antoni W. Mazurkiewicz. Trace theory. In Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986, Part II, Proceedings of an Advanced Course, Bad Honnef, Germany, 8-19 September 1986, pages 279–324, 1986.

Digital Library

[18]

Huyen T. T. Nguyen, César Rodríguez, Marcelo Sousa, Camille Coti, and Laure Petrucci. Quasi-optimal partial order reduction. In Hana Chockler and Georg Weissenbacher, editors, Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II, volume 10982 of Lecture Notes in Computer Science, pages 354–371. Springer, 2018.

[19]

César Rodríguez, Marcelo Sousa, Subodh Sharma, and Daniel Kroening. Unfolding-based partial order reduction. In 26th International Conference on Concurrency Theory, CONCUR 2015, Madrid, Spain, September 1.4, 2015, pages 456–469, 2015.

[20]

Antti Valmari. Stubborn Sets for Reduced State Space Generation. In Grzegorz Rozenberg, editor, Advances in Petri Nets 1990 {10th International Conference on Applications and Theory of Petri Nets, Bonn, Germany, June 1989, Proceedings}, volume 483 of Lecture Notes in Computer Science, pages 491–515. Springer, 1989.

Digital Library

[21]

Chao Wang, Zijiang Yang, Vineet Kahlon, and Aarti Gupta. Peephole Partial Order Reduction. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, volume 4963 of Lecture Notes in Computer Science, pages 382–396. Springer, 2008.

Digital Library

Cited By

Hähnle RKamburjan EScaletta M(2024)Context-Aware Trace ContractsActive Object Languages: Current Research Trends10.1007/978-3-031-51060-1_11(289-322)Online publication date: 29-Jan-2024
https://doi.org/10.1007/978-3-031-51060-1_11
Yang XYe CChen Y(2023)Depth-First Net Unfoldings and Equivalent ReductionSymmetry10.3390/sym1509177515:9(1775)Online publication date: 16-Sep-2023
https://doi.org/10.3390/sym15091775
Albert Ede la Banda MGómez-Zamalloa MIsabel MStuckey P(2023)Optimal dynamic partial order reduction with context-sensitive independence and observersJournal of Systems and Software10.1016/j.jss.2023.111730202(111730)Online publication date: Aug-2023
https://doi.org/10.1016/j.jss.2023.111730
Show More Cited By

Index Terms

Optimal context-sensitive dynamic partial order reduction with observers
1. Software and its engineering
  1. Software creation and management
    1. Software development techniques
      1. Automatic programming

Recommendations

Optimal dynamic partial order reduction with context-sensitive independence and observers
Abstract
Dynamic Partial Order Reduction (DPOR) algorithms are used in stateless model checking of concurrent programs to avoid the exploration of equivalent execution sequences. In order to detect equivalence, DPOR relies on the notion of independence ...
Highlights
- Extension of Context-sensitive DPOR to work over Optimal DPOR with wakeup trees.
- A new DPOR algorithm that integrates context-sensitive dependency and observers.
- Implementation and evaluation of these algorithms within the Nidhugg ...
Partial-Order Reduction in Symbolic State-Space Exploration
Special issue on CAV '97

State-space explosion is a fundamental obstacle in the formal verification of designs and protocols. Several techniques for combating this problem have emerged in the past few years, among which two are significant: partial-order reduction and symbolic ...
Cluster-Based Partial-Order Reduction

The verification of concurrent systems through an exhaustive traversal of the state space suffers from the infamous state-space-explosion problem, caused by the many interleavings of actions of different processes in the system. Partial-order reduction ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ISSTA 2019: Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis

July 2019

451 pages

ISBN:9781450362245

DOI:10.1145/3293882

General Chair:
Dongmei Zhang
Microsoft Research, China
,
Program Chair:
Anders Møller
Aarhus University, Denmark

Copyright © 2019 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

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 10 July 2019

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ISSTA '19

Sponsor:

SIGSOFT

ISSTA '19: 28th ACM SIGSOFT International Symposium on Software Testing and Analysis

July 15 - 19, 2019

Beijing, China

Acceptance Rates

Overall Acceptance Rate 58 of 213 submissions, 27%

Upcoming Conference

ISSTA '25

Sponsor:
sigsoft

34th ACM SIGSOFT International Symposium on Software Testing and Analysis

June 25 - 28, 2025

Trondheim , Norway

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
175
Total Downloads

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

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Hähnle RKamburjan EScaletta M(2024)Context-Aware Trace ContractsActive Object Languages: Current Research Trends10.1007/978-3-031-51060-1_11(289-322)Online publication date: 29-Jan-2024
https://doi.org/10.1007/978-3-031-51060-1_11
Yang XYe CChen Y(2023)Depth-First Net Unfoldings and Equivalent ReductionSymmetry10.3390/sym1509177515:9(1775)Online publication date: 16-Sep-2023
https://doi.org/10.3390/sym15091775
Albert Ede la Banda MGómez-Zamalloa MIsabel MStuckey P(2023)Optimal dynamic partial order reduction with context-sensitive independence and observersJournal of Systems and Software10.1016/j.jss.2023.111730202(111730)Online publication date: Aug-2023
https://doi.org/10.1016/j.jss.2023.111730
Gomez-Zamalloa MIsabel M(2021)Deadlock-Guided TestingIEEE Access10.1109/ACCESS.2021.30654219(46033-46048)Online publication date: 2021
https://doi.org/10.1109/ACCESS.2021.3065421
Coti CPetrucci LRodríguez CSousa M(2020)Quasi-optimal partial order reductionFormal Methods in System Design10.1007/s10703-020-00350-4Online publication date: 12-Oct-2020
https://doi.org/10.1007/s10703-020-00350-4
Schemmel DBüning JRodríguez CLaprell DWehrle K(2020)Symbolic Partial-Order Execution for Testing Multi-Threaded ProgramsComputer Aided Verification10.1007/978-3-030-53288-8_18(376-400)Online publication date: 14-Jul-2020
https://doi.org/10.1007/978-3-030-53288-8_18
Isabel MZhang DMøller A(2019)Conditional dynamic partial order reduction and optimality resultsProceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3293882.3338987(433-437)Online publication date: 10-Jul-2019
https://dl.acm.org/doi/10.1145/3293882.3338987

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