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

40th acm SIGPLAN-sigact symposium on principles of programming languages

作者： Batty, Mark Dodds, Mike Gotsman, Alexey Univ Cambridge Cambridge CB2 1TN England Univ York York YO10 5DD N Yorkshire England

ISBN: (纸本)9781450318327

When constructing complex concurrent systems, abstraction is vital: programmers should be able to reason about concurrent libraries in terms of abstract specifications that hide the implementation details. Relaxed memory models present substantial challenges in this respect, as libraries need not provide sequentially consistent abstractions: to avoid unnecessary synchronisation, they may allow clients to observe relaxed memory effects, and library specifications must capture these. In this paper, we propose a criterion for sound library abstraction in the new C11 and C++11 memory model, generalising the standard sequentially consistent notion of linearizability. We prove that our criterion soundly captures all client-library interactions, both through call and return values, and through the subtle synchronisation effects arising from the memory model. To illustrate our approach, we verify implementations against specifications for the lock-free Treiber stack and a producer-consumer queue. Ours is the first approach to compositional reasoning for concurrent C11/C++11 programs.

关键词： languages Theory Verification Verification Concurrency Modularity C C plus

来源：评论

学校读者我要写书评

暂无评论

The Ramifications of Sharing in Data Structures

The Ramifications of Sharing in Data Structures

引用

40th acm SIGPLAN-sigact symposium on principles of programming languages

作者： Hobor, Aquinas Villard, Jules Natl Univ Singapore Singapore Singapore UCL London WC1E 6BT England

ISBN: (纸本)9781450318327

Programs manipulating mutable data structures with intrinsic sharing present a challenge for modular verification. Deep aliasing inside data structures dramatically complicates reasoning in isolation over parts of these objects because changes to one part of the structure (say, the left child of a dag node) can affect other parts (the right child or some of its descendants) that may point into it. The result is that finding intuitive and compositional proofs of correctness is usually a struggle. We propose a compositional proof system that enables local reasoning in the presence of sharing. While the AI "frame problem" elegantly captures the reasoning required to verify programs without sharing, we contend that natural reasoning about programs with sharing instead requires an answer to a different and more challenging AI problem, the "ramification problem": reasoning about the indirect consequences of actions. Accordingly, we present a RAMIFY proof rule that attacks the ramification problem head-on and show how to reason with it. Our framework is valid in any separation logic and permits sound compositional and local reasoning in the context of both specified and unspecified sharing. We verify the correctness of a number of examples, including programs that manipulate dags, graphs, and overlaid data structures in nontrivial ways.

关键词： languages Theory Verification Aliasing Heap/Shape Modularity Separation logic

来源：评论

学校读者我要写书评

暂无评论

Towards Fully Automatic Placement of Security Sanitizers and Declassifiers

Towards Fully Automatic Placement of Security Sanitizers and...

引用

40th acm SIGPLAN-sigact symposium on principles of programming languages

作者： Livshits, Benjamin Chong, Stephen Harvard Univ Cambridge MA 02138 USA

ISBN: (纸本)9781450318327

A great deal of research on sanitizer placement, sanitizer correctness, checking path validity, and policy inference, has been done in the last five to ten years, involving type systems, static analysis and run-time monitoring and enforcement. However, in pretty much all work thus far, the burden of sanitizer placement has fallen on the developer. However, sanitizer placement in large-scale applications is difficult, and developers are likely to make errors, and thus create security vulnerabilities. This paper advocates a radically different approach: we aim to fully automate the placement of sanitizers by analyzing the flow of tainted data in the program. We argue that developers are better off leaving out sanitizers entirely instead of trying to place them. This paper proposes a fully automatic technique for sanitizer placement. Placement is static whenever possible, switching to run time when necessary. Run-time taint tracking techniques can be used to track the source of a value, and thus apply appropriate sanitization. However, due to the run-time overhead of run-time taint tracking, our technique avoids it wherever possible.

关键词： languages Security Verification Security analysis vulnerability prevention

来源：评论

学校读者我要写书评

暂无评论

The Type Discipline of Behavioral Separation

The Type Discipline of Behavioral Separation

引用

40th acm SIGPLAN-sigact symposium on principles of programming languages

作者： Caires, Luis Seco, Joao C. Univ Nova Lisboa CITI Fac Ciencias & Tecnol P-1200 Lisbon Portugal Univ Nova Lisboa Dept Informat Fac Ciencias & Tecnol P-1200 Lisbon Portugal

ISBN: (纸本)9781450318327

