research-article

Scheduling constraint based abstraction refinement for weak memory models

Authors:

Ji WangAuthors Info & Claims

ASE '18: Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering

Pages 645 - 655

https://doi.org/10.1145/3238147.3238223

Published: 03 September 2018 Publication History

Abstract

Scheduling constraint based abstraction refinement (SCAR) is one of the most efficient methods for verifying programs under sequential consistency (SC). However, most multi-processor architectures implement weak memory models (WMMs) in order to improve the performance of a program. Due to the nondeterministic execution of those memory operations by the same thread, the behavior of a program under WMMs is much more complex than that under SC, which significantly increases the verification complexity. This paper elegantly extends the SCAR method to WMMs such as TSO and PSO. To capture the order requirements of an abstraction counterexample under WMMs, we have enriched the event order graph (EOG) of a counterexample such that it is competent for both SC and WMMs. We have also proposed a unified EOG generation method which can always obtain a minimal EOG efficiently. Experimental results on a large set of multi-threaded C programs show promising results of our method. It significantly outperforms state-of-the-art tools, and the time and memory it required to verify a program under TSO and PSO are roughly comparable to that under SC.

References

[1]

Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, and Konstantinos Sagonas. 2015. Stateless Model Checking for TSO and PSO. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS. London, UK, 353–367.

Digital Library

[2]

Parosh Aziz Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. 2014. Optimal Dynamic Partial Order Reduction. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL. San Diego, CA, USA, 373–384.

Digital Library

[3]

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Carl Leonardsson, and Ahmed Rezine. 2012. Counter-Example Guided Fence Insertion under TSO. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS. Tallinn, Estonia, 204–219. 978-3-642-28756-5_15

Digital Library

[4]

Jade Alglave, Daniel Kroening, Vincent Nimal, and Michael Tautschnig. 2013. Software Verification for Weak Memory via Program Transformation. In European Symposium on Programming, ESOP. Rome, Italy, 512–532. 1007/978-3-642-37036-6_28

Digital Library

[5]

Jade Alglave, Daniel Kroening, and Michael Tautschnig. 2013. Partial Orders for Efficient Bounded Model Checking of Concurrent Software. In International Conference on Computer Aided Verification, CAV. Saint Petersburg, Russia, 141–157.

[6]

Mohamed Faouzi Atig, Ahmed Bouajjani, and Gennaro Parlato. 2011. Getting Rid of Store-Buffers in TSO Analysis. In International Conference on Computer Aided Verification, CAV. Snowbird, UT, USA, 99–115. 978-3-642-22110-1_9

Digital Library

[7]

Jiri Barnat, Lubos Brim, Vojtech Havel, Jan Havlícek, Jan Kriho, Milan Lenco, Petr Rockai, Vladimír Still, and Jirí Weiser. 2013. DiVinE 3.0 - An Explicit-State Model Checker for Multithreaded C & C++ Programs. In International Conference on Computer Aided Verification, CAV. Saint Petersburg, Russia, 863– 868.

[8]

Tom Bergan, Luis Ceze, and Dan Grossman. 2013. Input-covering schedules for multithreaded programs. In ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA. Indianapolis, IN, USA, 677–692.

Digital Library

[9]

Dirk Beyer. 2017. Software Verification with Validation of Results - (Report on SV-COMP 2017). In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS. Uppsala, Sweden, 331–349. SCAR for Weak Memory Models ASE ’18, September 3–7, 2018, Montpellier, France

Digital Library

[10]

Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. 1999. Symbolic Model Checking without BDDs. In International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS. Amsterdam, The Netherlands, 193–207.

Digital Library

[11]

Sebastian Burckhardt, Rajeev Alur, and Milo M. K. Martin. 2007. CheckFence: Checking Consistency of Concurrent Data Types on Relaxed Memory Models. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI. San Diego, California, USA, 12–21.

Digital Library

[12]

Katherine E. Coons, Madan Musuvathi, and Kathryn S. McKinley. 2013. Bounded Partial-Order Reduction. In ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA. Indianapolis, IN, USA, 833–848.

Digital Library

[13]

Andrei Marian Dan, Yuri Meshman, Martin T. Vechev, and Eran Yahav. 2013. Predicate Abstraction for Relaxed Memory Models. In International Symposium on Static Analysis, SAS. Seattle, WA, USA, 84–104. 978-3-642-38856-9_7

[14]

Brian Demsky and Patrick Lam. 2015. SATCheck: SAT-Directed Stateless Model Checking for SC and TSO. In ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA. Pittsburgh, PA, USA, 20–36.

Digital Library

