bluuebunny/crossref_metadata_2025 huggingface dataset:
Statically Contextualizing Large Language Models with Typed Holes
Authors: Blinn Andrew , Li Xiang , Kim June Hyung , Omar Cyrus
Published: October 2024

Large language models (LLMs) have reshaped the landscape of program synthesis. However, contemporary LLM-based code completion systems often hallucinate broken code because they lack appropriate code context, particularly when working with definitions that are neither in the training data nor near the cursor. This paper demonstrates that tighter integration with the type and binding structure of the programming language in use, as exposed by its language server, can help address this contextualization problem in a token-efficient manner. In short, we contend that AIs need IDEs, too! In particular, we integrate LLM code generation into the Hazel live program sketching environment. The Hazel Language Server is able to identify the type and typing context of the hole that the programmer is filling, with Hazel's total syntax and type error correction ensuring that a meaningful program sketch is available whenever the developer requests a completion. This allows the system to prompt the LLM with codebase-wide contextual information that is not lexically local to the cursor, nor necessarily in the same file, but that is likely to be semantically local to the developer's goal. Completions synthesized by the LLM are then iteratively refined via further dialog with the language server, which provides error localization and error messages. To evaluate these techniques, we introduce MVUBench, a dataset of model-view-update (MVU) web applications with accompanying unit tests that have been written from scratch to avoid data contamination, and that can easily be ported to new languages because they do not have large external library dependencies. These applications serve as challenge problems due to their extensive reliance on application-specific data structures. Through an ablation study, we examine the impact of contextualization with type definitions, function headers, and errors messages, individually and in combination. We find that contextualization with type definitions is particularly impactful. After introducing our ideas in the context of Hazel, a low-resource language, we duplicate our techniques and port MVUBench to TypeScript in order to validate the applicability of these methods to higher-resource mainstream languages. Finally, we outline ChatLSP, a conservative extension to the Language Server Protocol (LSP) that language servers can implement to expose capabilities that AI code completion systems of various designs can use to incorporate static context when generating prompts for an LLM.
Quantum Probabilistic Model Checking for Time-Bounded Properties
Authors: Jeon Seungmin , Cho Kyeongmin , Kang Chan Gu , Lee Janggun , Oh Hakjoo , Kang Jeehoon
Published: October 2024

Probabilistic model checking (PMC) is a verification technique for analyzing the properties of probabilistic systems. However, existing techniques face challenges in verifying large systems with high accuracy. PMC struggles with state explosion, where the number of states grows exponentially with the size of the system, making large system verification infeasible. While statistical model checking (SMC) avoids PMC’s state explosion problem by using a simulation approach, it suffers from runtime explosion, requiring numerous samples for high accuracy.

To address these limitations in verifying large systems with high accuracy, we present quantum probabilistic model checking (QPMC), the first method leveraging quantum computing for PMC with respect to time-bounded properties. QPMC addresses state explosion by encoding PMC problems into quantum circuits that superpose states within qubits. Additionally, QPMC resolves runtime explosion through Quantum Amplitude Estimation, efficiently estimating the probabilities of specified properties. We prove that QPMC correctly solves PMC problems and achieves a quadratic speedup in time complexity compared to SMC.
Verified Lock-Free Session Channels with Linking
Authors: Somers Thomas , Krebbers Robbert
Published: October 2024

Type systems and program logics based on session types provide powerful high-level reasoning principles for message-passing concurrency. Modern versions employ bidirectional session channels that (1) are asynchronous so that send operations do not block, (2) have buffers in both directions so that both parties can send messages in parallel, and (3) feature a link operation (also called forward) to concisely write programs in process style. These features complicate a low-level lock-free implementation of channels and therefore increase the gap between the meta theory of prior work—which is verified w.r.t. a high-level semantics of channels (e.g., π-calculus)—and the code that runs on an actual computer. We address this problem by verifying a low-level lock-free implementation of session channels w.r.t. a high-level specification based on session types. We carry out our verification in a layered manner by employing the Iris framework for concurrent separation logic. We start with an abstract specification of (unidirectional) queues—of which we provide a linked-list and array-segment based implementation—and gradually build up to session channels with all of the aforementioned features. To make a layered verification possible we develop two logical abstractions—queues with ghost linking and pairing invariants—to reason about the atomicity and changing endpoints due to linking, respectively. All our results are mechanized in the Coq proof assistant.
Merging Gradual Typing
Authors: Ye Wenjia , Oliveira Bruno C. d. S. , Toro Matías
Published: October 2024

Programming language mechanisms with a type-directed semantics are nowadays common and widely used. Such mechanisms include gradual typing, type classes, implicits and intersection types with a merge operator. While sharing common challenges in their design and having complementary strengths, type-directed mechanisms have been mostly independently studied.

