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

Dependence analysis for pointer variables

sigplan Notices (acm Special Interest Group on programming languages) 1989年第7期24卷 28-40页

作者： Horwitz, Susan Pfeiffer, Phil Reps, Thomas Univ of Wisconsin United States

Our concern is how to determine data dependences between program constructs in programming languages with pointer variables. We are particularly interested in computing data dependences for languages that manipulate heap-allocated storage, such as Lisp and Pascal. We have defined a family of algorithms that compute safe approximations to the flow, output, and anti-dependences of a program written in such a language. Our algorithms account for destructive updates to fields of a structure and thus are not limited to the cases where all structures are trees or acyclic graphs;they are applicable to programs that build cyclic structures. For structured programming constructs, the technique can be extended to distinguish between loop-carried and loop-independent dependences, as well as to determine lower bounds on minimum distances for loop-carried dependences.

关键词： Computer programming languages

来源：评论

学校读者我要写书评

暂无评论

Framework for construction and evaluation of high-level specifications for program analysis techniques

引用

sigplan Notices (acm Special Interest Group on programming languages) 1989年第7期24卷 1-12页

作者： Venkatesh, G.A. Univ of Wisconsin United States

We have developed and implemented a framework that can be used to construct concise high-level specifications of program analysis techniques. Use of such a framework in a system such as the Synthesizer Generator allows program analysis techniques to be incorporated into program development environments without a need to supply implementation details. This aids in rapid development of new program analysis techniques as well as techniques that share common features but are customized for specific applications. The choice of a denotational framework to express these specifications allows formal proofs of correctness to be established for each of these analysis techniques. The facilities provided by the framework result in clear and concise specifications that aid in the understanding of the corresponding analysis techniques.

关键词： Computer programming languages

来源：评论

学校读者我要写书评

暂无评论

P: Safe Asynchronous Event-Driven programming 13

P: Safe Asynchronous Event-Driven Programming

引用

acm sigplan conference on programming language design and implementation

作者： Ankush Desai Vivek Gupta Ethan Jackson Shaz Qadeer Sriram Rajamani Damien Zufferey Microsoft IST Austria

ISBN: (纸本)9781450320146

We describe the design and implementation of P, a domain-specific language to write asynchronous event driven code. P allows the programmer to specify the system as a collection of interacting state machines, which communicate with each other using events. P unifies modeling and programming into one activity for the programmer. Not only can a P program be compiled into executable code, but it can also be tested using model checking techniques. P allows the programmer to specify the environment, used to "close" the system during testing, as nondeterministic ghost machines. Ghost machines are erased during compilation to executable code; a type system ensures that the erasure is semantics preserving. The P language is designed so that a P program can be checked for responsiveness-the ability to handle every event in a timely manner. By default, a machine needs to handle every event that arrives in every state. But handling every event in every state is impractical. The language provides a notion of deferred events where the programmer can annotate when she wants to delay processing an event. The default safety checker looks for presence of unhandled events. The language also provides default liveness checks that an event cannot be potentially deferred forever. P was used to implement and verify the core of the USB device driver stack that ships with Microsoft Windows 8. The resulting driver is more reliable and performs better than its prior incarnation (which did not use P); we have more confidence in the robustness of its design due to the language abstractions and verification provided by P.

关键词： Domain-specific language Device driver Event-driven programming State machine Verification Systematic testing state machines Computer personnel event-driven programming Verification device drivers Phosphorus Executable code Device Programmer Component application-specific language language Microsoft Windows(software)

来源：评论

学校读者我要写书评

暂无评论

Sketching stencils

引用

acm sigplan NOTICES 2007年第6期42卷 167-178页

作者： Solar-Lezama, Armando Arnold, Gilad Tancau, Liviu Bodik, Rastislav Saraswat, Vijay Seshia, Sanjit IBM Corp TJ Watson Res Ctr Armonk NY 10504 USA Univ Calif Berkeley Berkeley CA 94720 USA

