Parameterized Verification under TSO with Data Types

TL;DR

This paper introduces a framework for parameterized verification of systems under TSO semantics with data types, translating reachability problems to register machines and establishing complexity bounds for various data types.

Contribution

It provides a novel translation framework for TSO-based systems with data types and derives tight complexity bounds for multiple classes of data structures.

Findings

Complexity bounds for TSO verification with push-down automata

Extension of bounds to higher order stacks and counters

Framework applicable to Petri nets and other data types

Abstract

We consider parameterized verification of systems executing according to the total store ordering (TSO) semantics. The processes manipulate abstract data types over potentially infinite domains. We present a framework that translates the reachability problem for such systems to the reachability problem for register machines enriched with the given abstract data type. We use the translation to obtain tight complexity bounds for TSO-based parameterized verification over several abstract data types, such as push-down automata, ordered multi push-down automata, one-counter nets, one-counter automata, and Petri nets. We apply the framework to get complexity bounds for higher order stack and counter variants as well.