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

acm sigplan '92 conference on programming language design and implementation, pldi 1992

作者： Hoover, Roger IBM Yorktown Heights NY United States

Alphonse is a program transformation system that uses dynamic dependency analysis and incremental computation techniques to automatically generate efficient dynamic implementations from simple exhaustive imperative pr... 详细信息

ISBN: (纸本)0897914759

关键词： Computer programming

来源：评论

学校读者我要写书评

暂无评论

SOAP 2022 - Proceedings of the 11th acm sigplan International Workshop on the State Of the Art in Program Analysis, co-located with pldi 2022

SOAP 2022 - Proceedings of the 11th ACM SIGPLAN Internationa...

引用

11th acm sigplan International Workshop on the State Of the Art in Program Analysis, SOAP 2022, co-located with the 43rd acm sigplan International conference on programming language design and implementation, pldi 2022

ISBN: (纸本)9781450392747

The proceedings contain 7 papers. The topics discussed include: BinFPE: accurate floating-point exception detection for GPU applications;modeling code manipulation in JIT compilers;statically detecting data leakages in data science code;ensuring determinism in blockchain software with GoLiSA: an industrial experience report;ADA: a tool for visualizing the architectural overview of open-source repositories;abstract interpretation of Michelson smart-contracts;and towards an implementation of differential dynamic logic in PVS.

关键词：

来源：评论

学校读者我要写书评

暂无评论

A static analyzer for large safety-critical software 03

引用

conference on programming language design and implementation

作者： Blanchet, B Cousot, P Cousot, R Feret, J Mauborgne, L Miné, A Monniaux, D Rival, X CNRS F-75700 Paris France Ecole Normale Super Paris France Ecole Polytech F-91128 Palaiseau France

ISBN: (纸本)9781581136623

We show that abstract interpretation-based static program analysis can be made efficient and precise enough to formally verify a class of properties for a family of large programs with few or no false alarms. This is achieved by refinement of a general purpose static analyzer and later adaptation to particular programs of the family by the end-user through parametrization. This is applied to the proof of soundness of data manipulation operations at the machine level for periodic synchronous safety critical embedded software. The main novelties are the design principle of static analyzers by refinement and adaptation through parametrization (Sect. 3 and 7), the symbolic manipulation of expressions to improve the precision of abstract transfer functions (Sect. 6.3), the octagon (Sect. 6.2.2), ellipsoid (Sect. 6.2.3), and decision tree (Sect. 6.2.4) abstract domains, all with sound handling of rounding errors in floating point computations, widening strategies (with thresholds: Sect. 7.1.2, delayed: Sect. 7.1.3) and the automatic determination of the parameters (parametrized packing: Sect. 7.2).

关键词： algorithms design experimentation reliability theory verification abstract interpretation abstract domains static analysis verification floating point embedded reactive real-time safety-critical software

来源：评论

学校读者我要写书评

暂无评论

Synthesizing Data Structure Transformations from Input-Output Examples 15

Synthesizing Data Structure Transformations from Input-Outpu...

引用

36th acm sigplan conference on programming language design and implementation

作者： Feser, John K. Chaudhuri, Swarat Dillig, Isil Rice Univ Houston TX 77251 USA UT Austin Austin TX 78712 USA

ISBN: (纸本)9781450334686

We present a method for example-guided synthesis of functional programs over recursive data structures. Given a set of input-output examples, our method synthesizes a program in a functional language with higher-order combinators like map and fold. The synthesized program is guaranteed to be the simplest program in the language to fit the examples. Our approach combines three technical ideas: inductive generalization, deduction, and enumerative search. First, we generalize the input-output examples into hypotheses about the structure of the target program. For each hypothesis, we use deduction to infer new input/output examples for the missing subexpressions. This leads to a new subproblem where the goal is to synthesize expressions within each hypothesis. Since not every hypothesis can be realized into a program that fits the examples, we use a combination of best-first enumeration and deduction to search for a hypothesis that meets our needs. We have implemented our method in a tool called lambda(2), and we evaluate this tool on a large set of synthesis problems involving lists, trees, and nested data structures. The experiments demonstrate the scalability and broad scope of lambda(2). A highlight is the synthesis of a program believed to be the world's earliest functional pearl.

关键词： Program synthesis programming by example data transformations search-based synthesis automated deduction

来源：评论

学校读者我要写书评

暂无评论

A Verified Compiler for a Functional Tensor language

引用

PROCEEDINGS OF THE acm ON programming languageS-PacmPL 2024年第PLDI期8卷 320-342页

