Explanations for black-box rankers with Generalized Additive Models

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...

Verifying weak memory concurrent data structure implementations

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...

Building a Compiler Optimizing C++ Atomic Accesses

Atomics is an important primitive for programming languages like C++ to develop concurrent software. Atomic variables, together with weak memory models allow for a bigger space for instruction reordering and compiler optimizations. However, the current compilers like LLVM do not support many transformations of atomics, which may lose chances of...

Expressing Intent: An evaluation of the Arm Machine Readable Specification

The behaviour of software is intrinsically linked to the hardware it runs on. As hardware innovations continuously change the landscape of computing, software has to adapt to these changes. Running legacy software on new hardware requires either the old hardware to be emulated, or a very time-consuming and error-prone process of reverse...

Fencing off unwanted behavior: Improving and evaluating the Fency static analysis tool

Computer architectures with weak memory models, such as ARMv8 and ARMv7, allow memory accesses to be reordered in many situations.<br/>Therefore, weak memory models may cause a program to exhibit more behavior than a strong memory model, such as x86.<br/>Fency is a static analysis tool that inserts memory fences to ensure that a program exhibits...

Probabilistic Testing for Weak Memory Concurrency

The Probabilistic Concurrency Testing (PCT) algorithm provides theoretical guarantees for the probability of detecting concurrency bugs in a sequential consistency memory model, but its theoretical guarantees do not apply to weak memory concurrency. The weak memory concurrency refers to the modern compiler’s optimization that relaxes the...

Evaluating Stochastic Floating-Point Superoptimization with STOKE

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...

Evaluating the egg Equality Saturation Superoptimizer

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...

Evaluating STOKE

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...

Evaluating Souper: A Synthesizing Superoptimizer

Modern compilers exploit syntax \&amp; semantics to optimize input programs.<br/>Often such optimization rules are arduous to get right and the output is not guaranteed to be globally optimal.<br/>Superoptimizers take a different approach to this problem by traversing the program space.<br/>This study focuses on Souper, a synthesizing...