Rust is a systems programming language that guarantees both performance and Memory Safety through its memory model. With unsafe rust it is possible to opt-out of some security guarantees made by the compiler. However, this comes at the risk of re-introducing memory bugs. While various tools already exist for detecting memory errors in (unsafe) Rust, they are either dynamic or focus on proving the absence of bugs. In this thesis we lay the foundations for a static analysis for Rust that focuses on proving the presence of bugs (Under Approximation) instead of their absence (Over Approximation). We show how we can use a formal framework called incorrectness separation logic (ISL) to show the presence of memory errors in Rust. We add Rust support to Infer, a static analysis tool by Meta that uses ISL to prove the presence of bugs. This is done by translating Rust to a Verification Intermediate Language. Finally, we show that our extension to can be used to detect memory bugs in Rust such as null pointer dereferences, dangling pointer dereferences and use after frees.

Dataset: https://doi.org/10.4121/f0b3b808-51c3-4637-b6ff-3654506da71c

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.

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.

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.

This thesis presents the first known implementation of a model checker for the Java memory model JAM21 within the GenMC framework - a tool for stateless model checking using custom memory models. In addition to the baseline GenMC implementation, we introduce a more efficient model checking algorithm based on vector clocks, which significantly outperforms the initial version. We provide a formal proof of equivalence between the new vector clock algorithm and the original implementation to ensure correctness. Our approach is evaluated using the standard suite of litmus tests included with GenMC. The results confirm that both algorithms correctly enforce the guarantees of JAM21. Furthermore, we successfully replicate prior findings by disallowing erroneous behaviors that went undetected under JAM19.

Developing correct concurrent data structures under weak memory models presents significant challenges due to subtle concurrency errors arising from relaxed ordering guarantees and complexities in Safe Memory Reclamation. Existing synthesis methods largely assume sequential consistency, overlooking critical reorderings allowed by realistic architectures.

This thesis introduces a synthesis-verification pipeline that iteratively generates concurrent data structures from partial code specifications using Large Language Models. The pipeline is expanded by integrating an advanced model checker, GenMC, enhanced specifically to verify SMR correctness under weak memory through automaton-based hazard pointer verification. This integration provides memory safety guarantees across diverse execution scenarios.

We evaluate our approach using established concurrent data structure benchmarks, demonstrating rapid convergence to correct implementations, outperforming state-of-the-art methods. These results highlight the pipeline’s effectiveness and scalability, illustrating its potential to support researchers in developing novel, reliable concurrent data structures under weak memory models.

Conventional neural network hardware faces dual challenges: the diminishing returns of Moore’s Law and the intensifying constraints of the memory wall. In contrast, an emerging specialized hardware architecture, namely compute-in-memory (CIM), is gaining attention, inherently mitigating the above challenges imposed by its in-memory computing capability. However, unlike the conventional computing hardware ecosystem, which benefits from mature toolchains and well-established methodologies, current CIM architectures still lack robust infrastructure for exploring optimization opportunities and pinpointing performance bottlenecks. To address this, this thesis proposes a two-tier static profiling framework that designs and combines a Multi-Level Intermediate Representation (MLIR) profiler with a hardware-oriented profiler to identify instruction scale, memory pressure, and parallelism ceilings with low compilation overhead. It also introduces a weight-based convolutional adaptation method that effectively addresses non-sequential access issues in convolutional compilation, reducing latency and energy consumption at the cost of additional hardware overhead. Comparative experiments demonstrate that the optimized framework outperforms state-of-the-art conventional hardware in terms of latency and energy consumption for small convolutional neural network models. This result presents an exploratory path for compilation optimization on CIM architectures.

The rapid advancement of neural network applications, including multilayer perceptrons (MLP) and deep convolutional neural networks (CNN), has revolutionized domains such as image recognition, speech processing, and classification. However, the increasing depth and complexity of neural network workloads impose significant computational and energy demands. Conventional hardware, such as CPUs and GPUs, faces growing challenges in meeting these demands due to the "memory wall" problem and the diminishing benefits of Moore’s law and Dennard scaling. These issues are particularly pronounced in edge devices where power and energy efficiency are critical.

To address these limitations, computing-in-memory (CIM) architectures, particularly memristor-based crossbar arrays, have emerged as promising solutions. CIM reduces data movement by performing computations directly within memory, significantly improving energy efficiency and performance. Memristor crossbars excel in analog matrix-vector multiplication (MVM), a fundamental operation in neural networks, making them an ideal candidate for accelerating neural network workloads.

This thesis proposes an end-to-end compilation framework that automates the translation and optimization of neural networks for CIM architectures. The framework supports converting high-level MLP models represented in PyTorch into low-level instructions optimized for crossbar-based spatial CIM architectures. Comprehensive experiments explore the impact of various quantization schemes and design space parameters, revealing trade-offs between performance, energy efficiency, and resource utilization. The results demonstrate the framework's potential to support diverse neuromorphic systems and facilitate the efficient deployment of neural networks on CIM architectures.

This dissertation is about translating concurrent programs between computer architectures. Legacy programs—built-for and tested-on x86—behave differently on newer architectures, such as Arm and RISC-V. Particularly, weak memory behaviors emerge when two micro-architectural features interact: (i) concurrency, where multiple CPU cores simultaneously execute parts of a program, and (ii) out-of-order execution, where a CPU core reorders instructions to increase throughput. Programs can non-deterministically show one of various weak memory behaviors, meaning it could behave differently when executing again. Those behaviors differ between architectures. When migrating programs from x86 to Arm or RISC-V, the same program could non-deterministically show behaviors never observed on x86.

