ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS (TOPLAS) 是报告编程语言领域最新研究进展的主要期刊，以及协助编程任务的系统。论文的风格可以是理论性的，也可以是实验性的，但无论哪种情况，它们都必须包含创新和新颖的内容，以推动编程语言和系统的最新发展。我们还邀请严格比较现有方法的实验论文，以及教程和调查论文。 TOPLAS 的范围包括但不限于以下主题： 用于顺序和并行编程的语言设计 编程语言实现 编程语言语义 编译器和解释器 用于程序执行存储分配和垃圾收集的运行时系统 用于编写程序规范的语言和方法 语言安全可靠的程序测试和程序验证方法及方法

The ACM Transactions on Programming Languages and Systems (TOPLAS) is a leading journal that reports on the latest research advancements in the field of programming languages and the systems that support programming tasks. The journal welcomes both theoretical and experimental papers, provided they contain innovative and novel content that advances the state of programming languages and systems. We also invite experimental papers that rigorously compare existing methods, as well as tutorial and survey papers. The scope of TOPLAS includes, but is not limited to, the following topics: language design for sequential and parallel programming, implementation of programming languages, semantics of programming languages, compilers and interpreters, runtime systems for program execution, memory allocation and garbage collection, languages and methods for writing program specifications, language safety, reliable program testing, and program verification methods.

《ACM Transactions on Programming Languages and Systems》（TOPLAS）是编程语言领域最新研究成果的重要期刊，致力于支持编程任务的系统研究。该期刊接受理论性和实验性的论文，但无论是哪种类型，论文都必须包含创新和新颖的内容，以推动编程语言和系统的发展。我们还欢迎对现有方法进行严格比较的实验论文，以及教程和调查性论文。TOPLAS的研究范围包括但不限于以下主题：顺序和并行编程的语言设计、编程语言的实现、编程语言的语义、编译器和解释器、用于程序执行的存储分配和垃圾收集的运行时系统、用于编写程序规范的语言和方法、语言安全性、可靠的程序测试和程序验证的方法。

ACM Transactions on Programming Languages and Systems

Writing low-level concurrent software has traditionally required intimate knowledge of the entire toolchain and often has involved coding in assembly. New language standards have extended C and C++ with support for low-level atomic operations and a weak memory model, enabling developers to write portable and efficient multithreaded code. In this article, we present CDSC hecker , a tool for exhaustively exploring the behaviors of concurrent code under the C/C++ memory model. We have used CDSC hecker to exhaustively unit test concurrent data structure implementations and have discovered errors in a published implementation of a work-stealing queue and a single producer, single consumer queue.

Brian Norris

Brian Demsky

A Practical Approach for Model Checking C/C++11 Code

一种实用的C/C++11代码模型检查方法

This article introduces a combinatorial optimization approach to register allocation and instruction scheduling, two central compiler problems. Combinatorial optimization has the potential to solve these problems optimally and to exploit processor-specific features readily. Our approach is the first to leverage this potential in practice : it captures the complete set of program transformations used in state-of-the-art compilers, scales to medium-sized functions of up to 1,000 instructions, and generates executable code. This level of practicality is reached by using constraint programming, a particularly suitable combinatorial optimization technique. Unison, the implementation of our approach, is open source, used in industry, and integrated with the LLVM toolchain. An extensive evaluation confirms that Unison generates better code than LLVM while scaling to medium-sized functions. The evaluation uses systematically selected benchmarks from MediaBench and SPEC CPU2006 and different processor architectures (Hexagon, ARM, MIPS). Mean estimated speedup ranges from 1.1% to 10% and mean code size reduction ranges from 1.3% to 3.8% for the different architectures. A significant part of this improvement is due to the integrated nature of the approach. Executing the generated code on Hexagon confirms that the estimated speedup results in actual speedup. Given a fixed time limit, Unison solves optimally functions of up to 946 instructions, nearly an order of magnitude larger than previous approaches. The results show that our combinatorial approach can be applied in practice to trade compilation time for code quality beyond the usual compiler optimization levels, identify improvement opportunities in heuristic algorithms, and fully exploit processor-specific features.