作者： Liu, Amanda Bernstein, Gilbert Chlipala, Adam Ragan-Kelley, Jonathan MIT 77 Massachusetts Ave Cambridge MA 02139 USA Univ Washington Seattle WA 98195 USA

Producing efficient array code is crucial in high-performance domains like image processing and machine learning. It requires the ability to control factors like compute intensity and locality by reordering computations into different stages and granularities with respect to where they are stored. However, traditional pure, functional tensor languages struggle to do so. In a previous publication, we introduced ATL as a pure, functional tensor language capable of systematically decoupling compute and storage order via a set of high-level combinators known as reshape operators. Reshape operators are a unique functional-programming construct since they manipulate storage location in the generated code by modifying the indices that appear on the left-hand sides of storage expressions. We present a formal correctness proof for an implementation of the compilation algorithm, marking the first verification of a lowering algorithm targeting imperative loop nests from a source functional language that enables separate control of compute and storage ordering. One of the core difficulties of this proof required properly formulating the complex invariants to ensure that these storage-index remappings were well-formed. Notably, this exercise revealed a soundness bug in the original published compilation algorithm regarding the truncation reshape operators. Our fix is a new type system that captures safety conditions that were previously implicit and enables us to prove compiler correctness for well-typed source programs. We evaluate this type system and compiler implementation on a range of common programs and optimizations, including but not limited to those previously studied to demonstrate performance comparable to established compilers like Halide.

关键词： functional programming array programming formal verification type systems tensors

来源：评论

学校读者我要写书评

暂无评论

Type analysis of Prolog using type graphs 94

Type analysis of Prolog using type graphs

引用

Proceedings of the acm sigplan'94 conference on programming language design and implementation (pldi)

作者： Van Hentenryck, P. Cortesi, A. Le Charlier, B. Brown Univ Providence United States

ISBN: (纸本)089791662X

Type analysis of Prolog is of primary importance for high-performance compilers, since type information may lead to better indexing and to sophisticated specializations of unification and built-in predicates to name a few. However, these optimizations often require a sophisticated type inference system capable of inferring disjunctive and recursive types and hence expensive in computation time. The purpose of this paper is to describe a type analysis system for Prolog based on abstract interpretation and type graphs (i.e. disjunctive rational trees) with this functionality. The system (about 15,000 lines of C) consists of the combination of a generic fixpoint algorithm, a generic pattern domain, and a type graph domain. The main contribution of the paper is to show that this approach can be engineered to be practical for medium-sized programs without sacrificing accuracy. The main technical contributions to achieve this result are (1) a novel widening operator for type graphs which appears to be accurate and effective in keeping the sizes of the graphs, and hence the computation time, reasonably small;(2) the use of the generic pattern domain to obtain a compact representation of equality constraints between subterms and to factor out sure structural information.

关键词： PROLOG (programming language)

来源：评论

学校读者我要写书评

暂无评论

Synthesizing Data Structure Refinements from Integrity Constraints 2021

Synthesizing Data Structure Refinements from Integrity Const...

引用

42nd acm sigplan International conference on programming language design and implementation (pldi)

作者： Pailoor, Shankara Wang, Yuepeng Wang, Xinyu Dillig, Isil Univ Texas Austin Austin TX 78712 USA Univ Penn Philadelphia PA 19104 USA Univ Michigan Ann Arbor MI 48109 USA

ISBN: (纸本)9781450383912

implementations of many data structures use several correlated fields to improve their performance;however, inconsistencies between these fields can be a source of serious program errors. To address this problem, we propose a new technique for automatically refining data structures from integrity constraints. In particular, consider a data structure D with fields F and methods M, as well as a new set of auxiliary fields F' that should be added to D. Given this input and an integrity constraint Phi relating F and F', our method automatically generates a refinement of.. that satisfies the provided integrity constraint. Our method is based on a modular instantiation of the CEGIS paradigm and uses a novel inductive synthesizer that augments top-down search with three key ideas. First, it computes necessary preconditions of partial programs to dramatically prune its search space. Second, it augments the grammar with promising new productions by leveraging the computed preconditions. Third, it guides top-down search using a probabilistic context-free grammar obtained by statically analyzing the integrity checking function and the original code base. We evaluated our method on 25 data structures from popular Java projects and show that our method can successfully refine 23 of them. We also compare our method against two state-of-the-art synthesis tools and perform an ablation study to justify our design choices. Our evaluation shows that (1) our method is successful at refining many data structure implementations in the wild, (2) it advances the state-of-the-art in synthesis, and (3) our proposed ideas are crucial for making this technique practical.

