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

Acute: High-level programming language design for distributed computation

acm sigplan NOTICES 2005年第9期40卷 15-26页

作者： Sewell, P Leifer, JJ Wansbrough, K Nardelli, FZ Allen-Williams, M Habouzit, P Vafeiadis, V Univ Cambridge Cambridge CB2 1TN England

Existing languages provide good support for typeful programming of standalone programs. In a distributed system, however, there may be interaction between multiple instances of many distinct programs, sharing some (but not necessarily all) of their module structure, and with some instances rebuilt with new versions of certain modules as time goes on. In this paper we discuss programming language support for such systems, focussing on their typing and naming issues. We describe an experimental language, Acute, which extends an ML core to support distributed development, deployment, and execution, allowing type-safe interaction between separately-built programs. The main features are: (1) type-safe marshalling of arbitrary values;(2) type names that are generated (freshly and by hashing) to ensure that type equality tests suffice to protect the invariants of abstract types, across the entire distributed system;(3) expression-level names generated to ensure that name equality tests suffice for type-safety of associated values, e.g. values carried on named channels;(4) controlled dynamic rebinding of marshalled values to local resources;and (5) thunkification of threads and mutexes to support computation mobility. These features are a large part of what is needed for typeful distributed programming. They are a relatively lightweight extension of M L, should be efficiently implementable, and are expressive enough to enable a wide variety of distributed infrastructure layers to be written as simple library code above the byte-string network and persistent store APIs. This disentangles the language runtime from communication intricacies. This paper highlights the main design choices in Acute. It is supported by a full language definition (of typing, compilation, and operational semantics), by a prototype implementation, and by example distribution libraries.

关键词： languages design programming languages distributed programming marshalling serialisation abstract types modules rebinding version control type theory ML

来源：评论

学校读者我要写书评

暂无评论

Proceedings of the conference on Object-Oriented programming Systems, languages, and Applications, OOPSLA

Proceedings of the Conference on Object-Oriented Programming...

引用

10th Annual conference on Object-Oriented programming Systems, languages, and Applications, OOPSLA 1995

ISBN: (纸本)0897917219

The proceedings contain 36 papers. The topics discussed include: application of domain analysis to object-oriented systems;applying object-oriented software engineering methods to the development of call center software: a case study;using objects to manage in-memory data intensive expert systems;the navigation toolkit project revisited;performance of a OODB in a online 7x24x365 manufacturing operation;why C++ is not just an object-oriented programming language;patterns: cult to culture?;OOPSLA'95 doctoral symposium;implementing a real -time, embedded, telecommunication switching system in SmallTalk;object oriented project management;OO process and metrics for effort estimation;semantic integration in complex systems: collective behavior in business rules and software transactions;workshop on design patterns for concurrent, parallel and distributed object-oriented systems;the object engine: foundation for next generation architectures;subjectivity in object-oriented systems workshop summary;objects and relational databases;object database behavior, benchmarks, and performance workshop addendum;workshop on adaptable and adaptive software;and legacy systems and object technology workshop summary.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Contracts for Modular Discrete Controller Synthesis

引用

acm sigplan NOTICES 2010年第4期45卷 57-66页

作者： Delaval, Gwenael Marchand, Herve Rutten, Eric INRIA Grenoble France INRIA Rennes France

We describe the extension of a reactive programming language with a behavioral contract construct. It is dedicated to the programming of reactive control of applications in embedded systems, and involves principles of the supervisory control of discrete event systems. Our contribution is in a language approach where modular discrete controller synthesis (DCS) is integrated, and it is concretized in the encapsulation of DCS into a compilation process. From transition system specifications of possible behaviors, DCS automatically produces controllers that make the controlled system satisfy the property given as objective. Our language features and compiling technique provide correctness-by-construction in that sense, and enhance reliability and verifiability. Our application domain is adaptive and reconfigurable systems: closed-loop adaptation mechanisms enable flexible execution of functionalities w.r.t. changing resource and environment conditions. Our language can serve programming such adaption controllers. This paper particularly describes the compilation of the language. We present a method for the modular application of discrete controller synthesis on synchronous programs, and its integration in the BZR language. We consider structured programs, as a composition of nodes, and first apply DCS on particular nodes of the program, in order to reduce the complexity of the controller computation;then, we allow the abstraction of parts of the program for this computation;and finally, we show how to recompose the different controllers computed from different abstractions for their correct co-execution with the initial program. Our work is illustrated with examples, and we present quantitative results about its implementation.

关键词： design languages Reliability Verification Discrete controller synthesis modularity components contracts reactive systems synchronous programming adaptive and reconfigurable systems

来源：评论

学校读者我要写书评

暂无评论