Roberto Castañeda Lozano

Mats Carlsson

Gabriel Hjort Blindell

Christian Schulte

Combinatorial Register Allocation and Instruction Scheduling

组合寄存器分配与指令调度

Reliable computer systems must handle malfunctioning components that give conflicting information to different parts of the system. This situation can be expressed abstractly in terms of a group of generals of the Byzantine army camped with their troops around an enemy city. Communicating only by messenger, the generals must agree upon a common battle plan. However, one or more of them may be traitors who will try to confuse the others. The problem is to find an algorithm to ensure that the loyal generals will reach agreement. It is shown that, using only oral messages, this problem is solvable if and only if more than two-thirds of the generals are loyal; so a single traitor can confound two loyal generals. With unforgeable written messages, the problem is solvable for any number of generals and possible traitors. Applications of the solutions to reliable computer systems are then discussed.

Leslie Lamport

Robert Shostak

Marshall Pease

ACM Trans. Program. Lang. Syst.

The Byzantine Generals Problem

拜占庭将军问题

In the past decade, processor speed has become significantly faster than memory speed. Small, fast cache memories are designed to overcome this discrepancy, but they are only effective when programs exhibit data locality . In the this article, we present compiler optimizations to improve data locality based on a simple yet accurate cost model. The model computes both temporal and spatial reuse of cache lines to find desirable loop organizations. The cost model drives the application of compound transformations consisting of loop permutation, loop fusion, loop distribution, and loop reversal. To validate our optimization strategy, we implemented our algorithms and ran experiments on a large collection of scientific programs and kernels. Experiments illustrate that for kernels our model and algorithm can select and achieve the best loop structure for a nest. For over 30 complete applications, we executed the original and transformed versions and simulated cache hit rates. We collected statistics about the inherent characteristics of these programs and our ability to improve their data locality. To our knowledge, these studies are the first of such breadth and depth. We found performance improvements were difficult to achieve bacause benchmark programs typically have high hit rates even for small data caches; however, our optimizations significanty improved several programs.

Kathryn S. McKinley

Steve Carr

Chau-Wen Tseng

Improving data locality with loop transformations

通过循环变换提高数据局部性

Constraint-solving-based program invariant synthesis takes a parametric invariant template and encodes the (inductive) invariant conditions into constraints. The problem of characterizing the set of all valid parameter assignments is referred to as the strong invariant synthesis problem , while the problem of finding a concrete valid parameter assignment is called the weak invariant synthesis problem . For both problems, the challenge lies in solving or reducing the encoded constraints, which are generally non-convex and lack efficient solvers. In this paper, we propose two novel algorithms for synthesizing invariants of polynomial programs using semidefinite programming (SDP): (1) The Cluster algorithm targets the strong invariant synthesis problem for polynomial invariant templates. Leveraging robust optimization techniques, it solves a series of SDP relaxations and yields a sequence of increasingly precise under-approximations of the set of valid parameter assignments. We prove the algorithm’s soundness, convergence, and weak completeness under a specific robustness assumption on templates. Moreover, the outputs can simplify the weak invariant synthesis problem. (2) The Mask algorithm addresses the weak invariant synthesis problem in scenarios where the aforementioned robustness assumption does not hold, rendering the Cluster algorithm ineffective. It identifies a specific subclass of invariant templates, termed masked templates, involving parameterized polynomial equalities and known inequalities. By applying variable substitution, the algorithm transforms constraints into an equivalent form amenable to SDP relaxations. Both algorithms have been implemented and demonstrated superior performance compared to state-of-the-art methods in our empirical evaluation.

Hao Wu

Qiuye Wang

Bai Xue

Naijun Zhan

Lihong Zhi

Zhi-Hong Yang

Synthesizing Invariants for Polynomial Programs by Semidefinite Programming

通过半定规划合成多项式程序的不变量

