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

Multiparty asynchronous session types

acm SIGPLAN NOTICES 2008年第1期43卷 273-284页

作者： Honda, Kohei Yoshida, Nobuko Carbone, Marco Univ London London WC1E 7HU England Univ London Imperial Coll Sci Technol & Med London SW7 2AZ England

Communication is becoming one of the central elements in software development. As a potential typed foundation for structured communication-centred programming, session types have been studied over the last decade for a wide range of process calculi and programming languages, focussing on binary (two-party) sessions. This work extends the foregoing theories of binary session types to multiparty, asynchronous sessions, which often arise in practical communication-centred applications. Presented as a typed calculus for mobile processes, the theory introduces a new notion of types in which interactions involving multiple peers are directly abstracted as a global scenario. Global types retain a friendly type syntax of binary session types while capturing complex causal chains of multiparty asynchronous interactions. A global type plays the role of a shared agreement among communication peers, and is used as a basis of efficient type checking through its projection onto individual peers. The fundamental properties of the session type discipline such as communication safety, progress and session fidelity are established for general n-party asynchronous interactions.

关键词： theory types design communications multiparty structured programming session types mobile processes causality choreography

来源：评论

学校读者我要写书评

暂无评论

A theory of platform-dependent low-level software

引用

acm SIGPLAN NOTICES 2008年第1期43卷 209-220页

作者： Nita, Marius Grossman, Dan Chambers, Craig Univ Washington Dept Comp Sci & Engn Seattle WA 98195 USA

The C language definition leaves the sizes and layouts of types partially unspecified. When a C program makes assumptions about type layout, its semantics is defined only on platforms (C compilers and the underlying hardware) on which those assumptions hold. Previous work on formalizing C-like languages has ignored this issue, either by assuming that programs do not make such assumptions or by assuming that all valid programs target only one platform. In the latter case, the platform's choices are hard-wired in the language semantics. In this paper, we present a practically-motivated model for a C-like language in which the memory layouts of types are left largely unspecified. The dynamic semantics is parameterized by a platform's layout policy and makes manifest the consequence of platform-dependent (i.e., unspecified) steps. A type-and-effect system produces a layout constraint: a logic formula encoding layout conditions under which the program is memory-safe. We prove that if a program type-checks, it is memory-safe on all platforms satisfying its constraint. Based on our theory, we have implemented a tool that discovers unportable layout assumptions in C programs. Our approach should generalize to other kinds of platform-dependent assumptions.

关键词： languages verification theory

来源：评论

学校读者我要写书评

暂无评论

Caml trading 08

Caml trading

引用

Proceedings of the 35th annual acm SIGPLAN-sigact symposium on principles of programming languages

作者： Yaron M. Minsky Jane Street Capital New York NY

ISBN: (纸本)9781595936899

Jane Street Capital is a successful proprietary trading company that has shifted from developing software in mainstream programming languages to developing software almost entirely in OCaml, a statically typed functional programming language that has only modest industrial use. The scope of the enterprise is small but growing: Jane Street now has over 20 OCaml programmers that have collectively written hundreds of thousands of lines of OCaml code. OCaml is used for building everything from trading systems to research infrastructure to user interfaces to systems administration tools. This talk will discuss the motivations behind Jane Street's adoption of OCaml, and why we think that statically typed functional programming languages are such a good fit for the world of trading and finance.

关键词： ML functional programming

来源：评论

学校读者我要写书评

暂无评论

Contextual effects for version-consistent dynamic software updating and safe concurrent programming

引用

acm SIGPLAN NOTICES 2008年第1期43卷 37-49页

作者： Neamtiu, Iulian Hicks, Michael Foster, Jeffrey S. Pratikakis, Polyvios Univ Maryland Dept Comp Sci College Pk MD 20742 USA

This paper presents a generalization of standard effect systems that we call contextual effects. A traditional effect system computes the effect of an expression e. Our system additionally computes the effects of the computational context in which e occurs. More specifically, we compute the effect of the computation that has already occurred (the prior effect) and the effect of the computation yet to take place (the future effect). Contextual effects are useful when the past or future computation of the program is relevant at various program points. We present two substantial examples. First, we show how prior and future effects can be used to enforce transactional version consistency (TVC), a novel correctness property for dynamic software updates. TVC ensures that programmer-designated transactional code blocks appear to execute entirely at the same code version, even if a dynamic update occurs in the middle of the block. Second, we show how future effects can be used in the analysis of multi-threaded programs to find thread-shared locations. This is an essential step in applications such as data race detection.