This paper studies a new calculus, called λM⋆, which combines two type-directed mechanisms: gradual typing and a merge operator based on intersection types. Gradual typing enables a smooth transition between dynamically and statically typed code, and is available in languages such as TypeScript or Flow. The merge operator generalizes record concatenation to allow merges of values of any two types. Recent work has shown that the merge operator enables modelling expressive OOP features like first-class traits/classes and dynamic inheritance with static type-checking. These features are not found in mainstream statically typed OOP languages, but they can be found in dynamically or gradually typed languages such as JavaScript or TypeScript. In λM⋆, by exploiting the complementary strengths of gradual typing and the merge operator, we obtain a foundation for modelling gradually typed languages with both first-class classes and dynamic inheritance. We study a static variant of λM⋆ (called λM); prove the type-soundness of λM⋆; show that λM⋆ can encode gradual rows and all well-typed terms in the GTFL≲ calculus; and show that λM⋆ satisfies gradual typing criteria. The dynamic gradual guarantee (DGG) is challenging due to the possibility of ambiguity errors. We establish a variant of the DGG using a semantic notion of precision based on a step-indexed logical relation.
Automatically Reducing Privilege for Access Control Policies
Authors: D’Antoni Loris , Ding Shuo , Goel Amit , Ramesh Mathangi , Rungta Neha , Sung Chungha
Published: October 2024

Access control policies are programs used to secure cloud resources. These polices should only grant the necessary permissions that a given application needs. However, it is challenging to write and maintain policies as applications and their required permissions change over time.

In this paper, we focus on the Amazon Web Services (AWS) IAM policy language and present an approach that, given a policy, synthesizes a modified policy that is more restrictive and better abides to the principle of least privilege. Our approach looks at the actual access history (e.g., access logs) used by an application and computes the least permissive local modification of the user-given policy that still provides the same permissions that were observed in the access history. We treat the problem of computing the least permissive policy as a generalization problem in a lattice of possible policies (i.e., the set of local modifications). We show that our synthesis algorithm comes with correctness guarantees and is amendable to an efficient implementation that is easy to parallelize. We implement our algorithm in a tool IAM-PolicyRefiner and evaluate it on policies attached to AWS roles with access logs. For each role, IAM-PolicyRefiner can compute easy-to-inspect refined policies in less than 1 minute, and the refined policies do not overfit to the requests in the log---i.e., the policies also allow requests in a left-out test set of requests.
CoolerSpace: A Language for Physically Correct and Computationally Efficient Color Programming
Authors: Chen Ethan , Chang Jiwon , Zhu Yuhao
Published: October 2024

Color programmers manipulate lights, materials, and the resulting colors from light-material interactions. Existing libraries for color programming provide only a thin layer of abstraction around matrix operations. Color programs are, thus, vulnerable to bugs arising from mathematically permissible but physically meaningless matrix computations. Correct implementations are difficult to write and optimize. We introduce CoolerSpace to facilitate physically correct and computationally efficient color programming. CoolerSpace raises the level of abstraction of color programming by allowing programmers to focus on describing the logic of color physics. Correctness and efficiency are handled by CoolerSpace. The type system in CoolerSpace assigns physical meaning and dimensions to user-defined objects. The typing rules permit only legal computations informed by color physics and perception. Along with type checking, CoolerSpace also generates performance-optimized programs using equality saturation. CoolerSpace is implemented as a Python library and compiles to ONNX, a common intermediate representation for tensor computations. CoolerSpace not only prevents common errors in color programming, but also does so without run-time overhead: even unoptimized CoolerSpace programs out-perform existing Python-based color programming systems by up to 5.7 times; our optimizations provide up to an additional 1.4 times speed-up.
The Ultimate Conditional Syntax
Authors: Cheng Luyu , Parreaux Lionel
Published: October 2024

Functional programming languages typically support expressive pattern-matching syntax allowing programmers

to write concise and type-safe code, especially appropriate for manipulating algebraic data types. Many

features have been proposed to enhance the expressiveness of stock pattern-matching syntax, such as pattern

bindings, pattern alternatives (a.k.a. disjunction), pattern conjunction, view patterns, pattern guards, pattern

synonyms, active patterns, ‘if-let’ patterns, multi-way if-expressions, etc. In this paper, we propose a new

pattern-matching syntax that is both more expressive and (we argue) simpler and more readable than previous

alternatives. Our syntax supports parallel and nested matches interleaved with computations and intermediate

bindings. This is achieved through a form of nested multi-way if-expressions with a condition-splitting mechanism

to factor common conditional prefixes as well as a binding technique we call conditional pattern flowing.

We motivate this new syntax with many examples in the setting of MLscript, a new ML-family programming

language. We describe a straightforward desugaring pass from our rich source syntax into a minimal core

syntax that only supports flat patterns and has an intuitive small-step semantics. We then provide a translation

from the core syntax into a normalized syntax without backtracking, which is more amenable to coverage

checking and compilation, and formally prove that our translation is semantics-preserving. We view this work

as a step towards rethinking pattern matching to make it more powerful and natural to use. Our syntax can

