Proving Skipping Refinement with ACL2s

TL;DR

This paper demonstrates how ACL2s can be used to verify skipping refinement in optimized reactive systems, enabling reasoning about systems that can skip or combine multiple specification steps due to optimizations.

Contribution

It introduces a method for proving skipping refinement with ACL2s and applies it to three case studies involving optimized reactive systems.

Findings

Successfully verified skipping refinement for a JVM-inspired stack machine

Proved correctness of a simple memory controller using skipping refinement

Validated a scalar to vector compiler transformation with ACL2s

Abstract

We describe three case studies illustrating the use of ACL2s to prove the correctness of optimized reactive systems using skipping refinement. Reasoning about reactive systems using refinement involves defining an abstract, high-level specification system and a concrete, low-level system. Next, one shows that the behaviors of the implementation system are allowed by the specification system. Skipping refinement allows us to reason about implementation systems that can "skip" specification states due to optimizations that allow the implementation system to take several specification steps at once. Skipping refinement also allows implementation systems to, i.e., to take several steps before completing a specification step. We show how ACL2s can be used to prove skipping refinement theorems by modeling and proving the correctness of three systems: a JVM-inspired stack machine, a simple memory controller, and a scalar to vector compiler transformation.