Functional Differentiation of Computer Programs

We present a purely functional implementation of the computational differentiation tools—the well known numeric (i.e., not symbolic) techniques which permit one to compute point-wise derivatives of functions defined by computer programs economically and exactly (with machine precision). We show how the use of lazy evaluation permits a transparent and elegant construction of the entire infinite tower of derivatives of higher order for any expressions present in the program. The formalism may be useful in various problems of scientific computing which often demand a hard and ungracious human preprocessing before writing the final code. Some concrete examples are given.     

面向收敛的并发程序执行轨迹静态简化方法

轨迹静态简化技术是在确保与原轨迹等价的前提下,通过随机减少程序执行时线程切换的数量,达到提高程序员调试并发程序效率的目的.然而,轨迹中可减少的线程切换分布往往是不均匀的,因此,随机简化策略难以有效地发现可简化的线程切换.为此,本文提出面向收敛的合并算法致力于这个问题.该算法基本思想是不断地随机选择一线程执行区间作为中心,在同一线程内,采用面向收敛的合并算法迭代地寻找可与其合并的前置执行区间和后置执行区间.实验证明,本文提出的方法可以高品质地减少执行轨迹中的线程切换数量,进而有助于程序员快速发现引发错误的线程交错。     

基于事件结构的并发程序可视化调试方法

在多核和并发技术得到广泛应用的今天,如何有效地调试并发程序,成为一个重要且亟待解决的研究课题.并发程序的不确定性及其行为的复杂性,使得传统的调试技术难以得到有效的应用;而软件维护场景中错误发现与错误调试过程的分离使得错误重现难以实现,面向缺陷报告的调试需求使得自动的错误定位技术难以应用,加剧了调试的困难.针对软件维护阶段由缺陷报告导向的程序调试场景,提出了可视化的并发程序调试方法.该方法能够根据缺陷报告中的信息对程序进行切片,缩小需要分析的代码范围;通过静态分析构造出程序行为的全局视图,帮助程序员发现隐含的程序执行路径;根据事件结构的语义简化程序行为视图,使得行为模型规模可控;根据图形中的分支,引导用户关注路径中的关键操作,从而更快地发现程序中的缺陷.与动态调试方法相比,该方法能够避免错误重现的代价.借助缺陷报告中的信息以及事件结构模型的特点,该方法能够尽量减少状态爆炸的发生.已开发出的交互式并发程序调试工具原型JESVis Debugger,初步实现了所提出的方法.     

Automated Fault Localization for C Programs

If a program does not fulfill a given specification, a model checker delivers a counterexample, a run which demonstrates the wrong behavior. Even with a counterexample, locating the actual fault in the source code is often a difficult task for the verification engineer.We present an automatic approach for fault localization in C programs. The method is based on model checking and reports only components that can be changed such that the difference between actual and intended behavior of the example is removed. To identify these components, we use the bounded model checker CBMC on an instrumented version of the program. We present experimental data that supports the applicability of our approach.     

A Two-Valued Logic for Properties of Strict Functional Programs Allowing Partial Functions

A typed program logic LMF for recursive specification and verification is presented. It comprises a strict functional programming language with polymorphic and recursively defined partial functions and polymorphic data types. The logic is two-valued with the equality symbol as only predicate. Quantifiers range over the values, which permits inductive proofs of properties. The semantics is based on a contextual (observational) semantics, which gives a consistent presentation of higher-order functions. Our analysis also sheds new light on the the role of partial functions and loose specifications. It is also an analysis of influence of extensions of programs on the tautologies. The main result is that universally quantified equations are conservative, which is also the base for several other conservative classes of formulas.     

Functional programming languages for verification tools: a comparison of Standard ML and Haskell

We compare Haskell with Standard ML as programming languages for verification tools based on our experience developing the verification platform Truth in Haskell and the Edinburgh Concurrency Workbench (CWB) in Standard ML. We review not only technical language features but also the worlds of the languages, for example, the availability of compilers, tools, and libraries. We also discuss the merits and difficulties of comparing programming languages in this wide sense and support our view that Truth and the CWB are similar enough to justify the conclusions drawn in this paper.     

一种基于变异分析的BPEL程序故障定位技术

不同于传统C,C++或Java程序,BPEL(Business Process Execution Language)程序由一组活动及其之间的交互组成,同时引入了并发、序列化、XML表示等新特征,这些新特点使得定位BPEL程序的故障具有一定的挑战性.针对现有故障定位技术在有效性方面的不足,提出一种基于变异分析的BPEL...     

Dynamic Query-Based Debugging of Object-Oriented Programs