easily be integrated, in part or in whole, into existing as well as future programming language designs.
Compilation of Shape Operators on Sparse Arrays
Authors: Root Alexander J , Yan Bobby , Liu Peiming , Gyurgyik Christophe , Bik Aart J.C. , Kjolstad Fredrik
Published: October 2024

We show how to build a compiler for a sparse array language that supports shape operators such as reshaping or concatenating arrays, in addition to compute operators. Existing sparse array programming systems implement generic shape operators for only some sparse data structures, reduce shape operators on other data structures to those, and do not support fusion. Our system compiles sparse array expressions to code that efficiently iterates over reshaped views of irregular sparse data structures, without needing to materialize temporary storage for intermediates. Our evaluation shows that our approach generates sparse array code competitive with popular sparse array libraries: our generated shape operators achieve geometric mean speed-ups of 1.66×–15.3× when compared to hand-written kernels in scipy.sparse and 1.67×–651× when compared to generic implementations in pydata/sparse. For operators that require data structure conversions in these libraries, our generated code achieves geometric mean speed-ups of 7.29×–13.0× when compared to scipy.sparse and 21.3×–511× when compared to pydata/sparse. Finally, our evaluation demonstrates that fusing shape and compute operators improves the performance of several expressions by geometric mean speed-ups of 1.22×–2.23×.
Making Formulog Fast: An Argument for Unconventional Datalog Evaluation
Authors: Bembenek Aaron , Greenberg Michael , Chong Stephen
Published: October 2024

With its combination of Datalog, SMT solving, and functional programming, the language Formulog provides an appealing mix of features for implementing SMT-based static analyses (e.g., refinement type checking, symbolic execution) in a natural, declarative way. At the same time, the performance of its custom Datalog solver can be an impediment to using Formulog beyond prototyping—a common problem for Datalog variants that aspire to solve large problem instances. In this work we speed up Formulog evaluation, with some surprising results: while 2.2× speedups can be obtained by using the conventional techniques for high-performance Datalog (e.g., compilation, specialized data structures), the big wins come by abandoning the central assumption in modern performant Datalog engines, semi-naive Datalog evaluation. In the place of semi-naive evaluation, we develop eager evaluation, a concurrent Datalog evaluation algorithm that explores the logical inference space via a depth-first traversal order. In practice, eager evaluation leads to an advantageous distribution of Formulog’s SMT workload to external SMT solvers and improved SMT solving times: our eager evaluation extensions to the Formulog interpreter and Soufflé’s code generator achieve mean 5.2× and 7.6× speedups, respectively, over the optimized code generated by off-the-shelf Soufflé on SMT-heavy Formulog benchmarks. All in all, using compilation and eager evaluation (as appropriate), Formulog implementations of refinement type checking, bottom-up pointer analysis, and symbolic execution achieve speedups on 20 out of 23 benchmarks over previously published, hand-tuned analyses written in F♯, Java, and C++, providing strong evidence that Formulog can be the basis of a realistic platform for SMT-based static analysis. Moreover, our experience adds nuance to the conventional wisdom that traditional semi-naive evaluation is the one-size-fits-all best Datalog evaluation algorithm for static analysis workloads.
Hypra: A Deductive Program Verifier for Hyper Hoare Logic
Authors: Dardinier Thibault , Li Anqi , Müller Peter
Published: October 2024

Hyperproperties relate multiple executions of a program and are useful to express common correctness properties (such as determinism) and security properties (such as non-interference). While there are a number of powerful program logics for the deductive verification of hyperproperties, their automation falls behind. Most existing deductive verification tools are limited to safety properties, but cannot reason about the existence of executions, for instance, to prove the violation of a safety property. Others support more flexible hyperproperties such as generalized non-interference, but have limitations in terms of the programs and proof structures they support.

In this paper, we present the first deductive verification technique for arbitrary hyperproperties over multiple executions of the same program. Our technique automates the generation of verification conditions for Hyper Hoare Logic. Our key insight is that arbitrary hyperproperties and the corresponding proof rules can be encoded into a standard intermediate verification language by representing sets of states of the input program explicitly in the states of the intermediate program. Verification is then automated using an existing SMT-based verifier for the intermediate language. We implement our technique in a tool called Hypra and demonstrate that it can reliably verify complex hyperproperties.
Multris: Functional Verification of Multiparty Message Passing in Separation Logic
Authors: Hinrichsen Jonas Kastberg , Jacobs Jules , Krebbers Robbert
Published: October 2024

