• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文OA文献 >Un marco unificado para análisis de recursos y tiempo de ejecución, validación dinámica y pruebas unitarias = a Unified Framework for Resource and Execution Time Analysis, Run-Time Checking and Unit-Testing
【2h】

Un marco unificado para análisis de recursos y tiempo de ejecución, validación dinámica y pruebas unitarias = a Unified Framework for Resource and Execution Time Analysis, Run-Time Checking and Unit-Testing

机译：资源和执行时间分析，运行时检查和单元测试的统一框架=资源和执行时间分析，运行时检查和单元测试的统一框架

页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Hemos desarrollado un marco general para inferir automáticamente cotas superiores e inferiores del uso que un programa lógico hace de los recursos en general, dadas como funciones de los tamaños de los datos de entrada. Este permite el tratamiento de recursos independientes de la plataforma (o definidos por el usuario/dependientes de la aplicación), tales como los bits enviados o recibidos por una aplicación a través de un socket, el número de llamadas a un predicado, archivos que se dejan abiertos, accesos a una base de datos, así como otros dependientes de la plataforma, como tiempo de ejecución o consumo de energía. El trabajo incluye un análisis global paramétrico respecto a los recursos y el tipo de aproximación (cotas superiores e inferiores). El usuario puede definir los parámetros del análisis para un recurso mediante aserciones, así como asociar costes a las operaciones básicas del programa que afectan el uso de dicho recurso. El análisis estático global infiere el uso del recurso para todas las partes del programa. Las aserciones pueden definirse a diferentes niveles de abstracción. Por ejemplo, pueden asociar funciones del uso de recursos para diferentes tipos de programas a nivel del código fuente y pueden describir también cómo se actualiza el valor de dichos recursos en las cabezas de los predicados o en la preparación de un literal en el cuerpo de dichos predicados. En este caso, el analizador usa una función de coste definida en la aserción para actualizar el uso del recurso mientras se analizan las cabezas de las cláusulas o los literales del cuerpo. Para los recursos dependientes de la plataforma, como el tiempo de ejecución, realizamos una única vez por plataforma un perfilado que calcula los parámetros asociados a operaciones básicas, a nivel de código fuente o byte- code. Hemos aplicado el marco general a tiempo de ejecución de dos maneras y experimentado con la información suministrada a nivel de fuente y de byte- code. En el primer enfoque, el análisis estático devuelve un vector de recursos independiente de la plataforma relacionado con las operaciones de bajo nivel de la ejecución del programa. Dichas operaciones deben verse reflejadas en el lenguaje de alto nivel. El perfilador calcula las constantes que aparecen en las funciones de recursos de la plataforma dada. A continuación usamos aserciones para definir el tiempo de ejecución como un recurso compuesto de los recursos independientes de la plataforma y los resultados del perfilado. En el segundo enfoque, en la etapa de perfilado se calculan las constantes y funciones que acotan el tiempo de ejecución de cada instrucción de la máquina abstracta. A continuación, en la etapa de estimación de recursos se emplea la información de dichos tiempos para inferir cotas del tiempo de ejecución dependientes de la plataforma. También el resultado puede mejorarse introduciendo aserciones a nivel de bytecode. Además, dado que no podemos verificar todas las propiedades estáticamente, presentamos un marco unificado para verificación estática, validación dinámica (o en tiempo de ejecución) y pruebas unitarias. Hemos diseñado métodos para compilar validaciones dinámicas de (parte de) las aserciones que no pueden ser verificadas estáticamente. Las pruebas unitarias permiten poner a prueba las validaciones dinámicas y (parte de) las pruebas verificadas estáticamente se eliminan. Además de las propiedades relacionadas con recursos, podemos tratar otras como la ausencia de fallo, el determinismo y las de estado (o funcionales) como los tipos de los argumentos de entrada/salida. Una contribución importante es que para todas las tareas hemos usado un lenguaje de aserciones unificado, el cual permite definir recursos y propiedades relacionadas y verificables con ayuda de los resultados del análisis que es lo suficientemente poderoso, general y extensible como para expresar una gran variedad de propiedades interesantes de los programas. Entre las aplicaciones del presente trabajo tenemos la verificación del consumo de recursos, depuración del rendimiento, certificación de propiedades para código móvil, control de granularidad en computación paralela/distribuida y especialización de programas orientada por los recursos. El marco para pruebas unitarias y en tiempo de ejecución se ha aplicado con éxito en la validación de la adecuación al estándar ISO-Prolog y en la detección de varios errores en el código fuente del sistema Ciao. El marco completo ha sido integrado con éxito en el sistema Ciao/CiaoPP. Abstract We have developed a general framework for automatically inferring both upper- and lower-bounds on the usage that a logic program makes of resources in general. Such bounds are given as functions of input data sizes. Our approach gives support for platform-independent (or user-de_ned/application- dependent) resources, such as bits sent or received by an application over a socket, number of calls to a predicate, number of _les left open, number of accesses to a database, as well as platform-dependent resources, such as execution time or energy. The framework includes a global analysis that is parametric with respect to resources and the type of approximation (lowerand upper-bounds). The user can de_ne the parameters of the analysis for a particular resource using assertions. It is also possible to associate basic cost functions with elementary program operations that a_ect the usage of such resource. Then, the global static analysis can infer the cost of all the procedures in the program. The assertions can be de_ned at di_erent abstraction levels. For example, they can associate resource usage functions to di_erent program constructs at source code level, can also describe how predicates update the value for those resources in the clause heads or in the preparation of the execution of its body literals. In such a case, a cost function de_ned in the assertion is used by the analyzer to update the resource usage when the clause heads or the body literals are analyzed. For platform-dependent resources (e.g., execution time) we perform a one-time pro_ling phase that computes parameters associated to basic operations, at source or bytecode-level. We have applied the general framework to execution time estimation in two ways and experimented with information supplied at source and bytecode-levels. In the _rst approach, the compiletime cost bounds analysis gives a vector of platform-independent resources that corresponds to particular low-level operations related to program execution. Such operations must be reected in the high-level language. The pro_ling phase determines the values of the constants appearing in the resource usage functions, for a given platform. Then, we use assertions to de_ne the platform-dependent resource (execution time) as a composition of the basic platform-independent resources and the values of the constants resulting from the pro_ling phase. In the second approach, the one-time pro- _ling stage calculates constants and functions bounding the execution time of each abstract machine instruction. Then, the compile-time resource usage estimation phase uses the instruction timing information (which is platformdependent) to infer bounds on execution time. To improve precision, resource usage assertions can also be given at bytecode level. Furthermore, since not all properties can be veri_ed statically, we have developed a framework that uni_es static veri_cation, run-time checking and unit testing. In that sense, we have designed methods for compiling run-time checks for (parts of) assertions which cannot be veri_ed at compile-time. Unit tests also provide test cases for the run-time checks, and (parts of) unit tests that can be veri_ed at compile-time are eliminated. In addition to those resource-related properties, we support other properties like non-failure, determinism and state (or functional) properties like types of input/output arguments on calls or successes. A key contribution of this work is that we preserve the use of a uni_ed assertion language for all tasks. Such language is used to de_ne resources and resource-related properties that can be veri_ed based on the results of the analysis and is powerful, general and extensible enough to express a large class of interesting properties. Applications of this work include resource usage veri_cation, performance debugging, certi_cation of resource usage properties in mobile code, resource and granularity control in parallel/distributed computing and resourceoriented specialization. The unit-testing and run-time checking framework has been e_ectively applied to the validation of ISO Prolog compliance and to the detection of di_erent types of bugs in the Ciao source. The overall uni_ed framework has been successfully integrated in the Ciao/CiaoPP system.
机译：我们已经开发了一个通用框架，可以根据逻辑程序对资源的使用情况自动推断出上限和下限，这是输入数据大小的函数。这允许处理平台无关（或用户定义/与应用程序相关）的资源，例如应用程序通过套接字发送或接收的位，对谓词的调用次数，它们保持开放状态，可以访问数据库以及平台的其他依赖项，例如运行时或功耗。该工作包括有关资源和近似类型（上限和下限）的全局参数分析。用户可以通过断言定义资源的分析参数，以及将成本与影响该资源使用的程序的基本操作相关联。全局静态分析可以推断程序所有部分的资源使用情况。可以在不同的抽象级别定义断言。例如，它们可以在源代码级别将资源使用的功能与不同类型的程序相关联，并且还可以描述谓词的头部或在所述主体的文本中的准备中如何更新所述资源的值。谓词。在这种情况下，解析器使用在断言中定义的代价函数来更新资源使用量，同时解析子句头或正文。对于与平台相关的资源（例如运行时），我们在每个平台上执行一次分析，以计算与源代码或字节码级别的基本操作相关的参数。我们以两种方式在运行时应用了通用框架，并尝试了在源代码和字节码级别提供的信息。在第一种方法中，静态分析返回与程序执行的低级操作有关的平台无关资源向量。这些操作必须以高级语言反映。探查器计算出现在给定平台的资源函数中的常数。然后，我们使用断言将运行时定义为由平台独立资源和分析结果组成的资源。在第二种方法中，在概要分析阶段，将计算限制抽象机每条指令执行时间的常数和函数。然后，在资源估计阶段，所述时间的信息用于推断平台相关的执行时间水平。通过在字节码级别引入断言也可以改善结果。另外，由于我们不能静态地验证所有属性，因此我们提供了一个用于静态验证，动态（或运行时）验证和单元测试的统一框架。我们设计了一些方法来编译无法静态验证的（部分）断言的动态验证。单元测试允许测试动态验证，并删除（部分）静态验证的测试。除了与资源相关的属性外，我们还可以处理其他属性，例如无故障，确定性和状态（或功能）属性，例如输入/输出参数类型。一个重要的贡献是，对于所有任务，我们都使用统一的断言语言，该语言使我们能够借助分析结果来定义相关且可验证的资源和属性，该功能强大，通用且可扩展，可以表达各种各样的程序的有趣特性。在这项工作的应用程序中，我们有资源消耗的验证，性能调试，移动代码属性的认证，并行/分布式计算中的粒度控制以及面向资源的程序专业化。运行时和单元测试框架已成功应用于验证是否符合ISO-Prolog标准以及检测Ciao系统源代码中的各种错误。完整的框架已成功集成到Ciao / CiaoPP系统中。摘要我们已经开发了一个通用框架，可以自动推断逻辑程序通常占用资源的上限和下限。这样的界限是作为输入数据大小的函数给出的。我们的方法支持与平台无关的（或用户定义的/与应用程序相关的）资源，例如应用程序通过套接字发送或接收的位，对谓词的调用次数，打开的_les数。，对数据库的访问次数以及与平台相关的资源，例如执行时间或能源。该框架包括一个针对资源和近似类型（下限和上限）进行参数化的全局分析。用户可以使用断言来定义特定资源的分析参数。也可以将基本成本函数与影响此类资源使用的基本程序操作相关联。然后，全局静态分析可以推断出程序中所有过程的成本。可以在不同的抽象级别定义断言。例如，它们可以在源代码级别将资源使用函数与不同的程序构造相关联，还可以描述谓词如何在子句标题中或在其主体文字的执行准备中更新这些资源的值。在这种情况下，当分析子句标题或正文文字时，分析器将使用断言中定义的成本函数来更新资源使用情况。对于平台相关的资源（例如执行时间），我们执行一次概要分析阶段，该阶段在源或字节码级别计算与基本操作相关的参数。我们已通过两种方式将通用框架应用于执行时间估计，并尝试了在源代码和字节码级别提供的信息。在第一种方法中，编译时成本边界分析提供了平台无关资源的向量，该资源与与程序执行相关的特定低级操作相对应。此类操作必须使用高级语言。对于给定的平台，配置阶段确定出现在资源使用函数中的常数的值。然后，我们使用断言来定义与平台无关的资源（执行时间），以作为与平台无关的基本资源以及由pro_ling阶段得出的常量值的组成。在第二种方法中，一次性配置阶段计算限制每个抽象机指令的执行时间的常量和函数。然后，编译时资源使用估计阶段使用指令时序信息（与平台有关）来推断执行时间的界限。为了提高精度，也可以在字节码级别给出资源使用声明。此外，由于并非所有属性都可以静态验证，因此我们开发了一个框架，可以统一进行静态验证，运行时检查和单元测试。从这个意义上讲，我们设计了用于编译（部分）断言的运行时检查的方法，这些断言在编译时无法验证。单元测试还提供了用于运行时检查的测试用例，并且消除了可以在编译时验证的（部分）单元测试。除了那些与资源相关的属性，我们还支持其他属性，例如非故障，确定性和状态（或功能）属性，例如调用或成功的输入/输出参数的类型。这项工作的主要贡献在于，我们在所有任务中都保留了统一的断言语言。这种语言用于定义可以基于分析结果进行验证的资源和与资源相关的属性，并且功能强大，通用且可扩展，足以表达一大类有趣的属性。这项工作的应用包括资源使用验证，性能调试，移动代码中资源使用属性的验证，并行/分布式计算中的资源和粒度控制以及面向资源的专业化。单元测试和运行时检查框架已有效地应用于ISO Prolog合规性验证以及Ciao源中各种错误类型的检测。整个统一框架已成功集成到Ciao / CiaoPP系统中。

著录项

  • 作者

    Mera Menéndez Edison Fernando;

  • 作者单位
  • 年度 2010
  • 总页数
  • 原文格式 PDF
  • 正文语种 {"code":"es","name":"Spanish","id":10}
  • 中图分类

相似文献

  • 外文文献
  • 中文文献
  • 专利

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号