Rob Sumners
ACL2 Seminar, Nov. 16, 2015

Title: Reducing Fair Stuttering Refinements of Transaction Systems

Abstract: Verifying or proving progress properties of larger-scale
systems is ubiquitously unfun. While various algorithms and procedures
exist to help tame the verification of safety properties, verifying
progress is still a daunting task for model checkers and theorem
provers and their brethren. We define a specific class of
transaction-based systems which afford moderately tractable reductions
and algorithms for proving fair stuttering refinements (a compact
specification which incorporates both safety and progress
properties). This capability comes at the price of fairly severe
restrictions on how transactions can interact (specifically,
transactions can only selectively block other transactions). We
attempt to show that even with these restrictions, one can still
define interesting systems (we will cover a cache coherence protocol
in the talk) with some adjustments to definitions and perspectives. We
will cover an implementation of a checker for these refinements
written in ACL2 which targets finite-state transactions (although the
number of transactions is unbounded) using BDDs. Future work to extend
this to general term rewriting (with extension via proven ACL2
theorems) and a hopeful correctness proof of the checker in ACL2 will
also be covered in the talk.. time permitting.