We introduce Multris, a separation logic for verifying functional correctness of programs that combine multiparty message-passing communication with shared-memory concurrency. The foundation of our work is a novel concept of multiparty protocol consistency, which guarantees safe communication among a set of parties, provided each party adheres to its prescribed protocol. Our concept of protocol consistency is inspired by the bottom-up approach for multiparty session types. However, by considering it in the context of separation logic instead of a type system, we go further in terms of generality by supporting new notions of implicit transfer of knowledge and implicit transfer of resources. We develop tactics for automatically verifying protocol consistency and for reasoning about message-passing operations in Multris. We evaluate Multris on a range of examples, including the well-known two- and three-buyer protocols, as well as a new verification benchmark based on Chang and Roberts's ring leader election protocol. To ensure the reliability of our work, we prove soundness of Multris w.r.t. a low-level channel semantics using the Iris framework in Coq.
HardTaint: Production-Run Dynamic Taint Analysis via Selective Hardware Tracing
Authors: Zhang Yiyu , Liu Tianyi , Wang Yueyang , Qi Yun , Ji Kai , Tang Jian , Wang Xiaoliang , Li Xuandong , Zuo Zhiqiang
Published: October 2024

Dynamic taint analysis (DTA), as a fundamental analysis technique, is widely used in security, privacy, and diagnosis, etc. As DTA demands to collect and analyze massive taint data online, it suffers extremely high runtime overhead. Over the past decades, numerous attempts have been made to lower the overhead of DTA. Unfortunately, the reductions they achieved are marginal, causing DTA only applicable to the debugging/testing scenarios. In this paper, we propose and implement HardTaint, a system that can realize production-run dynamic taint tracking. HardTaint adopts a hybrid and systematic design which combines static analysis, selective hardware tracing and parallel graph processing techniques. The comprehensive evaluations demonstrate that HardTaint introduces only around 8% runtime overhead which is an order of magnitude lower than the state-of-the-arts, while without sacrificing any taint detection capability.
HybridSA: GPU Acceleration of Multi-pattern Regex Matching using Bit Parallelism
Authors: Le Glaunec Alexis , Kong Lingkun , Mamouras Konstantinos
Published: October 2024

Multi-pattern matching is widely used in modern software for applications requiring high throughput such as protein search, network traffic inspection, virus or spam detection. Graphics Processor Units (GPUs) excel at executing massively parallel workloads. Regular expression (regex) matching is typically performed by simulating the execution of deterministic finite automata (DFAs) or nondeterministic finite automata (NFAs). The natural implementations of these automata simulation algorithms on GPUs are highly inefficient because they give rise to irregular memory access patterns.

This paper presents HybridSA, a heterogeneous CPU-GPU parallel engine for multi-pattern matching. HybridSA uses bit parallelism to efficiently simulate NFAs on GPUs, thus reducing the number of memory accesses and increasing the throughput. Our bit-parallel algorithms extend the classical shift-and algorithm for string matching to a large class of regular expressions and reduce automata simulation to a small number of bitwise operations. We have developed a compiler to translate regular expressions into bit masks, perform optimizations, and choose the best algorithms to run on the GPU. The majority of the regular expressions are accelerated on the GPU, while the patterns that exhibit random memory accesses are executed on the CPU in parallel. We evaluate HybridSA against state-of-the-art CPU and GPU engines, as well as a hybrid combination of the two. HybridSA achieves between 4 and 60 times higher throughput than the state-of-the-art CPU engine and between 4 and 233 times better than the state-of-the-art GPU engine across a collection of real-world benchmarks.
StarMalloc: Verifying a Modern, Hardened Memory Allocator
Authors: Reitz Antonin , Fromherz Aymeric , Protzenko Jonathan
Published: October 2024

We present StarMalloc, a verified, efficient, security-oriented, and concurrent memory allocator. Using the Steel separation logic framework, we show how to specify and verify a multitude of low-level patterns and delicate security mechanisms, by relying on a combination of dependent types, SMT, and modular abstractions to enable efficient verification. We produce a verified artifact, in C, that implements the entire API surface of an allocator, and as such works as a drop-in replacement for real-world projects, notably the Firefox browser.

As part of StarMalloc, we develop several generic datastructures and proof libraries directly reusable in future systems verification projects. We also extend the Steel toolchain to express several low-level idioms that were previously missing. Finally, we show that StarMalloc exhibits competitive performance by evaluating it against 10 state-of-the-art memory allocators, and against a variety of real-world projects, such as Redis, the Lean compiler, and the Z3 SMT solver.
AUTOMAP: Inferring Rank-Polymorphic Function Applications with Integer Linear Programming
Authors: Schenck Robert , Hinnerskov Nikolaj Hey , Henriksen Troels , Madsen Magnus , Elsman Martin
Published: October 2024

Dynamically typed array languages such as Python, APL, and Matlab lift scalar operations to arrays and replicate scalars to fit applications. We present a mechanism for automatically inferring map and replicate operations in a statically-typed language in a way that resembles the programming experience of a dynamically-typed language while preserving the static typing guarantees. Our type system---which supports parametric polymorphism, higher-order functions, and top-level let-generalization---makes use of integer linear programming in order to find the minimum number of operations needed to elaborate to a well-typed program. We argue that the inference system provides useful and unsurprising guarantees to the programmer. We demonstrate important theoretical properties of the mechanism and report on the implementation of the mechanism in the statically-typed array programming language Futhark.
Monotone Procedure Summarization via Vector Addition Systems and Inductive Potentials
Authors: Pimpalkhare Nikhil , Kincaid Zachary
Published: October 2024