We introduce the concept of behavioral separation as a general principle for disciplining interference in higher-order imperative concurrent programs, and present a type-based approach that systematically develops the concept in the context of an ML-like language extended with concurrency and synchronization primitives. Behavioral separation builds on notions originally introduced for behavioral type systems and separation logics, but shifts the focus from the separation of static program state properties towards the separation of dynamic usage behaviors of runtime values. Behavioral separation types specify how values may be safely used by client code, and can enforce fine-grained interference control disciplines while preserving compositionality, information hiding, and flexibility. We illustrate how our type system, even if based on a small set of general primitives, is already able to tackle fairly challenging program idioms, involving aliasing at various types, concurrency with first-class threads, manipulation of linked data structures, behavioral borrowing, and invariant-based separation.

关键词： Behavioral Types Separation Interference Concurrency Higher Order programming

来源：评论

学校读者我要写书评

暂无评论

Fault Tolerance via Idempotence

Fault Tolerance via Idempotence

引用

40th acm SIGPLAN-sigact symposium on principles of programming languages

作者： Ramalingam, G. Vaswani, Kapil Microsoft Research Bangalore India

ISBN: (纸本)9781450318327

Building distributed services and applications is challenging due to the pitfalls of distribution such as process and communication failures. A natural solution to these problems is to detect potential failures, and retry the failed computation and/or resend messages. Ensuring correctness in such an environment requires distributed services and applications to be idempotent. In this paper, we study the inter-related aspects of process failures, duplicate messages, and idempotence. We first introduce a simple core language (based on lambda-calculus) inspired by modern distributed computing platforms. This language formalizes the notions of a service, duplicate requests, process failures, data partitioning, and local atomic transactions that are restricted to a single store. We then formalize a desired (generic) correctness criterion for applications written in this language, consisting of idempotence (which captures the desired safety properties) and failure-freedom (which captures the desired progress properties). We then propose language support in the form of a monad that automatically ensures failfree idempotence. A key characteristic of our implementation is that it is decentralized and does not require distributed coordination. We show that the language support can be enriched with other useful constructs, such as compensations, while retaining the coordination-free decentralized nature of the implementation. We have implemented the idempotence monad (and its variants) in F# and C# and used our implementation to build realistic applications on Windows Azure. We find that the monad has low runtime overheads and leads to more declarative applications.

关键词： Reliability languages Design fault tolerance idempotence workflow transaction monad

来源：评论

学校读者我要写书评

暂无评论

Sigma*: Symbolic Learning of Input-Output Specifications

Sigma*: Symbolic Learning of Input-Output Specifications

引用

40th acm SIGPLAN-sigact symposium on principles of programming languages

作者： Botincan, Matko Babic, Domagoj Univ Cambridge Cambridge CB2 1TN England Univ Calif Berkeley Berkeley CA USA

ISBN: (纸本)9781450318327

We present Sigma*, a novel technique for learning symbolic models of software behavior. Sigma* addresses the challenge of synthesizing models of software by using symbolic conjectures and abstraction. By combining dynamic symbolic execution to discover symbolic input-output steps of the programs and counterexample guided abstraction refinement to over-approximate program behavior, Sigma* transforms arbitrary source representation of programs into faithful input-output models. We define a class of stream filters-programs that process streams of data items-for which Sigma* converges to a complete model if abstraction refinement eventually builds up a sufficiently strong abstraction. In other words, Sigma* is complete relative to abstraction. To represent inferred symbolic models, we use a variant of symbolic transducers that can be effectively composed and equivalence checked. Thus, Sigma* enables fully automatic analysis of behavioral properties such as commutativity, reversibility and idempotence, which is useful for web sanitizer verification and stream programs compiler optimizations, as we show experimentally. We also show how models inferred by Sigma* can boost performance of stream programs by parallelized code generation.

关键词： languages Theory Verification Inductive learning Specification synthesis Behavioral properties Equivalence checking Stream programs Compiler optimization Parallelization

来源：评论

学校读者我要写书评

暂无评论

POPL'12 - Proceedings of the 39th Annual acm SIGPLAN-sigact symposium on principles of programming languages

POPL'12 - Proceedings of the 39th Annual ACM SIGPLAN-SIGACT ...

引用

39th Annual acm SIGPLAN-sigact symposium on principles of programming languages, POPL'12

ISBN: (纸本)9781450310833