[15]

Henning Günther, Alfons Laarman, and Georg Weissenbacher. 2016. Vienna Verification Tool: IC3 for Parallel Software - (Competition Contribution). In International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS. Eindhoven, The Netherlands, 954–957. 978-3-662-49674-9_69

Digital Library

[16]

Ashutosh Gupta, Thomas A. Henzinger, Arjun Radhakrishna, Roopsha Samanta, and Thorsten Tarrach. 2015. Succinct Representation of Concurrent Trace Sets. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL. Mumbai, India, 433–444.

Digital Library

[17]

Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko. 2011. Predicate Abstraction and Refinement for Verifying Multi-threaded Programs. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL. Austin, TX, USA, 331–344.

Digital Library

[18]

Jeff Huang. 2015. Stateless Model Checking Concurrent Programs with Maximal Causality Reduction. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI. Portland, OR, USA, 165–174.

Digital Library

[19]

Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato. 2014. Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization. In International Conference on Computer Aided Verification, CAV. Vienna, Austria, 585–602.

Digital Library

[20]

Alexander Malkis, Andreas Podelski, and Andrey Rybalchenko. 2010. Thread-Modular Counterexample-Guided Abstraction Refinement. In International Static Analysis Symposium, SAS. 356–372. 22

Digital Library

[21]

Cathy May, Ed Silha, Rick Simpson, and Hank Warren. 1994. The PowerPC architecture: a specification for a new family of RISC processors. Morgan Kaufmann Publishers Inc.

Digital Library

[22]

Yuri Meshman, Andrei Marian Dan, Martin T. Vechev, and Eran Yahav. 2014. Synthesis of Memory Fences via Refinement Propagation. In International Symposium on Static Analysis, SAS. Munich, Germany, 237–252. 1007/978-3-319-10936-7_15

[23]

Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, and Magnus O. Myreen. 2010. x86-TSO: A Rigorous and Usable Programmer’s Model for x86 Multiprocessors. Commun. ACM 53, 7 (2010), 89–97. 1785414.1785443

Digital Library

[24]

Nishant Sinha and Chao Wang. 2011. On Interference Abstractions. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL. Austin, TX, USA, 423–434.

Digital Library

[25]

SV-COMP. 2018. 2018 software verification competition. http://sv-comp.sosy-lab. org/2018/.

[26]

Ermenegildo Tomasco, Omar Inverso, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato. 2015. Verifying Concurrent Programs by Memory Unwinding. In International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS. London, UK, 551–565. 978-3-662-46681-0_52

Digital Library

[27]

Ermenegildo Tomasco, Truc L. Nguyen, Omar Inverso, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato. 2016. Lazy Sequentialization for TSO and PSO via Shared Memory Abstractions. In 2016 Formal Methods in Computer-Aided Design, FMCAD 2016. Mountain View, CA, USA, 193–200. 1109/FMCAD.2016.7886679

Digital Library

[28]

David L. Weaver, Tom Germond, Ghassan Abbas, Published Ptr, and Prentice Hall. 1992. The SPARC Architecture Manual. Cliffs Nj (1992).

Digital Library

[29]

Jingyue Wu, Yang Tang, Gang Hu, Heming Cui, and Junfeng Yang. 2012. Sound and precise analysis of parallel programs through schedule specialization. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI. Beijing, China, 205–216.

Digital Library

[30]

Liangze Yin, Wei Dong, Wanwei Liu, Yunchou Li, and Ji Wang. 2018. YOGARCBMC: CBMC with Scheduling Constraint Based Abstraction Refinement - (Competition Contribution). In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS. Thessaloniki, Greece, 422–426.

[31]

Liangze Yin, Wei Dong, Wanwei Liu, and Ji Wang. 2017. Scheduling Constraint Based Abstraction Refinement for Multi-Threaded Program Verification. CoRR abs/1708.08323 (2017). http://arxiv.org/abs/1708.08323

Cited By

Kim YChoi Y(2024)PBE-Based Selective Abstraction and Refinement for Efficient Property Falsification of Embedded SoftwareProceedings of the ACM on Software Engineering10.1145/36437401:FSE(293-315)Online publication date: 12-Jul-2024
https://dl.acm.org/doi/10.1145/3643740
Fan HSun ZHe F(2023)Satisfiability Modulo Ordering Consistency Theory for SC, TSO, and PSO Memory ModelsACM Transactions on Programming Languages and Systems10.1145/357983545:1(1-37)Online publication date: 17-Jan-2023
https://dl.acm.org/doi/10.1145/3579835
Marmanis IVafeiadis V(2023)SMT-Based Verification of Persistency Invariants of Px86 ProgramsVerified Software. Theories, Tools and Experiments.10.1007/978-3-031-25803-9_6(92-110)Online publication date: 1-Feb-2023
https://doi.org/10.1007/978-3-031-25803-9_6
Show More Cited By

