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

GenSQL: A Probabilistic programming System for Querying Generative Models of Database Tables

PROCEEDINGS OF THE ACM ON programming languageS-PACMPL 2024年第PLDI期8卷 790-815页

作者： Huot, Mathieu Ghavami, Matin Lew, Alexander K. Schaechtle, Ulrich Freer, Cameron E. Shelby, Zane Rinard, Martin C. Saad, Feras A. Mansinghka, Vikash K. MIT Cambridge MA 02139 USA Digital Garage Tokyo Japan Carnegie Mellon Univ Pittsburgh PA USA

This article presents GenSQL, a probabilistic programming system for querying probabilistic generative models of database tables. By augmenting SQL with only a few key primitives for querying probabilistic models, GenSQL enables complex Bayesian inference workflows to be concisely implemented. GenSQL's query planner rests on a unified programmatic interface for interacting with probabilistic models of tabular data, which makes it possible to use models written in a variety of probabilistic programming languages that are tailored to specific workflows. Probabilistic models may be automatically learned via probabilistic program synthesis, hand-designed, or a combination of both. GenSQL is formalized using a novel type system and denotational semantics, which together enable us to establish proofs that precisely characterize its soundness guarantees. We evaluate our system on two case real-world studies-an anomaly detection in clinical trials and conditional synthetic data generation for a virtual wet lab-and show that GenSQL more accurately captures the complexity of the data as compared to common baselines. We also show that the declarative syntax in GenSQL is more concise and less error-prone as compared to several alternatives. Finally, GenSQL delivers a 1.7-6.8x speedup compared to its closest competitor on a representative benchmark set and runs in comparable time to hand-written code, in part due to its reusable optimizations and code specialization.

关键词： generative modeling Bayesian data science probabilistic query language

来源：评论

学校读者我要写书评

暂无评论

Guaranteed Bounds for Posterior Inference in Universal Probabilistic programming 2022

Guaranteed Bounds for Posterior Inference in Universal Proba...

引用

43rd ACM sigplan International conference on programming language design and implementation (PLDI)

作者： Beutner, Raven Ong, C-H Luke Zaiser, Fabian CISPA Helmholtz Ctr Informat Secur Saarbrucken Germany Univ Oxford Oxford England

ISBN: (纸本)9781450392655

We propose a new method to approximate the posterior distribution of probabilistic programs by means of computing guaranteed bounds. The starting point of our work is an interval-based trace semantics for a recursive, higher-order probabilistic programming language with continuous distributions. Taking the form of (super-/subadditive) measures, these lower/upper bounds are non-stochastic and provably correct: using the semantics, we prove that the actual posterior of a given program is sandwiched between the lower and upper bounds (soundness);moreover, the bounds converge to the posterior (completeness). As a practical and sound approximation, we introduce a weight-aware interval type system, which automatically infers interval bounds on not just the return value but also the weight of program executions, simultaneously. We have built a tool implementation, called GuBPI, which automatically computes these posterior lower/upper bounds. Our evaluation on examples from the literature shows that the bounds are useful, and can even be used to recognise wrong outputs from stochastic posterior inference procedures.

关键词： probabilistic programming Bayesian inference verification abstract interpretation operational semantics interval arithmetic type system symbolic execution

来源：评论

学校读者我要写书评

暂无评论

IRDL: An IR Definition language for SSA Compilers 2022

IRDL: An IR Definition Language for SSA Compilers

引用

43rd ACM sigplan International conference on programming language design and implementation (PLDI)

作者： Fehr, Mathieu Niu, Jeff Riddle, River Amini, Mehdi Su, Zhendong Grosser, Tobias Univ Edinburgh Edinburgh Midlothian Scotland Univ Waterloo Waterloo ON Canada Modular AI Seattle WA USA Google Mountain View CA USA Swiss Fed Inst Technol Zurich Switzerland

ISBN: (纸本)9781450392655

designing compiler intermediate representations (IRs) is often a manual process that makes exploration and innovation in this space costly. Developers typically use general-purpose programming languages to design IRs. As a result, IR implementations are verbose, manual modifications are expensive, and designing tooling for the inspection or generation of IRs is impractical. While compilers relied historically on a few slowly evolving IRs, domain-specific optimizations and specialized hardware motivate compilers to use and evolve many IRs. We facilitate the implementation of SSA-based IRs by introducing IRDL, a domain-specific language to define IRs. We analyze all 28 domain-specific IRs developed as part of LLVM's MLIR project over the last two years and demonstrate how to express these IRs exclusively in IRDL while only rarely falling back to IRDL's support for generic C++ extensions. By enabling the concise and explicit specification of IRs, we provide foundations for developing effective tooling to automate the compiler construction process.

关键词： Compilers Intermediate Representation MLIR

来源：评论

学校读者我要写书评

暂无评论

Recursion Synthesis with Unrealizability Witnesses 2022

Recursion Synthesis with Unrealizability Witnesses

引用

43rd ACM sigplan International conference on programming language design and implementation (PLDI)

作者： Farzan, Azadeh Lette, Danya Nicolet, Victor Univ Toronto Dept Comp Sci Toronto ON Canada

