Higher order data types

We consider a generalization of the concept of abstract data type suitable for modeling situations in which there is more than one level of functionality. An instance of such a situation is the difference in level of functionality between the query and update functions in a data base. We introduce the concept of a higher order data type to model this idea. The underlying algebraic ideas are outlined, and sample applications of the concept are presented.This work was partially supported by a research grant from the National Research Council of Canada.This work was partially supported by the Conselho Nacional de Desenvolvimento Cientifico e Tecnológico (CNPq; Brazil).     

Replicated abstract data types: Building blocks for collaborative applications

For distributed applications requiring collaboration, responsive and transparent interactivity is highly desired. Though such interactivity can be achieved with optimistic replication, maintaining replica consistency is difficult. To support efficient implementations of collaborative applications, this paper extends a few representative abstract data types (ADTs), such as arrays, hash tables, and growable arrays (or linked lists), into replicated abstract data types (RADTs). In RADTs, a shared ADT is replicated and modified with optimistic operations. Operation commutativity and precedence transitivity are two principles enabling RADTs to maintain consistency despite different execution orders. Especially, replicated growable arrays (RGAs) support insertion/deletion/update operations. Over previous approaches to the optimistic insertion and deletion, RGAs show significant improvement in performance, scalability, and reliability.     

Verifying abstract data types with SNOBOL4

The presentation of an abstract data type by a series of equational axioms has become an accepted specification mechanism. Verifying the correctness of such specifications has been recognized as a problem troubling their use. A means is presented for experimenting with a directly executable version of the axioms without having to choose representations for the data structures or describe algorithms for the operations.     

Fault-tolerant atomic computations in an object-based distributed system

A distributed system can support fault-tolerant applications by replicating data and computation at nodes that have independent failure modes. We present a scheme called parallel execution threads (PET) which can be used to implement fault-tolerant computations in an object-based distributed system. In a system that replicates objects, the PET scheme can be used to replicate a computation by creating a number of parallel threads which execute with different replicas of the invoked objects. A computation can be completed successfully if at least one thread does not encounter any failed nodes and its completion preserves the consistency of the objects. The PET scheme can tolerate failures that occur during the execution of the computation as long as all threads are not affected by the failures. We present the algorithms required to implement the PET scheme and also address some performance issues. Mustaque Ahamad received his B.E. (Hons.) degree in Electrical Engineering from the Birla Institute of Technology and Science, Pilani, India. He obtained his M.S. and Ph.D. degrees in Computer Science from the State University of New York at Stony Brook in 1983 and 1985 respectively. Since September 1985, he is an Assistant Professor in the School of Information and Computer Science at the Georgia Institute of Technology, Atlanta. His research interests include distributed operating systems, distributed algorithms, faulttolerant systems and performance evaluation. Partha Dasgupta is an Assistant Professor at Georgia Tech since 1984. He has a Ph.D. in Computer Science from the State University of New York at Stony Brook. He is the technical project director of the Clouds distributed operating systems project, as well as a coprincipal investigator of Georgia Tech's NSF-CER award. His research interests include building distributed operating systems, distributed algorithms, fault-tolerant systems and distributed programming support. Richard J. LeBlanc, Jr. received the B.S. degree in physics from Louisiana State University in 1972 and the M.S. and Ph.D. degrees in computer sciences from the University of Wisconsin-Madison in 1974 and 1977, respectively. He is currently a Professor in the School of Information and Computer Science of the Georgia Institute of Technology. His research interests include programming language design and implementation, programming environments, and software engineering. Dr. LeBlanc's current research work involves application of these interests in distributed processing systems. As co-director of the Clouds Project, he is studying language concepts and software engineering methodology for utilizing a highly reliable, object-based distributed system. He is also interested in specification-based software development methodologies and tools. Dr. LeBlanc is a member of the Association for Computing Machinery, the IEEE Computer Society and Sigma Xi.This work was supported in part by NSF grants CCR-8619886 and CCR-8806358, and RADC contract number F30602-86-C-0032     

Type-Safe Code Transformations in Haskell

