Scalable Typestate Analysis for Low-Latency Environments

TL;DR

This paper introduces a lightweight, scalable typestate analysis method for low-latency environments, using an expressive language and efficient automata to improve performance and usability in certifying code correctness.

Contribution

It presents a novel typestate analysis approach that employs a subclass of DFAs with bit-vector operations, enabling efficient contract specification and analysis in performance-critical settings.

Findings

Significant performance improvements over existing techniques

Enhanced usability through expressive contract specification language

Successful implementation in the Infer static analyzer

Abstract

Static analyses based on typestates are important in certifying correctness of code contracts. Such analyses rely on Deterministic Finite Automata (DFAs) to specify properties of an object. We target the analysis of contracts in low-latency environments, where many useful contracts are impractical to codify as DFAs and/or the size of their associated DFAs leads to sub-par performance. To address this bottleneck, we present a lightweight typestate analyzer, based on an expressive specification language that can succinctly specify code contracts. By implementing it in the static analyzer Infer, we demonstrate considerable performance and usability benefits when compared to existing techniques. A central insight is to rely on a sub-class of DFAs with efficient bit-vector operations.