PaperlayerView exact revision on arXiv

Source-linked AI summary

Amortised Resource Analysis with Separation Logic

Robert Atkey

arXiv:1104.1998v2cs.LO

TL;DR

Resource analysis for functional programs has been successful, but this paper brings amortised resource reasoning to imperative pointer-manipulating programs. It combines heap-shape assertions with consumable-resource assertions and formalises a sound program logic with automated inference. The authors demonstrate the approach on pointer-manipulating examples and conclude that it extends Separation Logic’s local reasoning to consumable resources.

  • Problem

    The paper addresses how to specify and verify resource-consuming pointer-manipulating programs by combining amortised analysis with heap-shape reasoning.

    Source: §1 · p. 1

  • Method

    The logic combines Separation Logic assertions about mutable heap structure with assertions about consumable resources, and its verification procedure uses proof search and linear programming to infer resource annotations.

    Source: §1 · p. 2, §5 · p. 23

  • Results

    The authors present a sound program logic that connects data-structure shape to processing resources and demonstrate it on resource-consuming pointer-manipulating examples.

    Source: §7 · pp. 30–31

  • Takeaways & Limitations

    The approach extends Separation Logic’s local reasoning principle from mutable heap resources to consumable resources such as time.

    Source: §7 · pp. 30–31

    Automated proof search supports only bounds linear in the sizes of lists in a procedure’s precondition; the program logic itself is not subject to this limitation.

    Source: §7 · p. 31

Abstract

from arXiv · show

Type-based amortised resource analysis following Hofmann and Jost---where resources are associated with individual elements of data structures and doled out to the programmer under a linear typing discipline---have been successful in providing concrete resource bounds for functional programs, with good support for inference. In this work we translate the idea of amortised resource analysis to imperative pointer-manipulating languages by embedding a logic of resources, based on the affine intuitionistic Logic of Bunched Implications, within Separation Logic. The Separation Logic component allows us to assert the presence and shape of mutable data structures on the heap, while the resource component allows us to state the consumable resources associated with each member of the structure. We present the logic on a small imperative language, based on Java bytecode, with procedures and mutable heap. We have formalised the logic and its soundness property within the Coq proof assistant and extracted a certified verification condition generator. We also describe an proof search procedure that allows generated verification conditions to be discharged while using linear programming to infer consumable resource annotations. We demonstrate the logic on some examples, including proving the termination of in-place list reversal on lists with cyclic tails.

1. Introduction

The paper combines amortised resource analysis with Separation Logic to reason about consumable resources alongside mutable heap structure. Its contributions include a sound program logic, automated resource inference, and examples of complex pointer manipulation and termination proofs.

1. Introduction

  • Amortised credits for later operations are combined with Separation Logic to specify and verify resource-consuming pointer-manipulating programs.The logic combines mutable heaps with consumable resources, extending Separation Logic beyond reasoning about heap mutation alone.Source: §1 · pp. 1–2
  • The logic bounds execution by requiring consumed resources plus resources still available to stay within a predefined bound at every state.A variant logic also permits dynamic but fallible resource acquisition.Source: §1 · p. 2
  • Interweaving resource assertions with heap-shape predicates lets specifications express resource amounts through data-structure shape rather than size or contents.For lists, the available resource is linearly proportional to list length without arithmetic reasoning about lengths.Source: §1 · pp. 2–3

1.1. Contributions.

  • The program logic mixes heap-shape and future-resource assertions, and its soundness proof is formalised in Coq.The assertion logic combines Boolean Bunched Implications, pointer primitives, and affine intuitionistic Bunched Implications for consumable resources.Source: §1.1 · p. 3
  • Automated proof search discharges verification conditions and uses linear programming to infer resource annotations, including from shape-only loop invariants.Examples demonstrate resource-aware specifications, complex pointer manipulation, and termination proofs for cyclic heap structures.Source: §1.1 · p. 3

1.2. Differences to previously published versions.

  • This revised and expanded version adds dynamic resource acquisition, more shape-resource predicates and discussion, refined proof-search material, and a merge-sort example.The merge-sort example came from an invited TGC 2010 paper.Source: §1.2 · pp. 3–4

2. Motivating Examples

The examples use functional queues and an in-place linked-list merge-sort loop to show how amortised resource accounting can simplify specifications and pointer-manipulation verification compared with a global ghost counter.

2.1. Functional Queues.

  • A global resource counter would expose both queue-list lengths in operation specifications, while the original dequeue specifications complicate client reasoning.The dequeue cases distinguish whether the head list is empty or has an element.Source: §2.1 · pp. 4–5
  • For functional queues, storing resources on tail-list elements pays for reversal and yields simpler operation specifications than separate empty- and nonempty-dequeue cases.Enqueue stores resource for a future reversal; dequeue uses that resource if reversal is needed.Source: §2.1 · p. 5

