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.     

Path Dependent Analysis of Logic Programs

This paper presents an abstract semantics that uses information about execution paths to improve precision of data flow analyses of logic programs. The abstract semantics is illustrated by abstracting execution paths using call strings of fixed length and the last transfer of control. Abstract domains that have been developed for logic program analyses can be used with the new abstract semantics without modification.     

Maximally Concurrent Programs

Typically, program design involves constructing a program P that implements a given specification S; that is, the set ${\overline P}$ of executions of P is a subset of the set ${\overline S}$ of executions satisfying S. In many cases, we seek a program P that not only implements S, but for which ${\overline P}$ = ${\overline S}$. Then, every execution satisfying the specification is a possible execution of the program; we then call P maximal for the specification S. We argue that maximality is an important criterion in the context of designing concurrent programs because it disallows implementations that do not exhibit enough concurrency. In addition, a maximal solution can serve as a basis for deriving a variety of implementations, each appropriate for execution on a specific computing platform. This paper also describes a method for proving the maximality of a program with respect to a given specification. Even though we prove facts about possible executions of programs, there is no need to appeal to branching time logics; we employ a fragment of linear temporal logic for our proofs. The method results in concise proofs of maximality for several non-trivial examples. The method may also serve as a guide in constructing maximal programs. Received September 1997 / Accepted in revised form May 2000     

并发Java程序动态分析及重演技术研究

Java语言在并发程序方面的广泛应用对软件测试提出了新的挑战。众所周知,由于并发程序的不确定性,使得并发程序的设计、开发、调试和测试都非常困难。文章介绍了Safepro／Java中的多线程测试技术,通过对Java源程序进行适当的修改并且保持语义不变,跟踪并发Java程序的运行过程,收集有关数据并对数据进行分析,最终控制并发Java程序的重演。     

Properties of Concurrent Programs

A program property is a predicate on programs. In this paper we explore program properties for safety, progress and parallel composition, of the form U ? V where U and V are either predicates on states of a program or program properties, and ? satisfies three rules that are also enjoyed by implication. We show how such properties can be used to reason about concurrent programs. Our motivation is to explore methods of reasoning based on a very small number of widely-known rules.     

The Evolution of Concurrent Programs

Process algebra are formal languages used for the rigorous specification and analysis of concurrent systems. By using a process algebra as the target language of a genetic programming system, the derivation of concurrent programs satisfying given problem specifications is possible. A genetic programming system based on Koza's model has been implemented. The target language used is Milner's CCS process algebra, and is chosen for its conciseness and simplicity. The genetic programming environment needs a few adaptations to the computational characteristics of concurrent programs. In particular, means for efficiently controlling the exponentially large computation spaces that are common with process algebra must be addressed. Experimental runs of the system successfully evolved a number of non–iterative CCS systems, hence proving the potential of evolutionary approaches to concurrent system development.     

A Polymorphic Type Dependency Analysis for Logic Programs

An analysis is presented that infers polymorphic type dependencies in logic programs. Using set union as a type constructor and non-deterministic type definitions, the analysis infers more precise information than previous type dependency inference analyses. The analysis is an abstract interpretation based on the S-semantics and derives success patterns for each predicate in the program.     

Updating Epistemic Logic Programs

We consider the problem of updating non-monotonic knowledgebases represented by epistemic logic programs where disjunctiveinformation and notions of knowledge and belief can be explicitlyexpressed. We propose a formulation for epistemic logic programupdate based on a principle called minimal change and maximalcoherence. The central feature of our approach is that duringan update or a sequence of updates, contradictory informationis removed on a basis of minimal change under the semanticsof epistemic logic programs and then coherent information ismaximally retained in the update result. Through various updatescenarios, we show that our approach provides both semanticand syntactic characterizations for an update problem. We alsoinvestigate essential semantic properties of epistemic logicprogram update.     

Strict completion of Logic Programs

The paper presents a new approach to the problem of completeness of the SLDNF-resolution. We propose a different reference theory that we call strict completion. This new concept of completion (comp^*(P)) is based on a program transformation that given any program transforms it into a strict one (with the same computational behaviour) and the usual notion of program completion. We consider it a reasonable reference theory to discuss program semantics and completeness results. The standard 2-valued logic is used. The new comp^*(P) is always consistent and the completeness of all allowed programs and goals w.r.t. comp^*(P) is proved.     

Bounded Nondeterminism of Logic Programs

We introduce the notion of bounded nondeterminism for logic programs and queries. A program and a query have bounded nondeterminism if there are finitely many refutations for them via any selection rule. We offer a declarative characterization of the class of programs and queries that have bounded nondeterminism by defining bounded programs and queries. The characterization is provided in terms of Herbrand interpretations and level mappings, in the style of existing characterizations of universal termination. A direct application of the theoretical framework is concerned with the automatic generation of a terminating control. We present a transformational approach that given a bounded program and a bounded query yields a terminating program and query with the same set of refutations. Concerning the issue of automating the approach, by means of an example we sketch how an automatic method for proving left termination can be adapted to the purpose of inferring boundedness. Such an adaption reveals that the method does not scale up to medium/large sized programs due to scarce modularity of the required proof obligations. We provide then a modular refinement of boundedness for the significant class of well-moded programs and queries.     

并发程序的切片模型检验方法

提出了一种对并发程序进行切片以缩减模型检验状态空间的方法,首先针对并发程序中的同步与通信定义了一组依赖关系,包括并发分支与接合．非确定性,信道,共享变量等特征,对于从要验证的时态逻辑性质中提取的关于多个程序点的切片标准,文中给出算法根据相应的依赖关系通过不动点运算得到并发程序切片,可以证明得到的切片与原程序对于该性质具有相同的可满足性。     

Error Detection in Concurrent Java Programs

Concurrency in multithreaded programs introduces additional complexity in software verification and testing, and thereby significantly increases the cost of Quality Assurance (QA). We present a case study in which a specialized model checker was used to discover concurrency errors in a large preexisting code base. The results revealed race conditions that lead to data corruption errors whose detection would have been prohibitively expensive with conventional testing and QA methods. We describe our methodology and highlight parts of the methodology that could be automated.     

逻辑程序的事实维护

事实是逻辑程序的重要组成部分,事实维护影响着整个逻辑程序的一致性和完整性,并能够促进和完善规则维护。论文在分析了人工进行维护操作的弊端后,对事实维护中可能出现的情况进行分类分析,提出了事实维护系统的框架,重点描述了预警检测子系统所扮演的核心作用。     

一种基于依赖分析的并发程序潜在死锁检测算法

死锁是并发程序特有的一种运行时错误,由于并发程序在执行时的不确定性,死锁的检测和定位是非常困难的.本文提出了一种基于依赖分析的并发程序潜在死锁检测算法,该算法是一种静态分析算法,能检测并发程序中是否存在潜在死锁,并能定位死锁发生时各线程可能被挂起的语句节点.本文给出了算法的形式化定义和时间复杂度分析,实验测试结果表明算法是正确且有效的.     

Logic Programs with Ordered Disjunction

Logic programs with ordered disjunction (LPODs) contain a new connective which allows representing alternative, ranked options for problem solutions in the heads of rules: A × B intuitively means that if possible A , but if A is not possible, then at least B . The semantics of logic programs with ordered disjunction is based on a preference relation on answer sets. We show how LPODs can be implemented using answer set solvers for normal programs. The implementation is based on a generator, which produces candidate answer sets and a tester which checks whether a given candidate is maximally preferred and produces a better candidate if it is not. We also discuss the complexity of reasoning tasks based on LPODs and possible applications.