research-article

Satisfiability modulo ordering consistency theory for multi-threaded program verification

Authors:

Hongyu FanAuthors Info & Claims

PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

Pages 1264 - 1279

https://doi.org/10.1145/3453483.3454108

Published: 18 June 2021 Publication History

Abstract

Analyzing multi-threaded programs is hard due to the number of thread interleavings. Partial orders can be used for modeling and analyzing multi-threaded programs. However, there is no dedicated decision procedure for solving partial-order constraints. In this paper, we propose a novel ordering consistency theory for multi-threaded program verification under sequential consistency, and we elaborate its theory solver, which realizes incremental consistency checking, minimal conflict clause generation, and specialized theory propagation to improve the efficiency of SMT solving. We conducted extensive experiments on credible benchmarks; the results show significant promotion of our approach.

References

[1]

Parosh Abdulla, Stavros Aronis, Bengt Jonsson, and Konstantinos Sagonas. 2014. Optimal Dynamic Partial Order Reduction. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’14). Association for Computing Machinery, New York, NY, USA. 373–384. isbn:9781450325448 https://doi.org/10.1145/2535838.2535845

Digital Library

[2]

Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, and Konstantinos Sagonas. 2015. Stateless Model Checking for TSO and PSO. In Tools and Algorithms for the Construction and Analysis of Systems, Christel Baier and Cesare Tinelli (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 353–367. isbn:978-3-662-46681-0 https://doi.org/10.1007/978-3-662-46681-0_28

Digital Library

[3]

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, and Carl Leonardsson. 2016. Stateless Model Checking for POWER. In Computer Aided Verification, Swarat Chaudhuri and Azadeh Farzan (Eds.). Springer International Publishing, Cham. 134–156. isbn:978-3-319-41540-6 https://doi.org/10.1007/978-3-319-41540-6_8

[4]

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, Magnus Lång, Tuan Phong Ngo, and Konstantinos Sagonas. 2019. Optimal Stateless Model Checking for Reads-from Equivalence under Sequential Consistency. Proc. ACM Program. Lang., 3, OOPSLA (2019), Article 150, Oct., 29 pages. https://doi.org/10.1145/3360576

Digital Library

[5]

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, Magnus Lång, Tuan Phong Ngo, and Konstantinos Sagonas. 2019. Optimal Stateless Model Checking for Reads-from Equivalence under Sequential Consistency. Proc. ACM Program. Lang., 3, OOPSLA (2019), Article 150, Oct., 29 pages. https://doi.org/10.1145/3360576

Digital Library

[6]

Sarita V Adve and Kourosh Gharachorloo. 1996. Shared memory consistency models: A tutorial. computer, 29, 12 (1996), 66–76. https://doi.org/10.1109/2.546611

Digital Library

[7]

Deepak Ajwani and Tobias Friedrich. 2007. Average-Case Analysis of Online Topological Ordering. In Proceedings of the 18th International Conference on Algorithms and Computation (ISAAC’07). Springer-Verlag, Berlin, Heidelberg. 464–475. isbn:3540771182 https://doi.org/10.1007/978-3-540-77120-3_41

[8]

Deepak Ajwani, Tobias Friedrich, and Ulrich Meyer. 2008. An O(N2.75) Algorithm for Incremental Topological Ordering. ACM Trans. Algorithms, 4, 4 (2008), Article 39, Aug., 14 pages. issn:1549-6325 https://doi.org/10.1145/1383369.1383370

Digital Library

[9]

Jade Alglave, Daniel Kroening, Vincent Nimal, and Daniel Poetzl. 2014. Don’t Sit on the Fence. In Computer Aided Verification, Armin Biere and Roderick Bloem (Eds.). Springer International Publishing, Cham. 508–524. isbn:978-3-319-08867-9 https://doi.org/10.1007/978-3-319-08867-9_33

Digital Library

[10]

Jade Alglave, Daniel Kroening, and Michael Tautschnig. 2013. Partial Orders for Efficient Bounded Model Checking of Concurrent Software. In Computer Aided Verification, Natasha Sharygina and Helmut Veith (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 141–157. isbn:978-3-642-39799-8 https://doi.org/10.1007/978-3-642-39799-8_9

[11]

Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. 2010. Fences in Weak Memory Models. In Computer Aided Verification, Tayssir Touili, Byron Cook, and Paul Jackson (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 258–272. isbn:978-3-642-14295-6 https://doi.org/10.1007/978-3-642-14295-6_25

Digital Library

[12]

Clark Barrett and Cesare Tinelli. 2018. Satisfiability Modulo Theories. Springer International Publishing, Cham. 305–343. isbn:978-3-319-10575-8 https://doi.org/10.1007/978-3-319-10575-8_11

[13]

Michael A. Bender, Jeremy T. Fineman, Seth Gilbert, and Robert E. Tarjan. 2015. A New Approach to Incremental Cycle Detection and Related Problems. ACM Trans. Algorithms, 12, 2 (2015), Article 14, Dec., 22 pages. issn:1549-6325 https://doi.org/10.1145/2756553

Digital Library

[14]

Dirk Beyer, Thomas A. Henzinger, and Grégory Théoduloz. 2007. Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis. In Computer Aided Verification, Werner Damm and Holger Hermanns (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 504–518. isbn:978-3-540-73368-3 https://doi.org/10.1007/978-3-540-73368-3_51

[15]

Dirk Beyer and M. Erkan Keremoglu. 2011. CPAchecker: A Tool for Configurable Software Verification. In Computer Aided Verification, Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 184–190. isbn:978-3-642-22110-1 https://doi.org/10.1007/978-3-642-22110-1_16

[16]

Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu. 1999. Symbolic Model Checking without BDDs. In Tools and Algorithms for the Construction and Analysis of Systems, W. Rance Cleaveland (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 193–207. isbn:978-3-540-49059-3 https://doi.org/10.1007/3-540-49059-0_14

[17]

Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya. 2017. Data-Centric Dynamic Partial Order Reduction. Proc. ACM Program. Lang., 2, POPL (2017), Article 31, Dec., 30 pages. https://doi.org/10.1145/3158119

Digital Library

[18]

Marek Chalupa, Krishnendu Chatterjee, Andreas Pavlogiannis, Nishant Sinha, and Kapil Vaidya. 2017. Data-Centric Dynamic Partial Order Reduction. Proc. ACM Program. Lang., 2, POPL (2017), Article 31, Dec., 30 pages. https://doi.org/10.1145/3158119

Digital Library

[19]

Edmund Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu. 2001. Bounded Model Checking Using Satisfiability Solving. Form. Methods Syst. Des., 19, 1 (2001), July, 7–34. issn:0925-9856 https://doi.org/10.1023/A:1011276507260

Digital Library

[20]

Lucas Cordeiro and Bernd Fischer. 2011. Verifying Multi-Threaded Software Using Smt-Based Context-Bounded Model Checking. In Proceedings of the 33rd International Conference on Software Engineering (ICSE ’11). Association for Computing Machinery, New York, NY, USA. 331–340. isbn:9781450304450 https://doi.org/10.1145/1985793.1985839

Digital Library

[21]

Ron Cytron, Jeanne Ferrante, Barry K. Rosen, Mark N. Wegman, and F. Kenneth Zadeck. 1991. Efficiently computing static single assignment form and the control dependence graph. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 13 (1991), 451–490. https://doi.org/10.1145/115372.115320

Digital Library

[22]

Martin Davis, George Logemann, and Donald Loveland. 1962. A Machine Program for Theorem-Proving. Commun. ACM, 5, 7 (1962), July, 394–397. issn:0001-0782 https://doi.org/10.1145/368273.368557

Digital Library

[23]

Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 337–340. isbn:978-3-540-78800-3 https://doi.org/10.1007/978-3-540-78800-3_24

[24]

Leonardo De Moura and Nikolaj Bjørner. 2011. Satisfiability modulo Theories: Introduction and Applications. Commun. ACM, 54, 9 (2011), Sept., 69–77. issn:0001-0782 https://doi.org/10.1145/1995376.1995394

Digital Library

[25]

Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, and Viktor Vafeiadis. 2010. Concurrent Abstract Predicates. In ECOOP 2010 – Object-Oriented Programming, Theo D’Hondt (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 504–528. isbn:978-3-642-14107-2 https://doi.org/10.1007/978-3-642-14107-2_24

[26]

Cormac Flanagan and Patrice Godefroid. 2005. Dynamic Partial-Order Reduction for Model Checking Software. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’05). Association for Computing Machinery, New York, NY, USA. 110–121. isbn:158113830X https://doi.org/10.1145/1040305.1040315

Digital Library

[27]

Malay K. Ganai and Aarti Gupta. 2008. Efficient Modeling of Concurrent Systems in BMC. In Model Checking Software, Klaus Havelund, Rupak Majumdar, and Jens Palsberg (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 114–133. isbn:978-3-540-85114-1 https://doi.org/10.1007/978-3-540-85114-1_10

Digital Library

[28]

Natalia Gavrilenko, Hernán Ponce-de León, Florian Furbach, Keijo Heljanko, and Roland Meyer. 2019. BMC for Weak Memory Models: Relation Analysis for Compact SMT Encodings. In Computer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.). Springer International Publishing, Cham. 355–365. isbn:978-3-030-25540-4 https://doi.org/10.1007/978-3-030-25540-4_19

[29]

Cunjing Ge, Feifei Ma, Jeff Huang, and Jian Zhang. 2016. SMT Solving for the Theory of Ordering Constraints. In Languages and Compilers for Parallel Computing, Xipeng Shen, Frank Mueller, and James Tuck (Eds.). Springer International Publishing, Cham. 287–302. isbn:978-3-319-29778-1 https://doi.org/10.1007/978-3-319-29778-1_18

Digital Library

[30]

Patrice Godefroid. 1997. Model Checking for Programming Languages Using VeriSoft. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’97). Association for Computing Machinery, New York, NY, USA. 174–186. isbn:0897918533 https://doi.org/10.1145/263699.263717

Digital Library

[31]

Ashutosh Gupta, Corneliu Popeea, and Andrey Rybalchenko. 2011. Predicate Abstraction and Refinement for Verifying Multi-Threaded Programs. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’11). Association for Computing Machinery, New York, NY, USA. 331–344. isbn:9781450304900 https://doi.org/10.1145/1926385.1926424

Digital Library

[32]

Bernhard Haeupler, Telikepalli Kavitha, Rogers Mathew, Siddhartha Sen, and Robert E. Tarjan. 2012. Incremental Cycle Detection, Topological Ordering, and Strong Component Maintenance. ACM Trans. Algorithms, 8, 1 (2012), Article 3, Jan., 33 pages. issn:1549-6325 https://doi.org/10.1145/2071379.2071382

Digital Library

[33]

Alex Horn and Jade Alglave. 2014. Concurrent Kleene Algebra of Partial Strings. arxiv:1407.0385. arxiv:1407.0385

[34]

Alex Horn and Daniel Kroening. 2015. On partial order semantics for SAT/SMT-based symbolic encodings of weak memory concurrency. arxiv:1504.00037. arxiv:1504.00037

[35]

Jeff Huang. 2015. Stateless Model Checking Concurrent Programs with Maximal Causality Reduction. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’15). Association for Computing Machinery, New York, NY, USA. 165–174. isbn:9781450334686 https://doi.org/10.1145/2737924.2737975

Digital Library

[36]

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 Computer Aided Verification, Armin Biere and Roderick Bloem (Eds.). Springer International Publishing, Cham. 585–602. isbn:978-3-319-08867-9 https://doi.org/10.1007/978-3-319-08867-9_39

Digital Library

[37]

Irit Katriel and Hans L. Bodlaender. 2006. Online Topological Ordering. ACM Trans. Algorithms, 2, 3 (2006), July, 364–379. issn:1549-6325 https://doi.org/10.1145/1159892.1159896

Digital Library

[38]

Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, and Viktor Vafeiadis. 2017. Effective Stateless Model Checking for C/C++ Concurrency. Proc. ACM Program. Lang., 2, POPL (2017), Article 17, Dec., 32 pages. https://doi.org/10.1145/3158105

Digital Library

[39]

Michalis Kokologiannakis, Azalea Raad, and Viktor Vafeiadis. 2019. Model Checking for Weakly Consistent Libraries. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2019). Association for Computing Machinery, New York, NY, USA. 96–110. isbn:9781450367127 https://doi.org/10.1145/3314221.3314609

Digital Library

[40]

Michalis Kokologiannakis, Azalea Raad, and Viktor Vafeiadis. 2019. Model Checking for Weakly Consistent Libraries. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2019). Association for Computing Machinery, New York, NY, USA. 96–110. isbn:9781450367127 https://doi.org/10.1145/3314221.3314609

