The Store-Order Consistency Testing Problem for C-like Memory Models
Consistency testing is the problem of determining if an abstract execution of a concurrent program is feasible under a given memory model, i.e. does it have a concrete execution consistent with the memory model, and finds many applications in the testing and verification of concurrent software. Consequently, the complexity of consistency testing has been studied across several parametrizations, memory models, and levels of abstractions. Unfortunately, the consistency testing problem for store-order abstract executions (henceforth “store-order testing”), where the store-order relation is specified, has been understudied.
In this work, we initiate the study of store-order testing by exploring its algorithmic and complexity-theoretic landscape under the memory models RC20, RA, SRA, Relaxed, and Relaxed-Acyclic. We show that store-order testing is intractable for (even the RMW-free fragments of) RC20, RA, SRA, and Relaxed-Acyclic. We next identify a practically motivated fragment for which the store-order testing problem becomes tractable. Specifically, the single-writer fragment, i.e. the fragment where every location is written to by exactly one thread, admits an efficient algorithm, running in time $O(nk)$, and in $O(n)$ for specific subfragments. We extend this result by generalizing the single-writer constraint to a weaker one, which can be cleanly formalized as a new memory model we call ‘RC20-Ordered’. We also show that these algorithms are optimal or nearly optimal by establishing conditional super-linear lower bounds that also apply to the respective RMW-free fragments.
Wed 22 JanDisplayed time zone: Mountain Time (US & Canada) change
18:00 - 20:00 | |||
18:00 2hPoster | Efficient Strong Simulation of High-level Quantum Gates Student Research Competition | ||
18:00 2hPoster | Value semantics in reference-based languages Student Research Competition Hamza Remmal EPFL, LAMP | ||
18:00 2hPoster | Intermittent Concurrency Student Research Competition Myra Dotzel Carnegie Mellon University, Milijana Surbatovich University of Maryland, Limin Jia Carnegie Mellon University | ||
18:00 2hPoster | APIdemic: Verifying Idempotency of REST API Clients Student Research Competition Bhavik Kamlesh Goplani University of Kansas | ||
18:00 2hPoster | Formalizing Erlang’s Success Typings Student Research Competition Elan Semenova University of Maryland, College Park, Leonidas Lampropoulos University of Maryland, College Park | ||
18:00 2hPoster | A Complete Translation from Planning Problems to linear logic Student Research Competition | ||
18:00 2hPoster | Wanco: WebAssembly AOT Compiler that supports Live Migration Student Research Competition | ||
18:00 2hPoster | Increasing the Expressiveness of a Gradual Verifier Student Research Competition Priyam Gupta Purdue University | ||
18:00 2hPoster | M3: A Multi-Stage ML with Mutation Student Research Competition Maite Kramarz University of Toronto | ||
18:00 2hPoster | Loop Invariants Using Neural Networks Student Research Competition Atticus Kuhn University of Cambridge, Abhinandan Pal University of Birmingham, Mirco Giacobbe University of Birmingham | ||
18:00 2hPoster | Property Testing Trace Languages Student Research Competition Jed Koh Jin Keat National University of Singapore | ||
18:00 2hPoster | Optimizing Asynchronous Rust with Hydroflow Student Research Competition Ryan Alameddine University of California, Berkeley | ||
18:00 2hPoster | Relational Hoare Logic for Sequential Program Verification Student Research Competition Shushu Wu Shanghai Jiao Tong University | ||
18:00 2hPoster | Expanding the Scope of Grammar-Based Enumerative Testing Student Research Competition Thea Kjeldsmark University of California, Irvine | ||
18:00 2hPoster | System $F^\omega$ with Coherent Implicit Resolution Student Research Competition Eugene Flesselle EPFL | ||
18:00 2hPoster | The Store-Order Consistency Testing Problem for C-like Memory Models Student Research Competition Grace Tan National University of Singapore | ||
18:00 2hPoster | Formalizing Representation Transformations: A Case Study of Bit Vector Types Student Research Competition Katherine Philip Portland State University |