Showing 1–50 of 55 results for author: Meyer, R

Separability in Büchi Vass and Singly Non-Linear Systems of Inequalities

Authors: Pascal Baumann, Eren Keskin, Roland Meyer, Georg Zetzsche

Abstract: The omega-regular separability problem for Büchi VASS coverability languages has recently been shown to be decidable, but with an EXPSPACE lower and a non-primitive recursive upper bound -- the exact complexity remained open. We close this gap and show that the problem is EXPSPACE-complete. A careful analysis of our complexity bounds additionally yields a PSPACE procedure in the case of fixed dime… ▽ More The omega-regular separability problem for Büchi VASS coverability languages has recently been shown to be decidable, but with an EXPSPACE lower and a non-primitive recursive upper bound -- the exact complexity remained open. We close this gap and show that the problem is EXPSPACE-complete. A careful analysis of our complexity bounds additionally yields a PSPACE procedure in the case of fixed dimension >= 1, which matches a pre-established lower bound of PSPACE for one dimensional Büchi VASS. Our algorithm is a non-deterministic search for a witness whose size, as we show, can be suitably bounded. Part of the procedure is to decide the existence of runs in VASS that satisfy certain non-linear properties. Therefore, a key technical ingredient is to analyze a class of systems of inequalities where one variable may occur in non-linear (polynomial) expressions. These so-called singly non-linear systems (SNLS) take the form A(x).y >= b(x), where A(x) and b(x) are a matrix resp. a vector whose entries are polynomials in x, and y ranges over vectors in the rationals. Our main contribution on SNLS is an exponential upper bound on the size of rational solutions to singly non-linear systems. The proof consists of three steps. First, we give a tailor-made quantifier elimination to characterize all real solutions to x. Second, using the root separation theorem about the distance of real roots of polynomials, we show that if a rational solution exists, then there is one with at most polynomially many bits. Third, we insert the solution for x into the SNLS, making it linear and allowing us to invoke standard solution bounds from convex geometry. Finally, we combine the results about SNLS with several techniques from the area of VASS to devise an EXPSPACE decision procedure for omega-regular separability of Büchi VASS. △ Less

Submitted 3 June, 2024; originally announced June 2024.

ACM Class: F.1.1

Realizability in Semantics-Guided Synthesis Done Eagerly

Authors: Roland Meyer, Jakob Tepe, Sebastian Wolff

Abstract: We present realizability and realization logic, two program logics that jointly address the problem of finding solutions in semantics-guided synthesis. What is new is that we proceed eagerly and not only analyze a single candidate program but a whole set. Realizability logic computes information about the set of candidate programs in a forward fashion. Realization logic uses this information as gu… ▽ More We present realizability and realization logic, two program logics that jointly address the problem of finding solutions in semantics-guided synthesis. What is new is that we proceed eagerly and not only analyze a single candidate program but a whole set. Realizability logic computes information about the set of candidate programs in a forward fashion. Realization logic uses this information as guidance to identify a suitable candidate in a backward fashion. Realizability logic is able to analyze a set of programs due to a new form of assertions that tracks synthesis alternatives. Realizability logic then picks alternatives to arrive at a program, and we give the guarantee that this process will not need backtracking. We show how to implement the program logics using verification conditions, and report on experiments with a prototype in the context of safe memory reclamation for lock-free data structures. △ Less

Submitted 8 March, 2024; originally announced March 2024.

Comments: 47 pages, 16 figures

On the Separability Problem of VASS Reachability Languages

Authors: Eren Keskin, Roland Meyer

Abstract: We show that the regular separability problem of VASS reachability languages is decidable and $\mathbf{F}_ω$-complete. At the heart of our decision procedure are doubly-marked graph transition sequences, a new proof object that tracks a suitable product of the VASS we wish to separate. We give a decomposition algorithm for DMGTS that not only achieves perfectness as known from MGTS, but also a new… ▽ More We show that the regular separability problem of VASS reachability languages is decidable and $\mathbf{F}_ω$-complete. At the heart of our decision procedure are doubly-marked graph transition sequences, a new proof object that tracks a suitable product of the VASS we wish to separate. We give a decomposition algorithm for DMGTS that not only achieves perfectness as known from MGTS, but also a new property called faithfulness. Faithfulness allows us to construct, from a regular separator for the $\mathbb{Z}$-versions of the VASS, a regular separator for the $\mathbb{N}$-versions. Behind faithfulness is the insight that, for separability, it is sufficient to track the counters of one VASS modulo a large number that is determined by the decomposition. △ Less

Submitted 29 January, 2024; originally announced January 2024.

Algorithm-agnostic low-rank approximation of operator monotone matrix functions

Authors: David Persson, Raphael A. Meyer, Christopher Musco

Abstract: Low-rank approximation of a matrix function, $f(A)$, is an important task in computational mathematics. Most methods require direct access to $f(A)$, which is often considerably more expensive than accessing $A$. Persson and Kressner (SIMAX 2023) avoid this issue for symmetric positive semidefinite matrices by proposing funNyström, which first constructs a Nyström approximation to $A$ using subspa… ▽ More Low-rank approximation of a matrix function, $f(A)$, is an important task in computational mathematics. Most methods require direct access to $f(A)$, which is often considerably more expensive than accessing $A$. Persson and Kressner (SIMAX 2023) avoid this issue for symmetric positive semidefinite matrices by proposing funNyström, which first constructs a Nyström approximation to $A$ using subspace iteration, and then uses the approximation to directly obtain a low-rank approximation for $f(A)$. They prove that the method yields a near-optimal approximation whenever $f$ is a continuous operator monotone function with $f(0) = 0$. We significantly generalize the results of Persson and Kressner beyond subspace iteration. We show that if $\widehat{A}$ is a near-optimal low-rank Nyström approximation to $A$ then $f(\widehat{A})$ is a near-optimal low-rank approximation to $f(A)$, independently of how $\widehat{A}$ is computed. Further, we show sufficient conditions for a basis $Q$ to produce a near-optimal Nyström approximation $\widehat{A} = AQ(Q^T AQ)^{\dagger} Q^T A$. We use these results to establish that many common low-rank approximation methods produce near-optimal Nyström approximations to $A$ and therefore to $f(A)$. △ Less

Submitted 23 November, 2023; originally announced November 2023.

MSC Class: 65F15; 65F55; 65F60; 68W25

Hutchinson's Estimator is Bad at Kronecker-Trace-Estimation

Authors: Raphael A. Meyer, Haim Avron

Abstract: We study the problem of estimating the trace of a matrix $\mathbf{A}$ that can only be accessed through Kronecker-matrix-vector products. That is, for any Kronecker-structured vector $\boldsymbol{\mathrm{x}} = \otimes_{i=1}^k \boldsymbol{\mathrm{x}}_i$, we can compute $\mathbf{A}\boldsymbol{\mathrm{x}}$. We focus on the natural generalization of Hutchinson's Estimator to this setting, proving tigh… ▽ More We study the problem of estimating the trace of a matrix $\mathbf{A}$ that can only be accessed through Kronecker-matrix-vector products. That is, for any Kronecker-structured vector $\boldsymbol{\mathrm{x}} = \otimes_{i=1}^k \boldsymbol{\mathrm{x}}_i$, we can compute $\mathbf{A}\boldsymbol{\mathrm{x}}$. We focus on the natural generalization of Hutchinson's Estimator to this setting, proving tight rates for the number of matrix-vector products this estimator needs to find a $(1\pm\varepsilon)$ approximation to the trace of $\mathbf{A}$. We find an exact equation for the variance of the estimator when using a Kronecker of Gaussian vectors, revealing an intimate relationship between Hutchinson's Estimator, the partial trace operator, and the partial transpose operator. Using this equation, we show that when using real vectors, in the worst case, this estimator needs $O(\frac{3^k}{\varepsilon^2})$ products to recover a $(1\pm\varepsilon)$ approximation of the trace of any PSD $\mathbf{A}$, and a matching lower bound for certain PSD $\mathbf{A}$. However, when using complex vectors, this can be exponentially improved to $Θ(\frac{2^k}{\varepsilon^2})$. We show that Hutchinson's Estimator converges slowest when $\mathbf{A}$ itself also has Kronecker structure. We conclude with some theoretical evidence suggesting that, by combining Hutchinson's Estimator with other techniques, it may be possible to avoid the exponential dependence on $k$. △ Less

Submitted 10 September, 2023; originally announced September 2023.

Comments: 35 pages

MSC Class: 65F99 (Primary) 15A69 (Secondary) ACM Class: G.1.3

Context-Aware Separation Logic

Authors: Roland Meyer, Thomas Wies, Sebastian Wolff

