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

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