Computing and Proving Well-founded Orderings through Finite Abstractions

TL;DR

This paper introduces a method for verifying progress in complex state machines by constructing finite abstractions and measures, ensuring progress properties without complex invariant derivation, with applications to microprocessor memory transactions.

Contribution

We develop a process to compute finite abstract graphs with decreasing measures, enabling progress verification in complex systems without complex invariants.

Findings

Successfully applied to the Bakery algorithm

Efficient extraction of abstract graphs using incremental SAT

Guarantees progress through measure reduction on system transitions

Abstract

A common technique for checking properties of complex state machines is to build a finite abstraction then check the property on the abstract system -- where a passing check on the abstract system is only transferred to the original system if the abstraction is proven to be representative. This approach does require the derivation or definition of the finite abstraction, but can avoid the need for complex invariant definition. For our work in checking progress of memory transactions in microprocessors, we need to prove that transactions in complex state machines always make progress to completion. As a part of this effort, we developed a process for computing a finite abstract graph of the target state machine along with annotations on whether certain measures decrease or not on arcs in the abstract graph. We then iteratively divide the abstract graph by splitting into strongly connected components and then building a measure for every node in the abstract graph which is ensured to be reducing on every transition of the original system guaranteeing progress. For finite state target systems (e.g. hardware designs), we present approaches for extracting the abstract graph efficiently using incremental SAT through GL and then the application of our process to check for progress. We present an implementation of the Bakery algorithm as an example application.