In part I, we look at binary translators, which are software systems that translate compiled binary programs between architectures. We study the translation process of three such real-world systems, identify errors in their translation of concurrency primitives, and fix them. We propose mathematically-rigorous weak memory models for these translators. We then define mapping schemes to translate concurrency primitives one-by-one from x86 to Arm and RISC-V. With the formal semantics, we prove those mapping schemes correct in the Agda proof assistant.

In part II, we study the common structure of our weak memory proofs written in Agda. As those proofs are often large, complex, and rigid, we identify their common structures for which we identify domain-specific abstractions. We implement those abstractions in our novel Agda proof framework Burrow to greatly simplify writing future weak memory proofs.

In part III, we use dynamic analysis to identify weak behaviors that were never seen on x86 but could appear on Arm. Our analysis simulates the program’s execution with the formal weak memory semantics of x86 and Arm. This analysis identifies only the new behaviors the program shows in practice. After finding any new behavior on Arm, we judiciously modify the program to eliminate only that behavior.

This thesis presents a methodology for the formal verification of memory organizations in System-on-Chip (SoC) designs described in IP-XACT. The approach involves modeling the address map structures of the design's IP-XACT description and its spreadsheet-based global address map specification into a unified graph model we developed, called an Address Map Graph (AMG). Additionally, it introduces an analysis of AMGs to determine the equivalence of their mapped addresses, called Graph Bitmapping Equivalence (GBE). The methodology was implemented through a series of modular programs integrated into a solution flow. These programs process the spreadsheet memory specifications and IP-XACT design representations into AMGs and perform efficient GBE calculation and detailed reporting. The solution was evaluated using a state-of-the-art mid-size SoC design as a case study. Verification of results was performed using commercially available design analysis tools. The results demonstrated the developed solution was effective to analyze and verify the memory organization of complex SoC designs and to assist in identifying the causes of discrepancies.

XMM is a newly designed multi-execution memory model that solves the out-of-thin-air exe- cutions problem, enables the most efficient compilation to all hardware platforms, and allows common compiler optimizations. Promising and Weakestmo are similar multi-execution models proposed recently. However, due to their complex semantics, they do not have an accompany- ing model checker with a proof of soundness. XMM is significantly less complex, which paved the way for implementing an XMM model checker. In our work, we present our design of a model checker algorithm for the XMM memory model called GenMC-XMM. Due to practical limitations of algorithmic time complexity, we could not design a complete model checker. However, we provide a proof of soundness. In other words, we cannot guarantee that our tool will find all possible executions of a program, but we can guarantee that the ones it finds are all XMM consistent. To our knowledge, GenMC-XMM is the first multi-execution model checker proven to be sound. We evaluated our tool against the state-of-the-art model checking tools for RC11, IMM, and Weakestmo2. We determined that GenMC-XMM explores the same or more executions than every other tool in all our tests. GenMC-XMM is only marginally slower than the other tools in real-world lock-free data- structure benchmarks. In synthetic tests designed to have thousands of data races, GenMC- XMM does not scale as well as the other tools as the number of races increases. GenMC-XMM is the next milestone in the automatic verification of multi-execution memory models. Based on our work on GenMC-XMM, other researchers may improve its performance and design a sound and complete algorithm.

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.

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.

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.

Machine learning has revolutionized recommendation systems by employing ranking models for personalized item suggestions. Despite their effectiveness, learning-to-rank (LTR) models often operate as complex systems, making it difficult to discern the factors influencing their ranking decisions. This lack of transparency raises concerns about potential errors, biases, and ethical implications. As a result, interpretable LTR models have emerged as a solution to enhance transparency and mitigate these challenges.
Currently, the state-of-the-art intrinsically interpretable ranking model is led by generalized additive models. However, ranking GAMs have some limitations that affect their successful application in experiment environments, such as being computationally intensive and struggling to handle high-dimensional data. In contrast to these drawbacks, post-hoc methods can potentially provide more scalable and efficient solutions for real-time ranking. In this study, we propose a post-hoc method for learning-to-rank tasks combined with the interpretable GAMs. The evaluation results tested with Kendall’s 𝜏 value indicate that our model can effectively explain different types of black-box rankers.

From formal hardware models to programming language implementations concurrency is everywhere. While there has been a lot of work done on verifying concurrent systems a large part of it is focused on SC. In practice, it is more common to encounter weak memory models for which the techniques developed for SC do not work. There exists previous research on verifying weak memory concurrent programs, however, this work is often limited in scope and is often difficult to understand and apply to a broader context. This thesis gives a general approach for calculating higher-level relations between function calls in a weak memory context that work for weak memory concurrent mutex, stack, and queue data structures. These relations allow us to abstract away implementation details for easier reasoning about program behaviour. These function-level relations and data structure models defined using them are implemented in a stateless model checker and used to verify several existing mutex, stack, and queue implementations.

This research explores the size variations of artifacts in Maven Central, a repository containing a large collection of Java artifacts. This analysis sheds light on the coding habits and dependency management ecosystems within Maven Central, emphasizing the importance of managing artifact sizes effectively. It also provides valuable insights to library maintainers and clients who want to download libraries. For example, we can determine the average amount of space required to download 100 libraries.
The analysis is done by selecting a single version for each artifact in Maven Central and extracting metadata from the corresponding files.
The results reveal that the average size of an artifact is 1447 KB, although this average is heavily influenced by a few exceptionally large artifacts. Approximately 86% of the artifacts have a size smaller than 400 KB, indicating that the majority of artifacts are relatively lightweight.
The large artifacts identified in the analysis are predominantly attributed to two categories. The first category contains extensive projects with a substantial number of files, while the second category includes machine learning or big data projects that include massive data files.