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

43rd acm sigplan International conference on programming language design and implementation, pldi 2022

ISBN: (纸本)9781450392655

The proceedings contain 68 papers. The topics discussed include: modular information flow through ownership;ANOSY: approximated knowledge synthesis with refinement types for declassification;hardening attack surfaces with formally proven binary format parsers;turning manual concurrent memory reclamation into automatic reference counting;low-latency, high-throughput garbage collection;mako: a low-pause, high-throughput evacuating collector for memory-disaggregated datacenters;visualization question answering using introspective program synthesis;synthesizing analytical SQL queries from computation demonstration;sequential reasoning for optimizing compilers under weak memory concurrency;and can reactive synthesis and syntax-guided synthesis be friends?.

关键词：

来源：评论

学校读者我要写书评

暂无评论

pldi 2021 - Proceedings of the 42nd acm sigplan International conference on programming language design and implementation

PLDI 2021 - Proceedings of the 42nd ACM SIGPLAN Internationa...

引用

42nd acm sigplan International conference on programming language design and implementation, pldi 2021

ISBN: (纸本)9781450383912

The proceedings contain 87 papers. The topics discussed include: incremental whole-program analysis in datalog with lattices;revamping hardware persistency models: view-based and axiomatic persistency models for intel-x86 and armv8;repairing serializability bugs in distributed database programs via automated schema refactoring;Gleipnir: toward practical error analysis for quantum programs;transfinite iris: resolving an existential dilemma of step-indexed separation logic;Perceus: garbage free reference counting with reuse;unleashing the hidden power of compiler optimization on binary code difference: an empirical study;RefinedC: automating the foundational verification of C code with refined ownership types;and wire sorts: a language abstraction for safe hardware composition.

关键词：

来源：评论

学校读者我要写书评

暂无评论

pldi 2020 - Proceedings of the 41st acm sigplan conference on programming language design and implementation

PLDI 2020 - Proceedings of the 41st ACM SIGPLAN Conference o...

引用

41st acm sigplan conference on programming language design and implementation, pldi 2020

ISBN: (纸本)9781450376136

The proceedings contain 77 papers. The topics discussed include: data-driven inference of representation invariants;type error feedback via analytic program repair;synthesizing structured CAD models with equality saturation and inverse transformations;compiler and runtime support for continuation marks;from folklore to fact: comparing implementations of stacks and continuations;learning nonlinear loop invariants with gated continuous logic networks;blended, precise semantic program embeddings;and BlankIt library debloating: getting what you want instead of cutting what you don't.

关键词：

来源：评论

学校读者我要写书评

暂无评论

pldi 2019 - Proceedings of the 40th acm sigplan conference on programming language design and implementation

PLDI 2019 - Proceedings of the 40th ACM SIGPLAN Conference o...

引用

40th acm sigplan conference on programming language design and implementation, pldi 2019

ISBN: (纸本)9781450367127

The proceedings contain 76 papers. The topics discussed include: data-trace types for distributed stream processing systems;cost analysis of nondeterministic probabilistic programs;mesh: compacting memory management for C/C++ applications;transactional concurrency control for intermittent, energy-harvesting computing systems;an applied quantum Hoare logic;Ignis: scaling distribution-oblivious systems with light-touch distribution;reusable inline caching for JavaScript performance;synthesizing database programs for schema refactoring;and lightweight multi-language syntax transformation with parser parser combinators.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Proceedings of the acm sigplan conference on programming language design and implementation (pldi)

Proceedings of the ACM SIGPLAN Conference on Programming Lan...

引用

39th acm sigplan conference on programming language design and implementation, pldi 2018

ISBN: (纸本)9781450356985