Program errors are hard to find because of the cause-effect gap between the instant when an error occurs and when the error becomes apparent to the programmer. Although debugging techniques such as conditional and data breakpoints help in finding errors in simple cases, they fail to effectively bridge the cause-effect gap in many situations. This paper proposes two debuggers that provide programmers with an instant error alert by continuously checking inter-object relationships while the debugged program is running. We call such tool a dynamic query-based debugger. To speed up dynamic query evaluation, our debugger implemented in portable Java uses a combination of program instrumentation, load-time code generation, query optimization, and incremental reevaluation. Experiments and a query cost model show that selection queries are efficient in most cases, while more costly join queries are practical when query evaluations are infrequent or query domains are small. To enable query-based debugging in the middle of program execution in a portable way, our debugger performs efficient Java class file instrumentation. We call such debugger an on-the-fly debugger. Though the on-the-fly debugger has a higher overhead than a dynamic query-based debugger, it offers additional interactive power and flexibility while maintaining complete portability.     

多核处理器并行程序的确定性重放研究

多核处理器并行程序的确定性重放是实现并行程序调试的有效手段,对并行编程有重要意义。但由于多核架构下存在共享访存不同步问题,并行程序确定性重放的研究依然面临多方面的挑战,给并行程序的调试带来很大困难,严重影响了多核架构下并行程序的普及和发展。分析了多核处理器造成并行程序确定性重放难以实现的关键因素,总结了确定性重放的评价指标,综述了近年来学术界对并行程序确定性重放的研究。根据总结的评价指标,从纯软件方式和硬件支持方式对目前的确定性重放方法进行了分析与对比,并在此基础上对多核架构下并行程序的确定性重放未来的研究趋势和应用前景进行了展望。     

Relative Debugging of Automatically Parallelized Programs

We describe a system that simplifies the process of debugging programs produced by computer-aided parallelization tools. The system uses relative debugging techniques to compare serial and parallel executions in order to show where the computations begin to differ. If the original serial code is correct, errors due to parallelization will be isolated by the comparison.One of the primary goals of the system is to minimize the effort required of the user. To that end, the debugging system uses information produced by the parallelization tool to drive the comparison process. In particular, the debugging system relies on the parallelization tool to provide information about where variables may have been modified and how arrays are distributed across multiple processes. User effort is also reduced through the use of dynamic instrumentation. This allows us to modify the program execution without changing the way the user builds the executable. The use of dynamic instrumentation also permits us to compare the executions in a fine-grained fashion and only involve the debugger when a difference has been detected. This reduces the overhead of executing instrumentation.     

跨平台可移植远程并行程序调试器的设计与实现

介绍了一个跨平台远程并行程序调试器的设计与实现.该调试器实现了平台可移植和模块可移植,支持从Windows平台远程调试Unix/Linux平台PVM/MPI并行程序.与相关工作的比较显示,该调试器降低了开发并行程序的复杂度,提高了机群系统的使用效率,具有很好的实用价值.     

Kima: An Automated Error Correction System for Concurrent Logic Programs

We have implemented Kima, an automated error correction system for concurrent logic programs. Kima corrects near-misses such as wrong variable occurrences in the absence of explicit declarations of program properties.Strong moding/typing and constraint-based analysis are turning out to play fundamental roles in debugging concurrent logic programs as well as in establishing the consistency of communication protocols and data types. Mode/type analysis of Moded Flat GHC is a constraint satisfaction problem with many simple mode/type constraints, and can be solved efficiently. We proposed a simple and efficient technique which, given a non-well-moded/typed program, diagnoses the reasons of inconsistency by finding minimal inconsistent subsets of mode/type constraints. Since each constraint keeps track of the symbol occurrence in the program, a minimal subset also tells possible sources of program errors.Kima realizes automated correction by replacing symbol occurrences around the possible sources and recalculating modes and types of the rewritten programs systematically. As long as bugs are near-misses, Kima proposes a rather small number of alternatives that include an intended program. Search space is kept small because the minimal subset confines possible sources of errors in advance. This paper presents the basic algorithm and various optimization techniques implemented in Kima, and then discusses its effectiveness based on quantitative experiments.     

一种监测函数语义信息访存地址序列的方法

准确地获取应用程序在真实系统上运行的访存地址序列(traces)是进行内存系统调度及结构优化的基础.HMTT是自主研发的软硬件结合的内存监测分析系统,能够实时获取完整的全系统访存traces.但是得到的traces与应用程序上层事件之间存在语义鸿沟问题,比如上层函数执行流与访存traces的同步问题.针对该问题提出了一种软硬件结合获取包含函数级别语义信息访存traces的方法,软件方面通过二进制插桩的方式,直接修改内存中的进程映像,在目标函数的入口及出口各插入标记tag访存指令,进而能够被HMTT卡监测并识别.采用二进制插桩不需要程序的源代码,不需要对程序重新编译链接,而且引入的运行开销很小.实验表明采用软硬件结合的方式能够有效地获取包含函数级别语义信息的访存traces,对于SPECCPU2006中的访存密集型程序引入的性能开销只是原程序的62%,而使用Pin工具的纯软件方式获取访存traces将导致至少10.4倍的性能开销.     

