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

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.

关键词：

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

DSLs in Racket: YouWant It How, Now? 17

DSLs in Racket: YouWant It How, Now?

引用

17th ACM sigplan International conference on Software language Engineering (SLE)

作者： Lee, Yunjeong Gopinathan, Kiran Yang, Ziyi Flatt, Matthew Sergey, Ilya Natl Univ Singapore Singapore Singapore Univ Utah Salt Lake City UT USA

ISBN: (纸本)9798400711800

Domain-Specific languages (DSLs) are a popular way to simplify and streamline programmatic solutions of commonly occurring yet specialized tasks. While the design of frameworks for implementing DSLs has been a popular topic of study in the research community, significantly less attention has been given to studying how those frameworks end up being used by practitioners and assessing utility of their features for building DSLs "in the wild". In this paper, we conduct such a study focusing on a particular framework for DSL construction: the Racket programming language. We provide (a) a novel taxonomy of language design intents enabled by Racket-embedded DSLs, and (b) a classification of ways to utilize Racket's mechanisms that make the implementation of those intents possible. We substantiate our taxonomy with an analysis of 30 popular Racket-based DSLs, discussing how they make use of the available mechanisms and accordingly achieve their design intents. The taxonomy serves as a reusable measure that can help language designers to systematically develop, compare, and analyze DSLs in Racket as well as other frameworks.

关键词： domain-specific languages meta-programming

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：