The proceedings contain 55 papers. The topics discussed include: BLeak: automatically debugging memory leaks in web applications;putting in all the stops: execution control for JavaScript;persistency for synchronization-free regions;write-rationing garbage collection for hybrid memories;mapping spiking neural networks onto a manycore neuromorphic architecture;static serializability analysis for causal consistency;Cuba: interprocedural context-unbounded analysis of concurrent programs;advanced automata-based algorithms for program termination checking;HHVM JIT: a profile-guided, region-based compiler for PHP and Hack;EffectiveSan: type and memory error detection using dynamically typed C/C++;calling-to-reference context translation via constraint-guided CFL-reachability;the semantics of transactions and weak memory in x86, power, ARM, and C++;MixT: a language for mixing consistency in geodistributed transactions;finding root causes of floating point error;to-many or to-one? all-in-one! efficient purely functional multi-maps with type-heterogeneous hash-tries;spatial: a language and compiler for application accelerators;enhancing computation-to-core assignment with physical location information;and SWOOP: so ware-hardware co-design for non-speculative, execute-ahead, in-order cores.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Associated Effects Flexible Abstractions for Effectful programming

引用

PROCEEDINGS OF THE acm ON programming languageS-PacmPL 2024年第PLDI期8卷 394-416页

作者： Lutze, Matthew Madsen, Magnus Aarhus Univ Aarhus Denmark

We present associated effects, a programming language feature that enables type classes to abstract over the effects of their function signatures, allowing each type class instance to specify its concrete effects. Associated effects significantly increase the flexibility and expressive power of a programming language that combines a type and effect system with type classes. In particular, associated effects allow us to (i) abstract over total and partial functions, where partial functions may throw exceptions, (ii) abstract over immutable data structures and mutable data structures that have heap effects, and (iii) implement adaptors that combine type classes with algebraic effects. We implement associated effects as an extension of the Flix programming language and refactor the Flix Standard Library to use associated effects, significantly increasing its flexibility and expressive power. Specifically, we add associated effects to 11 type classes, which enables us to add 28 new type class instances.

关键词： effect systems associated effects associated types generic programming type classes type functions ad-hoc polymorphism

来源：评论

学校读者我要写书评

暂无评论

VESTA: Power Modeling with language Runtime Events

引用

PROCEEDINGS OF THE acm ON programming languageS-PacmPL 2024年第PLDI期8卷 621-646页

作者： Raskind, Joseph Babakol, Timur Mahmoud, Khaled Liu, Yu David SUNY Binghamton Binghamton NY 13902 USA

Power modeling is an essential building block for computer systems in support of energy optimization, energy profiling, and energy-aware application development. We introduce VESTA, a novel approach to modeling the power consumption of applications with one key insight: language runtime events are often correlated with a sustained level of power consumption. When compared with the established approach of power modeling based on hardware performance counters (HPCs), VESTA has the benefit of solely requiring application-scoped information and enabling a higher level of explainability, while achieving comparable or even higher precision. Through experiments performed on 37 real-world applications on the Java Virtual Machine (JVM), we find the power model built by VESTA is capable of predicting energy consumption with a mean absolute percentage error of 1.56%, while the monitoring of language runtime events incurs small performance and energy overhead.

关键词： power modeling language runtimes Java virtual machines BPF

来源：评论

学校读者我要写书评

暂无评论

Compiling Probabilistic Programs for Variable Elimination with Information Flow

引用

PROCEEDINGS OF THE acm ON programming languageS-PacmPL 2024年第PLDI期8卷 1755-1780页

作者： Li, Jianlin Wang, Eric Zhang, Yizhou Univ Waterloo Waterloo ON Canada

A key promise of probabilistic programming is the ability to specify rich models using an expressive programming language. However, the expressive power that makes probabilistic programming languages enticing also poses challenges to inference, so much so that specialized approaches to inference ban language features such as recursion. We present an approach to variable elimination and marginal inference for probabilistic programs featuring bounded recursion, discrete distributions, and sometimes continuous distributions. A compiler eliminates probabilistic side effects, using a novel information-flow type system to factorize probabilistic computations and hoist independent subcomputations out of sums or integrals. For a broad class of recursive programs with dynamically recurring substructure, the compiler effectively decomposes a global marginal-inference problem, which may otherwise be intractable, into tractable subproblems. We prove the compilation correct by showing that it preserves denotational semantics. Experiments show that the compiled programs subsume widely used PTIME algorithms for recursive models and that the compilation time scales with the size of the inference problems. As a separate contribution, we develop a denotational, logical-relations model of information-flow types in the novel measure-theoretic setting of probabilistic programming;we use it to prove noninterference and consequently the correctness of variable elimination.

