Programming Languages

New submissions

• New submissions
• Cross-lists
• Replacements

New submissions for Fri, 31 May 24

[1]  arXiv:2405.19514 [pdf, other]

Title: Wavefront Threading Enables Effective High-Level Synthesis

Authors: Blake Pelton, Adam Sapek, Ken Eguro, Daniel Lo, Alessandro Forin, Matt Humphrey, Jinwen Xi, David Cox, Rajas Karandikar, Johannes de Fine Licht, Evgeny Babin, Adrian Caulfield, Doug Burger

Comments: Accepted to PLDI'24

Subjects: Programming Languages (cs.PL)

Digital systems are growing in importance and computing hardware is growing more heterogeneous. Hardware design, however, remains laborious and expensive, in part due to the limitations of conventional hardware description languages (HDLs) like VHDL and Verilog. A longstanding research goal has been programming hardware like software, with high-level languages that can generate efficient hardware designs. This paper describes Kanagawa, a language that takes a new approach to combine the programmer productivity benefits of traditional High-Level Synthesis (HLS) approaches with the expressibility and hardware efficiency of Register-Transfer Level (RTL) design. The language's concise syntax, matched with a hardware design-friendly execution model, permits a relatively simple toolchain to map high-level code into efficient hardware implementations.

Cross-lists for Fri, 31 May 24

[2]  arXiv:2405.19787 (cross-list from cs.CL) [pdf, other]

Title: From Symbolic Tasks to Code Generation: Diversification Yields Better Task Performers

Authors: Dylan Zhang, Justin Wang, Francois Charton

Subjects: Computation and Language (cs.CL); Artificial Intelligence (cs.AI); Machine Learning (cs.LG); Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

Instruction tuning -- tuning large language models on instruction-output pairs -- is a promising technique for making models better adapted to the real world. Yet, the key factors driving the model's capability to understand and follow instructions not seen during training remain under-explored. Our investigation begins with a series of synthetic experiments within the theoretical framework of a Turing-complete algorithm called Markov algorithm, which allows fine-grained control over the instruction-tuning data. Generalization and robustness with respect to the training distribution emerge once a diverse enough set of tasks is provided, even though very few examples are provided for each task. We extend these initial results to a real-world application scenario of code generation and find that a more diverse instruction set, extending beyond code-related tasks, improves the performance of code generation. Our observations suggest that a more diverse semantic space for instruction-tuning sets greatly improves the model's ability to follow instructions and perform tasks.

[3]  arXiv:2405.20083 (cross-list from cs.LO) [pdf, other]

Title: Tachis: Higher-Order Separation Logic with Credits for Expected Costs

Authors: Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon Oddershede Gregersen, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal

Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)

We present Tachis, a higher-order separation logic to reason about the expected cost of probabilistic programs. Inspired by the uses of time credits for reasoning about the running time of deterministic programs, we introduce a novel notion of probabilistic cost credit. Probabilistic cost credits are a separation logic resource that can be used to pay for the cost of operations in programs, and that can be distributed across all possible branches of sampling instructions according to their weight, thus enabling us to reason about expected cost. The representation of cost credits as separation logic resources gives Tachis a great deal of flexibility and expressivity. In particular, it permits reasoning about amortized expected cost by storing excess credits as potential into data structures to pay for future operations. Tachis further supports a range of cost models, including running time and entropy usage. We showcase the versatility of this approach by applying our techniques to prove upper bounds on the expected cost of a variety of probabilistic algorithms and data structures, including randomized quicksort, hash tables, and meldable heaps.
All of our results have been mechanized using Coq, Iris, and the Coquelicot real analysis library.

Replacements for Fri, 31 May 24

[4]  arXiv:2405.14068 (replaced) [pdf, other]

Title: Verifying Cake-Cutting, Faster

Authors: Noah Bertram, Tean Lai, Justin Hsu

Comments: 53 Pages, 12 Figures, CAV 2024

Subjects: Computer Science and Game Theory (cs.GT); Programming Languages (cs.PL)

[5]  arXiv:2405.17503 (replaced) [pdf, other]

Title: Code Repair with LLMs gives an Exploration-Exploitation Tradeoff

Authors: Hao Tang, Keya Hu, Jin Peng Zhou, Sicheng Zhong, Wei-Long Zheng, Xujie Si, Kevin Ellis

Subjects: Software Engineering (cs.SE); Artificial Intelligence (cs.AI); Computation and Language (cs.CL); Programming Languages (cs.PL)

• New submissions
• Cross-lists
• Replacements