2.2. Merge-sort Inner Loop.

  • The merge-sort inner loop processes two length-k sublists at a time, counts swaps at a designated branch, and is called log2 n times with doubling k for a full sort.The method steps through the list 2*k elements at a time.Source: §2.2 · pp. 5, 7
  • Its invariants distinguish the first outer-loop iteration from later ones and track resources on processed and pending list segments.A safety precondition prevents a null-pointer exception; the resource amounts are inferred by a linear solver.Source: §2.2 · pp. 7–8
  • The advance helper splits off up to k nodes; a separate method permits modular frame-rule reasoning, while its resource annotation must be preserved explicitly.The implementation uses a separate method because its JVM-like bytecode cannot easily apply the frame rule to the loop.Source: §2.2 · pp. 7–8
  • The inferred merge-sort annotations assign one resource per input-list element, leave processed segments without resources, and preserve resources on pending segments.The solution gives x = 1, y = 0, o2 = o4 = 1, a0 = 1, and i2 = 1, with the other listed annotations zero.Source: §2.2 · p. 8

2.2.1. Comparisons to other techniques.

  • SPEED handles heap-based structures only through abstract interfaces, while COSTA cannot handle the example’s shared heap pointers.SPEED’s interface specifications record effects on structure size; COSTA counts the longest path from a reference.Source: §2.2.1 · pp. 8–9
  • The amortised approach uses Separation Logic’s shape reasoning to account for resources locally, avoiding arithmetic links between whole-list sizes and consumption.The authors note that loop invariants may be supplied by other tools, with resource variables inserted automatically.Source: §2.2.1 · pp. 8–9

3. A Program Logic for Heap and Resources

The section develops a program logic for heaps and consumable resources and establishes its soundness for a Java-bytecode-like machine. It also addresses resource bounds and fallible dynamic resource acquisition, illustrating the latter with permission-controlled SMS sending.

3.3. Assertions.

  • The logic treats assertions as predicates over heaps and remaining resources, with procedure preconditions, postconditions, and instruction-level assertions supporting safe execution.Procedure specifications use an environment type for universally quantified variables; intermediate assertions specify sufficient preconditions for an instruction and its successors.Source: §3 · p. 9, §3.3 · p. 13

3.1. Semantic Domains.

  • Heaps are finite partial maps, while consumable resources form an ordered monoid whose ordering permits assertions to require more resources than execution needs.The resource model includes a single consumable resource or multisets of independently consumable named resources.Source: §3.1 · pp. 9–10

3.2. A Little Virtual Machine.

  • The machine is a stack-based virtual machine like Java bytecode, with mutable heap and procedures; its state tracks the heap, activation frames, and resources consumed so far.The heap and resource operational semantics record the resource consumed by each step.Source: §3.2 · pp. 10, 12

3.4. Program Logic.

  • The program logic assigns assertions to instructions, checks both conditional outcomes, and requires available heap or resources for mutation or consumption.Calls split the heap and resources between callee and caller, while return requirements derive from the procedure postcondition.Source: §3.4 · pp. 13–14

3.5. Soundness.

  • Every virtual-machine step preserves a safety invariant, and the logic’s soundness results are mechanically verified in Coq.The preservation results include locality: a mutating step leaves an unmentioned disjoint heap portion unaffected.Source: §3 · p. 9, §3.5 · pp. 14–15
  • Although mutating steps are local and calls apply framing implicitly, the logic lacks an explicit frame rule for modular reasoning inside procedures, which may hinder procedures with multiple loops.A hierarchical structure over bytecode could enable frame rules and local reasoning within procedures.Source: §3.5 · p. 15
  • Soundness guarantees that a program respects its fixed resource bound at every execution step and halts with its consumed resource within that bound.The theorem also guarantees a postcondition and identifies resources remaining at termination.Source: §3.5 · pp. 16–17
  • Soundness does not require a commutative resource monoid, but a usable mixed commutative/non-commutative proof theory is difficult, and resource acquisition requires commutativity.Source: §3.5 · p. 17

3.6. Allowing for Resource Acquisition.

  • The acquisition variant permits fallible, dynamically sized requests: successful acquire adds the named resource, failed requests add none, and only success can raise the bound.Its soundness theorem guarantees that the dynamic resource bound is respected throughout execution and at termination.Source: §3.6 · pp. 17–19

3.7. Resource Acquisition Example.

  • In the SMS example, permission is requested in advance; a list node carries sending permission when its permission field is 1, and carries none when it is 0.The resource logic ensures that messages are sent only to numbers for which permission has been obtained.Source: §3.7 · pp. 19–20

4. Deep Assertion Logic

The assertion logic combines boolean BI for heap descriptions with affine intuitionistic BI for consumable resources. Its inductive predicates associate resources locally with data-structure nodes, while resource separation can also share a heap view—with a soundness caveat.