ISBN: (纸本)9781450392655

We propose SE(2)GIS, a novel inductive recursion synthesis approach with the ability to both synthesize code and declare a problem unsolvable. SE(2)GIS combines a symbolic variant of counterexample-guided inductive synthesis (CEGIS) with a new dual inductive procedure, which focuses on proving a synthesis problem unsolvable rather than finding a solution for it. A vital component of this procedure is a new algorithm that produces a witness, a set of concrete assignments to relevant variables, as a proof that the synthesis instance is not solvable. Witnesses in the dual inductive procedure play the same role that solutions do in classic CEGIS;that is, they ensure progress. Given a reference function, invariants on the input recursive data types, and a target family of recursive functions, SE(2)GIS synthesizes an implementation in this family that is equivalent to the reference implementation, or declares the problem unsolvable and produces a witness for it. We demonstrate that SE(2)GIS is effective in both cases;that is, for interesting data types with complex invariants, it can synthesize non-trivial recursive functions or output witnesses that contain useful feedback for the user.

关键词： Program Synthesis Functional programming Invariants Unrealizability Recursion Abstraction

来源：评论

学校读者我要写书评

暂无评论

PyLSE: A Pulse-Transfer Level language for Superconductor Electronics 2022

PyLSE: A Pulse-Transfer Level Language for Superconductor El...

引用

43rd ACM sigplan International conference on programming language design and implementation (PLDI)

作者： Christensen, Michael Tzimpragos, Georgios Kringen, Harlan Volk, Jennifer Sherwood, Timothy Hardekopf, Ben UC Santa Barbara Santa Barbara CA 93106 USA UC Santa Barbara Dept Elect & Comp Engn Santa Barbara CA USA

ISBN: (纸本)9781450392655

Superconductor electronics (SCE) run at hundreds of GHz and consume only a fraction of the dynamic power of CMOS, but are naturally pulse-based, and operate on impulses with picosecond widths. The transiency of these operations necessitates using logic cells that are inherently stateful. Adopting stateful gates, however, implies an entire reconstruction of the design, simulation, and verification stack. Though challenging, this unique opportunity allows us to build a design framework from the ground up using fundamental principles of programming language design. To this end, we propose PyLSE, an embedded pulse-transfer level language for superconductor electronics. We define PyLSE through formal semantics based on transition systems, and build a framework around them to simulate and analyze SCE cells digitally. To demonstrate its features, we verify its results by model checking in UPPAAL, and compare its complexity and timing against a set of cells designed as analog circuit schematics and simulated in Cadence.

关键词： superconductor electronics hardware description language timed automata

来源：评论

学校读者我要写书评

暂无评论

Morello MicroPython: A Python Interpreter for CHERI 20

Morello MicroPython: A Python Interpreter for CHERI

引用

20th ACM sigplan International conference on Managed programming languages and Runtimes (MPLR)

作者： Lowther, Duncan Jacob, Dejice Singer, Jeremy Univ Glasgow Glasgow Scotland

ISBN: (纸本)9798400703805

Arm Morello is a prototype system that supports CHERI hardware capabilities for improving runtime security. As Morello becomes more widely available, there is a growing effort to port open source code projects to this novel platform. Although high-level applications generally need minimal code refactoring for CHERI compatibility, low-level systems code bases require significant modification to comply with the stringent memory safety constraints that are dynamically enforced by Morello. In this paper, we describe our work on porting the MicroPython interpreter to Morello with the CheriBSD OS. Our key contribution is to present a set of generic lessons for adapting managed runtime execution environments to CHERI, including (1) a characterization of necessary source code changes, (2) an evaluation of runtime performance of the interpreter on Morello, and (3) a demonstration of pragmatic memory safety bug detection. Although MicroPython is a lightweight interpreter, mostly written in C, we believe that the changes we have implemented and the lessons we have learned are more widely applicable. To the best of our knowledge, this is the first published description of meaningful experience for scripting language runtime engineering with CHERI and Morello.

关键词： CHERI capabilities software implementation

来源：评论

学校读者我要写书评

暂无评论

BatakJava: An Object-Oriented programming language with Versions 15

BatakJava: An Object-Oriented Programming Language with Vers...

引用

15th International conference on Software language Engineering (SLE)

作者： Lubis, Luthfan Anshar Tanabe, Yudai Aotani, Tomoyuki Masuhara, Hidehiko Tokyo Inst Technol Tokyo Japan Mamezou Co Ltd Tokyo Japan

ISBN: (纸本)9781450399197

programming with versions is a recent proposal that supports multiple versions of software components in a program. Though it would provide greater freedom for the programmer, the concept is only realized as a simple core calculus, called..VL, where a value consists of lambda-terms with multiple versions. We explore a design space of programming with versions in the presence of data structures and module systems, and propose BatakJava, an object-oriented programming language in which multiple versions of a class can be used in a program. This paper presents BatakJava's language design, its core semantics with subject reduction, an implementation as a source-to-Java translator, and a case study to understand how we can exploit multiple versions in BatakJava for developing an application program with an evolving library.