关键词： languages reliability theory verification contextual effects computation effects type and effect systems version consistency dynamic software updating data race detection

来源：评论

学校读者我要写书评

暂无评论

Foundations for structured programming with GADTs

引用

acm SIGPLAN NOTICES 2008年第1期43卷 297-308页

作者： Johann, Patricia Ghani, Neil Rutgers State Univ Camden NJ 08102 USA Univ Nottingham Nottingham NG7 2RD England

GADTs are at the cutting edge of functional programming and become more widely used every day. Nevertheless, the semantic foundations underlying GADTs are not well understood. In this paper we solve this problem by showing that the standard theory of data types as carriers of initial algebras of functors can be extended from algebraic and nested data types to GADTs. We then use this observation to derive an initial algebra semantics for GADTs, thus ensuring that all of the accumulated knowledge about initial algebras can be brought to bear on them. Next, we use our initial algebra semantics for GADTs to derive expressive and principled tools analogous to the well-known and widely-used ones for algebraic and nested data types - for reasoning about, programming with, and improving the performance of programs involving, GADTs;we christen such a collection of tools for a GADT an initial algebra package. Along the way, we give a constructive demonstration that every GADT can be reduced to one which uses only the equality GADT and existential quantification. Although other such reductions exist in the literature, ours is entirely local, is independent of any particular syntactic presentation of GADTs, and can be implemented in the host language, rather than existing solely as a metatheoretical artifact. The main technical ideas underlying our approach are (i) to modify the notion of a higher-order functor so that GADTs can be seen as carriers of initial algebras of higher-order functors, and (ii) to use left Kan extensions to trade arbitrary GADTs for simpler-but-equivalent ones for which initial algebra semantics can be derived.

关键词： languages theory

来源：评论

学校读者我要写书评

暂无评论

Generating precise and concise procedure summaries

引用

acm SIGPLAN NOTICES 2008年第1期43卷 221-234页

作者： Yorsh, Greta Yahav, Eran Chandra, Satish Tel Aviv Univ Tel Aviv Israel

We present a framework for generating procedure summaries that are precise - applying the summary in a given context yields the same result as re-analyzing the procedure in that context, and concise - the summary exploits the commonalities in the ways the procedure manipulates abstract values, and does not contain superfluous context information. The use of a precise and concise procedure summary in modular analyses provides a way to capture infinitely many possible contexts in a finite way;in interprocedural analyses, it provides a compact representation of an explicit input-output summary table without loss of precision. We define a class of abstract domains and transformers for which precise and concise summaries can be efficiently generated using our framework. Our framework is rich enough to encode a wide range of problems, including all IFDS and IDE problems. In addition, we show how the framework is instantiated to provide novel solutions to two hard problems: modular linear constant propagation and modular typestate verification, both in the presence of aliasing. We implemented a prototype of our framework that computes summaries for the typestate domain, and report on preliminary experimental results.

关键词： verification reliability languages algorithms summarization composition relational analysis symbolic summary typestate verification aliasing dataflow analysis micro-transformers

来源：评论

学校读者我要写书评

暂无评论

Relational inductive shape analysis

引用

acm SIGPLAN NOTICES 2008年第1期43卷 247-260页

作者： Chang, Bor-Yuh Evan Rival, Xavier Univ Calif Berkeley Berkeley CA 94720 USA INRIA Berkeley CA USA

Shape analyses are concerned with precise abstractions of the heap to capture detailed structural properties. To do so, they need to build and decompose summaries of disjoint memory regions. Unfortunately, many data structure invariants require relations be tracked across disjoint regions, such as intricate numerical data invariants or structural invariants concerning back and cross pointers. In this paper, we identify issues inherent to analyzing relational structures and design an abstract domain that is parameterized both by an abstract domain for pure data properties and by user-supplied specifications of the data structure invariants to check. Particularly, it supports hybrid invariants about shape and data and features a generic mechanism for materializing summaries at the beginning, middle, or end of inductive structures. Around this domain, we build a shape analysis whose interesting components include a pre-analysis on the user-supplied specifications that guides the abstract interpretation and a widening operator over the combined shape and data domain. We then demonstrate our techniques on the proof of preservation of the red-black tree invariants during insertion.

