Symbolic partial-order execution for testing multi-threaded programs

DOI10.1007/978-3-030-53288-8_18MaRDI QIDQ2225118zbMATH OpenOpenAlexFDO

Authors Daniel Schemmel, Julian Büning, César Rodríguez, David Laprell, Klaus Wehrle

Publication date 4 February 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2005.06688

zbMATH Keywords

software testingsymbolic executionpartial-order reduction

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Abstract: We describe a technique for systematic testing of multi-threaded programs. We combine Quasi-Optimal Partial-Order Reduction, a state-of-the-art technique that tackles path explosion due to interleaving non-determinism, with symbolic execution to handle data non-determinism. Our technique iteratively and exhaustively finds all executions of the program. It represents program executions using partial orders and finds the next execution using an underlying unfolding semantics. We avoid the exploration of redundant program traces using cutoff events. We implemented our technique as an extension of KLEE and evaluated it on a set of large multi-threaded C programs. Our experiments found several previously undiscovered bugs and undefined behaviors in memcached and GNU sort, showing that the new method is capable of finding bugs in industrial-size benchmarks.

Recommendations

• Monotonic Partial Order Reduction: An Optimal Symbolic Partial Order Reduction Technique
• Partial order aware concurrency sampling
• Framework for testing multi‐threaded Java programs
• scientific article; zbMATH DE number 1956607
• Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions

Cited in

(5)

• Compositional correctness and completeness for symbolic partial order reduction
• Multithreaded testing of program interfaces
• Quasi-optimal partial order reduction
• Framework for testing multi‐threaded Java programs
• Model checking race-freedom when ``sequential consistency for data-race-free programs is guaranteed

This page was built for publication: Symbolic partial-order execution for testing multi-threaded programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2225118)