The proceedings contain 44 papers. The topics discussed include: underspecified harnesses and interleaved bugs;towards a program logic for JavaScript;higher-order functional reactive programming in bounded space;the marriage of bisimulations and Kripke logical relations;information effects;a language for automatically enforcing privacy policies;probabilistic relational reasoning for differential privacy;access permission contracts for scripting languages;recursive proofs for inductive tree data-structures;symbolic finite state transducers: algorithms and applications;multiple facets for dynamic information flow;deciding choreography realizability;programming languages for programmable networks;a compiler and run-time system for network programming languages;an abstract interpretation framework for termination;run your research: on the effectiveness of lightweight mechanization;and verification of parameterized concurrent programs by modular reasoning about data and control.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Linear Dependent Types for Differential Privacy

Linear Dependent Types for Differential Privacy

引用

40th acm SIGPLAN-sigact symposium on principles of programming languages

作者： Gaboardi, Marco Haeberlen, Andreas Hsu, Justin Narayan, Arjun Pierce, Benjamin C. Univ Penn Philadelphia PA 19104 USA Univ Bologna INRIA EPI Focus I-40126 Bologna Italy

ISBN: (纸本)9781450318327

Differential privacy offers a way to answer queries about sensitive information while providing strong, provable privacy guarantees, ensuring that the presence or absence of a single individual in the database has a negligible statistical effect on the query's result. Proving that a given query has this property involves establishing a bound on the query's sensitivity-how much its result can change when a single record is added or removed. A variety of tools have been developed for certifying that a given query is differentially private. In one approach, Reed and Pierce [34] proposed a functional programming language, Fuzz, for writing differentially private queries. Fuzz uses linear types to track sensitivity and a probability monad to express randomized computation;it guarantees that any program with a certain type is differentially private. Fuzz can successfully verify many useful queries. However, it fails when the sensitivity analysis depends on values that are not known statically. We present DFuzz, an extension of Fuzz with a combination of linear indexed types and lightweight dependent types. This combination allows a richer sensitivity analysis that is able to certify a larger class of queries as differentially private, including ones whose sensitivity depends on runtime information. As in Fuzz, the differential privacy guarantee follows directly from the soundness theorem of the type system. We demonstrate the enhanced expressivity of DFuzz by certifying differential privacy for a broad class of iterative algorithms that could not be typed previously.

关键词： Design languages Theory differential privacy type systems linear logic dependent types

来源：评论

学校读者我要写书评

暂无评论

HALO: Haskell to Logic through Denotational Semantics

引用

acm SIGPLAN NOTICES 2013年第1期48卷 431-442页

作者： Vytiniotis, Dimitrios Jones, Simon Peyton Rosen, Dan Claessen, Koen Chalmers Univ Gothenburg Sweden

Even well-typed programs can go wrong in modern functional languages, by encountering a pattern-match failure, or simply returning the wrong answer. An increasingly-popular response is to allow programmers to write contracts that express semantic properties, such as crash-freedom or some useful post-condition. We study the static verification of such contracts. Our main contribution is a novel translation to first-order logic of both Haskell programs, and contracts written in Haskell, all justified by denotational semantics. This translation enables us to prove that functions satisfy their contracts using an off-the-shelf first-order logic theorem prover.

关键词： verification languages static contract checking first-order logic

来源：评论

学校读者我要写书评

暂无评论

Cache and I/O Efficient Functional Algorithms

Cache and I/O Efficient Functional Algorithms

引用

40th acm SIGPLAN-sigact symposium on principles of programming languages

作者： Blelloch, Guy E. Harper, Robert Carnegie Mellon Univ Pittsburgh PA 15213 USA

The widely studied I/O and ideal-cache models were developed to account for the large difference in costs to access memory at different levels of the memory hierarchy. Both models are based on a two level memory hierarchy with a fixed size primary memory (cache) of size M, an unbounded secondary memory organized in blocks of size B. The cost measure is based purely on the number of block transfers between the primary and secondary memory. All other operations are free. Many algorithms have been analyzed in these models and indeed these models predict the relative performance of algorithms much more accurately than the standard RAM model. The models, however, require specifying algorithms at a very low level requiring the user to carefully lay out their data in arrays in memory and manage their own memory allocation. In this paper we present a cost model for analyzing the memory efficiency of algorithms expressed in a simple functional language. We show how some algorithms written in standard forms using just lists and trees (no arrays) and requiring no explicit memory layout or memory management are efficient in the model. We then describe an implementation of the language and show provable bounds for mapping the cost in our model to the cost in the ideal-cache model. These bound imply that purely functional programs based on lists and trees with no special attention to any details of memory layout can be as asymptotically as efficient as the carefully designed imperative I/O efficient algorithms. For example we describe an O (n/B log(M)/(B) n/B) cost sorting algorithm, which is optimal in the ideal cache and I/O models.

关键词： Algorithms Design languages Performance Theory cost semantics I/O algorithms

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：