Abstract: Separation logic is often praised for its ability to closely mimic the locality of state updates when reasoning about them at the level of assertions. The prover only needs to concern themselves with the footprint of the computation at hand, i.e., the part of the state that is actually being accessed and manipulated. Modern concurrent separation logics lift this local reasoning principle from the… ▽ More Separation logic is often praised for its ability to closely mimic the locality of state updates when reasoning about them at the level of assertions. The prover only needs to concern themselves with the footprint of the computation at hand, i.e., the part of the state that is actually being accessed and manipulated. Modern concurrent separation logics lift this local reasoning principle from the physical state to abstract ghost state. For instance, these logics allow one to abstract the state of a fine-grained concurrent data structure by a predicate that provides a client the illusion of atomic access to the underlying state. However, these abstractions inadvertently increase the footprint of a computation: when reasoning about a local low-level state update, one needs to account for its effect on the abstraction, which encompasses a possibly unbounded portion of the low-level state. Often this gives the reasoning a global character. We present context-aware separation logic (CASL) to provide new opportunities for local reasoning in the presence of rich ghost state abstractions. CASL introduces the notion of a context of a computation, the part of the concrete state that is only affected on the abstract level. Contexts give rise to a new proof rule that allows one to reduce the footprint by the context, provided the computation preserves the context as an invariant. The context rule complements the frame rule of separation logic by enabling more local reasoning in cases where the predicate to be framed is known in advance. We instantiate our developed theory for the flow framework, which enables local reasoning about global properties of heap graphs. We then use the instantiation to obtain a fully local proof of functional correctness for a sequential binary search tree implementation that is inspired by fine-grained concurrent search structures. △ Less

Submitted 28 July, 2023; originally announced July 2023.

Urgency Annotations for Alternating Choices

Authors: Eren Keskin, Roland Meyer, Sören van der Wall

Abstract: We propose urgency programs, a new programming model with support for alternation, imperfect information, and recursion. The novelty are urgency annotations that decorate the (angelic and demonic) choice operators and control the order in which alternation is resolved. We study standard notions of contextual equivalence for urgency programs. Our first main result are fully abstract characterizatio… ▽ More We propose urgency programs, a new programming model with support for alternation, imperfect information, and recursion. The novelty are urgency annotations that decorate the (angelic and demonic) choice operators and control the order in which alternation is resolved. We study standard notions of contextual equivalence for urgency programs. Our first main result are fully abstract characterizations of these relations based on sound and complete axiomatizations. Our second main result settles their computability via a normal form construction. Notably, we show that the contextual preorder is (2h-1)-EXPTIME-complete for programs of maximal urgency h when the regular observable is given as an input resp. PTIME-complete when the regular observable is fixed. We designed urgency programs as a framework in which it is convenient to formulate and study verification and synthesis problems. We demonstrate this on a number of examples including the verification of concurrent and recursive programs and hyper model checking. △ Less

Submitted 20 October, 2023; v1 submitted 4 May, 2023; originally announced May 2023.

Separability and Non-Determinizability of WSTS

Authors: Wojciech Czerwiński, Eren Keskin, Sławomir Lasota, Roland Meyer, Sebastian Muskalla, K Narayan Kumar, Prakash Saivasan

Abstract: We study the languages recognized by well-structured transition systems (WSTS) with upward and downward compatibility. Our first result shows that every pair of disjoint WSTS languages is regularly separable: there is a regular language containing one of them while being disjoint from the other. As a consequence, if a language as well as its complement are both recognized by WSTS, then they are ne… ▽ More We study the languages recognized by well-structured transition systems (WSTS) with upward and downward compatibility. Our first result shows that every pair of disjoint WSTS languages is regularly separable: there is a regular language containing one of them while being disjoint from the other. As a consequence, if a language as well as its complement are both recognized by WSTS, then they are necessarily regular. Our second result shows that the languages recognized by deterministic WSTS form a strict subclass of the languages recognized by all WSTS: we give a non-deterministic WSTS language that we prove cannot be recognized by a deterministic WSTS. The proof relies on a novel characterization of the languages accepted by deterministic WSTS. △ Less

Submitted 31 May, 2024; v1 submitted 4 May, 2023; originally announced May 2023.

Comments: This paper is the journal version of the CONCUR23 paper "Separability and Non-Determinizability of WSTS'', which can be found in the previous version of this arxiv document. It covers both papers about regular separability in WSTS: the CONCUR23 paper and its predecessor the CONCUR18 paper. As this version does not contain an appendix, please refer to the previous version for missing proofs

On the Unreasonable Effectiveness of Single Vector Krylov Methods for Low-Rank Approximation

Authors: Raphael A. Meyer, Cameron Musco, Christopher Musco

Abstract: Krylov subspace methods are a ubiquitous tool for computing near-optimal rank $k$ approximations of large matrices. While "large block" Krylov methods with block size at least $k$ give the best known theoretical guarantees, block size one (a single vector) or a small constant is often preferred in practice. Despite their popularity, we lack theoretical bounds on the performance of such "small bloc… ▽ More Krylov subspace methods are a ubiquitous tool for computing near-optimal rank $k$ approximations of large matrices. While "large block" Krylov methods with block size at least $k$ give the best known theoretical guarantees, block size one (a single vector) or a small constant is often preferred in practice. Despite their popularity, we lack theoretical bounds on the performance of such "small block" Krylov methods for low-rank approximation. We address this gap between theory and practice by proving that small block Krylov methods essentially match all known low-rank approximation guarantees for large block methods. Via a black-box reduction we show, for example, that the standard single vector Krylov method run for $t$ iterations obtains the same spectral norm and Frobenius norm error bounds as a Krylov method with block size $\ell \geq k$ run for $O(t/\ell)$ iterations, up to a logarithmic dependence on the smallest gap between sequential singular values. That is, for a given number of matrix-vector products, single vector methods are essentially as effective as any choice of large block size. By combining our result with tail-bounds on eigenvalue gaps in random matrices, we prove that the dependence on the smallest singular value gap can be eliminated if the input matrix is perturbed by a small random matrix. Further, we show that single vector methods match the more complex algorithm of [Bakshi et al. `22], which combines the results of multiple block sizes to achieve an improved algorithm for Schatten $p$-norm low-rank approximation. △ Less

Submitted 6 November, 2023; v1 submitted 4 May, 2023; originally announced May 2023.

Comments: 41 pages, 7 figures. To appear at SODA 2024

MSC Class: 65F55 (Primary) 65F15 (Secondary) ACM Class: G.1.3; F.2.1

Make flows small again: revisiting the flow framework

Authors: Roland Meyer, Thomas Wies, Sebastian Wolff

Abstract: We present a new flow framework for separation logic reasoning about programs that manipulate general graphs. The framework overcomes problems in earlier developments: it is based on standard fixed point theory, guarantees least flows, rules out vanishing flows, and has an easy to understand notion of footprint as needed for soundness of the frame rule. In addition, we present algorithms for autom… ▽ More We present a new flow framework for separation logic reasoning about programs that manipulate general graphs. The framework overcomes problems in earlier developments: it is based on standard fixed point theory, guarantees least flows, rules out vanishing flows, and has an easy to understand notion of footprint as needed for soundness of the frame rule. In addition, we present algorithms for automating the frame rule, which we evaluate on graph updates extracted from linearizability proofs for concurrent data structures. The evaluation demonstrates that our algorithms help to automate key aspects of these proofs that have previously relied on user guidance or heuristics. △ Less

Submitted 10 April, 2023; originally announced April 2023.

Regular Separability in Büchi VASS

Authors: Pascal Baumann, Roland Meyer, Georg Zetzsche

Abstract: We study the ($ω$-)regular separability problem for Büchi VASS languages: Given two Büchi VASS with languages $L_1$ and $L_2$, check whether there is a regular language that fully contains $L_1$ while remaining disjoint from $L_2$. We show that the problem is decidable in general and PSPACE-complete in the 1-dimensional case, assuming succinct counter updates. The results rely on several arguments… ▽ More We study the ($ω$-)regular separability problem for Büchi VASS languages: Given two Büchi VASS with languages $L_1$ and $L_2$, check whether there is a regular language that fully contains $L_1$ while remaining disjoint from $L_2$. We show that the problem is decidable in general and PSPACE-complete in the 1-dimensional case, assuming succinct counter updates. The results rely on several arguments. We characterize the set of all regular languages disjoint from $L_2$. Based on this, we derive a (sound and complete) notion of inseparability witnesses, non-regular subsets of $L_1$. Finally, we show how to symbolically represent inseparability witnesses and how to check their existence. △ Less

Submitted 26 January, 2023; originally announced January 2023.

ACM Class: F.1.1

A Fair Loss Function for Network Pruning

Authors: Robbie Meyer, Alexander Wong

Abstract: Model pruning can enable the deployment of neural networks in environments with resource constraints. While pruning may have a small effect on the overall performance of the model, it can exacerbate existing biases into the model such that subsets of samples see significantly degraded performance. In this paper, we introduce the performance weighted loss function, a simple modified cross-entropy l… ▽ More Model pruning can enable the deployment of neural networks in environments with resource constraints. While pruning may have a small effect on the overall performance of the model, it can exacerbate existing biases into the model such that subsets of samples see significantly degraded performance. In this paper, we introduce the performance weighted loss function, a simple modified cross-entropy loss function that can be used to limit the introduction of biases during pruning. Experiments using biased classifiers for facial classification and skin-lesion classification tasks demonstrate that the proposed method is a simple and effective tool that can enable existing pruning methods to be used in fairness sensitive contexts. △ Less

Submitted 18 November, 2022; originally announced November 2022.

Comments: Trustworthy and Socially Responsible Machine Learning (TSRML 2022) workshop co-located with NeurIPS 2022

Near-Linear Sample Complexity for $L_p$ Polynomial Regression

Authors: Raphael A. Meyer, Cameron Musco, Christopher Musco, David P. Woodruff, Samson Zhou

