\emph{Runtime predictive analysis} is a technique for testing concurrent software where one observes the execution $\sigma$ of the program $P$ and determines if $\sigma$, \emph{or any execution equivalent to $\sigma$} violates the specification $\varphi$. Given an well-defined notion of equivalence, such an analysis would have larger coverage than the vanilla analysis that simply checks for membership of $\sigma$ in $\varphi$. We focus on \emph{trace equivalence}, proposed by Antoni Mazurkiewicz (Mazurkiewicz, 1995), which deems two executions (or strings) $\sigma_1, \sigma_2$ equivalent if one can be obtained from another by repeated swapping of neighbouring independent actions, denoted $\sigma_1 \equiv_{\mathcal{M}} \sigma_2$. The corresponding closure of a language $L$ is denoted $[L]{\mathcal{M}} = { \rho ,|, \exists \sigma \in L, \sigma \equiv{\mathcal{M}} \rho }$. In general, it is not possible to develop linear or sublinear deterministic algorithms for the membership problem of $[L]_{\mathcal{M}}$ when $L$ is a regular language (Ang & Mathur, 2024). In this work, we hope to use \emph{property testing} (Newman, 2010) to develop fast randomised algorithms for this problem.
A property tester is an algorithm that samples a few bits of the input (a string $w$ in our case) and attempts to check its membership in a pre-defined set (regular language $L$ in our setting). Alon et al. (2001) showed that for the vanilla membership problem $w \in L$, there is a constant-query 1-sided property tester. Property testing has indeed been previously used in the context of PL problems such as data race detection (Thokair et al., 2023) where the closure was known to be a regular language. Sampling for testing concurrent executions has been explored previously, but the algorithms proposed were not systematic, and do not generalise beyond the specific setting considered (Kallas et al., 2020). In our work, we want to systematically investigate the algorithmic landscape for sampling algorithms for concurrent executions through the lens of property testing and design property testers against trace closures of arbitrary regular languages. Our main result involves a subclass of regular languages, which we call \emph{atomic-star} languages. We show a two-sided $(c, \epsilon)$ tester for the trace closure of atomic-star languages. We also demonstrate a two-sided $(c, \epsilon)$-tester for the trace closure of any regular language when every pair of letters in the alphabet is independent. We use a combination of applying statistical methods on the numbers of each symbol, and regular language testing to obtain the above results. Finally, we establish some lower bounds for testing general trace regular languages.
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 |