Performance of stencil computations can be significantly improved through smart implementations that improve memory locality, computation reuse, or parallelize the computation. Unfortunately, efficient implementations are hard to obtain because they often involve non-traditional transformations, which means that they cannot be produced by optimizing the reference stencil with a compiler. In fact, many stencils are produced by code generators that were tediously handcrafted. In this paper, we show how stencil implementations can be produced with sketching. Sketching is a software synthesis approach where the programmer develops a partial implementation a sketch-and a separate specification of the desired functionality given by a reference (unoptimized) stencil. The synthesizer then completes the sketch to behave like the specification, filling in code fragments that are difficult to develop manually. Existing sketching systems work only for small finite programs, i.e., programs that can be represented as small Boolean circuits. In this paper, we develop a sketching synthesizer that works for stencil computations, a large class of programs that, unlike circuits, have unbounded inputs and outputs, as well as an unbounded number of computations. The key contribution is a reduction algorithm that turns a stencil into a circuit, allowing us to synthesize stencils using an existing sketching synthesizer.

关键词： languages design performance sketching stencil SAT

来源：评论

学校读者我要写书评

暂无评论

Semantics of program dependence

引用

sigplan Notices (acm Special Interest Group on programming languages) 1989年第7期24卷 13-27页

作者： Cartwright, Robert Felleisen, Matthias Rice Univ United States

Optimizing and parallelizing compilers for procedural languages rely on various forms of program dependence graphs (pdgs) to express the essential control and data dependences among atomic program operations. In this paper, we provide a semantic justification for this practice by deriving two different forms of program dependence graph - the output pdg and the def-order pdg - and their semantic definitions from non-strict generalizations of the denotational semantics of the programming language. In the process, we demonstrate that both the output pdg and the def-order pdg (with minor technical modifications) are conventional data-flow programs. In addition, we show that the semantics of the def-order pdg dominates the semantics of the output pdg and that both of these semantics dominate - rather than preserve - the semantics of sequential execution.

关键词： Computer programming languages

来源：评论

学校读者我要写书评

暂无评论

Component NextGen: A sound and expressive component framework for Java

引用

acm sigplan NOTICES 2007年第10期42卷 153-170页

作者： Sasitorn, James Cartwright, Robert Rice Univ Houston TX 77251 USA

Developing a general component system for a statically typed, object-oriented language is a challenging design problem for two reasons. First, mutually recursive references across components are common in object-oriented programs - an issue that has proven troublesome in the context of component systems for functional and procedural languages. Second, inheritance across component boundaries can cause accidental method overrides. Our recent research shows that a component framework can be constructed for a nominally typed object-oriented language supporting first-class(1) generic types simply by adding appropriate annotations, syntactic sugar, and component-level type-checking. The fundamental semantic building blocks for constructing, type-checking and manipulating components are provided by the underlying first-class generic type system. To demonstrate the simplicity and utility of this approach we have designed and implemented an extension of Java called Component NEXTGEN (CGEN). CGEN, which is based on the Sun Java 5.0 javac compiler, is backwards compatible with existing Java binary code and runs on current Java Virtual Machines. The primary contribution of this paper is a technical analysis of the subtle design issues involved in building a component framework for a nominally typed object-oriented language supporting first-class generics. In contrast to component systems for structurally typed languages, mutual recursion among components is accommodated in the type system and semantics without incorporating any special machinery. Our analysis includes a presentation of Core CGEN (CCG), a small, core language modeling the CGEN framework. It is based on Featherweight GJ and incorporates some ideas from MIXGEN. CCG adds the essential features to support components, but nothing more. Our discussion includes the type rules and semantics for CCG, as well as a proof of type safety.

关键词： design language first-class generics Java implementation custom class loader modules components signatures

来源：评论

学校读者我要写书评

暂无评论

Laws of concurrent programming 14

Laws of concurrent programming

引用

Proceedings of the 35th acm sigplan conference on programming language design and implementation

作者： Tony Hoare Microsoft Research Cambridge United Kingdom

ISBN: (纸本)9781450327848

The talk extends the Laws of programming [1] by four laws governing concurrent composition of programs. This operator is associative and commutative and distributive through union; and it has the same unit (do nothing) as sequential composition. Furthermore, sequential and concurrent composition distribute through each other, in accordance with an exchange law; this permits an implementation of concurrency by partial interleaving.

关键词： separation logic CCS verification concurrency

来源：评论

学校读者我要写书评

暂无评论

Fast Algorithms for Dyck-CFL-Reachability with Applications to Alias Analysis 13

Fast Algorithms for Dyck-CFL-Reachability with Applications ...

引用

acm sigplan conference on programming language design and implementation