Abstract: We study $L_p$ polynomial regression. Given query access to a function $f:[-1,1] \rightarrow \mathbb{R}$, the goal is to find a degree $d$ polynomial $\hat{q}$ such that, for a given parameter $\varepsilon > 0$, $$ \|\hat{q}-f\|_p\le (1+\varepsilon) \cdot \min_{q:\text{deg}(q)\le d}\|q-f\|_p. $$ Here $\|\cdot\|_p$ is the $L_p$ norm, $\|g\|_p = (\int_{-1}^1 |g(t)|^p dt)^{1/p}$. We show that queryin… ▽ More We study $L_p$ polynomial regression. Given query access to a function $f:[-1,1] \rightarrow \mathbb{R}$, the goal is to find a degree $d$ polynomial $\hat{q}$ such that, for a given parameter $\varepsilon > 0$, $$ \|\hat{q}-f\|_p\le (1+\varepsilon) \cdot \min_{q:\text{deg}(q)\le d}\|q-f\|_p. $$ Here $\|\cdot\|_p$ is the $L_p$ norm, $\|g\|_p = (\int_{-1}^1 |g(t)|^p dt)^{1/p}$. We show that querying $f$ at points randomly drawn from the Chebyshev measure on $[-1,1]$ is a near-optimal strategy for polynomial regression in all $L_p$ norms. In particular, to find $\hat q$, it suffices to sample $O(d\, \frac{\text{polylog}\,d}{\text{poly}\,\varepsilon})$ points from $[-1,1]$ with probabilities proportional to this measure. While the optimal sample complexity for polynomial regression was well understood for $L_2$ and $L_\infty$, our result is the first that achieves sample complexity linear in $d$ and error $(1+\varepsilon)$ for other values of $p$ without any assumptions. Our result requires two main technical contributions. The first concerns $p\leq 2$, for which we provide explicit bounds on the $L_p$ Lewis weight function of the infinite linear operator underlying polynomial regression. Using tools from the orthogonal polynomial literature, we show that this function is bounded by the Chebyshev density. Our second key contribution is to take advantage of the structure of polynomials to reduce the $p>2$ case to the $p\leq 2$ case. By doing so, we obtain a better sample complexity than what is possible for general $p$-norm linear regression problems, for which $Ω(d^{p/2})$ samples are required. △ Less

Submitted 12 November, 2022; originally announced November 2022.

Comments: 68 pages, to be presented at SODA 2023

MMRNet: Improving Reliability for Multimodal Object Detection and Segmentation for Bin Picking via Multimodal Redundancy

Authors: Yuhao Chen, Hayden Gunraj, E. Zhixuan Zeng, Robbie Meyer, Maximilian Gilles, Alexander Wong

Abstract: Recently, there has been tremendous interest in industry 4.0 infrastructure to address labor shortages in global supply chains. Deploying artificial intelligence-enabled robotic bin picking systems in real world has become particularly important for reducing stress and physical demands of workers while increasing speed and efficiency of warehouses. To this end, artificial intelligence-enabled robo… ▽ More Recently, there has been tremendous interest in industry 4.0 infrastructure to address labor shortages in global supply chains. Deploying artificial intelligence-enabled robotic bin picking systems in real world has become particularly important for reducing stress and physical demands of workers while increasing speed and efficiency of warehouses. To this end, artificial intelligence-enabled robotic bin picking systems may be used to automate order picking, but with the risk of causing expensive damage during an abnormal event such as sensor failure. As such, reliability becomes a critical factor for translating artificial intelligence research to real world applications and products. In this paper, we propose a reliable object detection and segmentation system with MultiModal Redundancy (MMRNet) for tackling object detection and segmentation for robotic bin picking using data from different modalities. This is the first system that introduces the concept of multimodal redundancy to address sensor failure issues during deployment. In particular, we realize the multimodal redundancy framework with a gate fusion module and dynamic ensemble learning. Finally, we present a new label-free multi-modal consistency (MC) score that utilizes the output from all modalities to measure the overall system output reliability and uncertainty. Through experiments, we demonstrate that in an event of missing modality, our system provides a much more reliable performance compared to baseline models. We also demonstrate that our MC score is a more reliability indicator for outputs during inference time compared to the model generated confidence scores that are often over-confident. △ Less

Submitted 7 May, 2023; v1 submitted 19 October, 2022; originally announced October 2022.

Comments: Accepted to CVPR TCV Workshop

Embedding Hindsight Reasoning in Separation Logic

Authors: Roland Meyer, Thomas Wies, Sebastian Wolff

Abstract: Proving linearizability of concurrent data structures remains a key challenge for verification. We present temporal interpolation as a new proof principle to conduct such proofs using hindsight arguments within concurrent separation logic. Temporal reasoning offers an easy-to-use alternative to prophecy variables and has the advantage of structuring proofs into easy-to-discharge hypotheses. To hin… ▽ More Proving linearizability of concurrent data structures remains a key challenge for verification. We present temporal interpolation as a new proof principle to conduct such proofs using hindsight arguments within concurrent separation logic. Temporal reasoning offers an easy-to-use alternative to prophecy variables and has the advantage of structuring proofs into easy-to-discharge hypotheses. To hindsight theory, our work brings the formal rigor and proof machinery of concurrent program logics. We substantiate the usefulness of our development by verifying the linearizability of the Logical Ordering (LO-)tree and RDCSS. Both of these involve complex proof arguments due to future-dependent linearization points. The LO-tree additionally features complex structure overlays. Our proof of the LO-tree is the first formal proof of this data structure. Interestingly, our formalization revealed an unknown bug and an existing informal proof as erroneous. △ Less

Submitted 21 April, 2023; v1 submitted 27 September, 2022; originally announced September 2022.

Journal ref: Proc. ACM Program. Lang. 7, PLDI, Article 182 (June 2023), 24 pages

Model-based Fault Classification for Automotive Software

Authors: Mike Becker, Roland Meyer, Tobias Runge, Ina Schaefer, Sören van der Wall, Sebastian Wolff

Abstract: Intensive testing using model-based approaches is the standard way of demonstrating the correctness of automotive software. Unfortunately, state-of-the-art techniques leave a crucial and labor intensive task to the test engineer: identifying bugs in failing tests. Our contribution is a model-based classification algorithm for failing tests that assists the engineer when identifying bugs. It consis… ▽ More Intensive testing using model-based approaches is the standard way of demonstrating the correctness of automotive software. Unfortunately, state-of-the-art techniques leave a crucial and labor intensive task to the test engineer: identifying bugs in failing tests. Our contribution is a model-based classification algorithm for failing tests that assists the engineer when identifying bugs. It consists of three steps. (i) Fault localization replays the test on the model to identify the moment when the two diverge. (ii) Fault explanation then computes the reason for the divergence. The reason is a subset of actions from the test that is sufficient for divergence. (iii) Fault classification groups together tests that fail for similar reasons. Our approach relies on machinery from formal methods: (i) symbolic execution, (ii) Hoare logic and a new relationship between the intermediary assertions constructed for a test, and (iii) a new relationship among Hoare proofs. A crucial aspect in automotive software is timing requirements, for which we develop appropriate Hoare logic theory. We also briefly report on our prototype implementation for the CAN bus Unified Diagnostic Services in an industrial project. △ Less

Submitted 15 December, 2022; v1 submitted 30 August, 2022; originally announced August 2022.

I still know it's you! On Challenges in Anonymizing Source Code

Authors: Micha Horlboge, Erwin Quiring, Roland Meyer, Konrad Rieck

Abstract: The source code of a program not only defines its semantics but also contains subtle clues that can identify its author. Several studies have shown that these clues can be automatically extracted using machine learning and allow for determining a program's author among hundreds of programmers. This attribution poses a significant threat to developers of anti-censorship and privacy-enhancing techno… ▽ More The source code of a program not only defines its semantics but also contains subtle clues that can identify its author. Several studies have shown that these clues can be automatically extracted using machine learning and allow for determining a program's author among hundreds of programmers. This attribution poses a significant threat to developers of anti-censorship and privacy-enhancing technologies, as they become identifiable and may be prosecuted. An ideal protection from this threat would be the anonymization of source code. However, neither theoretical nor practical principles of such an anonymization have been explored so far. In this paper, we tackle this problem and develop a framework for reasoning about code anonymization. We prove that the task of generating a $k$-anonymous program -- a program that cannot be attributed to one of $k$ authors -- is not computable in the general case. As a remedy, we introduce a relaxed concept called $k$-uncertainty, which enables us to measure the protection of developers. Based on this concept, we empirically study candidate techniques for anonymization, such as code normalization, coding style imitation, and code obfuscation. We find that none of the techniques provides sufficient protection when the attacker is aware of the anonymization. While we observe a notable reduction in attribution performance on real-world code, a reliable protection is not achieved for all developers. We conclude that code anonymization is a hard problem that requires further attention from the research community. △ Less

Submitted 10 April, 2024; v1 submitted 26 August, 2022; originally announced August 2022.

A Transferable Recommender Approach for Selecting the Best Density Functional Approximations in Chemical Discovery

Authors: Chenru Duan, Aditya Nandy, Ralf Meyer, Naveen Arunachalam, Heather J. Kulik

