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

proceedings of the acm sigplan 1989 conference on programming language design and implementation

作者： W. Horwat A. A. Chien W. J. Dally Artificial Intelligence Laboratory and Laboratory for Computer Science Massachusetts Institute of Technology Cambridge Massachusetts

ISBN: (纸本)9780897913065

CST is a programming language based on Smalltalk-802 that supports concurrency using locks, asynchronous messages, and distributed objects. In this paper, we describe CST: the language and its implementation. Example programs and initial programming experience with CST are described. Our implementation of CST generates native code for the J-machine, a fine-grained concurrent computer. Some compiler optimizations developed in conjunction with that implementation are also described.

关键词：

来源：评论

学校读者我要写书评

暂无评论

A certified type-preserving compiler from lambda calculus to assembly language

引用

acm sigplan NOTICES 2007年第6期42卷 54-65页

作者： Chlipala, Adam Univ Calif Berkeley Berkeley CA 94720 USA

We present a certified compiler from the simply-typed lambda calculus to assembly language. The compiler is certified in the sense that it comes with a machine-checked proof of semantics preservation, performed with the Coq proof assistant. The compiler and the terms of its several intermediate languages are given dependent types that guarantee that only well-typed programs are representable. Thus, type preservation for each compiler pass follows without any significant "proofs" of the usual kind. Semantics preservation is proved based on denotational semantics assigned to the intermediate languages. We demonstrate how working with a type-preserving compiler enables type-directed proof search to discharge large parts of our proof obligations automatically.

关键词： languages verification compiler verification interactive proof assistants dependent types denotational semantics

来源：评论

学校读者我要写书评

暂无评论

Mace: language support for building distributed systems

引用

acm sigplan NOTICES 2007年第6期42卷 179-188页

作者： Killian, Charles Anderson, James W. Braud, Ryan Jhala, Ranjit Vahdat, Amin Univ Calif San Diego La Jolla CA 92093 USA

Building distributed systems is particularly difficult because of the asynchronous, heterogeneous, and failure-prone environment where these systems must run. Tools for building distributed systems must strike a compromise between reducing programmer effort and increasing system efficiency. We present Mace, a C++ language extension and source-to-source compiler that translates a concise but expressive distributed system specification into a C++ implementation. Mace overcomes the limitations of low-level languages by providing a unified framework for networking and event handling, and the limitations of high-level languages by allowing programmers to write program components in a controlled and structured manner in C++. By imposing structure and restrictions on how applications can be written, Mace supports debugging at a higher level, including support for efficient model checking and causal-path debugging. Because Mace programs compile to C++, programmers can use existing C++ tools, including optimizers, profilers, and debuggers to analyze their systems.

关键词： languages reliability performance Mace domain specific languages model checking debugging distributed systems concurrency event driven programming

来源：评论

学校读者我要写书评

暂无评论

RTL-datapath verification using integer linear programming 7

RTL-datapath verification using integer linear programming

引用

7th Asia and South Pacific design Automation conference/15th International conference on VLSI design

作者： Brinkmann, R Drechsler, R Siemens AG Corp Technol D-81370 Munich Germany

ISBN: (纸本)0769514413

Satisfiability of complex word-level formulas often arises as a problem in formal verification of hardware designs described at the register transfer level (RTL). Even though most designs are described in a hardware description language (HDL), like Verilog or VHDL, usually, this problem is solved in the Boolean domain, using Boolean solvers. These engines often show a poor performance for data path verification. Instead of solving the problem at the bit-level, a method is proposed to transform conjunctions of bitvector equalities and inequalities into sets of integer linear arithmetic constraints. It is shown that it is possible to correctly model the modulo semantics of HDL operators as linear constraints. Integer linear constraint solvers are used as a decision procedure for bitvector arithmetic. In the implementation we focus on verification of arithmetic properties of Verilog-HDL designs. Experimental results show considerable performance advantages over high-end Boolean SAT solver approaches. The speed-up on the benchmarks studied is several orders of magnitude.

关键词： Semantics

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

Thread-modular shape analysis

引用

acm sigplan NOTICES 2007年第6期42卷 266-277页

作者： Gotsman, Alexey Berdine, Josh Cook, Byron Sagiv, Mooly Univ Cambridge Cambridge CB2 1TN England Microsoft Corp Redmond WA 98052 USA