This paper presents a technique for summarizing recursive procedures operating on integer variables. The motivation of our work is to create more predictable program analyzers, and in particular to formally guarantee compositionality and monotonicity of procedure summarization. To summarize a procedure, we compute its best abstraction as a vector addition system with resets (VASR) and exactly summarize the executions of this VASR over the context-free language of syntactic paths through the procedure. We improve upon this technique by refining the language of syntactic paths using (automatically synthesized) linearpotential functionsthat bound the number of recursive calls within valid executions of the input program. We implemented our summarization technique in an automated program verification tool; our experimental evaluation demonstrates that our technique computes more precise summaries than existing abstract interpreters and that our tool’s verification capabilities are comparable with state-of-the-art software model checkers.
Automated Verification of Parametric Channel-Based Process Communication
Authors: Saioc Georgian-Vlad , Lange Julien , Møller Anders
Published: October 2024

A challenge of writing concurrent message passing programs is ensuring the absence of partial deadlocks, which can cause severe memory leaks in long running systems. Several static analysis techniques have been proposed for automatically detecting partial deadlocks in Go programs. For a large enterprise code base, we found these tools too imprecise to reason about process communication that is parametric, i.e., where the number of channel communication operations or the channel capacities are determined at runtime.

We present a novel approach to automatically verify the absence of partial deadlocks in Go program fragments with such parametric process communication. The key idea is to translate Go fragments to a core language that is sufficiently expressive to represent real-world parametric communication patterns and can be encoded into Dafny programs annotated with postconditions enforcing partial deadlock freedom. In situations where a fragment is partial deadlock free only when the concurrency parameters satisfy certain conditions, a suitable precondition can often be inferred.

Experimental results on a real-world code base containing 583 program fragments that are beyond the reach of existing techniques have shown that the approach can verify the absence of partial deadlocks in 145 cases. For an additional 228 cases, a nontrivial precondition is inferred that the surrounding code must satisfy to ensure partial deadlock freedom.
Type Inference Logics
Authors: Carnier Denis , Pottier François , Keuchel Steven
Published: October 2024

Type inference is essential for statically-typed languages such as OCaml and Haskell. It can be decomposed into two (possibly interleaved) phases: a generator converts programs to constraints; a solver decides whether a constraint is satisfiable. Elaboration, the task of decorating a program with explicit type annotations, can also be structured in this way. Unfortunately, most machine-checked implementations of type inference do not follow this phase-separated, constraint-based approach. Those that do are rarely executable, lack effectful abstractions, and do not include elaboration. To close the gap between common practice in real-world implementations and mechanizations inside proof assistants, we propose an approach that enables modular reasoning about monadic constraint generation in the presence of elaboration. Our approach includes a domain-specific base logic for reasoning about metavariables and a program logic that allows us to reason abstractly about the meaning of constraints. To evaluate it, we report on a machine-checked implementation of our techniques inside the Coq proof assistant. As a case study, we verify both soundness and completeness for three elaborating type inferencers for the simply typed lambda calculus with Booleans. Our results are the first demonstration that type inference algorithms can be verified in the same form as they are implemented in practice: in an imperative style, modularly decomposed into constraint generation and solving, and delivering elaborated terms to the remainder of the compiler chain.
Wasm-R3: Record-Reduce-Replay for Realistic and Standalone WebAssembly Benchmarks
Authors: Baek Doehyun , Getz Jakob , Sim Yusung , Lehmann Daniel , Titzer Ben L. , Ryu Sukyoung , Pradel Michael
Published: October 2024

WebAssembly (Wasm for short) brings a new, powerful capability to the web as well as Edge, IoT, and embedded systems. Wasm is a portable, compact binary code format with high performance and robust sandboxing properties. As Wasm applications grow in size and importance, the complex performance characteristics of diverse Wasm engines demand robust, representative benchmarks for proper tuning. Stopgap benchmark suites, such as PolyBenchC and libsodium, continue to be used in the literature, though they are known to be unrepresentative. Porting of more complex suites remains difficult because Wasm lacks many system APIs and extracting real-world Wasm benchmarks from the web is difficult due to complex host interactions. To address this challenge, we introduce Wasm-R3, the first record and replay technique for Wasm. Wasm-R3 transparently injects instrumentation into Wasm modules to record an execution trace from inside the module, then reduces the execution trace via several optimizations, and finally produces a replay module that is executable standalone without any host environment-on any engine. The benchmarks created by our approach are (i) realistic, because the approach records real-world web applications, (ii) faithful to the original execution, because the replay benchmark includes the unmodified original code, only adding emulation of host interactions, and (iii) standalone, because the replay benchmarks run on any engine. Applying Wasm-R3 to web-based Wasm applications in the wild demonstrates the correctness of our approach as well as the effectiveness of our optimizations, which reduce the recorded traces by 99.53% and the size of the replay benchmark by 9.98%. We release the resulting benchmark suite of 27 applications, called Wasm-R3-Bench, to the community, to inspire a new generation of realistic and standalone Wasm benchmarks.
Mark–Scavenge: Waiting for Trash to Take Itself Out
Authors: Norlinder Jonas , Österlund Erik , Black-Schaffer David , Wrigstad Tobias
Published: October 2024

