PaperlayerView exact revision on arXiv

Source-linked AI summary

Algorithmic Verification of Single-Pass List Processing Programs

Rajeev Alur, Pavol Cerny

arXiv:1007.4958v2cs.PL

TL;DR

Single-pass list programs over data values pose a verification challenge, since classical one-way transducers cannot express even reversal. The paper introduces streaming data-string transducers and matching imperative and functional program classes. It shows that equivalence and pre/post-condition checking are in PSPACE and that these models support equivalence checking across programming styles.

  • Problem

    Classical one-way transducers cannot express reversal, while regular transductions are defined using two-way transducers, motivating a model for single-pass list programs.

    Source: §1 · p. 1

  • Method

    The paper models single-pass programs with transducers that scan tagged data strings left to right and identifies corresponding imperative and restricted-recursive functional program classes.

    Source: §1 · pp. 2–3

  • Results

    Equivalence and pre/post-condition checking for streaming transducers are in PSPACE, and the imperative and functional program classes correspond to the transducer model.

    Source: §1 · pp. 2–3

  • Takeaways & Limitations

    The results yield algorithms for checking equivalence between list-processing programs written in different styles, including commonly used routines.

    Source: §1 · p. 3, §7 · p. 28

    Streaming transducers cannot capture all linear-time streaming algorithms, including sorting data values and a two-head alternating merge of projections.

    Source: §2.5 · p. 8

Abstract

from arXiv · show

We introduce streaming data string transducers that map input data strings to output data strings in a single left-to-right pass in linear time. Data strings are (unbounded) sequences of data values, tagged with symbols from a finite set, over a potentially infinite data domain that supports only the operations of equality and ordering. The transducer uses a finite set of states, a finite set of variables ranging over the data domain, and a finite set of variables ranging over data strings. At every step, it can make decisions based on the next input symbol, updating its state, remembering the input data value in its data variables, and updating data-string variables by concatenating data-string variables and new symbols formed from data variables, while avoiding duplication. We establish that the problems of checking functional equivalence of two streaming transducers, and of checking whether a streaming transducer satisfies pre/post verification conditions specified by streaming acceptors over input/output data-strings, are in PSPACE. We identify a class of imperative and a class of functional programs, manipulating lists of data items, which can be effectively translated to streaming data-string transducers. The imperative programs dynamically modify a singly-linked heap by changing next-pointers of heap-nodes and by adding new nodes. The main restriction specifies how the next-pointers can be used for traversal. We also identify an expressively equivalent fragment of functional programs that traverse a list using syntactically restricted recursive calls. Our results lead to algorithms for assertion checking and for checking functional equivalence of two programs, written possibly in different programming styles, for commonly used routines such as insert, delete, and reverse.

1 Introduction

The paper introduces streaming data-string transducers as a model for single-pass programs on data sequences, then uses them to establish decidable verification and equivalence checks. It identifies corresponding imperative and functional list-processing classes, including programs that can be checked across programming styles.

1 Introduction

  • The transducer scans tagged data strings left to right in linear time, using equality and ordering tests over a potentially infinite data domain.It updates data-string variables by concatenation while preventing duplication of previously computed output.Source: §1 · p. 2
  • Equivalence and pre/post-condition checking for streaming transducers are in PSPACE, while several extensions make reachability undecidable.The checked preconditions and postconditions are expressed by streaming acceptors over data strings.Source: §1 · p. 2
  • The modeled list programs include insertion, deletion, membership, reversal, and sorting by tags, but not by data values.Their single-pass processing of the next list item at each step is the key restriction.Source: §1 · p. 2
  • A corresponding imperative class processes a heap-allocated input list in one pass, with traversal restricted to curr := curr.next from the input head.The programs can add nodes and modify node values and next-pointers.Source: §1 · pp. 2–3
  • The corresponding functional class traverses lists left to right through restricted recursive calls on the input tail, composing arguments and returned values without examining them.The imperative and functional classes can be translated to the same transducer model for semantic-equivalence checking.Source: §1 · p. 3

2 Streaming transducers

The section defines streaming transducers over tagged data strings and illustrates their expressive power and boundaries. It also describes streaming acceptors and properties of the transductions they recognize.

2.1 Data strings and transductions

  • A data string is a finite sequence of tagged values from a potentially infinite ordered domain, and a data transduction is a partial function between such strings.Examples include reversal, tag-based projection, deletion by matching values, and insertion into a sorted tail.Source: §2.1 · pp. 3–4