A 64-bit Stream Processor Architecture for Scientific Applications 07

A 64-bit Stream Processor Architecture for Scientific Applic...

引用

34th Annual International Symposium on Computer Architecture

作者： Yang, Xuejun Yan, Xiaobo Xing, Zuocheng Deng, Yu Jiang, Jiang Zhang, Ying Natl Univ Def Technol Natl Lab Paralleling & Distributed Proc Sch Comp Changsha 410073 Hunan Peoples R China

ISBN: (纸本)9781595937063

Stream architecture is a novel microprocessor architecture with wide application potential. But as for whether it can be used efficiently in scientific computing, many issues await further study. This paper first gives the design and implementation of a 64-bit stream processor, FT64 (Fei Teng 64), for scientific computing. The carrying out of 64-bit extension design and scientific computing oriented optimization are described in such aspects as instruction set architecture, stream controller, micro controller, ALU cluster, memory hierarchy and interconnection interface here. Second, two kinds of communications as message passing and stream communications are put forward. An interconnection based on the communications is designed for FT64-based high performance computers. Third, a novel stream programming language, SF95 (Stream FORTRAN95), and its compiler, SF95Compiler (Stream FORTRAN95 Compiler), are developed to facilitate the development of scientific applications. Finally, nine typical scientific application kernels are tested and the results show the efficiency of stream architecture for scientific computing.

关键词： stream processor architecture program language compiler scientific application high performance computing

来源：评论

学校读者我要写书评

暂无评论

PADS: A domain-specific language for processing ad hoc data

引用

acm sigplan NOTICES 2005年第6期40卷 295-304页

作者： Fisher, K Gruber, R AT&T Labs Res Florham Pk NJ 07932 USA Google Mountain View CA USA

PADS is a declarative data description language that allows data analysts to describe both the physical layout of ad hoc data sources and semantic properties of that data. From such descriptions, the PADS compiler generates libraries and tools for manipulating the data, including parsing routines, statistical profiling tools, translation programs to produce well-behaved formats such as XML or those required for loading relational databases, and tools for running XQueries over raw PADS data sources. The descriptions are concise enough to serve as "living" documentation while flexible enough to describe most of the ASCII, binary, and Cobol formats that we have seen in practice. The generated parsing library provides for robust, application-specific error handling.

关键词： data description language domain-specific languages

来源：评论

学校读者我要写书评

暂无评论

The GNAT implementation of controlled types

The GNAT implementation of controlled types

引用

International conference on TRI-Ada 1995: Ada's Role in Global Markets: Solutions for a Changing Complex World, TRI-Ada 1995

作者： Comar, Cyrille Dismukes, Gary Gasperoni, Franco Ada Core Technologies 73 Fifth Avenue New YorkNY10003 United States Ada Core Technologies 10397 Avenida Magnifica San DiegoCA92131 United States Telecom Paris-ENST Dep. INF 46 rue Barrault Paris Cedex 1375634 France

ISBN: (纸本)0897917057

This paper discusses the implementation model for supporting Ada 95 controlled types in the GNAT compiler [1]. After reviewing the semantics of controlled types, we outline the associated implementation problems and describe their solution in GNAT. The design addresses the management of controlled operations on various entities, including dynamically allocated objects, transient objects (function results and aggregates), and composite objects containing controlled components. The interaction of the controlled type features with exceptions is also covered. Finally, we discuss alternative implementation approaches and possible enhancements to the current model. © 1995 acm.

关键词： Aggregates

来源：评论

学校读者我要写书评

暂无评论

Linearity and PCF: a Semantic Insight! 11

Linearity and PCF: a Semantic Insight!

引用

16th acm sigplan International conference on Functional programming (ICFP 11)

作者： Gaboardi, Marco Paolini, Luca Piccolo, Mauro Univ Bologna INRIA Focus Team Dip Sci Informaz I-40127 Bologna Italy Univ Turin Dipartimento Informat I-10149 Turin Italy

ISBN: (纸本)9781450308656

Linearity is a multi-faceted and ubiquitous notion in the analysis and the development of programming language concepts. We study linearity in a denotational perspective by picking out programs that correspond to linear functions between coherence spaces. We introduce a language, named SlPCF(star), that increases the higher-order expressivity of a linear core of PCF by means of new operators related to exception handling and parallel evaluation. SlPCF(star) allows us to program all the finite elements of the model and, consequently, it entails a full abstraction result that makes the reasoning on the equivalence between programs simpler. Denotational linearity provides also crucial information for the operational evaluation of programs. We formalize two evaluation machineries for the language. The first one is an abstract and concise operational semantics designed with the aim of explaining the new operators, and is based on an infinite-branching search of the evaluation space. The second one is more concrete and it prunes such a space, by exploiting the linear assumptions. This can also be regarded as a base for an implementation.