关键词： Probabilistic programming probabilistic inference information flow

来源：评论

学校读者我要写书评

暂无评论

Descend: A Safe GPU Systems programming language

引用

PROCEEDINGS OF THE acm ON programming languageS-PacmPL 2024年第PLDI期8卷 841-864页

作者： Koepcke, Bastian Gorlatch, Sergei Steuwer, Michel Univ Munster Munster Germany Tech Univ Berlin Berlin Germany

Graphics Processing Units (GPU) offer tremendous computational power by following a throughput oriented paradigm where many thousand computational units operate in parallel. programming such massively parallel hardware is challenging. Programmers must correctly and efficiently coordinate thousands of threads and their accesses to various shared memory spaces. Existing mainstream GPU programming languages, such as CUDA and OpenCL, are based on C/C++ inheriting their fundamentally unsafe ways to access memory via raw pointers. This facilitates easy to make, but hard to detect bugs, such as data races and deadlocks. In this paper, we present Descend: a safe GPU programming language. In contrast to prior safe high-level GPU programming approaches, Descend is an imperative GPU systems programming language in the spirit of Rust, enforcing safe CPU and GPU memory management in the type system by tracking Ownership and Lifetimes. Descend introduces a new holistic GPU programming model where computations are hierarchically scheduled over the GPU's execution resources: grid, blocks, warps, and threads. Descend's extended Borrow checking ensures that execution resources safely access memory regions without data races. For this, we introduced views describing safe parallel access patterns of memory regions, as well as atomic variables. For memory accesses that can't be checked by our type system, users can annotate limited code sections as unsafe. We discuss the memory safety guarantees offered by Descend and evaluate our implementation using multiple benchmarks, demonstrating that Descend is capable of expressing real-world GPU programs showing competitive performance compared to manually written CUDA programs lacking Descend's safety guarantees.

关键词： GPU programming language design memory safety type systems

来源：评论

学校读者我要写书评

暂无评论

A Verified Compiler for a Functional Tensor language

引用

PROCEEDINGS OF THE acm ON programming languageS-PacmPL 2024年第PLDI期8卷 320-342页

作者： Liu, Amanda Bernstein, Gilbert Chlipala, Adam Ragan-Kelley, Jonathan MIT 77 Massachusetts Ave Cambridge MA 02139 USA Univ Washington Seattle WA 98195 USA

Producing efficient array code is crucial in high-performance domains like image processing and machine learning. It requires the ability to control factors like compute intensity and locality by reordering computations into different stages and granularities with respect to where they are stored. However, traditional pure, functional tensor languages struggle to do so. In a previous publication, we introduced ATL as a pure, functional tensor language capable of systematically decoupling compute and storage order via a set of high-level combinators known as reshape operators. Reshape operators are a unique functional-programming construct since they manipulate storage location in the generated code by modifying the indices that appear on the left-hand sides of storage expressions. We present a formal correctness proof for an implementation of the compilation algorithm, marking the first verification of a lowering algorithm targeting imperative loop nests from a source functional language that enables separate control of compute and storage ordering. One of the core difficulties of this proof required properly formulating the complex invariants to ensure that these storage-index remappings were well-formed. Notably, this exercise revealed a soundness bug in the original published compilation algorithm regarding the truncation reshape operators. Our fix is a new type system that captures safety conditions that were previously implicit and enables us to prove compiler correctness for well-typed source programs. We evaluate this type system and compiler implementation on a range of common programs and optimizations, including but not limited to those previously studied to demonstrate performance comparable to established compilers like Halide.

关键词： functional programming array programming formal verification type systems tensors

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：