Verification of an Incremental Garbage Collector in Hoare-Style Logic

Many of the current software systems rely on garbage collectors for automatic memory management. This is also the case for various software systems in real-time appli-cations. However, a real-time application often requires an incremental working style of the underlying garbage collection, which renders the garbage collector more complex and less trustworthy. We present a formal veriˉcation of the Yuasa incremental garbage collector in Hoare-style logic. The speciˉcation and proof of the collector are built on a concrete machine model and cover detailed behaviors of the collector which may lead to safety prob- lems but are often ignored in high-level veriˉcations. The work is fully implemented with the Coq proof assistant and can be packed as foundational proof-carrying-code packages.Our work makes an important step toward providing high-assurance garbage collection for mission-critical real-time systems.     

A Structured Temporal Logic Language:XYZ/SE

In order to enhance the readability and to simplify the verification of temporal logic programs in the XYZ system,we propose a structured temporal logic language called XYZ/SE,based on XYZ/BE which is the basis language of the XYZ system.A set of proof rules are given and proved to be sound and adequate for proving the partial correctness of XYZ/SE programs in a compositional way.Moreover,we show that every XYZ/BE program can be transformed into an equivalent XYZ/SE program.So we have developed a general conpositional verification method in the XYZ system concerning the sequential case.     

A Shape Graph Logic and A Shape System

Analysis and verification of pointer programs are still difficult problems so far. This paper uses a shape graph logic and a shape system to solve these problems in two stages. First, shape graphs at every program point are constructed using an analysis tool. Then, they are used to support the verification of other properties （e.g., orderedness）. Our prototype supports automatic verification of programs manipulating complex data structures such as splay trees, treaps, AVL trees and AA trees, etc. The proposed shape graph logic, as an extension to Hoare logic, uses shape graphs directly as assertions. It can be used in the analysis and verification of programs manipulating mutable data structures. The benefit using shape graphs as assertions is that it is convenient for acquiring the relations between pointers in the verification stage. The proposed shape system requires programmers to provide lightweight shape declarations in recursive structure type declarations. It can help rule out programs that construct shapes deviating from what programmers expect （reflected in shape declarations） in the analysis stage. As a benefit, programmers need not provide specifications （e.g., pre-/post-conditions, loop invariants） about pointers. Moreover, we present a method doing verification in the second stage using traditional Hoare logic rules directly by eliminating aliasing with the aid of shape graphs. Thus, verification conditions could be discharged by general theorem provers.     

构造类型论与计算机程序设计

Recent years,in the area of computer programming language theories,automated deduction,and more generalized area of logic and computing,a lot of systems based on constructive type theory are used widely to design type system for computer programming languages,to do formal system develpment and verification,and to be used as foundation of mathematics and computing.constructive type theory provides computer scientists with a framework to combine logic and computer program design in an elegant and flexible way.In this paper,the evolvement of constructive type theory is first introduced.The several foundations of type theory are then discussed,together with analysis of the relationships between them.The relation between constructive type theory and computer programming is explored in-depth.In the last,Martin Lof‘‘‘‘s intuitionistic type theory is used as an example to demonstrate how to do program development and verification in the same formal system.     

Program Constructionby Verifying Specification

A program construction method based on Gamma language is proposed.The problem to be solved is specified by first-order predicate logic and a semantic verification program is constructed directly from the specification.Ways for improving efficiency of the program are also studied.The method differs from the one proposed by Manna and Waldinger,where a program is extracted from the proof of the existence of an object meeting the given specification.On the other hand,it also differs from the classical one used for deriving Gamma programs of Banatre and Le metayes,which consists in decomposing the specification into an invariant and a termination conditon.     

On Local Stratifiability of Logic Prograns and Databases

In this paper,we deal with the problem of verifying local stratifiability of logic programs and databases presented by Przymusinski.Necessary and sufficient condition for the local stratifiability of logic programs are presented and algorithms of performing the verification are developed.Finally,we prove that a database D B containing clauses with disjunctive consequents can be easily converted into a logic program P such that D B is locally statified iff P is locally stratified.     

FC-normal and extended stratified logic program

This paper investigates the consistency property of FC-normal logic program and presents an equivalent deciding condition whether a logic program P is an FC-normal program. The deciding condition describes the characterizations of FC-normal program. By the Petri-net presentation of a logic program, the characterizations of stratification of FC-normal program are investigated. The stratification of FC-normal program motivates us to introduce a new kind of stratification, extended stratification, over logic program. It is shown that an extended (locally) stratified logic program is an FC-normal program. Thus, an extended (locally) stratified logic program has at least one stable model. Finally, we have presented algorithms about computation of consistency property and a few equivalent deciding methods of the finite FC-normal program.     

Verification of Authentication Protocols for Epistemic Goals via SAT Compilation