关键词： languages verification shape analysis inductive definitions heap analysis separation logic symbolic abstract domain materialization

来源：评论

学校读者我要写书评

暂无评论

Enhancing modular OO verification with separation logic

引用

acm SIGPLAN NOTICES 2008年第1期43卷 87-99页

作者： Chin, Wei-Ngan David, Cristina Nguyen, Huu Hai Qin, Shengchao Natl Univ Singapore Dept Comp Sci Singapore 117548 Singapore Singapore MIT Alliance Comp Sci Program Singapore Singapore Univ Durham Dept Comp Sci Durham DH1 3HP England

Conventional specifications for object-oriented (OO) programs must adhere to behavioral subtyping in support of class inheritance and method overriding. However, this requirement inherently weakens the specifications of overridden methods in superclasses, leading to imprecision during program reasoning. To address this, we advocate a fresh approach to OO verification that focuses on the distinction and relation between specifications that cater to calls with static dispatching from those for calls with dynamic dispatching. We formulate a novel specification subsumption that can avoid code re-verification, where possible. Using a predicate mechanism, we propose a flexible scheme for supporting class invariant and lossless casting. Our aim is to lay the foundation for a practical verification system that is precise, concise and modular for sequential OO programs. We exploit the separation logic formalism to achieve this.

关键词： languages theory verification automated verification enhanced subsumption separation logic lossless casting static and dynamic specifications

来源：评论

学校读者我要写书评

暂无评论

A theory of contracts for web services

引用

acm SIGPLAN NOTICES 2008年第1期43卷 261-272页

作者： Castagna, Giuseppe Gesbert, Nils Padovani, Luca Univ Paris 07 CNRS PPS Paris France Univ Paris 11 CNRS LRI F-91405 Orsay France Univ Urbino ISTI I-61029 Urbino Italy

Contracts are behavioural descriptions of Web services. We devise a theory of contracts that formalises the compatibility of a client to a service, and the safe replacement of a service with another service. The use of contracts statically ensures the successful completion of every possible interaction between compatible clients and services. The technical device that underlies the theory is the definition of filters, which are explicit coercions that prevent some possible behaviours of services and, in doing so, they make services compatible with different usage scenarios. We show that filters can be seen as proofs of a sound and complete subcontracting deduction system which simultaneously refines and extends Hennessy's classical axiomatisation of the must testing preorder. The relation is decidable and the decision algorithm is obtained via a cut-elimination process that proves the coherence of subcontracting as a logical system. Despite the richness of the technical development, the resulting approach is based on simple ideas and basic intuitions. Remarkably, its application is mostly independent of the language used to program the services or the clients. We also outline the possible practical impact of such a work and the perspectives of future research it opens.

关键词： languages standardization theory Web services contracts concurrency theory CCS must testing type theory subtyping explicit coercions

来源：评论

学校读者我要写书评

暂无评论

Demand-driven alias analysis for C

引用

acm SIGPLAN NOTICES 2008年第1期43卷 197-208页

作者： Zheng, Xin Rugina, Radu Cornell Univ Dept Comp Sci Ithaca NY 14853 USA

This paper presents a demand-driven, flow-insensitive analysis algorithm for answering may-alias queries. We formulate the computation of alias queries as a CFL-reachability problem, and use this formulation to derive a demand-driven analysis algorithm. The analysis uses a worklist algorithm that gradually explores the program structure and stops as soon as enough evidence is gathered to answer the query. Unlike existing techniques, our approach does not require building or intersecting points-to sets. Experiments show that our technique is effective at answering alias queries accurately and efficiently in a demand-driven fashion. For a set of alias queries from the SPEC2000 benchmarks, an implementation of our analysis is able to accurately answer 96% of the queries in 0.5 milliseconds per query on average, using only 65 KB of memory. Compared to a demand-driven points-to analysis that constructs and intersects points-to sets on the fly, our alias analysis can achieve better accuracy while running more than 30 times faster. The low run-time cost and low memory demands of the analysis make it a very good candidate not only for compilers, but also for interactive tools, such as program understanding tools or integrated development environments (IDEs).

关键词： algorithms languages pointer analysis alias analysis memory disambiguation demand-driven analysis CFL reachability

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：