Memory models are formal specifications of concurrent-program executions, accounting for weak behaviors introduced by compiler and architectural optimizations. The increase of their number and complexity has spawned efforts for uniform verification across whole classes of models, by axiomatizing the models in an adequate metatheory that admits a uniform treatment. In this work, we formally study Monadic Second-Order logic (MSO) as a metatheory for weak memory, by proving results on the treewidth and MSO-expressibility of various popular weak-memory models, as this combination allows us to uniformly tackle several verification problems. In summary, our results are as follows. First, we prove that executions under Sequential Consistency (SC) have bounded treewidth, while already those under Total Store Order (TSO) do not. Second, we prove that a broad range of models, including Release/Acquire and the full RC20, are MSO-axiomatizable, while others, such as Strong Release/Acquire and TSO, are not, unless the Orthogonal Vectors problem - which requires quadratic time under SETH - can be solved in linear time. Finally, we introduce the notion of reads-from robustness, as an extension to recent work on coarse robustness criteria. We show that our treewidth bounds (both upper and lower) have far-reaching algorithmic implications for any of our MSO-axiomatizable models MM: there is an algorithm that, for every program 𝖯, either verifies 𝖯 under MM or reports that 𝖯 is not reads-from robust against MM. Overall, our results establish a rich and versatile theoretical framework for weak-memory verification and robustness.

We present efficient combinatorial parameterized algorithms for several classical graph-based counting problems in computational chemistry, including (i) Kekulé structures, (ii) the Hosoya index, (iii) the Merrifield–Simmons index, and (iv) Graph entropy based on matchings and independent sets. All these problems were known to be #P-complete. Building on the intuition that molecular graphs are often sparse and tree-like, we provide fixed-parameter tractable (FPT) algorithms using treewidth as our parameter. We also provide extensive experimental results over the entire PubChem database of chemical compounds, containing more than 113 million real-world molecules. In our experiments, we observe that the molecules are indeed sparse and tree-like, with more than 99.9% of them having a treewidth of at most 5. Our experiments also illustrate considerable improvements over the previous approaches. Based on these results, we argue that parameterized algorithms, especially based on treewidth, should be adopted as the default approach for problems in computational chemistry that are defined over molecular graphs.

Context-free language (CFL) reachability is a standard approach in static analyses, where the analysis question (e.g., is there a dataflow from x to y ?) is phrased as a language reachability problem on a graph G wrt a CFL L . However, CFLs lack the expressiveness needed for high analysis precision. On the other hand, common formalisms for context-sensitive languages are too expressive, in the sense that the corresponding reachability problem becomes undecidable. Are there useful context-sensitive language-reachability models for static analysis? In this paper, we introduce Multiple Context-Free Language (MCFL) reachability as an expressive yet tractable model for static program analysis. MCFLs form an infinite hierarchy of mildly context sensitive languages parameterized by a dimension d and a rank r . Larger d and r yield progressively more expressive MCFLs, offering tunable analysis precision. We showcase the utility of MCFL reachability by developing a family of MCFLs that approximate interleaved Dyck reachability, a common but undecidable static analysis problem. Given the increased expressiveness of MCFLs, one natural question pertains to their algorithmic complexity, i.e., how fast can MCFL reachability be computed ? We show that the problem takes O n 2 d + 1 time on a graph of n nodes when r = 1 , and O n d r + 1 time when r > 1 . Moreover, we show that when r = 1 , even the simpler membership problem has a lower bound of n 2 d based on the Strong Exponential Time Hypothesis, while reachability for d = 1 has a lower bound of n 3 based on the combinatorial Boolean Matrix Multiplication Hypothesis. Thus, for

Abstract Interleaved Dyck Reachability is a standard, graph-based formulation of a plethora of static analyses that seek to be context- and field-sensitive, where each type of sensitivity is expressed via a CFL/Dyck language. Unfortunately, the problem is well known to be undecidable in general, and thus existing approaches resort to clever overapproximations. Recently, a mutual-refinement algorithm, that iteratively considers each of the two sensitivities in isolation until a fixpoint is reached, was shown to achieve high precision. In this work we present a more precise approximation of Interleaved Dyck Reachability, by extending the mutual-refinement algorithm in three general directions. First, we develop refined CFLs to express each type of sensitivity precisely, while simultaneously also lightly overapproximating the opposite type. Second, we modify the graph information in a way to highlight unreachable paths not previously captured by the algorithm. Third, we apply the resulting algorithm on an on-demand basis, which effectively masks out imprecision incurred by parts of the graph that are irrelevant for the query at hand. Our experiments show that the new approach offers significantly higher precision than the vanilla mutual-refinement algorithm and other common baselines; for a particularly challenging benchmark, we report, on average, $51\%$ 51 % of the reachable pairs compared to the most recent alternative.