This paper introduces a new methodology for epistemic logic, to analyze communication protocols that uses knowledge structures, a specific form of Kripke semantics over hostile networks. The paper particularly focuses on automatic verification of authentication protocols. Our approach is based on the actual definitions of a protocol, not on some difficultto-establish justifications. The proposed methodology is different from many previous approaches to automatic verification of security protocols in that it is justification-oriented instead of falsification-oriented, i.e., finding bugs in a protocol. The main idea is based on observations： separating a principal executing a run of protocol from the role in the protocol, and inferring a principal＇s knowledge from the local observations of the principal. And we show analytically and empirically that this model can be easily reduced to Satisfiability （SAT） problem and efficiently implemented by a modern SAT solver.     

An Introduction to IN CAPS System

INCAPS，a subsystem of XYZ system,is an INteractive Computer-Assisted Proving System,The primary targets to develop it range from proving temporal logic formal theorem to verifying XYZ/SE program‘s correctness which are supported respectively by the mechanized logics-FOTL logic and Hoare-like proof system.This paper discusses five main topics concerning INCAPS system:the rules,implementation,tactics,forward proof and backward proof.It also gives several typical examples for demonstration of INCAPS‘ working principle.The achievement to data in that we have now accomplished successfully the verification of the hierarchical specification of AB protocol and the correctness of XYZ/SE program.     

Symmetric structure in logic programming

It is argued that some symmetric structure in logic programs could be taken into account when implementing semantics in logic programming. This may enhance the declarative ability or expressive power of the semantics. The work presented here may be seen as representative examples along this line. The focus is on the derivation of negative information and some other classic semantic issues. We first define a permutation group associated with a given logic program. Since usually the canonical models used to reflect the common sense or intended meaning are minimal or completed models of the program, we expose the relationships between minimal models and completed models of the original program and its so-called G-reduced form newly-derived via the permutation group defined. By means of this G-reduced form, we introduce a rule to assume negative information termed G-CWA, which is actually a generalization of the GCWA. We also develop the notions of G-definite, G-hierarchical and G-stratified logic programs,     

A mechanically verified incremental garbage collector

As an application of a system designed for concurrent program verification, we describe a formalisation and mechanical proof of the correctness of Ben-Ari's incremental garbage collection algorithm. The proof system is based on the Manna-Pnueli model of concurrency and is implemented as an extension of the Boyer-Moore prover. The correctness of the garbage collector is represented by two theorems, stating a) that nothing except garbage is ever collected (safety), and b) that all garbage is eventually collected (liveness). We compare our mechanised treatment with several published proofs of the same results.     

基于隔离逻辑的并行程序可靠性验证方法

并行程序验证的复杂性在于执行流程的不确定性以及由此导致的执行规模变大,使得验证的内容和目标之间的关系不明确。为解决该问题,提出一种基于隔离逻辑的并行程序可靠性验证方法。通过变量的执行关系图,描述变量相关的语句及执行关系,将所需验证的程序性质逻辑式转换为变量并行语句序列的逻辑组合式,使得性质表达式与并发程序的语句相关联。根据逻辑组合式确定语句执行序列和前后件逻辑表达式,基于并发隔离逻辑的公理系统对语句执行序列进行验证,并根据验证结果对并发程序进行修改和完善。通过对银行柜台业务办理的功能模块验证结果表明该方法是有效的。     

基于插桩和布尔逻辑的运行时程序验证框架

针对软件测试和静态程序验证中存在的连续性程序执行验证和推理问题,提出一个基于程序插桩和布尔逻辑的运行时程序验证框架——RPA。定义一种用于描述运行时程序性质和规范的动态逻辑语言RPAL,实现自动化插桩以收集运行时程序状态信息,设计一个支持高效验证的句子调度算法。实验结果表明,结合合适的谓词扩展,RPA可以有效地验证和分析软件逻辑,发现潜在的软件错误。     

A multicomputer garbage collector for a single-assignment language

An asynchronous garbage collector for a message-passing multiprocessor (multicomputer) is described. This combines Weighted Reference Counting (WRC) interprocessor collection and tracing intraprocessor collection to permit individual processors to reclaim local storage independently. A novel feature is the integration of Weighted Reference Counting collection and the communication algorithms required to support a global address space in a single assignment language. This significantly reduces communication overhead and space requirements attributable to garbage collection. In addition, techniques are described that avoid the creation of cyclic structures that cannot be reclaimed using WRC. Experimental studies performed in a concurrent logic programming system that incorporates the collector confirm its efficiency and the benefits of integrating garbage collector and language implementation.     

基于分离逻辑的程序验证研究综述