Abstract: Approximate density functional theory (DFT) has become indispensable owing to its cost-accuracy trade-off in comparison to more computationally demanding but accurate correlated wavefunction theory. To date, however, no single density functional approximation (DFA) with universal accuracy has been identified, leading to uncertainty in the quality of data generated from DFT. With electron density f… ▽ More Approximate density functional theory (DFT) has become indispensable owing to its cost-accuracy trade-off in comparison to more computationally demanding but accurate correlated wavefunction theory. To date, however, no single density functional approximation (DFA) with universal accuracy has been identified, leading to uncertainty in the quality of data generated from DFT. With electron density fitting and transfer learning, we build a DFA recommender that selects the DFA with the lowest expected error with respect to gold standard but cost-prohibitive coupled cluster theory in a system-specific manner. We demonstrate this recommender approach on vertical spin-splitting energy evaluation for challenging transition metal complexes. Our recommender predicts top-performing DFAs and yields excellent accuracy (ca. 2 kcal/mol) for chemical discovery, outperforming both individual transfer learning models and the single best functional in a set of 48 DFAs. We demonstrate the transferability of the DFA recommender to experimentally synthesized compounds with distinct chemistry. △ Less

Submitted 21 July, 2022; originally announced July 2022.

A Concurrent Program Logic with a Future and History

Authors: Roland Meyer, Thomas Wies, Sebastian Wolff

Abstract: Verifying fine-grained optimistic concurrent programs remains an open problem. Modern program logics provide abstraction mechanisms and compositional reasoning principles to deal with the inherent complexity. However, their use is mostly confined to pencil-and-paper or mechanized proofs. We devise a new separation logic geared towards the lacking automation. While local reasoning is known to be cr… ▽ More Verifying fine-grained optimistic concurrent programs remains an open problem. Modern program logics provide abstraction mechanisms and compositional reasoning principles to deal with the inherent complexity. However, their use is mostly confined to pencil-and-paper or mechanized proofs. We devise a new separation logic geared towards the lacking automation. While local reasoning is known to be crucial for automation, we are the first to show how to retain this locality for (i) reasoning about inductive properties without the need for ghost code, and (ii) reasoning about computation histories in hindsight. We implemented our new logic in a tool and used it to automatically verify challenging concurrent search structures that require inductive properties and hindsight reasoning, such as the Harris set. △ Less

Submitted 11 November, 2022; v1 submitted 5 July, 2022; originally announced July 2022.

Journal ref: Proc. ACM Program. Lang. 6, OOPSLA2, Article 174 (October 2022), 30 pages

Fast Regression for Structured Inputs

Authors: Raphael A. Meyer, Cameron Musco, Christopher Musco, David P. Woodruff, Samson Zhou

Abstract: We study the $\ell_p$ regression problem, which requires finding $\mathbf{x}\in\mathbb R^{d}$ that minimizes $\|\mathbf{A}\mathbf{x}-\mathbf{b}\|_p$ for a matrix $\mathbf{A}\in\mathbb R^{n \times d}$ and response vector $\mathbf{b}\in\mathbb R^{n}$. There has been recent interest in develo** subsampling methods for this problem that can outperform standard techniques when $n$ is very large. Howe… ▽ More We study the $\ell_p$ regression problem, which requires finding $\mathbf{x}\in\mathbb R^{d}$ that minimizes $\|\mathbf{A}\mathbf{x}-\mathbf{b}\|_p$ for a matrix $\mathbf{A}\in\mathbb R^{n \times d}$ and response vector $\mathbf{b}\in\mathbb R^{n}$. There has been recent interest in develo** subsampling methods for this problem that can outperform standard techniques when $n$ is very large. However, all known subsampling approaches have run time that depends exponentially on $p$, typically, $d^{\mathcal{O}(p)}$, which can be prohibitively expensive. We improve on this work by showing that for a large class of common \emph{structured matrices}, such as combinations of low-rank matrices, sparse matrices, and Vandermonde matrices, there are subsampling based methods for $\ell_p$ regression that depend polynomially on $p$. For example, we give an algorithm for $\ell_p$ regression on Vandermonde matrices that runs in time $\mathcal{O}(n\log^3 n+(dp^2)^{0.5+ω}\cdot\text{polylog}\,n)$, where $ω$ is the exponent of matrix multiplication. The polynomial dependence on $p$ crucially allows our algorithms to extend naturally to efficient algorithms for $\ell_\infty$ regression, via approximation of $\ell_\infty$ by $\ell_{\mathcal{O}(\log n)}$. Of practical interest, we also develop a new subsampling algorithm for $\ell_p$ regression for arbitrary matrices, which is simpler than previous approaches for $p \ge 4$. △ Less

Submitted 14 March, 2022; originally announced March 2022.

Verifying and Optimizing Compact NUMA-Aware Locks on Weak Memory Models

Authors: Antonio Paolillo, Hernán Ponce-de-León, Thomas Haas, Diogo Behrens, Rafael Chehab, Ming Fu, Roland Meyer

Abstract: Develo** concurrent software is challenging, especially if it has to run on modern architectures with Weak Memory Models (WMMs) such as ARMv8, Power, or RISC-V. For the sake of performance, WMMs allow hardware and compilers to aggressively reorder memory accesses. To guarantee correctness, developers have to carefully place memory barriers in the code to enforce ordering among critical memory op… ▽ More Develo** concurrent software is challenging, especially if it has to run on modern architectures with Weak Memory Models (WMMs) such as ARMv8, Power, or RISC-V. For the sake of performance, WMMs allow hardware and compilers to aggressively reorder memory accesses. To guarantee correctness, developers have to carefully place memory barriers in the code to enforce ordering among critical memory operations. While WMM architectures are growing in popularity, identifying the necessary and sufficient barriers of complex synchronization primitives is notoriously difficult. Unfortunately, publications often consider barriers to be just implementation details and omit them. In this technical note, we report our efforts in verifying the correctness of the Compact NUMA-Aware (CNA) lock algorithm on WMMs. The CNA lock is of special interest because it has been proposed as a new slowpath for Linux qspinlock, the main spinlock in Linux. Besides determining a correct and efficient set of barriers for the original CNA algorithm on WMMs, we investigate the correctness of Linux qspinlock and the latest Linux CNA patch (v15) on the memory models LKMM, ARMv8, and Power. Surprisingly, we have found that Linux qspinlock and, consequently, Linux CNA are incorrect according to LKMM, but are still correct when compiled to ARMv8 or Power. △ Less

Submitted 9 July, 2022; v1 submitted 30 November, 2021; originally announced November 2021.

Safety Verification of Parameterized Systems under Release-Acquire

Authors: Adwait Godbole, Shankara Narayanan Krishna, Roland Meyer

