Cost Analysis for Import and Export Using an Abstract Machine

TL;DR

This paper introduces a formal abstract machine for JavaScript XML language, incorporating a cost model and a type system that over-approximates execution costs, with proofs of soundness and an implementation.

Contribution

It develops a novel cost-annotated abstract machine and a sound type system that over-approximates execution costs, including handling of unknowns from loops.

Findings

Type system soundly over-approximates program cost

Implementation demonstrates practical applicability

Formal proofs validate the approach

Abstract

This paper presents the syntax and reduction rules for an abstract machine based on the JavaScript XML language. We incorporate the notion of cost into our reduction rules, and create a type system that over-approximate this cost. This over-approximation results in an equation that may contain unknowns originating from while loops. We conclude with a formal proof of soundness of the type system for our abstract machine, demonstrating that it over-approximates the cost of any terminating program. An implementation of the type system, constraint gathering, and the abstract machine is also presented