Index Terms

Scheduling constraint based abstraction refinement for weak memory models
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation

Recommendations

Parameterized Static Analysis for Weak Memory Models
ISEC '24: Proceedings of the 17th Innovations in Software Engineering Conference

Verifying programs under weak memory models (WMMs) is vital due to their prevalence in modern computer architectures. These models introduce complexities, allowing unexpected reordering and visibility of memory operations. Ensuring correctness is ...
Abstraction refinement for termination
SAS'05: Proceedings of the 12th international conference on Static Analysis

Abstraction can often lead to spurious counterexamples. Counterexample-guided abstraction refinement is a method of strengthening abstractions based on the analysis of these spurious counterexamples. For invariance properties, a counterexample is a ...
SAT-based counterexample-guided abstraction refinement

We describe new techniques for model checking in the counterexample-guided abstraction-refinement framework. The abstraction phase "hides" the logic of various variables, hence considering them as inputs. This type of abstraction may lead to "spurious" ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ASE '18: Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering

September 2018

955 pages

ISBN:9781450359375

DOI:10.1145/3238147

General Chair:
Marianne Huchard
University of Montpellier, France
,
Program Chairs:
Christian Kästner
Carnegie Mellon University, USA
,
Gordon Fraser
University of Passau, Germany

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

SIGAI: ACM Special Interest Group on Artificial Intelligence
CNRS: Centre National De La Rechercue Scientifique
SIGSOFT: ACM Special Interest Group on Software Engineering
IEEE-CS: Computer Society

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 03 September 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

National key R&D program of China
National Nature Science Foundation of China

Conference

ASE '18

Sponsor:

SIGAI
CNRS
SIGSOFT
IEEE-CS

ASE '18: 33rd ACM/IEEE International Conference on Automated Software Engineering

September 3 - 7, 2018

Montpellier, France

Acceptance Rates

Overall Acceptance Rate 82 of 337 submissions, 24%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
184
Total Downloads

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

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kim YChoi Y(2024)PBE-Based Selective Abstraction and Refinement for Efficient Property Falsification of Embedded SoftwareProceedings of the ACM on Software Engineering10.1145/36437401:FSE(293-315)Online publication date: 12-Jul-2024
https://dl.acm.org/doi/10.1145/3643740
Fan HSun ZHe F(2023)Satisfiability Modulo Ordering Consistency Theory for SC, TSO, and PSO Memory ModelsACM Transactions on Programming Languages and Systems10.1145/357983545:1(1-37)Online publication date: 17-Jan-2023
https://dl.acm.org/doi/10.1145/3579835
Marmanis IVafeiadis V(2023)SMT-Based Verification of Persistency Invariants of Px86 ProgramsVerified Software. Theories, Tools and Experiments.10.1007/978-3-031-25803-9_6(92-110)Online publication date: 1-Feb-2023
https://doi.org/10.1007/978-3-031-25803-9_6
Sun ZFan HHe F(2022)Consistency-preserving propagation for SMT solving of concurrent program verificationProceedings of the ACM on Programming Languages10.1145/35633216:OOPSLA2(929-956)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563321
Fan HLiu WHe FLee JAgrawal KSpear M(2022)Interference relation-guided SMT solving for multi-threaded program verificationProceedings of the 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming10.1145/3503221.3508424(163-176)Online publication date: 2-Apr-2022
https://dl.acm.org/doi/10.1145/3503221.3508424
He FSun ZFan HFreund SYahav E(2021)Satisfiability modulo ordering consistency theory for multi-threaded program verificationProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454108(1264-1279)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454108
Wang HXu CGuo BMa XLu J(2021)Generic Adaptive Scheduling for Efficient Context Inconsistency DetectionIEEE Transactions on Software Engineering10.1109/TSE.2019.289897647:3(464-497)Online publication date: 1-Mar-2021
https://doi.org/10.1109/TSE.2019.2898976
Verma AKalita PPandey ARoy SMars JTang LXue JWu P(2020)Interactive debugging of concurrent programs under relaxed memory modelsProceedings of the 18th ACM/IEEE International Symposium on Code Generation and Optimization10.1145/3368826.3377910(68-80)Online publication date: 22-Feb-2020
https://dl.acm.org/doi/10.1145/3368826.3377910

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