Moving garbage collectors (GCs) typically free memory by evacuating live objects in order to reclaim contiguous
memory regions. Evacuation is typically done either during tracing (scavenging), or after tracing when
identification of live objects is complete (mark–evacuate). Scavenging typically requires more memory (memory
for all objects to be moved), but performs less work in sparse memory areas (single pass). This makes it
attractive for collecting young objects. Mark–evacuate typically requires less memory and performs less
work in memory areas with dense object clusters, by focusing relocation around sparse regions, making it
attractive for collecting old objects. Mark–evacuate also completes identification of live objects faster, making
it attractive for concurrent GCs that can reclaim memory immediately after identification of live objects
finishes (as opposed to when evacuation finishes), at the expense of more work compared to scavenging, for
young objects.

We propose an alternative approach for concurrent GCs to combine the benefits of scavenging with the
benefits of mark–evacuate, for young objects. The approach is based on the observation that by the time
young objects are relocated by a concurrent GC, they are likely to already be unreachable. By performing
relocation lazily, most of the relocations in the defragmentation phase of mark–evacuate can typically be
eliminated. Similar to scavenging, objects are relocated during tracing with the proposed approach. However,
instead of relocating all objects that are live in the current GC cycle, it lazily relocates profitable sparse object
clusters that survived from the previous GC cycle. This turns the memory headroom that concurrent GCs
typically “waste” in order to safely avoid running out of memory before GC finishes, into an asset used to
eliminate much of the relocation work, which constitutes a significant portion of the GC work.

We call this technique mark–scavenge and implement it on-top of ZGC in OpenJDK in a collector we call
MS-ZGC. We perform a performance evaluation that compares MS-ZGC against ZGC. The most striking result
is (up to) 91% reduction in relocation of dead objects (depending on machine-dependent factors).
Dependency-Aware Code Naturalness
Authors: Yang Chen , Chen Junjie , Jiang Jiajun , Huang Yuliang
Published: October 2024

Code naturalness, which captures repetitiveness and predictability in programming languages, has proven valuable for various code-related tasks in software engineering. However, precisely measuring code naturalness remains a fundamental challenge. Existing methods measure code naturalness over individual lines of code while ignoring the deep semantic relations among different lines, e.g., program dependency, which may negatively affect the precision of the measure. Despite the intuitive appeal of extending the code naturalness measure to the code dependency domain (as there are some work that have initiated the utilization of code dependency for diverse code-related tasks), this assumption remains unexplored and warrants direct investigation. In this study, we aim to perform the first empirical study to investigate whether incorporating code dependency, instead of analyzing individual lines, can enhance the precision of measuring code naturalness.

To achieve that, we first propose a new method named DAN for measuring code naturalness by incorporating the rich dependency information in the code. Specifically, DAN extracts multiple sequences of code lines by traversing the program dependency graph, where different code lines are connected by dependencies in each sequence, and then the code naturalness will be measured by taking each sequence as a whole. In this way, the dependency information can be well captured. Finally, we have conducted an extensive study to evaluate the influence of code dependency for measuring code naturalness with DAN, and compared it with the state-of-the-art methods under three emerging application scenarios of code naturalness. The results demonstrate that DAN can not only better distinguish natural and unnatural code, but also substantially boost two important downstream applications of code naturalness, i.e., distinguishing buggy and non-buggy code lines and data cleansing for training better code models, reflecting the significance of code dependency in measuring code naturalness.
Fast and Optimal Extraction for Sparse Equality Graphs
Authors: Goharshady Amir Kafshdar , Lam Chun Kit , Parreaux Lionel
Published: October 2024