The Wiener index of a graph G is the sum of distances between all pairs of its vertices. It is a widely-used graph property in chemistry, initially introduced to examine the link between boiling points and structural properties of alkanes, which later found notable applications in drug design. Thus, computing or approximating the Wiener index of molecular graphs, i.e. graphs in which every vertex models an atom of a molecule and every edge models a bond, is of significant interest to the computational chemistry community. In this work, we build upon the observation that molecular graphs are sparse and tree-like and focus on developing efficient algorithms parameterized by treewidth to approximate the Wiener index. We present a new randomized approximation algorithm using a combination of tree decompositions and centroid decompositions. Our algorithm approximates the Wiener index within any desired multiplicative factor (1 ± ε) in time O(n ⋅ log n ⋅ k³ + √n ⋅ k/ε²), where n is the number of vertices of the graph and k is the treewidth. This time bound is almost-linear in n. Finally, we provide experimental results over standard benchmark molecules from PubChem and the Protein Data Bank, showcasing the applicability and scalability of our approach on real-world chemical graphs and comparing it with previous methods.

Algebraic Program Analysis (APA) is a ubiquitous framework that has been employed as a unifying model for various problems in data-flow analysis, termination analysis, invariant generation, predicate abstraction and a wide variety of other standard static analysis tasks. APA models program summaries as elements of a regular algebra . Suppose that a summary inAis assigned to every transition of the program and that we aim to compute the effect of running the program starting at linesand ending at linet. APA first computes a regular expression capturing all program paths of interest. In case of intraprocedural analysis, models all paths fromstot, whereas in the interprocedural case it models all interprocedurally-valid paths, i.e. ‍paths that go back to the right caller function when a callee returns. This regular expression is then interpreted over the algebra to obtain the desired result. Suppose the program hasnlines of code and each evaluation of an operation in the regular algebra takesO(k) time. It is well-known that a single APA query, or a set of queries with the same starting points, can be answered inO(n· α(n) ·k), where α is the inverse Ackermann function. In this work, we consider an on-demand setting for APA: the program is given in the input and can be preprocessed. The analysis has to then answer a large number of on-line queries, each providing a pair (s,t) of program lines which are the start and end point of the query, respectively. The goal is to avoid the significant cost of running a fresh APA instance for each query. Our main contribution is a series of algorithms that, after a lightweight preprocessing ofO(n· lgn·k), answer each query inO(k) time. In other words, our preprocessing has almost the same asymptotic complexity as a single APA query, except for a sub-logarithmic factor, and then every future query is answered instantly, i.e. ‍by a constant number of operations in the algebra. We achieve this remarkable speedup by relying on certain structural sparsity properties of control-flow and call graphs (CFGs and CGs). Specifically, we exploit the fact that control-flow graphs of real-world programs have a tree-like structure and bounded treewidth and nesting depth and that their call graphs have small treedepth in comparison to the size of the program. Finally, we provide experimental results demonstrating the effectiveness and efficiency of our approach and showing that it beats the runtime of classical APA by several orders of magnitude.

Pathwidth and treewidth are standard and well-studied graph sparsity parameters which intuitively model the degree to which a given graph resembles a path or a tree, respectively. It is well-known that the control-flow graphs of structured goto-free programs have a tree-like shape and bounded treewidth. This fact has been exploited to design considerably more efficient algorithms for a wide variety of static analysis and compiler optimization problems, such as register allocation, µ-calculus model-checking and parity games, data-flow analysis, cache management, and liftetime-optimal redundancy elimination. However, there is no bound in the literature for thepathwidthof programs, except the general inequality that the pathwidth of a graph is at mostO(lgn) times its treewidth, wherenis the number of vertices of the graph. In this work, we prove that control-flow graphs of structured programs have bounded pathwidth and provide a linear-time algorithm to obtain a path decomposition of small width. Specifically, we establish a bound of 2 ·don the pathwidth of programs with nesting depthd. Since real-world programs have small nesting depth, they also have bounded pathwidth. This is significant for a number of reasons: (i) ‍pathwidth is a strictly stronger parameter than treewidth, i.e. ‍any graph family with bounded pathwidth has bounded treewidth, but the converse does not hold; (ii) ‍any algorithm that is designed with treewidth in mind can be applied to bounded-pathwidth graphs with no change; (iii) ‍there are problems that are fixed-parameter tractable with respect to pathwidth but not treewidth; (iv) ‍verification algorithms that are designed based on treewidth would become significantly faster when using pathwidth as the parameter; and (v) ‍it is easier to design algorithms based on bounded pathwidth since one does not have to consider the often-challenging case of merge nodes in treewidth-based dynamic programming. Thus, we invite the static analysis and compiler optimization communities to adopt pathwidth as their parameter of choice instead of, or in addition to, treewidth. Intuitively, control-flow graphs are not only tree-like, but also path-like and one can obtain simpler and more scalable algorithms by relying on path-likeness instead of tree-likeness. As a motivating example, we provide a simpler and more efficient algorithm for spill-free register allocation using bounded pathwidth instead of treewidth. Our algorithm reduces the runtime fromO(n·r2 ·tw·r+ 2 ·r) toO(n·pw·rpw·r+r+ 1), wherenis the number of lines of code,ris the number of registers,pwis the pathwidth of the control-flow graph andtwis its treewidth. We provide extensive experimental results showing that our approach is applicable to a wide variety of real-world embedded benchmarks from SDCC and obtains runtime improvements of 2-3 orders of magnitude. This is because the pathwidth is equal to the treewidth, or one more, in the overwhelming majority of real-world CFGs and thus our algorithm provides an exponential runtime improvement. As such, the benefits of using pathwidth are not limited to the theoretical side and simplicity in algorithm design, but are also apparent in practice.