Quantified formulas over linear integer arithmetic (LIA) are common in formal verification, yet they present significant challenges for satisfiability modulo theories (SMT) solvers such as Z3. In this paper, we explore whether quantifier elimination can improve solver performance on the 2-coin Frobenius Coin Problem, a benchmark involving quantified LIA formulas with structural simplicity. While Z3's default strategy relies on solving satisfiability of a quantified formula directly, we evaluate an alternative tactic-based approach using the \texttt{qe\_rec} tactic to eliminate quantifiers first and produce a quantifier-free formula, which is then solved by the general purpose SMT solver. We conduct benchmarking across 54 satisfiable instances involving pairs of prime coin denominations. Our results indicate that quantifier elimination achieves better performance in both runtime and memory usage, solving more instances and offering consistent speed-ups of up to 10$\times$ compared to the default strategy.

To solve floating-point SMT problems, a variety of algorithms can be used, but there is not one algorithm that truly stands out at solving any kind of problem, as most have their own specific subset of problems where they perform well. A solution to maintaining efficiency in solving any kind of floating-point SMT problem is to run many of these domain specific solvers in parallel, allowing the best to always come out on top. This paper aims to provide an insight into possible improvements using parallelization by running multiple solvers (in parallel) on a large and diverse set of problems. We show that by parallelizing diverse solvers we can obtain a significant speedup over individual solvers on complex problems.

Satisfiability modulo theories solvers serve as the backbone of software verifiers, static analyzers, and proof assistants; the versatile bit-vector arithmetic theory is particularly important for these applications. As solvers continue to be developed, they become more capable but also more difficult to configure optimally. The widely-used Z3 prover offers a multitude of configurable techniques for solving bit-vector problems, however, the pace of development has not allowed for a comprehensive comparative analysis of them. We study the available bit-vector algorithms and parallelization methods, on established sets of problems. Through an experimental evaluation, we find that properly configuring Z3 for a specific use case can have significant effects on performance. We offer guidance to developers on how to go about that, which should help to make formal verification tools more efficient.

Z3 is a widely used SMT solver with support for linear and non-linear arithmetic. While powerful, its performance is dependent on tactics -- user-defined strategies that guide the solving process. This paper systematically analyzes the performance of Z3 across various tactic sequences, including ones with parallelization, on benchmarks from SMT-LIB. The results reveal that certain problems can get a speed-up of up to 5 times with the appropriate strategy, however different approaches come with certain limitations. We explore a pattern in linear problems where parallelization and heavy preprocessing make a big difference to performance. Additionally, we discuss two non-linear benchmarks for which it is very evident that the right approach to tactic selection matters and there is no single optimal strategy in SMT solving. These are all important observations since SMT solvers are a key part of many industrial processes where speed and accuracy are crucial.

Build systems are essential tools for compiling codebases of any complexity. In order to maximize performance, they use parallelism to complete multiple build steps simultaneously. In this thesis, we examine the effectiveness with which common build systems distribute work across available CPUs. We design an automatic process for fetching, compiling, and inspecting the build steps of common C/C++ codebases, and use it to benchmark various build systems. Based on empirical performance measurements and an analysis of the source code of these build systems, we find that the differences in task scheduling between build systems do not significantly affect performance.

Over the past decades, Single Instruction, Multiple Data (SIMD) instructions have become common- place in conventional hardware. Lexical analysis, the first stage of compilation, can take advantage of this by splitting its workload across sub lexers that identify groups of tokens with similar structures. Each sub lexer can leverage SIMD to search for these structures across multiple characters in paral- lel and extract token positions efficiently. This pa- per presents a lexer with this architecture for the C programming language, along with implementation details for x86/x64 processors. Benchmark results show a 12x speed up in throughput compared to the lexer found in GCC, a state-of-the-art compiler.

In the field of software engineering, the speed of compilation plays a crucial role in enhancing development productivity. This thesis investigates the impact of optimising the memory layout of Abstract Syntax Trees (ASTs) on the performance of the type checking and code generation phases in the compilation process of strictly-typed procedural programming languages. Existing compilers often employ a traditional Object-Oriented (OO) approach to AST construction, leading to inefficiencies such as high memory overhead and suboptimal cache usage. We applied Data-Oriented Design (DOD) principles to restructure ASTs, aiming to enhance data locality and reduce memory access times.

The study investigates various AST memory layouts, including a transition from a naive OO model to a Struct-of-Arrays (SoA) model. We evaluated the effect of these memory layouts on compiler performance using a set of benchmarks based on real-world code. We executed the benchmarks on diverse hardware platforms, measuring key performance metrics such as type checking time, code generation time, and cache miss rates.

The results demonstrate that adopting an SoA model for ASTs significantly reduces the duration of the type checking and code generation phases, with improvements varying across different hardware architectures. We provide empirical evidence supporting the application of DOD principles and specifically SoA to ASTs for performance improvements. By highlighting and addressing the performance bottlenecks associated with traditional AST layouts, we contribute to the broader goal of advancing compiler design and optimisation.

Term-rewriting super-optimisation during compilation uses rewrite rules in order to restructure a provided code expression into the optimal form, comparing different expressions using a cost function. To reduce the compilation time taken by term-rewriting, the ruleset can be optimised by combining rules that were commonly chained during previous optimisation runs. With an any-time super-optimiser a specialised ruleset makes it possible to attain the optimal code expression, under the ruleset constraints, with a lower time requirement.

