面向OCaml的自动资源边界分析
编程语言
2016-11-03 v1
摘要
本文提出了一个针对OCaml程序的资源分析系统。该系统自动推导具有用户定义归纳类型的高阶多态程序的最坏情况资源边界。该技术在资源上是参数化的，可以推导时间、内存分配和能量使用的边界。推导出的边界是多元资源多项式，它们是依赖于标准OCaml类型的不同大小参数的函数。边界推断是完全自动的，并被归约为一个线性优化问题，传递给现成的LP求解器。从技术上讲，该分析系统基于一种新颖的多元自动摊销资源分析(AARA)。它建立在现有针对具有用户定义归纳类型的高阶程序的线性AARA工作，以及针对具有内置列表和二叉树的一阶程序的多元AARA工作之上。首次能够自动推导高阶函数的多项式边界以及依赖于用户定义归纳类型的多项式边界。此外，该分析处理带有副作用的程序，甚至优于先前系统的线性边界推断。同时，它保留了现有AARA技术的表达能力和效率。该分析系统的实用性通过一种实现以及与Inria的OCaml编译器的集成得到展示。该实现用于自动推导来自OCaml库、CompCert编译器和教科书算法实现的411个函数和6018行代码的资源边界。在一个案例研究中，该系统推断OCaml程序发送给DynamoDB(一个商业NoSQL云数据库服务)的查询次数的边界。
引用
@article{arxiv.1611.00692,
title = {Towards Automatic Resource Bound Analysis for OCaml},
author = {Jan Hoffmann and Ankush Das and Shu-Chun Weng},
journal= {arXiv preprint arXiv:1611.00692},
year = {2016}
}
备注
74 pages, technical report, short version accepted at POPL 2017