Static and Dynamic Slicing of Constraint Logic Programs

Slicing is a program analysis technique originally developed for imperative languages. It facilitates understanding of data flow and debugging.This paper discusses slicing of Constraint Logic Programs. Constraint Logic Programming (CLP) is an emerging software technology with a growing number of applications. Data flow in constraint programs is not explicit, and for this reason the concepts of slice and the slicing techniques of imperative languages are not directly applicable.This paper formulates declarative notions of slice suitable for CLP. They provide a basis for defining slicing techniques (both dynamic and static) based on variable sharing. The techniques are further extended by using groundness information.A prototype dynamic slicer of CLP programs implementing the presented ideas is briefly described together with the results of some slicing experiments.     

基于模板匹配的BPEL程序故障修复及优化技术

BPEL (business process execution language)是一种可执行的Web服务组合语言. 与传统程序相比, BPEL程序在编程模型、执行方式等方面存在较大差异. 这些新特点使得如何定位并修改测试阶段发现的BPEL程序故障成为挑战, 面向传统软件的故障修复技术难以直接应用于BPEL程序. 从变异分析角度出发, 提出一种基于模板匹配的BPEL程序故障修复方法BPELRepair. 为了克服基于变异分析的故障修复技术计算开销高的缺点, 从补丁生成、测试用例选择以及终止条件3个角度提出多种优化策略. 开发一个BPEL故障修复支持工具, 提高故障修复的自动化程度与效率. 采用经验研究的方式, 评估所提故障修复技术及优化策略的有效性. 实验结果表明, 所提故障修复方法能够成功修复约53%的BPEL程序故障; 所提优化策略能够显著降低搜索匹配、补丁程序验证、测试用例执行与故障修复等方面的开销.     

Visualization Methods and Algorithms for Graph Representation of Functional Programs

Programming and Computer Software - This paper is devoted to the visualization of intermediate representations (the so-called IR graphs) of programs in the Cloud Sisal functional language for the...     

Comparing Parallel Functional Languages: Programming and Performance

This paper presents a practical evaluation and comparison of three state-of-the-art parallel functional languages. The evaluation is based on implementations of three typical symbolic computation programs, with performance measured on a Beowulf-class parallel architecture.We assess three mature parallel functional languages: PMLS, a system for implicitly parallel execution of ML programs; GPH, a mainly implicit parallel extension of Haskell; and Eden, a more explicit parallel extension of Haskell designed for both distributed and parallel execution. While all three languages employ a completely implicit approach to communication, each language takes a different approach to specifying and controlling parallelism, ranging from explicit identification of processes as language constructs (Eden) through annotation of potential parallelism (GPH) to automatic detection of parallel skeletons in sequential code (PMLS).We present detailed performance measurements of all three systems on a widely available parallel architecture: a Beowulf cluster of low-cost commodity workstations. We use three representative symbolic applications: a matrix multiplication algorithm, an exact linear system solver, and a simple ray-tracer. Our results show how moderate speedups can be achieved with little or no changes to the sequential code, and that parallel performance can be significantly improved even within our high-level model of parallel functional programming by controlling key aspects of the program such as load distribution and thread granularity.     

The Evaluation Dependence Tree as a Basis for Lazy Functional Debugging

Lazy functional languages are declarative and allow the programmer to write programs where operational issues such as the evaluation order are left implicit. This should be reflected in the design of debuggers for such languages to avoid burdening the programmer with operational details, e.g. concerning the actual evaluation order. Conventional debugging techniques tend to focus too much on operational aspects to be suitable in this context. A record of the execution that only captures the declarative aspects of the execution, leaving out operational details, would be a viable basis for debugging lazy functional programs. Various declarative debugging tools could then be developed on top of such records. In this paper we propose a structure which we call the Evaluation Dependence Tree (EDT) for this purpose, and we describe two different construction methods. Performance problems are discussed along with possible solutions.     

Abstract Correction of First-Order Functional Programs

DEBUSSY is an (abstract) declarative diagnosis tool for functional programs which are written in OBJ style. The tool does not require the user to either provide error symptoms in advance or answer any question concerning program correctness. In this paper, we formalize an inductive learning methodology for repairing program bugs in OBJ-like programs, which is based on the so-called example-guided unfolding[6]. Correct programs are synthesized by unfolding and removing rules of the faulty program. Rules to be unfolded (deleted) are selected according to the examples, which can be automatically generated as an outcome by the DEBUSSY diagnoser.