The use of typed intermediate languages can significantly increase the reliability of a compiler. By type-checking the code produced at each transformation stage, one can identify bugs in the compiler that would otherwise be much harder to find. We propose to take the use of types in compilation a step further by verifying that the transformation itself is type correct, in the sense that it is impossible that it produces an ill typed term given a well typed term as input.We base our approach on higher-order abstract syntax (HOAS), a representation of programs where variables in the object language are represented by meta-variables. We use a representation that accounts for the object language's type system using generalized algebraic data types (GADTs). In this way, the full binding and type structure of the object language is exposed to the host language's type system. In this setting we encode a type preservation property of a CPS conversion in Haskell's type system, using witnesses of a type correctness proof encoded in a GADT.     

Methodical specification of abstract data types via rewriting systems

A data type is often given by an informal model. Its formal specification is an important task, but also difficult and error-prone. Here a methodology for this task is presented. Its steps are, first, the election of a canonical form defining a canonical term algebra; second, a system of sound rewriting rules powerful enough to achieve the syntactical transformations of the canonical term algebra. The final translation of rewriting rules into equations is immediate. The methodology is illustrated by the detailed presentation of a simple example.Research partly sponsored by FINEP, CNPq and the French Ministry for Foreign Affairs.     

移动Agent的一种支持安全与容错的迁移机制

移动Agent计算模式将成为未来网络计算的主流模式。移动Agent的迁移机制是其技术核心之一,受到了广泛的关注。为了提高移动Agent迁移的可靠性和安全性,提出一种支持安全与容错的迁移机制。该机制利用结构化迁移机制寻址,并引入分布式事务、可靠认证与加密等机制,使得移动Agent在迁移过程中能有效保护主机与移动Agent的安全性,并提供容错支持。     

Simple algebraic data types for C

Adt is a simple tool in the spirit of Lex and Yacc that makes monomorphic algebraic data types, polymorphic built‐in types like the list and an efficient form of pattern matching available in C programs. C programs built with ADTs typically use NULL pointers only to indicate don't care values, and not as sentinels. This reduces the scope for errors involving NULL pointers. The Adt tool generates runtime checks, which catch many of the remaining NULL pointer dereferences. The runtime checks may consume a significant amount of CPU time; hence they can be switched off once the program is suitably debugged. Copyright © 2011 John Wiley & Sons, Ltd.     

基于逻辑程序的安全协议验证

安全协议本质上是分布式并发程序,可以自然地描述为多个子进程的并发合成系统．将安全协议对应的并发合成系统抽象为逻辑程序进行消解,能够对安全协议无穷多个会话的交叠运行进行验证．该文提出了安全协议逻辑程序中逻辑规则的一个分类方法,基于该分类方法提出了安全协议逻辑程序不动点的迭代计算方法．逻辑规则的分类优化了安全协议逻辑程序不动点的迭代计算和安全性质验证过程中的计算．由于安全协议逻辑程序不动点迭代计算过程不一定终止,文中提出了每进行k≥1步安全协议逻辑程序不动点迭代计算验证一次安全性质的验证策略．     

抽象解释及其应用研究进展

抽象解释是一种对用于形式描述复杂系统行为的数学结构进行抽象和近似并推导或验证其性质的理论. 抽象解释自20世纪70年代提出以来,在语义模型、程序分析验证、混成系统验证、程序转换、系统生物学模型分析等领域取得了广泛应用. 近年来,抽象解释在程序分析、神经网络验证、完备性推理、抽象域改进等方面取得较大进展. 基于此,系统综述了抽象解释及其应用的研究进展. 首先概述了抽象解释理论的基本概念,介绍了抽象解释理论、抽象域的研究进展;然后概述了基于抽象解释的程序分析方面的研究进展; 之后概述了基于抽象解释的神经网络模型验证、神经网络模型鲁棒训练、深度学习程序的分析等方面的研究进展;又对抽象解释在智能合约可信保证、信息安全保证、量子计算可信保证等方面的应用进展进行了介绍;最后指明了抽象解释未来可能的研究方向.

     