关键词： backward compatibility dependency problem Java

来源：评论

学校读者我要写书评

暂无评论

A Study of Real-World Data Races in Golang 2022

A Study of Real-World Data Races in Golang

引用

43rd ACM sigplan International conference on programming language design and implementation (PLDI)

作者： Chabbi, Milind Ramanathan, Murali Krishna Uber Technol Inc Programming Syst Grp Sunnyvale CA 94086 USA

ISBN: (纸本)9781450392655

The concurrent programming literature is rich with tools and techniques for data race detection. Less, however, has been known about real-world, industry-scale deployment, experience, and insights about data races. Golang (Go for short) is a modern programming language that makes concurrency a first-class citizen. Go offers both message passing and shared memory for communicating among concurrent threads. Go is gaining popularity in modern microservice-based systems. Data races in Go stand in the face of its emerging popularity. In this paper, using our industrial codebase as an example, we demonstrate that Go developers embrace concurrency and show how the abundance of concurrency alongside language idioms and nuances make Go programs highly susceptible to data races. Google's Go distribution ships with a built-in dynamic data race detector based on ThreadSanitizer. However, dynamic race detectors pose scalability and flakiness challenges;we discuss various software engineering trade-offs to make this detector work effectively at scale. We have deployed this detector in Uber's 46 million lines of Go codebase hosting 2100 distinct microservices, found over 2000 data races, and fixed over 1000 data races, spanning 790 distinct code patches submitted by 210 unique developers over a six-month period. Based on a detailed investigation of these data race patterns in Go, we make seven high-level observations relating to the complex interplay between the Go language paradigm and data races.

关键词： Data race Golang Dynamic analysis

来源：评论

学校读者我要写书评

暂无评论

PDL A High-Level Hardware design language for Pipelined Processors 2022

PDL A High-Level Hardware Design Language for Pipelined Proc...

引用

43rd ACM sigplan International conference on programming language design and implementation (PLDI)

作者： Zagieboylo, Drew Sherk, Charles Suh, Gookwon Edward Myers, Andrew C. Cornell Univ Dept Comp Sci Ithaca NY 14853 USA Cornell Univ Sch Elect & Comp Engn Ithaca NY 14853 USA

ISBN: (纸本)9781450392655

Processors are typically designed in Register Transfer Level (RTL) languages, which give designers low-level control over circuit structure and timing. To achieve good performance, processors are pipelined, with multiple instructions executing concurrently in different parts of the circuit. Thus even though processors implement a fundamentally sequential specification (the instruction set architecture), the implementation is highly concurrent. The interactions of multiple instructions-potentially speculative-can cause incorrect behavior. We present PDL, a novel hardware description language targeted at the construction of pipelined processors. PDL provides one-instruction-at-a-time semantics: the first language to enforce that the generated pipelined circuit has the same behavior as a sequential specification. This enforcement facilitates design-space exploration. Adding or removing pipeline stages, moving operations across stages, or otherwise changing pipeline structure normally requires careful analysis of bypass paths and stall logic;with PDL, this analysis is handled by the PDL compiler. At the same time, PDL still offers designers fine-grained control over performance-critical microarchitectural choices such as timing of operations, data forwarding, and speculation. We demonstrate PDL's expressive power and ease of design exploration by implementing several RISC-V cores with differing microarchitectures. Our results show that PDL does not impose significant performance or area overhead compared to a standard HDL.

关键词： Computer Architecture language design

来源：评论

学校读者我要写书评

暂无评论

Exocompilation for Productive programming of Hardware Accelerators 2022

Exocompilation for Productive Programming of Hardware Accele...

引用

43rd ACM sigplan International conference on programming language design and implementation (PLDI)

作者： Ikarashi, Yuka Bernstein, Gilbert Louis Reinking, Alex Genc, Hasan Ragan-Kelley, Jonathan MIT CSAIL Cambridge MA 02139 USA Univ Calif Berkeley Berkeley CA USA

ISBN: (纸本)9781450392655

High-performance kernel libraries are critical to exploiting accelerators and specialized instructions in many applications. Because compilers are difficult to extend to support diverse and rapidly-evolving hardware targets, and automatic optimization is often insufficient to guarantee state-of-the-art performance, these libraries are commonly still coded and optimized by hand, at great expense, in low-level C and assembly. To better support development of high-performance libraries for specialized hardware, we propose a new programming language, Exo, based on the principle of exocompilation: externalizing target-specific code generation support and optimization policies to user-level code. Exo allows custom hardware instructions, specialized memories, and accelerator configuration state to be defined in user libraries. It builds on the idea of user scheduling to externalize hardware mapping and optimization decisions. Schedules are defined as composable rewrites within the language, and we develop a set of effect analyses which guarantee program equivalence and memory safety through these transformations. We show that Exo enables rapid development of state-of-the-art matrix-matrix multiply and convolutional neural network kernels, for both an embedded neural accelerator and x86 with AVX-512 extensions, in a few dozen lines of code each.

关键词： program optimization hardware accelerators user-schedulable languages instruction abstraction scheduling user-extensible backend & scheduling

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：