Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Deciding Serializability in Network Systems

Guy Amir, Mark Barbone, Nicolas Amat, Jules Jacobs

TL;DR

This work addresses the challenge of verifying serializability for unbounded concurrent systems by introducing the SER modeling language and a network-system abstraction that enables automatic verification. The authors develop an end-to-end decision procedure that either proves serializability with a certificate or exposes a counterexample trace by reducing the problem to Petri-net reachability and semilinear constraints, with practical optimizations to manage the inherent Ackermann-complete hardness. The Ser toolchain translates SER programs into NS, then into Petri nets, and uses a reachability engine to produce proofs or counterexamples; optimizations like bidirectional slicing and semilinear pruning dramatically improve scalability. Empirical evaluation on a rich benchmark suite— including stateful firewalls and BGP routing models—demonstrates the framework’s ability to handle non-trivial real-world-like programs, offering a first-end-to-end, certificate-generating verifier for unbounded serializability in networked systems.

Abstract

We present the SER modeling language for automatically verifying serializability of concurrent programs, i.e., whether every concurrent execution of the program is equivalent to some serial execution. SER programs are suitably restricted to make this problem decidable, while still allowing for an unbounded number of concurrent threads of execution, each potentially running for an unbounded number of steps. Building on prior theoretical results, we give the first automated end-to-end decision procedure that either proves serializability by producing a checkable certificate, or refutes it by producing a counterexample trace. We also present a network-system abstraction to which SER programs compile. Our decision procedure then reduces serializability in this setting to a Petri net reachability query. Furthermore, in order to scale, we curtail the search space via multiple optimizations, including Petri net slicing, semilinear-set compression, and Presburger-formula manipulation. We extensively evaluate our framework and show that, despite the theoretical hardness of the problem, it can successfully handle various models of real-world programs, including stateful firewalls, BGP routers, and more.

Deciding Serializability in Network Systems

TL;DR

This work addresses the challenge of verifying serializability for unbounded concurrent systems by introducing the SER modeling language and a network-system abstraction that enables automatic verification. The authors develop an end-to-end decision procedure that either proves serializability with a certificate or exposes a counterexample trace by reducing the problem to Petri-net reachability and semilinear constraints, with practical optimizations to manage the inherent Ackermann-complete hardness. The Ser toolchain translates SER programs into NS, then into Petri nets, and uses a reachability engine to produce proofs or counterexamples; optimizations like bidirectional slicing and semilinear pruning dramatically improve scalability. Empirical evaluation on a rich benchmark suite— including stateful firewalls and BGP routing models—demonstrates the framework’s ability to handle non-trivial real-world-like programs, offering a first-end-to-end, certificate-generating verifier for unbounded serializability in networked systems.

Abstract

We present the SER modeling language for automatically verifying serializability of concurrent programs, i.e., whether every concurrent execution of the program is equivalent to some serial execution. SER programs are suitably restricted to make this problem decidable, while still allowing for an unbounded number of concurrent threads of execution, each potentially running for an unbounded number of steps. Building on prior theoretical results, we give the first automated end-to-end decision procedure that either proves serializability by producing a checkable certificate, or refutes it by producing a counterexample trace. We also present a network-system abstraction to which SER programs compile. Our decision procedure then reduces serializability in this setting to a Petri net reachability query. Furthermore, in order to scale, we curtail the search space via multiple optimizations, including Petri net slicing, semilinear-set compression, and Presburger-formula manipulation. We extensively evaluate our framework and show that, despite the theoretical hardness of the problem, it can successfully handle various models of real-world programs, including stateful firewalls, BGP routers, and more.
Paper Structure (48 sections, 5 theorems, 50 equations, 16 figures, 7 tables)

This paper contains 48 sections, 5 theorems, 50 equations, 16 figures, 7 tables.

Table of Contents

  1. Introduction
  2. Problem Definition
  3. Background
  4. The SER Language
  5. Network System
  6. Translating SER Programs to Network Systems
  7. Formal Results
  8. The Algorithm (without Optimizations)
  9. Optimizations
  10. Implementation
  11. Code Architecture
  12. Benchmark Overview
  13. Evaluation
  14. Related Work
  15. Discussion
  16. ...and 33 more sections

Key Result

theorem thmcountertheorem

Let $N = (P, T, \mathsf{pre}, \mathsf{post}, M_0)$ be a Petri net and $S$ a target set. Let $N' = (P',T',\,\mathsf{pre}|_{P'\times T'},\,\mathsf{post}|_{P'\times T'},\,M_0|_{P'})$ be the sliced net. Then $S$ is reachable from $N$ iff it is reachable from $N'$.

Figures (16)

  • Figure 1: The network system for Listing \ref{['lst:MotivatingExample2NonSer']}. Local states show the variable assignments (yellow rectangles ) and the remaining code; edges indicate transitions of global states (blue rectangles ). Requests and responses appear as $\blacklozenge$ (green) and $\blacklozenge$ (red) diamonds, respectively. From left to right: ${\color{ForestGreen}\blacklozenge_{\text{main}}}$ spawns a request with [y=0] and the full program; after yielding, $\delta$ steps with global state [X=1] and local state [y=0], then updates y based on the global value, returning it as the final response (either $\blacklozenge_0$ or $\blacklozenge_1$).
  • Figure 2: Serial NFA of Listing \ref{['lst:MotivatingExample2NonSer']}.
  • Figure 3: The PN encoding interleaved executions of the program in Listing \ref{['lst:MotivatingExample2NonSer']}.
  • Figure 4: Full program flow (simplified, without backward arrows to the NS level).
  • Figure 5: Two routing policies.
  • ...and 11 more figures

Theorems & Definitions (13)

  • theorem thmcountertheorem: Bidirectional Slicing Soundness
  • proof
  • proof
  • definition thmcounterdefinition: Forward Over-Approximation
  • definition thmcounterdefinition: Backward Over-Approximation
  • definition thmcounterdefinition: Sliced Net
  • definition thmcounterdefinition: Witnessable Place
  • theorem thmcountertheorem: Slicing Invariant
  • proof
  • corollary thmcountercorollary
  • ...and 3 more