We introduce layering to modal type theory to support meta-programming and intensional analysis coherently. In particular, we demonstrate this idea by developing a 2-layered modal type theory. At the core of this type theory (layer 0) is a simply typed λ -calculus with no modality. Layer 1 is obtained by extending the core language with one layer of contextual ◻ types to support pattern matching on potentially open code from layer 0 while retaining normalization. Although both layers fundamentally share a uniform syntax and the same typing judgment, we only allow computation at layer 1. As a consequence, layer 0 accurately captures the syntactic representation of code in contrast to the computational behaviors at layer 1. Moreover, the uniform syntax at both layers enables quotation and code running. The system is justified by normalization by evaluation (NbE) using a presheaf model. The normalization algorithm extracted from the model is sound and complete and is implemented in Agda. Layered modal type theory provides a uniform foundation for meta-programming with intensional analysis. We see this work as an important step towards a foundational way to support meta-programming in proof assistants.

Jason Z. S. Hu

Brigitte Pientka

A Layered Approach to Intensional Analysis in Type Theory

类型论中内涵分析的分层方法

Current static verification techniques such as separation logic support a wide range of programs. However, such techniques only support complete and detailed specifications, which places an undue burden on users. To solve this problem, prior work proposed gradual verification, which handles complete, partial, or missing specifications by soundly combining static and dynamic checking. Gradual verification has also been extended to programs that manipulate recursive, mutable data structures on the heap. Unfortunately, this extension does not reward users with decreased dynamic checking as more specifications are written and more static guarantees are made. In fact, all properties are checked dynamically regardless of any static guarantees. Additionally, no full-fledged implementation of gradual verification exists so far, which prevents studying its performance and applicability in practice. We present Gradual C0, the first practicable gradual verifier for recursive heap data structures, which targets C0, a safe subset of C designed for education. Static verifiers supporting separation logic or implicit dynamic frames use symbolic execution for reasoning; so Gradual C0, which extends one such verifier, adopts symbolic execution at its core instead of the weakest liberal precondition approach used in prior work. Our approach addresses technical challenges related to symbolic execution with imprecise specifications, heap ownership, and branching in both program statements and specification formulas. We also deal with challenges related to minimizing insertion of dynamic checks and extensibility to other programming languages beyond C0. Finally, we provide the first empirical performance evaluation of a gradual verifier, and found that on average, Gradual C0 decreases run-time overhead between 7.1-40.2% compared to the fully-dynamic approach used in prior work (for context, the worst cases for Wise et al. [2020]’s approach range from 0.1-4.5 seconds depending on the benchmark). Further, the worst-case scenarios for performance are predictable and avoidable. This work paves the way towards evaluating gradual verification at scale.

Jenna DiVincenzo

Ian McCormack

Conrad Zimmerman

Hemant Gouni

Jacob Gorenburg

Jan-Paul Ramos-Dávila

Mona Zhang

Joshua Sunshine

Éric Tanter

Jonathan Aldrich

Gradual C0: Symbolic Execution for Gradual Verification

渐进式C0：渐进验证的符号执行

Big data analytics frameworks, such as Spark and Giraph, need to process and cache massive datasets that do not always fit on the managed heap. Therefore, frameworks temporarily move long-lived objects outside the heap (off-heap) on a fast storage device. However, this practice results in (1) high serialization/deserialization (S/D) cost and (2) high memory pressure when off-heap objects are moved back for processing. In this article, we propose TeraHeap , a system that eliminates S/D overhead and expensive GC scans for a large portion of objects in analytics frameworks. TeraHeap relies on three concepts: (1) It eliminates S/D by extending the managed runtime (JVM) to use a second high-capacity heap (H2) over a fast storage device. (2) It offers a simple hint-based interface, allowing analytics frameworks to leverage object knowledge to populate H2. (3) It reduces GC cost by fencing the collector from scanning H2 objects while maintaining the illusion of a single managed heap, ensuring memory safety. We implement TeraHeap in OpenJDK8 and OpenJDK17 and evaluate it with fifteen widely used applications in two real-world big data frameworks, Spark and Giraph. We find that for the same DRAM size, TeraHeap improves performance by up to 73% and 28% compared to native Spark and Giraph. Also, it can still provide better performance by consuming up to \(4.6\times\) and \(1.2\times\) less DRAM than native Spark and Giraph, respectively. TeraHeap can also be used for in-memory frameworks and applying it to the Neo4j Graph Data Science library improves its performance by up to 26%. Finally, it outperforms Panthera, a state-of-the-art garbage collector for hybrid DRAM-NVM memories, by up to 69%.