Equality graphs (e-graphs) are used to compactly represent equivalence classes of terms in symbolic reasoning systems. Beyond their original roots in automated theorem proving, e-graphs have been used in a variety of applications. They have become particularly important as the key ingredient in the popular technique of equality saturation, which has notable applications in compiler optimization, program synthesis, program verification, and symbolic execution, among others. In a typical equality saturation workflow, an e-graph is used to store a large number of equalities that are generated by local rewrites during a saturation phase, after which an optimal term is extracted from the e-graph as the output of the technique. However, despite its crucial role in equality saturation, e-graph extraction has received relatively little attention in the literature, which we seek to start addressing in this paper. Extraction is a challenging problem and is notably known to be NP-hard in general, so current equality saturation tools rely either on slow optimal extraction algorithms based on integer linear programming (ILP) or on heuristics that may not always produce the optimal result. In fact, in this paper, we show that e-graph extraction is hard to approximate within any constant ratio. Thus, any such heuristic will produce wildly suboptimal results in the worst case. Fortunately, we show that the problem becomes tractable when the e-graph is sparse, which is the case in many practical applications. We present a novel parameterized algorithm for extracting optimal terms from e-graphs with low treewidth, a measure of how “tree-like” a graph is, and prove its correctness. We also present an efficient Rust implementation of our algorithm and evaluate it against ILP on a number of benchmarks extracted from the Cranelift benchmark suite, a real-world compiler optimization library based on equality saturation. Our algorithm optimally extracts e-graphs with treewidths of up to 10 in a fraction of the time taken by ILP. These results suggest that our algorithm can be a valuable tool for equality saturation users who need to extract optimal terms from sparse e-graphs.
Area-driven Boolean bi-decomposition by function approximation
Authors: Bernasconi Anna , Ciriani Valentina , Cortadella Jordi , Costa Marco , Villa Tiziano
Published: October 2024

Bi-decomposition rewrites logic functions as the composition of simpler components. It is related to Boolean division, where a given function is rewritten as the product of a divisor and a quotient, but bi-decomposition can be defined for any Boolean operation of two operands. The key questions are how to find a good divisor and then how to compute the quotient. In this article, we select the divisor by approximation of the original function and then characterize by an incompletely specified function the full flexibility of the quotient for each binary operator. We target area-driven exact bi-decomposition, and we apply it to the bi-decomposition of Sum-of-Products (SOP) forms. We report experiments that exhibit significant gains in literals of SOP forms when rewritten as bi-decompositions with respect to the product operator. This suggests the application of this framework to other logic forms and binary operations, both for exact and approximate implementations.
The Role of (E)-β-Farnesene in Tritrophic Interactions: Biosynthesis, Chemoreception, and Evolution
Authors: Wang Bing , Jacquin-Joly Emmanuelle , Wang Guirong
Published: October 2024

(E)-β-farnesene (EBF) stands out as a crucial volatile organic compound, exerting significant influence on the complex interactions between plants, aphids, and predator insects. Serving as an alarm signal within aphids, EBF is also emitted by plants as a defense mechanism to attract aphid predators. This review delves into EBF sources, functions, biosynthesis, detection mechanisms, and its coevolutionary impacts on aphids and insect predators. The exploration underscores the need to comprehend the biophysical and structural foundations of EBF receptors in aphids, emphasizing their role in unraveling the intricate patterns and mechanisms of interaction between EBF and target receptors. Furthermore, we advocate for adopting structure-based or machine-learning methodologies to anticipate receptor–ligand interactions. On the basis of this knowledge, we propose future research directions aiming at designing, optimizing, and screening more stable and efficient active odorants. A pivotal outcome of this comprehensive investigation aims to contribute to the development of more effective aphid-targeted control strategies.
The Social Psychology of Justice Repair
Authors: Okimoto Tyler G. , Gollwitzer Mario
Published: October 2024

Justice scholars have elaborated a variety of social psychological mechanisms that contribute to our desire to see some action following an injustice, to see justice done. Research over the past 20 years has significantly advanced our understanding of how to repair a sense of justice by articulating the psychological needs that follow from its experience from victim, offender, and observer perspectives. In this review, we summarize key insights from this literature, including the specific needs identified as relevant to justice, the challenges that arise when seeking justice for multiple parties in a conflict, and the procedural approaches that can aid in reconciling disparate perspectives. Following this review, we challenge our own assumption that justice repair is necessary. As a departure from this deficit model, we draw inspiration from adjacent fields of study to propose “justice making” as an alternative avenue for reconciliation in situations where justice repair is unachievable.
Boosting Deep Learning for Interpretable Brain MRI Lesion Detection through the Integration of Radiology Report Information
Authors: Dai Lisong , Lei Jiayu , Ma Fenglong , Sun Zheng , Du Haiyan , Zhang Houwang , Jiang Jingxuan , Wei Jianyong , Wang Dan , Tan Guang , Song Xinyu , Zhu Jinyu , Zhao Qianqian , Ai Songtao , Shang Ai , Li Zhaohui , Zhang Ya , Li Yuehua
Published: October 2024

A deep learning model incorporating radiology report–derived textual features outperformed a basic deep learning model trained without textual features in identifying 14 brain diseases and normal brain on MR images while providing interpretable attention maps.
Wet-Chemical Synthesis of a Protective Coating on NCM111 Cathode: The Quantified Effects of Washing, Sintering and Coating
Authors: Maskova Liga , Ignatans Reinis , Viksna Arturs , Sarakovskis Anatolijs , Knite Maris , Kucinskis Gints
Published: October 2024