2.2 Transducer definition

  • An SDST reads tagged data strings left to right, using finite state, data variables, and copyless string updates to produce output in linear time.Data tests use ordering comparisons; copyless updates rearrange accumulated output chunks without duplication.Source: §2.2 · pp. 4–5, §2.5 · pp. 7–8

2.3 Examples

  • Reverse uses front insertion into one output variable, while tag-based projection accumulates private and public entries in separate variables before concatenating them.The sorted-tail insertion example outputs the head in its sorted position only when the tail is sorted.Source: §2.3 · pp. 5–7
  • F3, which deletes a private entry when a matching public entry occurs, is not streaming-regular because finitely many variables cannot test an unbounded set of data values.An SDST with k variables can effectively test only k data values at a step.Source: §2.3 · p. 6

2.4 Streaming acceptors

  • A streaming data-string acceptor is an SDST without data-string variables; sorted strings are streaming-regular, but strings without duplicates are not.Sortedness can be checked by retaining the previous data value; the duplicate-free language is excluded by an argument like that for F3.Source: §2.4 · p. 7

2.5 Properties

  • Streaming-regular transductions have output length O(|w|), run in O(|w|) time, and cannot introduce data values absent from the input.The output-length bound depends on copyless assignments, which also allow string variables stored as linked lists to be updated by changing a constant number of pointers.Source: §2.5 · pp. 7–8
  • The model excludes some linear-time streaming algorithms, including alternating merges of two tag-based projections, because those require multiple input read-heads.The traversal restriction is designed to ensure decidability of key analysis problems.Source: §2.5 · p. 8
  • Streaming-regular transductions are not generally closed under composition, though they are closed under conditional choice using a streaming-regular test; finite data domains restore composition closure.The paper's unbounded-domain counterexample composes reversal with repetition of the first value.Source: §2.5 · pp. 8–9

3 Imperative Programs Updating Linked Lists

The imperative fragment models single-pass processing of heap-allocated lists, restricting traversal to the unique input pointer while allowing pointer updates and new nodes. The paper translates these programs to streaming transducers and gives a translation back, linking heap-based routines to the transducer model.

3 Imperative Programs Updating Linked Lists

  • Only `curr := curr.next` may traverse the input; programs may update other nodes’ next-pointers only when those nodes differ from `curr`.The heap stores tagged data nodes, and programs can also create nodes and manipulate data, tag, Boolean, and pointer variables.Source: §3 · p. 9

3.2 Semantics

  • The operational semantics represents a heap using nodes, data and tag functions, and next-pointers; a finite execution returns the list reachable from the output reference, while nontermination or a cyclic output makes it undefined.The initial heap contains one node per input symbol, linked in input order.Source: §3.2 · pp. 12–13

3.3 Streaming transducers with ϵ-transitions

  • Allowing ε-transitions does not add expressive power: they can be eliminated while preserving the transduction and the numbers of states and variables.The extension is used in translating list-processing programs to transducers.Source: §3.3 · pp. 13–14

3.4 From single-pass programs to streaming transducers

  • Heap nodes at referenced pointers are stored explicitly, while uninterrupted heap segments are represented by data-string variables, with at most 2k − 1 segments for k references.The transducer’s finite-state control tracks the heap shape; when segments merge, their strings are concatenated.Source: §3.4 · p. 15
  • Every single-pass imperative program can be translated to an equivalent transducer with ε-transitions, and every such transducer has an equivalent single-pass list-processing program.For a program with m locations, kr references, kb Boolean variables, kt tag variables, and kd data variables, Proposition 6 gives the transducer’s variable counts and state bound.Source: §3.4 · pp. 15–16
  • The transducer simulates `curr := curr.next` as its input-consuming step; other program statements become ε-transitions that update stored control and heap information.The transition updates the pointer partition and heap shape, and appends the current input symbol to a string variable when needed.Source: §3.4 · p. 16

4 Functional programs on lists

The paper defines a syntactically restricted functional fragment for left-to-right list processing and shows how it relates to streaming transducers. Its restrictions include recursive calls on the input tail and controlled use of returned values, while still covering routines such as insert, delete, and reverse.

4 Functional programs on lists

  • The functional fragment captures left-to-right single-pass list processing and includes routines such as insert, delete, and reverse, with tail-recursive and non-tail-recursive forms.Callers may operate on returned values but may not test them.Source: §4 · p. 17
  • Recursive calls must process `tail l`, occur in a final caller expression, and obey restrictions on how list variables and returned values are used.The constraints include a copyless-style rule limiting where each list variable may appear and rules restricting which returned values may be used.Source: §4 · pp. 17–18

