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

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

End-to-End Verification of Information-Flow Security for C and Assembly Programs

引用

acm sigplan NOTICES 2016年第6期51卷 648-664页

作者： Costanzo, David Shao, Zhong Gu, Ronghui Yale Univ New Haven CT 06520 USA

Protecting the confidentiality of information manipulated by a computing system is one of the most important challenges facing today's cybersecurity community. A promising step toward conquering this challenge is to formally verify that the end-to-end behavior of the computing system really satisfies various information-flow policies. Unfortunately, because today's system software still consists of both C and assembly programs, the end-to-end verification necessarily requires that we not only prove the security properties of individual components, but also carefully preserve these properties through compilation and cross-language linking. In this paper, we present a novel methodology for formally verifying end-to-end security of a software system that consists of both C and assembly programs. We introduce a general definition of observation function that unifies the concepts of policy specification, state indistinguishability, and whole-execution behaviors. We show how to use different observation functions for different levels of abstraction, and how to link different security proofs across abstraction levels using a special kind of simulation that is guaranteed to preserve state indistinguishability. To demonstrate the effectiveness of our new methodology, we have successfully constructed an end-to-end security proof, fully formalized in the Coq proof assistant, of a nontrivial operating system kernel (running on an extended CompCert x86 assembly machine model). Some parts of the kernel are written in C and some are written in assembly;we verify all of the code, regardless of language.

关键词： Verification Security Reliability languages design Information Flow Control Security Policy Specification Security-Preserving Simulation Program Verification Certified OS Kernels

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

XMem: Type-safe, transparent, shared memory for cross-runtime communication and coordination

引用

acm sigplan NOTICES 2008年第6期43卷 327-338页

作者： Wegiel, Michal Krintz, Chandra Univ Calif Santa Barbara Dept Comp Sci Santa Barbara CA 93106 USA

Developers commonly build contemporary enterprise applications using type-safe, component-based platforms, such as J2EE, and architect them to comprise multiple tiers, such as a web container, application server, and database engine. Administrators increasingly execute each tier in its own managed runtime environment (MRE) to improve reliability and to manage system complexity through the fault containment and modularity offered by isolated MRE instances. Such isolation, however, necessitates expensive cross-tier communication based on protocols such as object serialization and remote procedure calls. Administrators commonly co-locate communicating MREs on a single host to reduce communication overhead and to better exploit increasing numbers of available processing cores. However, state-of-the-art MREs offer no support for more efficient communication between co-located MREs, while fast inter-process communication mechanisms, such as shared memory, are widely available as a standard operating system service on most modern platforms. To address this growing need, we present the design and implementation of XMem - type-safe, transparent, shared memory support for co-located MREs. XMem guarantees type-safety through coordinated, parallel, multi-process class loading and garbage collection. To avoid introducing any level of indirection, XMem manipulates virtual memory mapping. In addition, object sharing in XMem is fully transparent: shared objects are identical to local objects in terms of field access, synchronization, garbage collection, and method invocation, with the only difference being that shared-to-private pointers are disallowed. XMem facilitates easy integration and use by existing communication technologies and software systems, such as RMI, JNDI, JDBC, serialization/XML, and network sockets. We have implemented XMem in the open-source, production-quality HotSpot Java Virtual Machine. Our experimental evaluation, based on core communication technologies un

关键词： design experimentation languages management measurement performance interprocess communication managed runtimes shared memory transparent type-safe garbage collection synchronization class loading parallel

来源：评论

学校读者我要写书评

暂无评论

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)

来源：评论

学校读者我要写书评

暂无评论

Shangri-la: Achieving high performance from compiled network applications while enabling ease of programming

引用

acm sigplan NOTICES 2005年第6期40卷 224-236页

作者： Chen, MK Li, XF Lian, RQ Lin, JH Liu, LX Liu, T Ju, R Intel Corp Microproc Technol Labs Santa Clara CA 95051 USA Intel China Res Ctr Ltd Beijing Peoples R China Chinese Acad Sci Inst Comp Technol Beijing Peoples R China

programming network processors is challenging. To sustain high line rates, network processors have extremely tight memory access and instruction budgets. Achieving desired performance has traditionally required hand-coded assembly. Researchers have recently proposed high-level programming languages for packet processing, but the challenges of compiling these languages into code that is competitive with hand-tuned assembly remain unanswered. This paper describes the Shangri-La compiler, which accepts a packet program written in a C-like high-level language and applies scalar and specialized optimizations to generate a highly optimized binary. Hot code paths identified by profiling are mapped across processing elements to maximize processor utilization. Since our compilation target has no hardware caches, software-controlled caches are generated for frequently accessed application data structures. Packet handling optimizations significantly reduce per-packet memory access and instruction counts. Finally, a custom stack model maps stack frames to the fastest levels of the target processor's heterogeneous memory hierarchy. Binaries generated by the compiler were evaluated on the Intel IXP2400 network processor with eight packet processing cores and eight threads per core. Our results show the importance of both traditional and specialized optimization techniques for achieving the maximum forwarding rates on three network applications, L3-Switch, MPLS and Firewall.

关键词： packet processing network processors chip multiprocessors throughput-oriented computing program partitioning dataflow programming

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：