关键词： programming languages Program Synthesis Data structure refinement

来源：评论

学校读者我要写书评

暂无评论

Min-cut program decomposition for thread-level speculation

Min-cut program decomposition for thread-level speculation

引用

Proceedings of the 2004 acm sigplan conference on programming language design and implementation (pldi'04)

作者： Johnson, Troy A. Eigenmann, Rudolf Vijaykumar, T.N. Sch. of Elec. and Comp. Engineering Purdue University West Lafayette IN 47907 United States

With billion-transistor chips on the horizon, single-chip multiprocessors (CMPs) are likely to become commodity components. Speculative CMPs use hardware to enforce dependence, allowing the compiler to improve performance by speculating on ambiguous dependences without absolute guarantees of independence. The compiler is responsible for decomposing a sequential program into speculatively parallel threads, while considering multiple performance overheads related to data dependence, load imbalance, and thread prediction. Although the decomposition problem lends itself to a min-cut-based approach, the over-heads depend on the thread size, requiring the edge weights to be changed as the algorithm progresses. The changing weights make our approach different from graph-theoretic solutions to the general problem of task scheduling. One recent work uses a set of heuristics, each targeting a specific overhead in isolation, and gives precedence to thread prediction, without comparing the performance of the threads resulting from each heuristic. By contrast, our method uses a sequence of balanced min-cuts that give equal consideration to all the overheads, and adjusts the edge weights after every cut. This method achieves an (geometric) average speedup of 74% for floating-point programs and 23% for integer programs on a four-processor chip, improving on the 52% and 13% achieved by the previous heuristics.

关键词： Computer programming

来源：评论

学校读者我要写书评

暂无评论

Meta optimization: Improving compiler heuristics with machine learning 03

引用

conference on programming language design and implementation

作者： Stephenson, M Amarasinghe, S Martin, M O'Reilly, UM MIT Comp Sci Lab Cambridge MA 02139 USA MIT Artificial Intelligence Lab Cambridge MA 02139 USA

ISBN: (纸本)9781581136623

Compiler writers have crafted many heuristics over the years to approximately solve NP-hard problems efficiently. Finding a heuristic that performs well on a broad range of applications is a tedious and difficult process. This paper introduces Meta Optimization, a methodology for automatically fine-tuning compiler heuristics. Meta Optimization uses machine-learning techniques to automatically search the space of compiler heuristics. Our techniques reduce compiler design complexity by relieving compiler writers of the tedium of heuristic tuning. Our machine-learning system uses an evolutionary algorithm to automatically find effective compiler heuristics. We present promising experimental results. In one mode of operation Meta Optimization creates application-specific heuristics which often result in impressive speedups. For hyperblock formation, one optimization we present in this paper, we obtain an average speedup of 23% (up to 73%) for the applications in our suite. Furthermore, by evolving a compiler's heuristic over several benchmarks, we can create effective, general-purpose heuristics. The best general-purpose heuristic our system found for hyperblock formation improved performance by an average of 25% on our training set, and 9% on a completely unrelated test set. We demonstrate the efficacy of our techniques - on three different optimizations in this paper: hyperblock formation, register allocation, and data prefetching.

关键词： machine learning priority functions genetic programming compiler heuristics

来源：评论

学校读者我要写书评

暂无评论

Synchronization via scheduling: Techniques for efficiently managing shared state 11

Synchronization via scheduling: Techniques for efficiently m...

引用

32nd acm conference on programming language design and implementation, pldi 2011

作者： Best, Micah J. Mottishaw, Shane Mustard, Craig Roth, Mark Fedorova, Alexandra Brownsword, Andrew University of British Columbia Canada Simon Fraser University Canada Electronic Arts Inc. Canada

ISBN: (纸本)9781450306638

Shared state access conflicts are one of the greatest sources of error for fine grained parallelism in any domain. Notoriously hard to debug, these conflicts reduce reliability and increase development time. The standard task graph model dictates that tasks with potential conflicting accesses to shared state must be linked by a dependency, even if there is no explicit logical ordering on their execution. In cases where it is difficult to understand if such implicit dependencies exist, the programmer often creates more dependencies than needed, which results in constrained graphs with large monolithic tasks and limited parallelism. We propose a new technique, Synchronization via Scheduling (SvS), that uses the results of static and dynamic code analysis to manage potential shared state conflicts by exposing the data accesses of each task to the scheduler. We present an in-depth performance analysis of SvS via examples from video games, our target domain, and show that SvS performs well in comparison to software transactional memory (TM) and fine grained mutexes. © 2011 acm.

关键词： Parallel programming

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：