4. Deep Assertion Logic

  • The logic combines boolean BI for describing heaps with affine intuitionistic BI for consumable resources.This provides a syntax for assertions in the program logic.Source: §4 · p. 20

4.1. Syntax and Semantics.

  • The resource-only assertions form an affine intuitionistic BI sub-logic, as established by Proposition 4.1.This follows from the resource ordering and the chosen semantics of emp, separating conjunction, and magic wand.Source: §4.1 · p. 21

4.2. Inductively Defined Shape and Resource Predicates.

  • Resource-aware inductive predicates associate consumable resources with nodes in lists, and can extend to doubly-linked lists and trees.The paper also describes polynomially proportional list resources and annotations conditional on node data.Source: §4.2 · pp. 21–22

4.3. Heap and Resource Separation.

  • A resource-frame rule can share a heap while separating resource views, but soundness requires preserving the heap shape that carries those associations.The logic cannot currently enforce that a procedure avoids heap modifications that violate the resource associations.Source: §4.3 · p. 23

5. Automated Verification

The paper automates verification using restricted assertions, backward verification-condition generation, and proof search that generates linear constraints for resource inference. The proof search is terminating and sound, while the VC-generation approach can grow exponentially with program size.

5. Automated Verification

  • The VC-generate-and-solve approach can have exponential blow-up in program size.The paper notes that forward symbolic execution may prune unreachable paths and merge similar feasible paths using heuristics.Source: §5 · p. 23

5.1. Restricted Assertion Logic.

  • The restricted assertion syntax represents pure facts, heap assertions, and resource amounts separately, making proof search practical.Resource amounts are linear expressions over globally existentially quantified meta-variables.Source: §5.1 · pp. 23–24

5.2. Verification Condition Generation.

  • Verification conditions are generated backwards using weakest liberal preconditions, with loop invariants required at backward-jump targets.The method produces a VC for the procedure precondition and one for each annotated instruction.Source: §5.2 · p. 24

5.3. Proof Search.

  • Proof search adds linear constraints to resource matching obligations, which a linear solver can use to infer resource annotations.The solver also requires positive variables and minimizes variables appearing in the precondition.Source: §5.3 · pp. 25, 28
  • Proof search terminates and is sound with respect to the assertion logic.The verification-condition generator is formalised and proved sound in Coq, then extracted and instantiated with the proof-search logic.Source: §5.2 · p. 25, §5.3 · p. 28

6. Examples of Automated Verification

The automated procedure inferred resource annotations on small examples and handled in-place reversal of lists with cyclic tails. In the latter example, the inferred resources decrease to zero and verify termination with a loop-count bound tied to input shape.

6.1. Small Examples.

  • Small examples used seeded heap-shape loop invariants while the tool inferred resource bounds, including for recursive tree procedures.The procedure also verifies memory safety; the reported example timings were trivial, but real-world scalability remains untested.Source: §6.1 · pp. 28–29
  • The authors report potential exponential blow-up in generated formula size, leaving scalability to real-world code uncertain.They suggest a forward symbolic-execution approach as a likely direction for a more realistic implementation.Source: §6.1 · p. 29

6.2. Frying Pan List Reversal.

  • The inferred annotations verify termination of cyclic-tail list reversal and bound loop executions in terms of input shape.The handle receives two resource units per node for its two passes, while the pan receives one per node; resources are consumed until they reach zero.Source: §6.2 · pp. 29–30

7. Conclusions

The logic extends Separation Logic’s local reasoning from mutable resources such as the heap to consumable resources such as time. It connects data-structure shape with resource requirements and supports automated inference, with the current procedure limited to linear bounds in list size.

7. Conclusions

  • The logic extends Separation Logic’s local reasoning to consumable resources and connects data-structure shape with the resources needed to process it.This lets specifications express resources associated with structure members.Source: §7 · pp. 30–31
  • The automated proof procedure infers consumable resource annotations from shape-invariant programs, but supports only bounds linear in the size of precondition lists.The authors distinguish this automation limit from the program logic, and report promising initial experiments toward polynomial inference using potential lists.Source: §7 · p. 31
  • Mixed shape and resource assertions simplify resource specifications, a benefit the authors expect could extend to proof-search extensions or interactive systems.The paper also notes that Aspinall et al. use a layered logic for reasoning about Hofmann-Jost system output.Source: §7 · p. 31
  • Future work includes studying assertion-logics’ expressiveness for resource magnitudes and the proof theory of the combined Boolean and affine intuitionistic BI.The authors conjecture their deep assertion logic with lseg can express resources linear in heap size.Source: §7 · p. 31
  • The authors identify numerical-bound loops as a capability their current prototype lacks while investigating extensions for non-linear and numerically driven bounds.The cited alternative inference procedures handle non-linear bounds, but the passage notes their approach to heap structures can add specification complexity.Source: §7 · p. 31
Loading 1104.1998v2…