作者： Qirun Zhang Michael R. Lyu Hao Yuan Zhendong Su The Chinese University of Hong Kong BOPU Technologies University of California

ISBN: (纸本)9781450320146

The context-free language (CFL) reachability problem is a well-known fundamental formulation in program analysis. In practice, many program analyses, especially pointer analyses, adopt a restricted version of CFL-reachability, Dyck-CFL-reachability, and compute on edge-labeled bidirected graphs. Solving the all-pairs Dyck-CFL-reachability on such bidirected graphs is expensive. For a bidirected graph with n nodes and m edges, the traditional dynamic programming style algorithm exhibits a subcubic time complexity for the Dyck language with k kinds of parentheses. When the underlying graphs are restricted to bidirected trees, an algorithm with O(n log n log k) time complexity was proposed recently. This paper studies the Dyck-CFL-reachability problems on bidirected trees and graphs. In particular, it presents two fast algorithms with O(n) and O(n + m log m) time complexities on trees and graphs respectively. We have implemented and evaluated our algorithms on a state-of-the-art alias analysis for Java. Results on standard benchmarks show that our algorithms achieve orders of magnitude speedup and consume less memory.

关键词： Dyck-CFL-reachability Alias analysis Algorithms design Experimentation languages algorithms language experimentation analysis programme complexity classes Parentheses logs logarithm (log)

来源：评论

学校读者我要写书评

暂无评论

A design and Verification Methodology for Secure Isolated Regions

引用

acm sigplan NOTICES 2016年第6期51卷 665-681页

作者： Sinha, Rohit Costa, Manuel Lal, Akash Lopes, Nuno P. Rajamani, Sriram Seshia, Sanjit A. Vaswani, Kapil Univ Calif Berkeley Berkeley CA 94720 USA Microsoft Res London England Microsoft Res Bengaluru Karnataka India

Hardware support for isolated execution (such as Intel SGX) enables development of applications that keep their code and data confidential even while running on a hostile or compromised host. However, automatically verifying that such applications satisfy confidentiality remains challenging. We present a methodology for designing such applications in a way that enables certifying their confidentiality. Our methodology consists of forcing the application to communicate with the external world through a narrow interface, compiling it with runtime checks that aid verification, and linking it with a small runtime library that implements the interface. The runtime library includes core services such as secure communication channels and memory management. We formalize this restriction on the application as Information Release Confinement (IRC), and we show that it allows us to decompose the task of proving confidentiality into (a) one-time, human-assisted functional verification of the runtime to ensure that it does not leak secrets, (b) automatic verification of the application's machine code to ensure that it satisfies IRC and does not directly read or corrupt the runtime's internal state. We present/CONFIDENTIAL: a verifier for IRC that is modular, automatic, and keeps our compiler out of the trusted computing base. Our evaluation suggests that the methodology scales to real-world applications.

关键词： Enclave Programs Secure Computation Confidentiality Formal Verification

来源：评论

学校读者我要写书评

暂无评论

A General Constraint-centric Scheduling Framework for Spatial Architectures 13

A General Constraint-centric Scheduling Framework for Spatia...

引用

acm sigplan conference on programming language design and implementation

作者： Tony Nowatzki Michael Sartin-Tarm Lorenzo De Carli Karthikeyan Sankaralingam Cristian Estan Behnam Robatmili University of Wisconsin-Madison Broadcom Qualcomm Research Silicon Valley

ISBN: (纸本)9781450320146

Specialized execution using spatial architectures provides energy efficient computation, but requires effective algorithms for spatially scheduling the computation. Generally, this has been solved with architecture-specific heuristics, an approach which suffers from poor compiler/architect productivity, lack of insight on optimality, and inhibits migration of techniques between architectures. Our goal is to develop a scheduling framework usable for all spatial architectures. To this end, we expresses spatial scheduling as a constraint satisfaction problem using Integer Linear programming (ILP). We observe that architecture primitives and scheduler responsibilities can be related through five abstractions: placement of computation, routing of data, managing event timing, managing resource utilization, and forming the optimization objectives. We encode these responsibilities as 20 general ILP constraints, which are used to create schedulers for the disparate TRIPS, DySER, and PLUG architectures. Our results show that a general declarative approach using ILP is implementable, practical, and typically matches or outperforms specialized schedulers.

关键词： Spatial Architectures Spatial Architecture Scheduling Integer Linear programming

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：