Iacovos G. Kolokasis

Giannos Evdorou

Shoaib Akram

Christos Kozanitis

Anastasios Papagiannis

Foivos S. Zakkak

Polyvios Pratikakis

Angelos Bilas

TeraHeap: Exploiting Flash Storage for Mitigating DRAM Pressure in Managed Big Data Frameworks

TeraHeap：利用闪存存储缓解托管大数据框架中的DRAM压力

This paper discusses the relationship between two frameworks: universal composability (UC) and robust compilation ( RC ). In cryptography, UC is a framework for the specification and analysis of cryptographic protocols with a strong compositionality guarantee: UC protocols remain secure even when composed with other protocols. In programming language security, RC is a novel framework for determining secure compilation by proving whether compiled programs are as secure as their source-level counterparts no matter what target-level code they interact with. Presently, these disciplines are studied in isolation, though we argue that there is a deep connection between them and exploring this connection will benefit both research fields. This paper formally proves the connection between UC and RC and then it explores the benefits of this connection (focussing on perfect, rather than computational UC). For this, this paper first identifies which conditions must programming languages fulfil in order to possibly attain UC-like composition. Then, it proves UC of both an existing and a new commitment protocol as a corollary of the related compilers attaining RC . Finally, it mechanises these proofs in Deepsec, obtaining symbolic guarantees that the protocol is indeed UC. Our connection lays the groundwork towards a better and deeper understanding of both UC and RC , and the benefits we showcase from this connection provide evidence of scalable mechanised proofs for UC. In order to differentiate various sub-parts of the UC and RC frameworks, we use syntax highlighting to a degree that colourblind and black&amp;white readers can benefit from [78]. UC talks about ideal functionalities (typeset in a verbatim, emerald font) and protocol implementations (typeset in a sans-serif, orange font). RC deals with source languages (typeset in an italics, blue font) and target ones (typeset in a bold, red font). Elements that are common to each framework are typeset in a black, sans-serif font for UC and in a black, italicised font for RC to avoid repetition. For a better experience, please view this paper in colour.

Abbreviation	ACM Trans. Program. Lang. Syst.
Journal Impact	1.70
Quartiles(Global)	COMPUTER SCIENCE, SOFTWARE ENGINEERING(Q3)

ISSN	0164-0925, 1558-4593
h-index	73

Publication Information	Publisher: Association for Computing Machinery (ACM)，Publishing cycle: Bimonthly，Journal Type: journal，Open Access Journals: No
Basic data	Year of publication: 1979，Proportion of original research papers: 100.00%，Self Citation Rate:0.00%， Gold OA Rate: 6.06%
Average review cycle	网友分享经验：>12周，或约稿
Average recruitment ratio	网友分享经验：容易

ACM Transactions on Programming Languages and Systems

Journal Citation Format

A journal article with 1 author

A journal article with 2 authors

A journal article with 3 authors

A journal article with 5 or more authors

Books Citation Format

Thesis Citation Format

Web sites Citation Format

Patent Citation Format

Staying up late manually editing references? ivySCI automatically matches journals and helps you generate references with a single click.

Share Submission Experience

A Practical Approach for Model Checking C/C++11 Code

Combinatorial Register Allocation and Instruction Scheduling

The Byzantine Generals Problem

Improving data locality with loop transformations

Synthesizing Invariants for Polynomial Programs by Semidefinite Programming

Synthesizing Invariants for Polynomial Programs by Semidefinite Programming

A Layered Approach to Intensional Analysis in Type Theory

Gradual C0: Symbolic Execution for Gradual Verification

TeraHeap: Exploiting Flash Storage for Mitigating DRAM Pressure in Managed Big Data Frameworks

Universal Composability is Robust Compilation