LiNixCoyMn1-x-yO2 (NCM) cathodes, especially with high Ni content, are widely expected to keep advancing the energy density of Li-ion batteries. However, ensuring a good cycle life remains a key challenge. Applying inert protective coatings on the surface of NCMs is a common route for mitigating surface-based degradation. In this study a sustainable ethanol-based wet-chemical coating method for covering the material with Al2O3 is developed and demonstrated on NCM111. The effect of the synthesis procedure is carefully evaluated to distinguish the benefits of the protective coating from the contributions of re-sintering and removal of surface contaminants, all taking place during the synthesis of the coated material. We show that while the cycling stability is significantly improved by the material regeneration alone (65% vs 79% state-of-health after 500 charge-discharge cycles at voltage range 2.7–4.3 V vs Li/Li+), the Al2O3-coated material displays further cycle life gains, maintaining 88% of initial capacity after 500 charge-discharge cycles. This work thus demonstrates both a sustainable wet-chemical coating method and the importance of establishing a proper baseline for characterization of inert protective coatings in general. The importance of both gains further prominence with the transition to inherently less stable higher Ni content NCMs.
Construction and Analysis of Battery Equivalent Circuit Model Considering Liquid Phase Lithium Ion Diffusion Under High-Rate Conditions
Authors: Chen Yan , Lin Jian , Tang Yuwei , Qi Ziyi , Tang Honglin
Published: October 2024

In order to obtain the internal state of lithium-ion battery quickly and accurately, the problem that the internal state of the battery is difficult to estimate quickly and accurately is solved. The discharge performance of lithium ion is affected by the electrode current during the charge and discharge process. This paper analyzes the key factors of the electrochemical model at high rate, considers the change of lithium ion concentration in the liquid phase of the battery, integrates the electrochemical mechanism and the equivalent circuit, and establishes a mechanism equivalent circuit model with more computational advantages through circuit elements. The equivalent circuit model can describe the physical characteristics of the lithium battery. Under high rate constant current and dynamic conditions, the model shows good electrical characteristics. Compared with the traditional empirical equivalent circuit model, the accuracy of the model is improved, and the state quantity is reduced by 15 compared with the electrochemical model. The model is of great significance in practical application.
MnO2@Fe2O3 Cathode for Aqueous Zinc/Manganese Batteries: Enhanced Discharge Capacity and Stability through Forming FeMnO3
Authors: Weng Haochen , Li Mingqiang , Xu Shuailiang , Li Jingwen
Published: October 2024

Rechargeable Zn/MnO2 batteries suffer from limited cycle life and low capacity. We utilized MnO2@Fe2O3 as the cathode material, achieving a discharge capacity of 290 mAh g−1 at 1 A g−1. The Zn/MnO2@Fe2O3 battery maintained over 90% coulombic efficiency after 1800 cycles at 1 A g−1. Even at 5 A g−1, it reached 154 mAh g−1. The addition of Fe2O3 changed the reaction mechanism and realized the MnO2@Fe2O3 transformation between MnO2@Fe2O3 and MnOOH, FeMnO3 based on the co-doping and conversion of H+/Fe(III). This study underscores the immense potential of the MnO2@Fe2O3 electrode in energy storage applications and highlights the significance of Fe2O3 in enhancing cathode cycling stability and discharge capacity.
Calcitonin gene-related peptide promotes epithelial reparative and anticolitic functions of IL-4 educated human macrophages
Authors: Callejas Blanca E. , Sousa James A. , Flannigan Kyle L. , Wang Arthur , Higgins Eve , Herik Aydin I. , Li Shuhua , Rajeev Sruthi , Rosentreter Ryan , Panaccione Remo , McKay Derek M.
Published: October 2024

A novel pathway is identified whereby interleukin-4-educated human macrophages [M(IL4)s] exposed to calcitonin gene-related peptide (CGRP) reduce oxazolone-induced colitis and promote epithelial wound healing in vitro through COX1-dependent signaling. Support is provided for the concept of macrophage transfer to treat enteric inflammation where neuroimmune interaction, in this case CGRP neuropeptide, produced under inflammatory conditions will reinforce the anticolitic and wound repair capacity of M(IL4) autologous-based therapy for IBD treatment.
Microtubule Reorganization and Quiescence: an Intertwined Relationship
Authors: Laporte Damien , Sagot Isabelle
Published: October 2024

Quiescence is operationally defined as a reversible proliferation arrest. This cellular state is central to both organism development and homeostasis, and its dysregulation causes many pathologies. The quiescent state encompasses very diverse cellular situations depending on the cell type and its environment. Further, quiescent cell properties evolve with time, a process that is thought to be the origin of aging in multicellular organisms. Microtubules are found in all eukaryotes and are essential for cell proliferation as they support chromosome segregation and intracellular trafficking. Upon proliferation cessation and quiescence establishment, the microtubule cytoskeleton was shown to undergo significant remodeling. The purpose of this review is to examine the literature in search of evidence to determine whether the observed microtubule reorganizations are merely a consequence of quiescence establishment or if they somehow participate in this cell fate decision.