We found rule chaining methods to be effective at reducing the time necessary to obtain the canonical form. The methods performed well on synthetic benchmarks, as well as ones representative of real C projects. The frequency of the chained rule use and their uniqueness compared to the other compound rules directly dictates how great of a performance improvement its addition provides. Optimised sets demonstrated poor generality, indicating over-specialisation.

This study examines the differences between two modern linkers, LLD and mold, focusing on their efficiency during software development. Although the linking process, which combines multiple object files into a single executable, typically occupies a minor fraction of the total compilation time, optimizing it can significantly enhance the overall build efficiency - particularly during the development of large-scale projects. The research aims to determine codebase-level differences between these linkers and assess their performance across various metrics, including linking time, memory usage, and the time spent on different phases of the linking process, using CMake and Bitcoin Core as benchmarks. Furthermore, the study extends to examining the executables produced by both linkers from the HDiffPatch project, comparing their execution times and sizes. The findings consistently show that mold outperforms LLD in terms of speed and efficiency, which results from its comprehensive utilization of parallel processing techniques. Nonetheless, LLD offers broader applicability by supporting a wider range of file formats and being suitable for both embedded and kernel programming. Therefore, the selection of a linker ultimately depends on the specific requirements of the project and the characteristics of the target machine.

Modern compilers exploit syntax \& semantics to optimize input programs.
Often such optimization rules are arduous to get right and the output is not guaranteed to be globally optimal.
Superoptimizers take a different approach to this problem by traversing the program space.
This study focuses on Souper, a synthesizing superoptimizer which makes use of an enhanced counter-example-guided inductive synthesis loop to find optimizations.
We first detail the working mechanism of the superoptimizer and its components, then we explain our attempts at reproducing the results mentioned by Souper's authors.
Finally, we give three program classes each exercising different aspects of the superoptimizer and how these are useful in gaining insight into Souper's optimization capabilities and use cases.

STOKE is one of the Superoptimizers which are programs that given a function and a set of instructions of a processor, traverse through a space of programs that compute a given function and try to find the optimal usually in terms of execution speed or size of the binary. Authors of STOKE make some extraordinary claims. They suggest that it is able to produce programs that are multiple times faster than programs without any optimization, and programs which are at least as efficient as programs produced by gcc -O3 and sometimes expert handwritten assembly. The goal of this paper is to check these claims. In this paper classes of programs that STOKE may handle particularly well and any class of programs that stochastic optimization might not be able to handle will be identified. We conclude from the experiments described in this paper that STOKE is able to fulfill that statement in some cases. The searching algorithm of STOKE is not always able to find programs that are at least as efficient as programs optimized by gcc -O3. STOKE works particularly well in programs where a lot consecutive logical and mathematical operations are calculating (e.g. counting bits). It is often not that successful with programs containing loops where it sometimes can’t find a solution at all.

The superoptimizer STOKE has previously been shown to be effective at optimizing programs containing floating-point numbers. The STOKE optimizer obtains these results by running a stochastic search over the set of all programs and selecting the best-optimized one. This study aims to find more clearly what floating-point programs STOKE optimizes particularly well and for which ones it fails to find significant rewrites. To answer the research question, STOKE and GCC optimized multiple small programs, and I compared these on execution speed. The results showed numerous cases where STOKE failed to obtain a better optimization than GCC. The results suggest that for specific floating-point functions, there exist limitations in both the test case generator and the STOKE search algorithm that prevent it from finding good optimizations. The findings of this paper suggest further research on the STOKEs test case generator to improve its performance.

Superoptimization is the idea of creating the most optimal program possible from a given input program. Equality saturation is a method of superoptimization using rewrite rules and e-graphs. A rewrite rule defines a piece of code that can be rewritten as another part while keeping equal behavior. This is added to an e-graph, a data structure which is able to express a lot of equal programs efficiently using e-nodes and e-classes. Egg is a general equality saturation superoptimizer developed in Rust, which has been the basis of multiple extensions. This research first aimed to validate claims made by the creators of egg which stated that rebuilding improved equality saturation. Secondly, the research aimed to evaluate the performance of egg when supplying a different amount of rewrite rules. The research found that egg indeed does improve equality saturation, with an 88× speedup for a part of the algorithm as claimed by the creators, but a claim of 21× overall speedup is an overestimate, as an overall speedup of between 16.4× and 17.4× was achieved. The second part shows that providing egg with extra unused rewrite rules slows the algorithm down, although the slowdown seems to decrease when the size of the program increases. The second part also tried to draw a conclusion on adding rewrite rules which will be applied indirectly via multiple other rewrite rules, called implied rewrite rules. Two tests indicated a speedup, but another indicated a slowdown. This means it is unknown if adding implied rewrite rules is beneficial, as no general conclusion could be drawn. Therefore, egg seems to benefit from removing unused rewrite rules, and might benefit from adding implied rewrite rules.

Computer architectures with weak memory models, such as ARMv8 and ARMv7, allow memory accesses to be reordered in many situations.
Therefore, weak memory models may cause a program to exhibit more behavior than a strong memory model, such as x86.
Fency is a static analysis tool that inserts memory fences to ensure that a program exhibits the same behavior when run on a weaker memory model.
However, Fency lacks important features such as function call support, does not use LLVM's alias analysis algorithms, and inserts too many fences when targeting ARMv8.

We expand Fency with a new dependency tracking analysis, integrate it with LLVM's alias analysis infrastructure, and improve its usability.
We show that while the new alias analysis fixes a vital soundness issue, it does not reduce the number of fences Fency inserts.
Additionally, our evaluation of the dependency tracking analysis shows that it can eliminate some redundant fences.
Finally, we run Fency on larger C/C++ programs, which we made possible by reimplementing Fency as a module pass.