POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States
Thu 23 Jan 2025 13:46 - 14:00 at Keep Away - SRC Finalist Presentations

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.

Thu 23 Jan

Displayed time zone: Mountain Time (US & Canada) change

13:20 - 14:40
SRC Finalist PresentationsStudent Research Competition at Keep Away
13:20
13m
Talk
System $F^\omega$ with Coherent Implicit Resolution
Student Research Competition
13:33
13m
Talk
Efficient Strong Simulation of High-level Quantum Gates
Student Research Competition
13:46
13m
Talk
The Store-Order Consistency Testing Problem for C-like Memory Models
Student Research Competition
Grace Tan National University of Singapore
14:00
13m
Talk
Wanco: WebAssembly AOT Compiler that supports Live Migration
Student Research Competition
Raiki Tamura Kyoto University
14:13
13m
Talk
Optimizing Asynchronous Rust with Hydroflow
Student Research Competition
Ryan Alameddine University of California, Berkeley
14:26
13m
Talk
Property Testing Trace Languages
Student Research Competition
Jed Koh Jin Keat National University of Singapore