Digital Library

[41]

Daniel Kroening and Michael Tautschnig. 2014. CBMC – C Bounded Model Checker. In Tools and Algorithms for the Construction and Analysis of Systems, Erika Ábrahám and Klaus Havelund (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 389–391. isbn:978-3-642-54862-8 https://doi.org/10.1007/978-3-642-54862-8_26

[42]

Leslie Lamport. 1979. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Computer Architecture Letters, 28, 09 (1979), 690–691. http://doi.org/10.1109/TC.1979.1675439

Digital Library

[43]

Alberto Marchetti-Spaccamela, Umberto Nanni, and Hans Rohnert. 1996. Maintaining a topological order under edge insertions. Inform. Process. Lett., 59, 1 (1996), 53 – 58. issn:0020-0190 https://doi.org/10.1016/0020-0190(96)00075-0

Digital Library

[44]

Antoni Mazurkiewicz. 1987. Trace theory. In Petri Nets: Applications and Relationships to Other Models of Concurrency, W. Brauer, W. Reisig, and G. Rozenberg (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 278–324. isbn:978-3-540-47926-0

[45]

Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. 2001. Chaff: Engineering an Efficient SAT Solver. In Proceedings of the 38th Annual Design Automation Conference (DAC ’01). Association for Computing Machinery, New York, NY, USA. 530–535. isbn:1581132972 https://doi.org/10.1145/378239.379017

Digital Library

[46]

Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. 2006. Solving SAT and SAT Modulo Theories: From an Abstract Davis–Putnam–Logemann–Loveland Procedure to DPLL(T). J. ACM, 53, 6 (2006), Nov., 937–977. issn:0004-5411 https://doi.org/10.1145/1217856.1217859

Digital Library

[47]

David J. Pearce and Paul H. J. Kelly. 2007. A Dynamic Topological Sort Algorithm for Directed Acyclic Graphs. ACM J. Exp. Algorithmics, 11 (2007), Feb., 1.7–es. issn:1084-6654 https://doi.org/10.1145/1187436.1210590

Digital Library

[48]

Alexander Schrijver. 1986. Theory of Linear and Integer Programming. John Wiley & Sons, Inc., USA. isbn:0471908541

[49]

Dennis Shasha and Marc Snir. 1988. Efficient and Correct Execution of Parallel Programs That Share Memory. ACM Trans. Program. Lang. Syst., 10, 2 (1988), April, 282–312. issn:0164-0925 https://doi.org/10.1145/42190.42277

Digital Library

[50]

Nishant Sinha and Chao Wang. 2011. On Interference Abstractions. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’11). Association for Computing Machinery, New York, NY, USA. 423–434. isbn:9781450304900 https://doi.org/10.1145/1926385.1926433

Digital Library

[51]

Chao Wang, HoonSang Jin, Gary D. Hachtel, and Fabio Somenzi. 2004. Refining the SAT Decision Ordering for Bounded Model Checking. In Proceedings of the 41st Annual Design Automation Conference (DAC ’04). Association for Computing Machinery, New York, NY, USA. 535–538. isbn:1581138288 https://doi.org/10.1145/996566.996713

Digital Library

[52]

Chao Wang, Sudipta Kundu, Malay Ganai, and Aarti Gupta. 2009. Symbolic Predictive Analysis for Concurrent Programs. In FM 2009: Formal Methods, Ana Cavalcanti and Dennis R. Dams (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 256–272. isbn:978-3-642-05089-3 https://doi.org/10.1007/978-3-642-05089-3_17

Digital Library

[53]

Chao Wang, Zijiang Yang, Vineet Kahlon, and Aarti Gupta. 2008. Peephole Partial Order Reduction. In Tools and Algorithms for the Construction and Analysis of Systems, C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 382–396. isbn:978-3-540-78800-3 https://doi.org/10.1007/978-3-540-78800-3_29

[54]

Liangze Yin, Wei Dong, Wanwei Liu, Yunchou Li, and Ji Wang. 2018. YOGAR-CBMC: CBMC with Scheduling Constraint Based Abstraction Refinement. In Tools and Algorithms for the Construction and Analysis of Systems, Dirk Beyer and Marieke Huisman (Eds.). Springer International Publishing, Cham. 422–426. isbn:978-3-319-89963-3 https://doi.org/10.1007/978-3-319-89963-3_25

[55]

Liangze Yin, Wei Dong, Wanwei Liu, and Ji Wang. 2018. Scheduling Constraint Based Abstraction Refinement for Weak Memory Models. In Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering (ASE 2018). Association for Computing Machinery, New York, NY, USA. 645–655. isbn:9781450359375 https://doi.org/10.1145/3238147.3238223

Digital Library

[56]

L. Yin, W. Dong, W. Liu, and J. Wang. 2020. On Scheduling Constraint Abstraction for Multi-Threaded Program Verification. IEEE Transactions on Software Engineering, 46, 5 (2020), may, 549–565. issn:1939-3520 https://doi.org/10.1109/TSE.2018.2864122

[57]

Naling Zhang, Markus Kusano, and Chao Wang. 2015. Dynamic Partial Order Reduction for Relaxed Memory Models. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’15). Association for Computing Machinery, New York, NY, USA. 250–259. isbn:9781450334686 https://doi.org/10.1145/2737924.2737956

Digital Library

Cited By

Heizmann MKlumpp DNitzke LSchüssele F(2024)Petrification: Software Model Checking for Programs with Dynamic Thread ManagementVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-50521-8_1(3-25)Online publication date: 15-Jan-2024
https://dl.acm.org/doi/10.1007/978-3-031-50521-8_1
Haas TMaseli RMeyer RPonce de León H(2023)Static Analysis of Memory Models for SMT EncodingsProceedings of the ACM on Programming Languages10.1145/36228557:OOPSLA2(1618-1647)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622855
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: 3-Mar-2023
https://dl.acm.org/doi/10.1145/3579835
Show More Cited By

Index Terms

Satisfiability modulo ordering consistency theory for multi-threaded program verification
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
2. Theory of computation
  1. Logic
    1. Logic and verification

Recommendations

Interference relation-guided SMT solving for multi-threaded program verification
PPoPP '22: Proceedings of the 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming

Concurrent program verification is challenging due to a large number of thread interferences. A popular approach is to encode concurrent programs as SMT formulas and then rely on off-the-shelf SMT solvers to accomplish the verification. In most existing ...
Satisfiability Modulo Ordering Consistency Theory for SC, TSO, and PSO Memory Models
Automatically verifying multi-threaded programs is difficult because of the vast number of thread interleavings, a problem aggravated by weak memory consistency. Partial orders can help with verification because they can represent many thread ...
Consistency-preserving propagation for SMT solving of concurrent program verification

The happens-before orders have been widely adopted to model thread interleaving behaviors of concurrent programs. A dedicated ordering theory solver, usually composed of theory propagation, consistency checking, and conflict clause generation, plays a ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 2021

1341 pages

ISBN:9781450383912

DOI:10.1145/3453483

General Chair:
Stephen N. Freund
Williams College, USA
,
Program Chair:
Eran Yahav
Technion, Israel

Copyright © 2021 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 the author(s) 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: 18 June 2021

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

PLDI '21

Sponsor:

SIGPLAN

PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 20 - 25, 2021

Virtual, Canada

Acceptance Rates

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

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
508
Total Downloads

Downloads (Last 12 months)107
Downloads (Last 6 weeks)11

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Heizmann MKlumpp DNitzke LSchüssele F(2024)Petrification: Software Model Checking for Programs with Dynamic Thread ManagementVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-50521-8_1(3-25)Online publication date: 15-Jan-2024
https://dl.acm.org/doi/10.1007/978-3-031-50521-8_1
Haas TMaseli RMeyer RPonce de León H(2023)Static Analysis of Memory Models for SMT EncodingsProceedings of the ACM on Programming Languages10.1145/36228557:OOPSLA2(1618-1647)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622855
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: 3-Mar-2023
https://dl.acm.org/doi/10.1145/3579835
Kokologiannakis MLahav OVafeiadis V(2023)Kater: Automating Weak Memory Model Metatheory and Consistency CheckingProceedings of the ACM on Programming Languages10.1145/35712127:POPL(544-572)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571212
Sharma RKulshreshtha SThakur MShirani POnut INg TKent KBaşar AOnut I(2022)ZS3: Marrying Static Analyzers and Constraint Solvers to Parallelize Loops in Managed RuntimesProceedings of the 32nd Annual International Conference on Computer Science and Software Engineering10.5555/3566055.3566082(213-220)Online publication date: 15-Nov-2022
https://dl.acm.org/doi/10.5555/3566055.3566082
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
Haas TMeyer RPonce de León H(2022)CAAT: consistency as a theoryProceedings of the ACM on Programming Languages10.1145/35632926:OOPSLA2(114-144)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563292
Aljaafari FMenezes RManino EShmarov FMustafa MCordeiro L(2022)Combining BMC and Fuzzing Techniques for Finding Software Vulnerabilities in Concurrent ProgramsIEEE Access10.1109/ACCESS.2022.322335910(121365-121384)Online publication date: 2022
https://doi.org/10.1109/ACCESS.2022.3223359
Marmanis IVafeiadis V(2022)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: 17-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-25803-9_6

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