Verifying Contextual Refinement with Ownership Transfer

Contextual refinement is a compositional approach to compositional verification of concurrent objects.There has been much work designing program logics to prove the contextual refinement between the object implementation and its abstract specification.However,these program logics for contextual refinement verification cannot support objects with resource ownership transfer,which is a common pattern in many concurrent objects,such as the memory management module in OS kernels,which transfers the allocated memory block between the object and clients.In this paper,we propose a new approach to give abstract and implementation independent specifications to concurrent objects with ownership transfer.We also design a program logic to verify contextual refinement of concurrent objects w.r.t.their abstract specifications.We have successfully applied our logic to verifying an implementation of the memory management module,where the implementation is an appropriately simplified version of the original version from a real-world preemptive OS kernel.     

Verifying the determinant in parallel

In this paper, we investigate the complexity of verifying problems whose computation is equivalent to the determinant, both in the Boolean arithmetic circuit and in the Boolean circuit model. We observe that for a few problems, there exists an easy (NC ¹) verification algorithm. To characterize the harder ones, we define the class of problems that are reducible to the verification of the determinant, under two different reductions, and establish a list of complete problems in these classes. In particular, we prove that computing the rank is equivalent under AC ⁰ reductions to verifying the determinant. We show in the Boolean case that none of the complete problems can be recognized in NC ¹ unless L = NL. On the other hand, we show that for functions, there exists an NC ¹ checker even if they are hard to verify, and that they can be extended into functions whose verification is easy. received 24 August 1995     

Dynamic Partitioning in Linear Relation Analysis: Application to the Verification of Reactive Systems

We apply linear relation analysis (P. Cousot and N. Halbwachs, in 5th ACM Symposium on Principles of Programming Languages, POPL'78, Tucson (Arizona), January 1978; N. Halbwachs, Y.E. Proy, and P. Roumanoff, Formal Methods in System Design, Vol. 11, No. 2, pp. 157–185, 1997) to the verification of declarative synchronous programs (N. Halbwachs, Science of Computer Programming, Special Issue on SAS'94, Vol. 31, No. 1, 1998). In this approach, state partitioning plays an important role: on one hand the precision of the results highly depends on the fineness of the partitioning; on the other hand, a too much detailed partitioning may result in an exponential explosion of the analysis. In this paper, we propose to dynamically select a suitable partitioning according to the property to be proved. The presented approach is quite general and can be applied to other abstract interpretations.     

通过抽象程序证明复杂具体程序

本文描述了证明抽象程序和具体程序满足一致性关系的方法.抽象程序使用抽象数据结构（ADTs）如set、list、map及其上的操作.具体程序使用类C语言中的类型.抽象程序和具体程序一致性证明需要用户给出抽象变量和具体变量的关系,抽象程序程序点和具体程序程序点的对应关系.基于对应关系,抽象程序和具体程序一致性证明可以分解,从而容易并可能自动证明.     

Verifying Time Partitioning in the DEOS Scheduling Kernel

This paper describes an experiment to use the Spin model checking system to support automated verification of time partitioning in the Honeywell DEOS real-time scheduling kernel. The goal of the experiment was to investigate whether model checking with minimal abstraction could be used to find a subtle implementation error that was originally discovered and fixed during the standard formal review process. The experiment involved translating a core slice of the DEOS scheduling kernel from C++ into Promela, constructing an abstract “test-driver” environment and carefully introducing several abstractions into the system to support verification. Attempted verification of several properties related to time-partitioning led to the rediscovery of the known error in the implementation. The case study indicated several limitations in existing tools to support model checking of software. The most difficult task in the original DEOS experiment was constructing an adequate environment to close the system for verification. The fidelity of the environment was of crucial importance for achieving meaningful results during model checking. In this paper, we describe the initial environment modeling effort and a follow-on experiment with using semi-automated environment generation methods. Program abstraction techniques were also critical for enabling verification of DEOS. We describe an implementation scheme for predicate abstraction, an approach based on abstract interpretation, which was developed to support DEOS verification.