检索结果-内蒙古大学图书馆

INTERNATIONAL JOURNAL OF COMPUTER & INFORMATION SCIENCES 1975年第2期4卷 105-132页

作者： HOARE, CAR QUEENS UNIV BELFAST DEPT COMP SCIBELFAST BT7 1NNNORTH IRELAND

The power and convenience of a programming language may be enhanced for certain applications by permitting treelike data structures to be defined by recursion. This paper suggests a pleasing notation by which such structures can be declared and processed; it gives the axioms which specify their properties, and suggests an efficient implementation method. It shows how a recursive data structure may be used to represent another data type, for example, a set. It then discusses two ways in which significant gains in efficiency can be made by selective updating of structures, and gives the relevant proof rules and hints for implementation. The examples show that a certain range of applications in symbol manipulation can be efficiently programmed without introducing the low-level concept of a reference into a high-level programming language.

关键词： axiomatic proof rules data representation data structures dynamic storage allocation pointers (abolition of) programming language design programming language features programming language implementation recursive data structures references (abolition of) symbol manipulation

来源：评论

学校读者我要写书评

暂无评论

Rewrite-Based Satisfiability Procedures for recursive data structures

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2007年第8期174卷 55-70页

作者： Bonacina, Maria Paola Echenim, Mnacho Univ Studi Verona Dipartimento Informat Verona Italy

If a rewrite-based inference system is guaranteed to terminate on the axioms of a theory T and any set of ground literals, then any theorem-proving strategy based on that inference system is a rewrite-based decision procedure for T-satisfiability. In this paper, we consider the class of theories defining recursive data structures, that might appear out of reach for this approach, because they are defined by an infinite set of axioms. We overcome this obstacle by designing a problem reduction that allows us to prove a general termination result for all these theories. We also show that the theorem-proving strategy decides satisfiability problems in any combination of these theories with other theories decided by the rewrite-based approach.

关键词： Rewrite-based inference systems recursive data structures

来源：评论

学校读者我要写书评

暂无评论

recursive data-structures IN APL

引用

COMMUNICATIONS OF THE ACM 1979年第2期22卷 79-96页

作者： GULL, WE JENKINS, MA QUEENS UNIV DEPT COMP & INFORMAT SCIKINGSTON K7L 3N6ONTARIOCANADA

Presents the mathematical study of approaches for defining nested arrays in APL, a computer program language. Discussion on the extension of data structure capability of APL; data structure of APL; Characteristics of ... 详细信息

关键词： APL arrays data-driven algorithms nested arrays recursive data structures theory of arrays trees

来源：评论

学校读者我要写书评

暂无评论

Decision procedures for term algebras with integer constraints

引用

INFORMATION AND COMPUTATION 2006年第10期204卷 1526-1574页

作者： Zhang, Ting Sipma, Henny B. Manna, Zohar Stanford Univ Dept Comp Sci Stanford CA 94305 USA

Term algebras can model recursive data structures which are widely used in programming languages. To verify programs we must be able to reason about these structures. However, as programming languages often involve multiple data domains, in program verification decision procedures for a single theory are usually not applicable. An important class of mixed constraints consists of combinations of data structures with integer constraints on the size of data structures. Such constraints can express memory safety properties such as absence of memory overflow and out-of-bound array access, which are crucial for program correctness. In this paper we extend the theory of term algebras with the length function which maps a term to its size, resulting in a combined theory of term algebras and Presburger arithmetic. This arithmetic extension provides a natural but tight coupling between the two theories, and hence the general purpose combination methods like Nelson-Oppen combination are not applicable. We present decision procedures for quantifier-free theories in structures with an infinite constant domain and with a finite constant domain. We also present a quantifier elimination procedure for the extended first-order theory that can remove a block of existential quantifiers in one step. (c) 2006 Elsevier Inc. All rights reserved.

关键词： decision-procedures recursive data structures term algebras Presburger arithmetic quantifier elimination combination of satisfiability procedures

来源：评论

学校读者我要写书评

暂无评论

Parallelizing graph construction operations in programs with cyclic graphs

引用

PARALLEL COMPUTING 2002年第9期28卷 1307-1328页

作者： Hwang, YS Natl Taiwan Ocean Univ Dept Comp Sci Chilung 20224 Taiwan

Pointer analysis has been an active research field in recent years. Combining pointer analysis and dependence analysis can identify parallelism in programs with pointers or graphs, which are in turn represented by dynamic pointer-linked data structures. After parallelism is identified, programs can be parallelized and then executed on parallel multiprocessor systems to achieve high performance. The compiler analysis techniques that have been proposed so far can only recognize parallelism in the traversal references of programs with cyclic graphs by analyzing the traversal patterns on graphs. Consequently, only the graph traversal operations will be parallelized while the graph construction operations will be left to be executed in sequential. Although this approach can usually parallelize the most time-consuming part of these programs (the graph traversal operations account for over 90% of total execution times in most programs), the rest of programs that accounts for less than 10% will dominate the execution on multiprocessor systems according to Amdahl's law. This paper presents a technique that can identify parallelism in the construction operations of programs even with cyclic graphs. This technique is designed to facilitate automatic parallelization of scientific computational applications that construct cyclic graphs to represent adjacent lists, which in turn describe the interactions of simulated objects. Experimental results show this approach can parallelize the construction phase of such programs and achieve good speedup on multiprocessor systems. (C) 2002 Elsevier Science B.V. All rights reserved.

关键词： parallelizing compilers recursive data structures cyclic graphs pointer analysis dependence analysis

来源：评论

学校读者我要写书评

暂无评论

High-Performance Derivative Computations using CoDiPack

引用

ACM TRANSACTIONS ON MATHEMATICAL SOFTWARE 2019年第4期45卷 1–26页