We present the first shape analysis for multithreaded programs that avoids the explicit enumeration of execution-interleavings. Our approach is to automatically infer a resource invariant associated with each lock that describes the part of the heap protected by the lock. This allows us to use a sequential shape analysis on each thread. We show that resource invariants of a certain class can be characterized as least fixed points and computed via repeated applications of shape analysis only on each individual thread. Based on this approach, we have implemented a thread-modular shape analysis tool and applied it to concurrent heap-manipulating code from Windows device drivers.

关键词： abstract interpretation concurrent programming shape analysis static analysis

来源：评论

学校读者我要写书评

暂无评论

It''s Alive! Continuous Feedback in UI programming 13

It''s Alive! Continuous Feedback in UI Programming

引用

acm sigplan conference on programming language design and implementation

作者： Sebastian Burckhardt Peli de Halleux Michal Moskal Manuel Fahndrich Sean McDirmid Nikolai Tillmann Jun Kato Microsoft Research The University of Tokyo

ISBN: (纸本)9781450320146

Live programming allows programmers to edit the code of a running program and immediately see the effect of the code changes. This tightening of the traditional edit-compile-run cycle reduces the cognitive gap between program code and execution, improving the learning experience of beginning programmers while boosting the productivity of seasoned ones. Unfortunately, live programming is difficult to realize in practice as imperative languages lack well-defined abstraction boundaries that make live programming responsive or its feedback comprehensible. This paper enables live programming for user interface programming by cleanly separating the rendering and non-rendering aspects of a UI program, allowing the display to be refreshed on a code change without restarting the program. A type and effect system formalizes this separation and provides an evaluation model that incorporates the code update step. By putting live programming on a more formal footing, we hope to enable critical and technical discussion of live programming systems.

关键词： Live programming Graphical User Interface languages Human Factors

来源：评论

学校读者我要写书评

暂无评论

Automatic generation of DAG parallelism

引用

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

作者： Cytron, Ron Hind, Michael Hsieh, Wilson IBM T.J. Watson Research Cent United States

We present an algorithm for automatically generating a nested, fork-join parallel program from a sequential program represented in terms of control and data dependences. This algorithm embodies two techniques for dealing with data dependences: the first implicitly satisfies such dependences by reducing parallelism, and the second eliminates some dependences by introducing private variables. This algorithm has been implemented in the PTRAN system.

关键词： Computer programming languages

来源：评论

学校读者我要写书评

暂无评论

design OF A FLEXIBLE DISTRIBUTED TESTBED FOR COMMUNICATION SYSTEMS.

DESIGN OF A FLEXIBLE DISTRIBUTED TESTBED FOR COMMUNICATION S...

引用

proceedings of the Twenty-First Annual Hawaii International conference on System Sciences. Volume II: Software Track.

作者： Thoet, William Hauser, James Baker, Dennis Jaycor Jaycor

ISBN: (纸本)0818608420

The structure and design of a simulation testbed for communication systems are described. The testbed, which is called the Distributed Simulation and Prototyping Testbed (DSPT), models the physical-layer activities of communication networks with a design that facilitates the addition of higher-layer protocols either as part of the simulation program itself or as prototype software that can execute concurrently with the simulation on a separate machine. As is typical of R&D systems, the DSPT requirements have evolved with the projects that it supports. The author shows some of the benefits of developing software using the object-oriented methodology in the dynamic R&D environment. The design involved extensions to the Simula programming language, which were easily implemented using Simula's class inheritance capability. The author explores these extensions and discusses further needs of the Simula language that appeared during the implementation of the DPST.

关键词： TELECOMMUNICATION SYSTEMS

来源：评论

学校读者我要写书评

暂无评论

Reconciling Exhaustive Pattern Matching with Objects 13

Reconciling Exhaustive Pattern Matching with Objects

引用

acm sigplan conference on programming language design and implementation

作者： Chinawat Isradisaikul Andrew C. Myers Department of Computer Science Cornell University

ISBN: (纸本)9781450320146

Pattern matching, an important feature of functional languages, is in conflict with data abstraction and extensibility, which are central to object-oriented languages. Modal abstraction offers an integration of deep pattern matching and convenient iteration abstractions into an object-oriented setting; however, because of data abstraction, it is challenging for a compiler to statically verify properties such as exhaustiveness. In this work, we extend modal abstraction in the JMatch language to support static, modular reasoning about exhaustiveness and redundancy. New matching specifications allow these properties to be checked using an SMT solver. We also introduce expressive pattern-matching constructs. Our evaluation shows that these new features enable more concise code and that the performance of checking exhaustiveness and redundancy is acceptable.

关键词： JMatch Pattern matching Named constructor Equality constructor Matching specification Exhaustiveness Redundancy Modal abstraction Java Data abstraction Subtyping design Verification languages

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：