关键词： languages Theory design PCF Linear Logic Denotational Semantics Operational Semantics

来源：评论

学校读者我要写书评

暂无评论

Sapper: A language for hardware-level security policy enforcement 14

Sapper: A language for hardware-level security policy enforc...

引用

19th International conference on Architectural Support for programming languages and Operating Systems, ASPLOS 2014

作者： Li, Xun Kashyap, Vineeth Oberg, Jason K. Tiwari, Mohit Rajarathinam, Vasanth Ram Kastner, Ryan Sherwood, Timothy Hardekopf, Ben Chong, Frederic T. Facebook United States University of California Santa Barbara United States University of California San Diego United States University of Texas Austin United States AMD United States

ISBN: (纸本)9781450323055

Privacy and integrity are important security concerns. These concerns are addressed by controlling information flow, i.e., restricting how information can flow through a system. Most proposed systems that restrict information flow make the implicit assumption that the hardware used by the system is fully " correct" and that the hardware's instruction set accurately describes its behavior in all circumstances. The truth is more complicated: modern hardware designs defy complete verification, many aspects of the timing and ordering of events are left totally unspecified, and implementation bugs present themselves with surprising frequency. In this work we describe Sapper, a novel hardware description language for designing security-critical hardware components. Sapper seeks to address these problems by using static analysis at compile-time to automatically insert dynamic checks in the resulting hardware that provably enforce a given information flow policy at execution time. We present Sapper's design and formal semantics along with a proof sketch of its security. In addition, we have implemented a compiler for Sapper and used it to create a non-trivial secure embedded processor with many modern microarchitectural features. We empirically evaluate the resulting hardware's area and energy over-head and compare them with alternative designs. Copyright © 2014 acm.

关键词： Static analysis

来源：评论

学校读者我要写书评

暂无评论

Temporal NetKAT

引用

acm sigplan NOTICES 2016年第6期51卷 386-401页

作者： Beckett, Ryan Greenberg, Michael Walker, David Princeton Univ Princeton NJ 08544 USA Pomona Coll Claremont CA 91711 USA

Over the past 5-10 years, the rise of software-defined networking (SDN) has inspired a wide range of new systems, libraries, hypervisors and languages for programming, monitoring, and debugging network behavior. Oftentimes, these systems are disjoint-one language for programming and another for verification, and yet another for run-time monitoring and debugging. In this paper, we present a new, unified framework, called Temporal NetKAT, capable of facilitating all of these tasks at once. As its name suggests, Temporal NetKAT is the synthesis of two formal theories: past-time (finite trace) linear temporal logic and (network) Kleene Algebra with Tests. Temporal predicates allow programmers to write down concise properties of a packet's path through the network and to make dynamic packet-forwarding, access control or debugging decisions on that basis. In addition to being useful for programming, the combined equational theory of LTL and NetKAT facilitates proofs of pathbased correctness properties. Using new, general, proof techniques, we show that the equational semantics is sound with respect to the denotational semantics, and, for a class of programs we call network-wide programs, complete. We have also implemented a compiler for temporal NetKAT, evaluated its performance on a range of benchmarks, and studied the effectiveness of several optimizations.

关键词： Software-defined networking Network programming languages Domain-specific languages Kleene algebra with tests NetKAT Temporal logic

来源：评论

学校读者我要写书评

暂无评论

Adding delimited and composable control to a production programming environment

引用

acm sigplan NOTICES 2007年第9期42卷 165-176页

作者： Flatt, Matthew Yu, Gang Findler, Robert Bruce Felleisen, Matthias Univ Utah Salt Lake City UT 84112 USA Chinese Acad Sci Inst Software Beijing 100864 Peoples R China Univ Chicago Chicago IL 60637 USA Northeastern Univ Boston MA 02115 USA

Operators for delimiting control and for capturing composable continuations litter the landscape of theoretical programming language research. Numerous papers explain their advantages, how the operators explain each other (or don't), and other aspects of the operators' existence. Production programming languages, however, do not support these operators, partly because their relationship to existing and demonstrably useful constructs-such as exceptions and dynamic binding-remains relatively unexplored. In this paper, we report on our effort of translating the theory of delimited and composable control into a viable implementation for a production system. The report shows how this effort involved a substantial design element, including work with a formal model, as well as significant practical exploration and engineering. The resulting version of PLT Scheme incorporates the expressive combination of delimited and composable control alongside dynamic-wind, dynamic binding, and exception handling. None of the additional operators subvert the intended benefits of existing control operators, so that programmers can freely mix and match control operators.

关键词： design languages

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：