上世纪60-70年代以来,虽然有Floyd-Hoare逻辑的出现,但是使用形式化工具对命令式程序的正确性和可靠性进行自动验证一直被认为是极具挑战性、神圣不可及的工作.上世纪末由于更多的科研投入,特别是微软、IBM等大型公司研发部门的大量人力物力的投入,程序验证方面在本世纪初取得了不少进展,例如用于验证空客代码无运行时错误的ASTRÉE工具,用于Windows设备驱动里关于过程调用的协议验证的SLAM工具.但这些工具并没有考虑动态创建的堆（Heap）：ASTRÉE工具假设待验证代码没有动态创建的堆,也没有递归;SLAM假设待验证系统已经有了内存安全性.事实上很多重要的程序,例如Linux内核、Apache、操作系统设备驱动程序等等,都涉及到对动态创建堆的操作.如何对这类操作堆的程序（heap-manipulating programs）进行自动验证仍然是个难题.2001-2002年分离逻辑（separation logic）提出后,其分离（separation）思想和相应的框（frame）规则使得局部推理（local reasoning）可以很好地应用到程序验证中.自2004年以来,基于分离逻辑对操作动态创建堆的程序进行自动验证方面的研究有了很大的进展,取得了很多令人瞩目的成果,例如SpaceInvader/Abductor、Slayer、HIP/SLEEK、CSL等工作.本文将着重对这方面的部分重要工作进行阐述.     

基于智能指针的垃圾收集器的研究与实现

内存泄漏是软件开发过程中最令人棘手的问题之一。通常,使用垃圾收集机制自动进行内存管理,以减轻程序员的负担。通过研究智能指针以及现有垃圾收集机制的工作原理,本文首先设计出一个基于c＋＋智能指针的垃圾收集器。实验结果表明,该垃圾收集器不仅满足了应用程序的要求,且具有良好的可扩展性。对于使用c＋＋等保守式程序设计语言进行大型软件的开发而言,该垃圾收集器具有一定的理论价值和实用价值。     

步进索引模型下的语义及其形式化

霍尔逻辑作为计算机程序的逻辑基础,可以用于描述一般程序的验证.分离逻辑作为霍尔逻辑的扩展,可以支持很多现代程序语言中的高阶特性.步进索引模型被用于定义自递归谓词.步进索引逻辑被广泛应用于各种基于交互式定理证明器的程序验证工具中,然而,基于步进索引逻辑的推理却比经典逻辑复杂、繁琐.事实上,也可以在步进索引模型上定义更加简洁清晰的、与“步数”无关的经典逻辑体系下的非步进索引程序语义.人们希望找到步进索引逻辑和非步进索引逻辑之间的关系,但发现两种逻辑并不等价.对实际的程序验证工作中涉及的命题进行归纳总结,找出它们共同的特征,给出关于程序状态的断言的约束条件;分别定义步进索引逻辑和非步进索引逻辑体系中断言的语义,并证明在该约束条件下两种语义的等价性;在Coq中,形式化以上所有定义和证明;最后,对未来值得关注的研究方向进行初步探讨.     

一个Windows应用程序的垃圾回收器

为减少长期运行的Windows应用程序持续堆内存泄漏而造成的系统性能损失,设计并实现了一个运行时自动垃圾回收器RT-AGC。RT-AGC采用传统Mark—Sweep算法的一个变种,对回收触发条件进行改进,使其具有更大的灵活性。利用Windows下应用程序的存储结构和系统API函数,通过扫描可能存储指针变量的区域,RT—AGC可以在应用程序运行时检测并处理内存泄漏,而不需要对目标应用程序重新编译或链接。文中描述了所采用的关键算法流程和主要实现技术,并编写了测试程序对RT—AGC的回收效果进行验证。实验证明可以有效地抑制应用程序的内存泄漏。     

Yama: a scalable generational garbage collector for Java in multiprocessor systems

The current state-of-the-art generational garbage collector pauses all the program threads when it performs young and old generation garbage collection. As the number of program threads increases, the delay due to garbage collection also increases, thus restricting the scalability of the collector. In order to improve the scalability and reduce the pause time, an on-the-fly generational garbage collector called Yama is proposed for multiprocessor systems. This uses the on-the-fly deferred reference counting in the young generation and the DLG (Doligez Leroy Gonthier) on-the-fly mark and sweep garbage collector in the old generation. We have proposed and experimented with two novel variations of the on-the-fly deferred reference counting called Chitragupt1 and Chitragupt2 in the young generation. Yama does not pause all the application threads simultaneously. An adaptive tenuring policy based on object reference count and survival rate is also proposed. Yama has been implemented in the IBM Jikes RVM (research virtual machine). The above claims are supported with experimental results for standard benchmark programs. The results show that Yama has an extremely low pause time in both the young and the old generation. The pause time reduction results in better response times for the user programs.