4.1 Examples

  • The fragment includes a non-tail-recursive delete function, and the paper’s construction supports checking it for semantic equivalence with an imperative Delete program.The recursive call can be wrapped in a list-construction operation, and the equivalence check can support verification using one program as the specification for the other.Source: §4.1 · pp. 18–19

4.2 From list processing functions to streaming transducers

  • Each single-pass functional program can be translated to an equivalent streaming transducer, with O(2^kb · |Σ|^kt) states, kd data variables, and kl + 1 data-string variables.Here kb, kt, kd, and kl count the recursive function’s Boolean, tag, data, and list variables, respectively.Source: §4.2 · p. 19
  • Conversely, each single-pass data-string transducer can be translated into an equivalent single-pass list-processing function.The construction encodes transducer state with Boolean arguments, data variables with data arguments, and data-string variables with list arguments.Source: §4.2 · pp. 19–20

5 Decision Problems

Streaming transducer equivalence and pre/post-condition checking are in PSPACE, using finite abstractions of data-variable order and equality. Several extensions, including two-way traversal and multiple traversal pointers, make reachability undecidable.

5.1 Sound and complete abstraction for order and equality

  • Defined data variables can be abstracted by their equality classes and the strict total order among those classes.The abstraction is intended to be sound and complete; its proof uses the infinite ordered domain's unbounded chains.Source: §5.1 · pp. 20–21

5 Decision Problems

  • Both streaming-transducer equivalence and pre/post-condition checking are in PSPACE.Pre/post checking also has a PSPACE algorithm for total correctness.Source: §5.2 · p. 22, §5.3 · p. 25

5.2 Equivalence checking

  • Equivalence checking reduces to 1-counter reachability, yielding a PSPACE bound that also applies to the corresponding list-processing programs.The construction tracks variable order and equality plus output-position information while simulating both transducers.Source: §5.2 · pp. 22, 24, 25

5.3 Checking pre/post conditions and assertions

  • Pre/post checking verifies that every output produced for an input accepted by the precondition is accepted by the postcondition.The framework also supports assertion checks such as program-location reachability and heap-cycle detection in PSPACE.Source: §5.3 · pp. 25–26

5.4 Undecidable extensions

  • Reachability becomes undecidable for two-way transducers, programs with multiple traversal pointers, and data-string variable equality.The reductions use two-counter automata for the first two extensions and Post’s correspondence problem for string-variable equality.Source: §5.4 · pp. 26–27

6 Related Work

Prior work studies list safety, concurrent list access, regular model checking, and shape analysis, but the approaches differ in scope and guarantees. The paper emphasizes complete verification and equivalence checking for its restricted single-pass class.

6 Related Work

  • Earlier list-safety results concern non-nested loops that do not modify the list, while this paper restricts traversal to one pointer and assumes an initially acyclic heap.The paper allows its analyses to detect cycles introduced during execution.Source: §6 · p. 27
  • Concurrent list-access work permits concurrency and nondeterminism but cannot express list reversal; its intricate restrictions motivated this study's automata-theoretic model.Source: §6 · p. 27
  • Regular model checking composes statement transducers, but reachable heaps need not form a regular language under unbounded union.For a program that outputs ww, the iterative fixpoint may not terminate; this paper's procedures do not compute the reachable-heap set.Source: §6 · pp. 27–28
  • Shape-analysis methods often compute heap invariants, whereas this approach claims sound and complete checks for its defined program class and also checks program equivalence.The comparison is to abstraction-based methods described as sound but not complete for safety properties.Source: §6 · p. 28

7 Conclusions

The paper presents streaming transducers as a model for single-pass list processing and uses them to check program equivalence. It identifies future theoretical work on bounded data domains, learning, and tree-structured data.

7 Conclusions

  • Streaming transducers provide a foundational model for single-pass list-processing programs and support equivalence checking across programming styles.The conclusion notes commonly used routines for processing list data items.Source: §7 · p. 28
  • Future directions include studying expressiveness over bounded data domains, learning streaming string transducers from examples, and extending the model to tree-structured data.The paper also reports that a subsequent paper established equivalence with two-way transducers and MSO-definable string transductions.Source: §7 · p. 28
Loading 1007.4958v2…