Abstract: We study the safety verification problem for parameterized systems under the release-acquire (RA) semantics. It has been shown that the problem is intractable for systems with unlimited access to atomic compare-and-swap (CAS) instructions. We show that, from a verification perspective where approximate results help, this is overly pessimistic. We study parameterized systems consisting of an unboun… ▽ More We study the safety verification problem for parameterized systems under the release-acquire (RA) semantics. It has been shown that the problem is intractable for systems with unlimited access to atomic compare-and-swap (CAS) instructions. We show that, from a verification perspective where approximate results help, this is overly pessimistic. We study parameterized systems consisting of an unbounded number of environment threads executing identical but CAS-free programs and a fixed number of distinguished threads that are unrestricted. Our first contribution is a new semantics that considerably simplifies RA but is still equivalent for the above systems as far as safety verification is concerned. We apply this (general) result to two subclasses of our model. We show that safety verification is only \pspace-complete for the bounded model checking problem where the distinguished threads are loop-free. Interestingly, we can still afford the unbounded environment. We show that the complexity jumps to \nexp-complete for thread-modular verification where an unrestricted distinguished `ego' thread interacts with an environment of CAS-free threads plus loop-free distinguished threads (as in the earlier setting). Besides the usefulness for verification, the results are strong in that they delineate the tractability border for an established semantics. △ Less

Submitted 5 May, 2022; v1 submitted 28 January, 2021; originally announced January 2021.

Hutch++: Optimal Stochastic Trace Estimation

Authors: Raphael A. Meyer, Cameron Musco, Christopher Musco, David P. Woodruff

Abstract: We study the problem of estimating the trace of a matrix $A$ that can only be accessed through matrix-vector multiplication. We introduce a new randomized algorithm, Hutch++, which computes a $(1 \pm ε)$ approximation to $tr(A)$ for any positive semidefinite (PSD) $A$ using just $O(1/ε)$ matrix-vector products. This improves on the ubiquitous Hutchinson's estimator, which requires $O(1/ε^2)$ matri… ▽ More We study the problem of estimating the trace of a matrix $A$ that can only be accessed through matrix-vector multiplication. We introduce a new randomized algorithm, Hutch++, which computes a $(1 \pm ε)$ approximation to $tr(A)$ for any positive semidefinite (PSD) $A$ using just $O(1/ε)$ matrix-vector products. This improves on the ubiquitous Hutchinson's estimator, which requires $O(1/ε^2)$ matrix-vector products. Our approach is based on a simple technique for reducing the variance of Hutchinson's estimator using a low-rank approximation step, and is easy to implement and analyze. Moreover, we prove that, up to a logarithmic factor, the complexity of Hutch++ is optimal amongst all matrix-vector query algorithms, even when queries can be chosen adaptively. We show that it significantly outperforms Hutchinson's method in experiments. While our theory mainly requires $A$ to be positive semidefinite, we provide generalized guarantees for general square matrices, and show empirical gains in such applications. △ Less

Submitted 10 June, 2021; v1 submitted 19 October, 2020; originally announced October 2020.

Comments: SIAM Symposium on Simplicity in Algorithms (SOSA21)

The Statistical Cost of Robust Kernel Hyperparameter Tuning

Authors: Raphael A. Meyer, Christopher Musco

Abstract: This paper studies the statistical complexity of kernel hyperparameter tuning in the setting of active regression under adversarial noise. We consider the problem of finding the best interpolant from a class of kernels with unknown hyperparameters, assuming only that the noise is square-integrable. We provide finite-sample guarantees for the problem, characterizing how increasing the complexity of… ▽ More This paper studies the statistical complexity of kernel hyperparameter tuning in the setting of active regression under adversarial noise. We consider the problem of finding the best interpolant from a class of kernels with unknown hyperparameters, assuming only that the noise is square-integrable. We provide finite-sample guarantees for the problem, characterizing how increasing the complexity of the kernel class increases the complexity of learning kernel hyperparameters. For common kernel classes (e.g. squared-exponential kernels with unknown lengthscale), our results show that hyperparameter optimization increases sample complexity by just a logarithmic factor, in comparison to the setting where optimal parameters are known in advance. Our result is based on a subsampling guarantee for linear regression under multiple design matrices, combined with an ε-net argument for discretizing kernel parameterizations. △ Less

Submitted 14 June, 2020; originally announced June 2020.

ACM Class: G.3

Pointer Life Cycle Types for Lock-Free Data Structures with Memory Reclamation

Authors: Roland Meyer, Sebastian Wolff

Abstract: We consider the verification of lock-free data structures that manually manage their memory with the help of a safe memory reclamation (SMR) algorithm. Our first contribution is a type system that checks whether a program properly manages its memory. If the type check succeeds, it is safe to ignore the SMR algorithm and consider the program under garbage collection. Intuitively, our types track th… ▽ More We consider the verification of lock-free data structures that manually manage their memory with the help of a safe memory reclamation (SMR) algorithm. Our first contribution is a type system that checks whether a program properly manages its memory. If the type check succeeds, it is safe to ignore the SMR algorithm and consider the program under garbage collection. Intuitively, our types track the protection of pointers as guaranteed by the SMR algorithm. There are two design decisions. The type system does not track any shape information, which makes it extremely lightweight. Instead, we rely on invariant annotations that postulate a protection by the SMR. To this end, we introduce angels, ghost variables with an angelic semantics. Moreover, the SMR algorithm is not hard-coded but a parameter of the type system definition. To achieve this, we rely on a recent specification language for SMR algorithms. Our second contribution is to automate the type inference and the invariant check. For the type inference, we show a quadratic-time algorithm. For the invariant check, we give a source-to-source translation that links our programs to off-the-shelf verification tools. It compiles away the angelic semantics. This allows us to infer appropriate annotations automatically in a guess-and-check manner. To demonstrate the effectiveness of our type-based verification approach, we check linearizability for various list and set implementations from the literature with both hazard pointers and epoch-based memory reclamation. For many of the examples, this is the first time they are verified automatically. For the ones where there is a competitor, we obtain a speed-up of up to two orders of magnitude. △ Less

Submitted 26 November, 2019; v1 submitted 25 October, 2019; originally announced October 2019.

Complexity of Liveness in Parameterized Systems

Authors: Peter Chini, Roland Meyer, Prakash Saivasan

Abstract: We investigate the fine-grained complexity of liveness verification for leader contributor systems. These consist of a designated leader thread and an arbitrary number of identical contributor threads communicating via a shared memory. The liveness verification problem asks whether there is an infinite computation of the system in which the leader reaches a final state infinitely often. Like its r… ▽ More We investigate the fine-grained complexity of liveness verification for leader contributor systems. These consist of a designated leader thread and an arbitrary number of identical contributor threads communicating via a shared memory. The liveness verification problem asks whether there is an infinite computation of the system in which the leader reaches a final state infinitely often. Like its reachability counterpart, the problem is known to be NP-complete. Our results show that, even from a fine-grained point of view, the complexities differ only by a polynomial factor. Liveness verification decomposes into reachability and cycle detection. We present a fixed point iteration solving the latter in polynomial time. For reachability, we reconsider the two standard parameterizations. When parameterized by the number of states of the leader L and the size of the data domain D, we show an (L + D)^O(L + D)-time algorithm. It improves on a previous algorithm, thereby settling an open problem. When parameterized by the number of states of the contributor C, we reuse an O*(2^C)-time algorithm. We show how to connect both algorithms with the cycle detection to obtain algorithms for liveness verification. The running times of the composed algorithms match those of reachability, proving that the fine-grained lower bounds for liveness verification are met. △ Less

Submitted 7 October, 2019; v1 submitted 26 September, 2019; originally announced September 2019.

Liveness in Broadcast Networks

Authors: Peter Chini, Roland Meyer, Prakash Saivasan

Abstract: We study liveness and model checking problems for broadcast networks, a system model of identical clients communicating via message passing. The first problem that we consider is Liveness Verification. It asks whether there is a computation such that one of the clients visits a final state infinitely often. The complexity of the problem has been open since 2010 when it was shown to be P-hard and s… ▽ More We study liveness and model checking problems for broadcast networks, a system model of identical clients communicating via message passing. The first problem that we consider is Liveness Verification. It asks whether there is a computation such that one of the clients visits a final state infinitely often. The complexity of the problem has been open since 2010 when it was shown to be P-hard and solvable in EXPSPACE. We close the gap by a polynomial-time algorithm. The algorithm relies on a characterization of live computations in terms of paths in a suitable graph, combined with a fixed-point iteration to efficiently check the existence of such paths. The second problem is Fair Liveness Verification. It asks for a computation where all participating clients visit a final state infinitely often. We adjust the algorithm to also solve fair liveness in polynomial time. Both problems can be instrumented to answer model checking questions for broadcast networks against linear time temporal logic specifications. The first problem in this context is Fair Model Checking. It demands that for all computations of a broadcast network, all participating clients satisfy the specification. We solve the problem via the Vardi-Wolper construction and a reduction to Liveness Verification. The second problem is Sparse Model Checking. It asks whether each computation has a participating client that satisfies the specification. We reduce the problem to Fair Liveness Verification. △ Less

Submitted 21 July, 2020; v1 submitted 1 April, 2019; originally announced April 2019.

Optimality Implies Kernel Sum Classifiers are Statistically Efficient

Authors: Raphael Arkady Meyer, Jean Honorio

Abstract: We propose a novel combination of optimization tools with learning theory bounds in order to analyze the sample complexity of optimal kernel sum classifiers. This contrasts the typical learning theoretic results which hold for all (potentially suboptimal) classifiers. Our work also justifies assumptions made in prior work on multiple kernel learning. As a byproduct of our analysis, we also provide… ▽ More We propose a novel combination of optimization tools with learning theory bounds in order to analyze the sample complexity of optimal kernel sum classifiers. This contrasts the typical learning theoretic results which hold for all (potentially suboptimal) classifiers. Our work also justifies assumptions made in prior work on multiple kernel learning. As a byproduct of our analysis, we also provide a new form of Rademacher complexity for hypothesis classes containing only optimal classifiers. △ Less

Submitted 2 June, 2019; v1 submitted 25 January, 2019; originally announced January 2019.

Journal ref: International Conference on Machine Learning (ICML) 2019

Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis

Authors: Roland Meyer, Sebastian Wolff

Abstract: Verification of concurrent data structures is one of the most challenging tasks in software verification. The topic has received considerable attention over the course of the last decade. Nevertheless, human-driven techniques remain cumbersome and notoriously difficult while automated approaches suffer from limited applicability. The main obstacle for automation is the complexity of concurrent dat… ▽ More Verification of concurrent data structures is one of the most challenging tasks in software verification. The topic has received considerable attention over the course of the last decade. Nevertheless, human-driven techniques remain cumbersome and notoriously difficult while automated approaches suffer from limited applicability. The main obstacle for automation is the complexity of concurrent data structures. This is particularly true in the absence of garbage collection. The intricacy of lock-free memory management paired with the complexity of concurrent data structures makes automated verification prohibitive. In this work we present a method for verifying concurrent data structures and their memory management separately. We suggest two simpler verification tasks that imply the correctness of the data structure. The first task establishes an over-approximation of the reclamation behavior of the memory management. The second task exploits this over-approximation to verify the data structure without the need to consider the implementation of the memory management itself. To make the resulting verification tasks tractable for automated techniques, we establish a second result. We show that a verification tool needs to consider only executions where a single memory location is reused. We implemented our approach and were able to verify linearizability of Michael&Scott's queue and the DGLM queue for both hazard pointers and epoch-based reclamation. To the best of our knowledge, we are the first to verify such implementations fully automatically. △ Less

Submitted 9 November, 2018; v1 submitted 25 October, 2018; originally announced October 2018.

Fast Witness Counting

Authors: Peter Chini, Rehab Massoud, Roland Meyer, Prakash Saivasan

Abstract: We study the witness-counting problem: given a set of vectors $V$ in the $d$-dimensional vector space over $\mathbb{F}_2$, a target vector $t$, and an integer $k$, count all ways to sum-up exactly $k$ different vectors from $V$ to reach $t$. The problem is well-known in coding theory and received considerable attention in complexity theory. Recently, it appeared in the context of hardware monitori… ▽ More We study the witness-counting problem: given a set of vectors $V$ in the $d$-dimensional vector space over $\mathbb{F}_2$, a target vector $t$, and an integer $k$, count all ways to sum-up exactly $k$ different vectors from $V$ to reach $t$. The problem is well-known in coding theory and received considerable attention in complexity theory. Recently, it appeared in the context of hardware monitoring. Our contribution is an algorithm for witness counting that is optimal in the sense of fine-grained complexity. It runs in time $\mathcal{O}^*(2^d)$ with only a logarithmic dependence on $m=|V|$. The algorithm makes use of the Walsh-Hadamard transform to compute convolutions over $\mathbb{F}_2^d$. The transform, however, overcounts the solutions. Inspired by the inclusion-exclusion principle, we introduce correction terms. The correction leads to a recurrence that we show how to solve efficiently. The correction terms are obtained from equivalence relations over $\mathbb{F}_2^d$. We complement our upper bound with two lower bounds on the problem. The first relies on $\# ETH$ and prohibits an $2^{o(d)}$-time algorithm. The second bound states the non-existence of a polynomial kernel for the decision version of the problem. △ Less

Submitted 16 July, 2018; originally announced July 2018.

Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems

Authors: Matthew Hague, Roland Meyer, Sebastian Muskalla, Martin Zimmermann

Abstract: We give a direct polynomial-time reduction from parity games played over the configuration graphs of collapsible pushdown systems to safety games played over the same class of graphs. That a polynomial-time reduction would exist was known since both problems are complete for the same complexity class. Coming up with a direct reduction, however, has been an open problem. Our solution to the puzzle… ▽ More We give a direct polynomial-time reduction from parity games played over the configuration graphs of collapsible pushdown systems to safety games played over the same class of graphs. That a polynomial-time reduction would exist was known since both problems are complete for the same complexity class. Coming up with a direct reduction, however, has been an open problem. Our solution to the puzzle brings together a number of techniques for pushdown games and adds three new ones. This work contributes to a recent trend of liveness to safety reductions which allow the advanced state-of-the-art in safety checking to be used for more expressive specifications. △ Less

Submitted 5 July, 2018; v1 submitted 8 May, 2018; originally announced May 2018.

Bounded Context Switching for Valence Systems

Authors: Roland Meyer, Sebastian Muskalla, Georg Zetzsche

Abstract: We study valence systems, finite-control programs over infinite-state memories modeled in terms of graph monoids. Our contribution is a notion of bounded context switching (BCS). Valence systems generalize pushdowns, concurrent pushdowns, and Petri nets. In these settings, our definition conservatively generalizes existing notions. The main finding is that reachability within a bounded number of c… ▽ More We study valence systems, finite-control programs over infinite-state memories modeled in terms of graph monoids. Our contribution is a notion of bounded context switching (BCS). Valence systems generalize pushdowns, concurrent pushdowns, and Petri nets. In these settings, our definition conservatively generalizes existing notions. The main finding is that reachability within a bounded number of context switches is in NP, independent of the memory (the graph monoid). Our proof is genuinely algebraic, and therefore contributes a new way to think about BCS. In addition, we exhibit a class of storage mechanisms for which BCS reachability belongs to P. △ Less

Submitted 5 July, 2018; v1 submitted 26 March, 2018; originally announced March 2018.

Fine-Grained Complexity of Safety Verification

Authors: Peter Chini, Roland Meyer, Prakash Saivasan

Abstract: We study the fine-grained complexity of Leader Contributor Reachability (LCR) and Bounded-Stage Reachability (BSR), two variants of the safety verification problem for shared memory concurrent programs. For both problems, the memory is a single variable over a finite data domain. Our contributions are new verification algorithms and lower bounds. The latter are based on the Exponential Time Hypoth… ▽ More We study the fine-grained complexity of Leader Contributor Reachability (LCR) and Bounded-Stage Reachability (BSR), two variants of the safety verification problem for shared memory concurrent programs. For both problems, the memory is a single variable over a finite data domain. Our contributions are new verification algorithms and lower bounds. The latter are based on the Exponential Time Hypothesis (ETH), the problem Set Cover, and cross-compositions. LCR is the question whether a designated leader thread can reach an unsafe state when interacting with a certain number of equal contributor threads. We suggest two parameterizations: (1) By the size of the data domain D and the size of the leader L, and (2) by the size of the contributors C. We present algorithms for both cases. The key techniques are compact witnesses and dynamic programming. The algorithms run in O*((L(D+1))^(LD) * D^D) and O*(2^C) time, showing that both parameterizations are fixed-parameter tractable. We complement the upper bounds by (matching) lower bounds based on ETH and Set Cover. Moreover, we prove the absence of polynomial kernels. For BSR, we consider programs involving t different threads. We restrict the analysis to computations where the write permission changes s times between the threads. BSR asks whether a given configuration is reachable via such an s-stage computation. When parameterized by P, the maximum size of a thread, and t, the interesting observation is that the problem has a large number of difficult instances. Formally, we show that there is no polynomial kernel, no compression algorithm that reduces the size of the data domain D or the number of stages s to a polynomial dependence on P and t. This indicates that symbolic methods may be harder to find for this problem. △ Less

Submitted 10 January, 2020; v1 submitted 15 February, 2018; originally announced February 2018.

Effect Summaries for Thread-Modular Analysis

Authors: Lukáš Holík, Roland Meyer, Tomáš Vojnar, Sebastian Wolff

Abstract: We propose a novel guess-and-check principle to increase the efficiency of thread-modular verification of lock-free data structures. We build on a heuristic that guesses candidates for stateless effect summaries of programs by searching the code for instances of a copy-and-check programming idiom common in lock-free data structures. These candidate summaries are used to compute the interference am… ▽ More We propose a novel guess-and-check principle to increase the efficiency of thread-modular verification of lock-free data structures. We build on a heuristic that guesses candidates for stateless effect summaries of programs by searching the code for instances of a copy-and-check programming idiom common in lock-free data structures. These candidate summaries are used to compute the interference among threads in linear time. Since a candidate summary need not be a sound effect summary, we show how to fully automatically check whether the precision of candidate summaries is sufficient. We can thus perform sound verification despite relying on an unsound heuristic. We have implemented our approach and found it up to two orders of magnitude faster than existing ones. △ Less

Submitted 10 May, 2017; originally announced May 2017.

Domains for Higher-Order Games

Authors: Matthew Hague, Roland Meyer, Sebastian Muskalla

Abstract: We study two-player inclusion games played over word-generating higher-order recursion schemes. While inclusion checks are known to capture verification problems, two-player games generalize this relationship to program synthesis. In such games, non-terminals of the grammar are controlled by opposing players. The goal of the existential player is to avoid producing a word that lies outside of a re… ▽ More We study two-player inclusion games played over word-generating higher-order recursion schemes. While inclusion checks are known to capture verification problems, two-player games generalize this relationship to program synthesis. In such games, non-terminals of the grammar are controlled by opposing players. The goal of the existential player is to avoid producing a word that lies outside of a regular language of safe words. We contribute a new domain that provides a representation of the winning region of such games. Our domain is based on (functions over) potentially infinite Boolean formulas with words as atomic propositions. We develop an abstract interpretation framework that we instantiate to abstract this domain into a domain where the propositions are replaced by states of a finite automaton. This second domain is therefore finite and we obtain, via standard fixed-point techniques, a direct algorithm for the analysis of two-player inclusion games. We show, via a second instantiation of the framework, that our finite domain can be optimized, leading to a (k+1)EXP algorithm for order-k recursion schemes. We give a matching lower bound, showing that our approach is optimal. Since our approach is based on standard Kleene iteration, existing techniques and tools for fixed-point computations can be applied. △ Less

Submitted 5 August, 2017; v1 submitted 30 April, 2017; originally announced May 2017.

Comments: Conference version accepted for presentation and publication at the 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

ACM Class: F.1.1

Locality and Singularity for Store-Atomic Memory Models

Authors: Egor Derevenetc, Roland Meyer, Sebastian Schweizer

Abstract: Robustness is a correctness notion for concurrent programs running under relaxed consistency models. The task is to check that the relaxed behavior coincides (up to traces) with sequential consistency (SC). Although computationally simple on paper (robustness has been shown to be PSPACE-complete for TSO, PGAS, and Power), building a practical robustness checker remains a challenge. The problem is… ▽ More Robustness is a correctness notion for concurrent programs running under relaxed consistency models. The task is to check that the relaxed behavior coincides (up to traces) with sequential consistency (SC). Although computationally simple on paper (robustness has been shown to be PSPACE-complete for TSO, PGAS, and Power), building a practical robustness checker remains a challenge. The problem is that the various relaxations lead to a dramatic number of computations, only few of which violate robustness. In the present paper, we set out to reduce the search space for robustness checkers. We focus on store-atomic consistency models and establish two completeness results. The first result, called locality, states that a non-robust program always contains a violating computation where only one thread delays commands. The second result, called singularity, is even stronger but restricted to programs without lightweight fences. It states that there is a violating computation where a single store is delayed. As an application of the results, we derive a linear-size source-to-source translation of robustness to SC-reachability. It applies to general programs, regardless of the data domain and potentially with an unbounded number of threads and with unbounded buffers. We have implemented the translation and verified, for the first time, PGAS algorithms in a fully automated fashion. For TSO, our analysis outperforms existing tools. △ Less

Submitted 14 March, 2017; originally announced March 2017.

Portability Analysis for Axiomatic Memory Models. PORTHOS: One Tool for all Models

Authors: Hernán Ponce-de-León, Florian Furbach, Keijo Heljanko, Roland Meyer

Abstract: We present Porthos, the first tool that discovers porting bugs in performance-critical code. Porthos takes as input a program and the memory models of the source architecture for which the program has been developed and the target model to which it is ported. If the code is not portable, Porthos finds a bug in the form of an unexpected execution - an execution that is consistent with the target bu… ▽ More We present Porthos, the first tool that discovers porting bugs in performance-critical code. Porthos takes as input a program and the memory models of the source architecture for which the program has been developed and the target model to which it is ported. If the code is not portable, Porthos finds a bug in the form of an unexpected execution - an execution that is consistent with the target but inconsistent with the source memory model. Technically, Porthos implements a bounded model checking method that reduces the portability analysis problem to satisfiability modulo theories (SMT). There are two main problems in the reduction that we present novel and efficient solutions for. First, the formulation of the portability problem contains a quantifier alternation (consistent + inconsistent). We introduce a formula that encodes both in a single existential query. Second, the supported memory models (e.g., Power) contain recursive definitions. We compute the required least fixed point semantics for recursion (a problem that was left open in [47]) efficiently in SMT. Finally we present the first experimental analysis of portability from TSO to Power. △ Less

Submitted 28 April, 2017; v1 submitted 22 February, 2017; originally announced February 2017.

Regular Separability of Well Structured Transition Systems

Authors: Wojciech Czerwiński, Sławomir Lasota, Roland Meyer, Sebastian Muskalla, K Narayan Kumar, Prakash Saivasan

Abstract: We investigate the languages recognized by well-structured transition systems (WSTS) with upward and downward compatibility. Our first result shows that, under very mild assumptions, every two disjoint WSTS languages are regular separable: There is a regular language containing one of them and being disjoint from the other. As a consequence, if a language as well as its complement are both recogni… ▽ More We investigate the languages recognized by well-structured transition systems (WSTS) with upward and downward compatibility. Our first result shows that, under very mild assumptions, every two disjoint WSTS languages are regular separable: There is a regular language containing one of them and being disjoint from the other. As a consequence, if a language as well as its complement are both recognized by WSTS, then they are necessarily regular. In particular, no subclass of WSTS languages beyond the regular languages is closed under complement. Our second result shows that for Petri nets, the complexity of the backwards coverability algorithm yields a bound on the size of the regular separator. We complement it by a lower bound construction. △ Less

Submitted 5 July, 2018; v1 submitted 17 February, 2017; originally announced February 2017.

Liveness Verification and Synthesis: New Algorithms for Recursive Programs

Authors: Roland Meyer, Sebastian Muskalla, Elisabeth Neumann

Abstract: We consider the problems of liveness verification and liveness synthesis for recursive programs. The liveness verification problem (LVP) is to decide whether a given omega-context-free language is contained in a given omega-regular language. The liveness synthesis problem (LSP) is to compute a strategy so that a given omega-context-free game, when played along the strategy, is guaranteed to derive… ▽ More We consider the problems of liveness verification and liveness synthesis for recursive programs. The liveness verification problem (LVP) is to decide whether a given omega-context-free language is contained in a given omega-regular language. The liveness synthesis problem (LSP) is to compute a strategy so that a given omega-context-free game, when played along the strategy, is guaranteed to derive a word in a given omega-regular language. The problems are known to be EXPTIME-complete and EXPTIME-complete, respectively. Our contributions are new algorithms with optimal time complexity. For LVP, we generalize recent lasso-finding algorithms (also known as Ramsey-based algorithms) from finite to recursive programs. For LSP, we generalize a recent summary-based algorithm from finite to infinite words. Lasso finding and summaries have proven to be efficient in a number of implementations for the finite state and finite word setting. △ Less

Submitted 11 January, 2017; originally announced January 2017.

ACM Class: F.1.1

On the Upward/Downward Closures of Petri Nets

Authors: Mohamed Faouzi Atig, Roland Meyer, Sebastian Muskalla, Prakash Saivasan

Abstract: We study the size and the complexity of computing finite state automata (FSA) representing and approximating the downward and the upward closure of Petri net languages with coverability as the acceptance condition. We show how to construct an FSA recognizing the upward closure of a Petri net language in doubly-exponential time, and therefore the size is at most doubly exponential. For downward clo… ▽ More We study the size and the complexity of computing finite state automata (FSA) representing and approximating the downward and the upward closure of Petri net languages with coverability as the acceptance condition. We show how to construct an FSA recognizing the upward closure of a Petri net language in doubly-exponential time, and therefore the size is at most doubly exponential. For downward closures, we prove that the size of the minimal automata can be non-primitive recursive. In the case of BPP nets, a well-known subclass of Petri nets, we show that an FSA accepting the downward/upward closure can be constructed in exponential time. Furthermore, we consider the problem of checking whether a simple regular language is included in the downward/upward closure of a Petri net/BPP net language. We show that this problem is EXPSPACE-complete (resp. NP-complete) in the case of Petri nets (resp. BPP nets). Finally, we show that it is decidable whether a Petri net language is upward/downward closed. To this end, we prove that one can decide whether a given regular language is a subset of a Petri net coverability language. △ Less

Submitted 6 April, 2018; v1 submitted 11 January, 2017; originally announced January 2017.

Comments: The conference version of this paper has been published in the proceedings of the 42nd International Symposium on Mathematical Foundations of Computer Science, MFCS 2017

ACM Class: F.1.1

Managing Usability and Reliability Aspects in Cloud Computing

Authors: Maria Spichkova, Heinz W. Schmidt, Ian E. Thomas, Iman I. Yusuf, Steve Androulakis, Grischa R. Meyer

Abstract: Cloud computing provides a great opportunity for scientists, as it enables large-scale experiments that cannot are too long to run on local desktop machines. Cloud-based computations can be highly parallel, long running and data-intensive, which is desirable for many kinds of scientific experiments. However, to unlock this power, we need a user-friendly interface and an easy-to-use methodology for… ▽ More Cloud computing provides a great opportunity for scientists, as it enables large-scale experiments that cannot are too long to run on local desktop machines. Cloud-based computations can be highly parallel, long running and data-intensive, which is desirable for many kinds of scientific experiments. However, to unlock this power, we need a user-friendly interface and an easy-to-use methodology for conducting these experiments. For this reason, we introduce here a formal model of a cloud-based platform and the corresponding open-source implementation. The proposed solution allows to conduct experiments without having a deep technical understanding of cloud-computing, HPC, fault tolerance, or data management in order to leverage the benefits of cloud computing. In the current version, we have focused on biophysics and structural chemistry experiments, based on the analysis of big data from synchrotrons and atomic force microscopy. The domain experts noted the time savings for computing and data management, as well as user-friendly interface. △ Less

Submitted 6 December, 2016; originally announced December 2016.

Comments: Preprint. Accepted to the 11th International Conference on Evaluation of Novel Approaches to Software Engineering (ENASE 2016). Final version published by SCITEPRESS, http://www.scitepress.org

On the Complexity of Bounded Context Switching

Authors: Peter Chini, Jonathan Kolberg, Andreas Krebs, Roland Meyer, Prakash Saivasan

Abstract: Bounded context switching (BCS) is an under-approximate method for finding violations to safety properties in shared memory concurrent programs. Technically, BCS is a reachability problem that is known to be NP-complete. Our contribution is a parameterized analysis of BCS. The first result is an algorithm that solves BCS when parameterized by the number of context switches (cs) and the size of t… ▽ More Bounded context switching (BCS) is an under-approximate method for finding violations to safety properties in shared memory concurrent programs. Technically, BCS is a reachability problem that is known to be NP-complete. Our contribution is a parameterized analysis of BCS. The first result is an algorithm that solves BCS when parameterized by the number of context switches (cs) and the size of the memory (m) in O*(m^(cs)2^(cs)). This is achieved by creating instances of the easier problem Shuff which we solve via fast subset convolution. We also present a lower bound for BCS of the form m^o(cs / log(cs)), based on the exponential time hypothesis. Interestingly, closing the gap means settling a conjecture that has been open since FOCS'07. Further, we prove that BCS admits no polynomial kernel. Next, we introduce a measure, called scheduling dimension, that captures the complexity of schedules. We study BCS parameterized by the scheduling dimension (sdim) and show that it can be solved in O*((2m)^(4sdim)4^t)$, where t is the number of threads. We consider variants of the problem for which we obtain (matching) upper and lower bounds. △ Less

Submitted 24 April, 2017; v1 submitted 30 September, 2016; originally announced September 2016.

Munchausen Iteration

Authors: Roland Meyer, Sebastian Muskalla

Abstract: We present a method for solving polynomial equations over idempotent omega-continuous semirings. The idea is to iterate over the semiring of functions rather than the semiring of interest, and only evaluate when needed. The key operation is substitution. In the initial step, we compute a linear completion of the system of equations that exhaustively inserts the equations into one another. With fun… ▽ More We present a method for solving polynomial equations over idempotent omega-continuous semirings. The idea is to iterate over the semiring of functions rather than the semiring of interest, and only evaluate when needed. The key operation is substitution. In the initial step, we compute a linear completion of the system of equations that exhaustively inserts the equations into one another. With functions as approximants, the following steps insert the current approximant into itself. Since the iteration improves its precision by substitution rather than computation we named it Munchausen, after the fictional baron that pulled himself out of a swamp by his own hair. The first result shows that an evaluation of the n-th Munchausen approximant coincides with the 2^n-th Newton approximant. Second, we show how to compute linear completions with standard techniques from automata theory. In particular, we are not bound to (but can use) the notion of differentials prominent in Newton iteration. △ Less

Submitted 2 May, 2016; originally announced May 2016.

Summaries for Context-Free Games

Authors: Lukáš Holík, Roland Meyer, Sebastian Muskalla

Abstract: We study two-player games played on the infinite graph of sentential forms induced by a context-free grammar (that comes with an ownership partitioning of the non-terminals). The winning condition is inclusion of the derived terminal word in the language of a finite automaton. Our contribution is a new algorithm to decide the winning player and to compute her strategy. It is based on a novel repre… ▽ More We study two-player games played on the infinite graph of sentential forms induced by a context-free grammar (that comes with an ownership partitioning of the non-terminals). The winning condition is inclusion of the derived terminal word in the language of a finite automaton. Our contribution is a new algorithm to decide the winning player and to compute her strategy. It is based on a novel representation of all plays starting in a non-terminal. The representation uses the domain of Boolean formulas over the transition monoid of the target automaton. The elements of the monoid are essentially procedure summaries, and our approach can be seen as the first summary-based algorithm for the synthesis of recursive programs. We show that our algorithm has optimal (doubly exponential) time complexity, that it is compatible with recent antichain optimizations, and that it admits a lazy evaluation strategy. Our preliminary experiments indeed show encouraging results, indicating a speed up of three orders of magnitude over a competitor. △ Less

Submitted 1 November, 2016; v1 submitted 23 March, 2016; originally announced March 2016.

Comments: The conference version of this paper was accepted for FSTTCS 2016

ACM Class: F.1.1

Pointer Race Freedom

Authors: Frédéric Haziza, Lukáš Holík, Roland Meyer, Sebastian Wolff

Abstract: We propose a novel notion of pointer race for concurrent programs manipulating a shared heap. A pointer race is an access to a memory address which was freed, and it is out of the accessor's control whether or not the cell has been re-allocated. We establish two results. (1) Under the assumption of pointer race freedom, it is sound to verify a program running under explicit memory management as if… ▽ More We propose a novel notion of pointer race for concurrent programs manipulating a shared heap. A pointer race is an access to a memory address which was freed, and it is out of the accessor's control whether or not the cell has been re-allocated. We establish two results. (1) Under the assumption of pointer race freedom, it is sound to verify a program running under explicit memory management as if it was running with garbage collection. (2) Even the requirement of pointer race freedom itself can be verified under the garbage-collected semantics. We then prove analogues of the theorems for a stronger notion of pointer race needed to cope with performance-critical code purposely using racy comparisons and even racy dereferences of pointers. As a practical contribution, we apply our results to optimize a thread-modular analysis under explicit memory management. Our experiments confirm a speed-up of up to two orders of magnitude. △ Less

Submitted 11 November, 2015; v1 submitted 31 October, 2015; originally announced November 2015.

Report number: FIT-TR-2015-05

Satellite Quantum Communication via the Alphasat Laser Communication Terminal

Authors: Dominique Elser, Kevin Günthner, Imran Khan, Birgit Stiller, Christoph Marquardt, Gerd Leuchs, Karen Saucke, Daniel Tröndle, Frank Heine, Stefan Seel, Peter Greulich, Herwig Zech, Björn Gütlich, Ines Richter, Rolf Meyer

Abstract: By harnessing quantum effects, we nowadays can use encryption that is in principle proven to withstand any conceivable attack. These fascinating quantum features have been implemented in metropolitan quantum networks around the world. In order to interconnect such networks over long distances, optical satellite communication is the method of choice. Standard telecommunication components allow one… ▽ More By harnessing quantum effects, we nowadays can use encryption that is in principle proven to withstand any conceivable attack. These fascinating quantum features have been implemented in metropolitan quantum networks around the world. In order to interconnect such networks over long distances, optical satellite communication is the method of choice. Standard telecommunication components allow one to efficiently implement quantum communication by measuring field quadratures (continuous variables). This opens the possibility to adapt our Laser Communication Terminals (LCTs) to quantum key distribution (QKD). First satellite measurement campaigns are currently validating our approach. △ Less

Submitted 15 October, 2015; originally announced October 2015.

Comments: International Conference on Space Optical Systems and Applications (IEEE ICSOS 2015), October 27 and 28, 2015, New Orleans, USA, 4 pages, 5 figures

Chiminey: Reliable Computing and Data Management Platform in the Cloud

Authors: Iman I. Yusuf, Ian E. Thomas, Maria Spichkova, Steve Androulakis, Grischa R. Meyer, Daniel W. Drumm, George Opletal, Salvy P. Russo, Ashley M. Buckle, Heinz W. Schmidt

Abstract: The enabling of scientific experiments that are embarrassingly parallel, long running and data-intensive into a cloud-based execution environment is a desirable, though complex undertaking for many researchers. The management of such virtual environments is cumbersome and not necessarily within the core skill set for scientists and engineers. We present here Chiminey, a software platform that enab… ▽ More The enabling of scientific experiments that are embarrassingly parallel, long running and data-intensive into a cloud-based execution environment is a desirable, though complex undertaking for many researchers. The management of such virtual environments is cumbersome and not necessarily within the core skill set for scientists and engineers. We present here Chiminey, a software platform that enables researchers to (i) run applications on both traditional high-performance computing and cloud-based computing infrastructures, (ii) handle failure during execution, (iii) curate and visualise execution outputs, (iv) share such data with collaborators or the public, and (v) search for publicly available data. △ Less

Submitted 5 July, 2015; originally announced July 2015.

Comments: Preprint, ICSE 2015

Lazy TSO Reachability

Authors: Ahmed Bouajjani, Georgel Calin, Egor Derevenetc, Roland Meyer

Abstract: We address the problem of checking state reachability for programs running under Total Store Order (TSO). The problem has been shown to be decidable but the cost is prohibitive, namely non-primitive recursive. We propose here to give up completeness. Our contribution is a new algorithm for TSO reachability: it uses the standard SC semantics and introduces the TSO semantics lazily and only where ne… ▽ More We address the problem of checking state reachability for programs running under Total Store Order (TSO). The problem has been shown to be decidable but the cost is prohibitive, namely non-primitive recursive. We propose here to give up completeness. Our contribution is a new algorithm for TSO reachability: it uses the standard SC semantics and introduces the TSO semantics lazily and only where needed. At the heart of our algorithm is an iterative refinement of the program of interest. If the program's goal state is SC-reachable, we are done. If the goal state is not SC-reachable, this may be due to the fact that SC under-approximates TSO. We employ a second algorithm that determines TSO computations which are infeasible under SC, and hence likely to lead to new states. We enrich the program to emulate, under SC, these TSO computations. Altogether, this yields an iterative under-approximation that we prove sound and complete for bug hunting, i.e., a semi-decision procedure halting for positive cases of reachability. We have implemented the procedure as an extension to the tool Trencher and compared it to the Memorax and CBMC model checkers. △ Less

Submitted 12 January, 2015; originally announced January 2015.

Comments: accepted to FASE 2015

MSC Class: 68Q60 ACM Class: D.2.4; D.1.3; D.3.4

Robustness against Power is PSPACE-complete

Authors: Egor Derevenetc, Roland Meyer

Abstract: Power is a RISC architecture developed by IBM, Freescale, and several other companies and implemented in a series of POWER processors. The architecture features a relaxed memory model providing very weak guarantees with respect to the ordering and atomicity of memory accesses. Due to these weaknesses, some programs that are correct under sequential consistency (SC) show undesirable effects when… ▽ More Power is a RISC architecture developed by IBM, Freescale, and several other companies and implemented in a series of POWER processors. The architecture features a relaxed memory model providing very weak guarantees with respect to the ordering and atomicity of memory accesses. Due to these weaknesses, some programs that are correct under sequential consistency (SC) show undesirable effects when run under Power. We call these programs not robust against the Power memory model. Formally, a program is robust if every computation under Power has the same data and control dependencies as some SC computation. Our contribution is a decision procedure for robustness of concurrent programs against the Power memory model. It is based on three ideas. First, we reformulate robustness in terms of the acyclicity of a happens-before relation. Second, we prove that among the computations with cyclic happens-before relation there is one in a certain normal form. Finally, we reduce the existence of such a normal-form computation to a language emptiness problem. Altogether, this yields a PSPACE algorithm for checking robustness against Power. We complement it by a matching lower bound to show PSPACE-completeness. △ Less

Submitted 28 April, 2014; originally announced April 2014.

MSC Class: 68Q60 ACM Class: D.2.4; D.1.3

A Polynomial Translation of pi-calculus FCPs to Safe Petri Nets

Authors: Victor Khomenko, Roland Meyer, Reiner Hüchting

Abstract: We develop a polynomial translation from finite control pi-calculus processes to safe low-level Petri nets. To our knowledge, this is the first such translation. It is natural in that there is a close correspondence between the control flows, enjoys a bisimulation result, and is suitable for practical model checking. We develop a polynomial translation from finite control pi-calculus processes to safe low-level Petri nets. To our knowledge, this is the first such translation. It is natural in that there is a close correspondence between the control flows, enjoys a bisimulation result, and is suitable for practical model checking. △ Less

Submitted 16 September, 2013; v1 submitted 3 September, 2013; originally announced September 2013.

Comments: To appear in special issue on best papers of CONCUR'12 of Logical Methods in Computer Science

Journal ref: Logical Methods in Computer Science, Volume 9, Issue 3 (September 17, 2013) lmcs:932