作者： Sagebaum, Max Albring, Tim Gauger, Nicolas R. TU Kaiserslautern Bldg 34Paul Ehrlich Str D-67663 Kaiserslautern Germany

There are several AD tools available that all implement different strategies for the reverse mode of AD. The most common strategies are primal value taping (implemented e.g. by ADOL-C) and Jacobian taping (implemented e.g. by Adept and dco/c++). Particulary for Jacobian taping, recent advances using expression templates make it very attractive for large scale software. However, the current implementations are either closed source or miss essential features and flexibility. Therefore, we present the new AD tool CoDiPack (Code Differentiation Package) in this paper. It is specifically designed for minimal memory consumption and optimal runtime, such that it can be used for the differentiation of large scale software. An essential part of the design of CoDiPack is the modular layout and the recursive data structures which not only allow the efficient implementation of the Jacobian taping approach but will also enable other approaches like the primal value taping or new research ideas. We will finally present the performance values of CoDiPack on a generic PDE example and on the SU2 code.

关键词： Algorithmic differentiation expression templates recursive data structures efficient implementation maintainable implementation

来源：评论

学校读者我要写书评

暂无评论

A framework to capture dynamic data structures in pointer-based codes

引用

IEEE TRANSACTIONS ON PARALLEL AND DISTRIBUTED SYSTEMS 2004年第2期15卷 151-166页

作者： Corbera, F Asenjo, R Zapata, EL Univ Malaga Dept Comp Sci E-29080 Malaga Spain

To successfully exploit all the possibilities of current computer/multicomputer architectures, optimization compiling techniques are a must. However, for codes based on pointers. and dynamic data structures, these optimization techniques have to be necessarily Carried out after identifying the characteristics and properties of the data structure used in the code. In this paper, we describe the framework and the analyzer we have implemented to capture complex data structures generated, traversed, and modified in codes based on pointers. Our method assigns a Reduced Set of Reference Shape Graph (RSRSG) to each statement to approximate the shape,of the data structure after the execution of such a statement. With the properties and operations that define the behavior of our RSRSG, the method can accurately detect complex recursive data structures such as a doubly linked list of pointers to trees where the leaves point to additional lists. Several experiments are carried out with real codes to validate the capabilities of our analyzer.

关键词： shape analysis pointers recursive data structures shape graphs optimizing compiler irregular codes

来源：评论

学校读者我要写书评

暂无评论

New shape analysis and interprocedural techniques for automatic parallelization of C codes

引用

INTERNATIONAL JOURNAL OF PARALLEL PROGRAMMING 2002年第1期30卷 37-64页

作者： Corbera, F Asenjo, R Zapata, E Univ Malaga Comp Architecture Dept E-29080 Malaga Spain

Automatic parallelization of codes with complex data structures is becoming very important. These complex, and often recursive, data structures are widely used in scientific computing. Shape analysis is one of the key steps in the automatic parallelization of such codes. In this paper we extend the Static Shape Graph (SSG) method to enable the successful and accurate detection of complex doubly-linked structures. We have also included an interprocedural analysis in our framework. These techniques have been implemented in a compiler, which has been validated for several C codes. In particular, we present the results the compiler achieves for the C sparse LU factorization algorithm and for a recursive code generating a tree data structure. The output SSG perfectly describes the complex data structure used in these codes.

关键词： parallelizing compiler shape analysis pointers recursive data structures shape graphs

来源：评论

学校读者我要写书评

暂无评论

Automatic compiler-inserted prefetching for pointer-based applications

引用

IEEE TRANSACTIONS ON COMPUTERS 1999年第2期48卷 134-141页

作者： Luk, CK Mowry, TC Univ Toronto Dept Comp Sci Toronto ON M5S 3G4 Canada Carnegie Mellon Univ Dept Comp Sci Pittsburgh PA 15213 USA

As the disparity between processor and memory speeds continues to grow, memory latency is becoming an increasingly important performance bottleneck. While software-controlled prefetching is an attractive technique for tolerating this latency, its success has been limited thus far to array-based numeric codes. In this paper, we expand the scope of automatic compiler-inserted prefetching to also include the recursive data structures commonly found in pointer-based applications. We propose three compiler-based prefetching schemes, and automate the most widely applicable scheme (greedy prefetching) in an optimizing research compiler. Our experimental results demonstrate that compiler-inserted prefetching can offer significant performance gains on both uniprocessors and large-scale shared-memory multiprocessors.

关键词： caches prefetching pointer-based applications recursive data structures compiler optimization shared-memory multiprocessors performance evaluation

来源：评论

学校读者我要写书评

暂无评论

A 7-TUPLE REPRESENTATION FOR HIERARCHICAL data-structures

引用

INFORMATION SYSTEMS 1983年第3期8卷 151-157页

作者： NIEMI, T University of Tampere Department of Mathematical Sciences Computer Science P.O. Box 607 SF-33101 Tampere 10 Finland

Different kinds of data structure diagrams, especially Bachman's, and tabular representations are very often used to visualize hierarchical data structures. The popularity of these visual modes of representation is due to the possibility they afford of describing data structures clearly and regardless of any implementation. However, it has been observed in diverse contexts that instead of the visualization we need a general and exact representation containing the same structural components as these visual representations. In this paper we introduce a seven-tuple representation which can be used for exact description of any hierarchical data structure. We give both the explicit construction operations and the implicit rules which can be utilized in forming any hierarchical data structure. We show that the formal representation introduced contains the descriptive power of the visualization methods mentioned above. Furthermore we examine how, in the context of this representation, it is possible to define flexibly general analyzing functions for hierarchical data structures.

关键词： hierarchical data structures data structure diagrams tabular representation recursive data structures

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：