bluuebunny/crossref_metadata_2025 huggingface dataset:
One-step embedding method for maintaining orientation of pathological tissue specimens using agar thin films
Authors: Uchiyama Atsushi , Kimura Fumikazu , Wakatsuki Yoshie , Yoshida Erika , Kato Ayako , Kato Kurumi , Yoshida Rio , Ito Yurie , Okimura Akira , Nakatsugawa Munehide
Published: October 2023

Pathological histology examination involves handling a variety of specimens that are cut according to regulations and placed in cassettes. Tissue fragments in the cassettes are then diagnosed after processing, embedding, thin sectioning, staining and other procedures using a processing machine. Maintaining tissue fragment order and orientation during these processes is important for accurate diagnosis. In this study, we present a method of maintaining tissue fragment order and orientation using a thin film of ultra-high-strength agar and evaluate its usefulness during tissue sectioning.

Cassettes were prepared, each containing three pieces of porcine liver, and compared embedding time with and without agar thin films (ATFs). Embedding was performed by three medical laboratory scientists with different levels of experience.

To enable one-step tissue sample embedding, ATFs were integrated with samples in the cassettes. This resulted in an average reduction of 6.22 s of embedding time per cassette compared with traditional embedding methods.

Through the use of ATFs, tissue fragment order and orientation is maintained, and embedding process time shortened. Additionally, ATFs are easily prepared and stored in 10% neutral buffered formalin over extended periods, allowing for immediate use during sectioning. This method is ideal to implement in busy pathology laboratories.
Is ageing still undesirable? A reply to Räsänen
Authors: García-Barranquero Pablo , Llorca Albareda Joan , Díaz-Cobacho Gonzalo
Published: October 2023

We have recently stated the reasons why we claim that biological ageing is undesirable. Räsänen has responded to our article by arguing that this process has certain desirable aspects and, therefore, our position is inconsistent. Räsänen develops two arguments to defend his position. We will call the first the argument from the totality of the ageing process and the second the argument from the reduced goods of the ageing process. In this reply, we will give reasons to show that both arguments fail. The first, on the one hand, starts from a dubious conception of ageing and, on the other hand, even accepting this conception, its reformulation is morally empty. The second incurs in an absurd conclusion.
Surveillance is the first step to preventing injury among fast jet aircrew: results of a 2-year prospective cohort study
Authors: Wallace James Byron , Osmotherly Peter G , Gabbett Tim J , Spratford Wayne , Newman Phil Mark
Published: October 2023

Objectives

Injury surveillance is imperative for injury prevention but difficult in military populations. Our objective was to accurately describe the pattern of musculoskeletal complaints among Royal Australian Air Force (RAAF) fast jet aircrew (FJA) using the validated University of Canberra Fast Jet Aircrew Musculoskeletal Questionnaire (UC-FJAMQ) over a 2-year period, and determine injury burden on the workforce and operational capability.

Methods

306 RAAF FJA were monitored over a 2-year period (4×5 month reporting periods). Musculoskeletal complaint episodes (MCEs) were captured weekly using the UC-FJAMQ. Time loss episodes (TLEs) were captured from the UC-FJAMQ and injury registers completed by embedded physiotherapists. Cumulative severity and operational impact scores from the UC-FJAMQ, and time loss duration, were used to describe severity and calculate burden.

Results

Mean weekly UC-FJAMQ response rate was 62%. 1012 MCEs were captured, with a mean weekly prevalence of 14.9% (95% CI 14.2–15.6), and incidence of 4.1 episodes per person-year (95% CI 3.9–4.4). A total of 145 TLEs were captured, with a mean 5-month prevalence of 12.4% (range 8.9–15.3%), and incidence of 0.37 episodes per person-year (95% CI 0.31–0.43). Spinal regions accounted for 81% of MCEs and contributed 76% and 85% of burden in relation to cumulative severity and operational impact, respectively. 57% of TLE burden came from spinal regions.

Conclusions

Despite modest weekly UC-FJAMQ response rates, musculoskeletal complaints were shown to be widespread and negatively impact operational capability. Future injury prevention efforts among FJA should focus on spinal regions, particularly the neck.
Droplets and supersolids in ultra-cold atomic quantum gases
Authors: Mukherjee K. , Cardinale T. Arnone , Chergui L. , Stürmer P. , Reimann S. M.
Published: October 2023

In this mini-review, we briefly summarize some of the main concepts and ideas behind highly dilute self-bound quantum droplets of both binary and dipolar character. The latter type of systems has more recently led to the experimental discovery of a dipolar supersolid state that allows entirely new insights on this long-sought purely quantum state of matter, with exciting prospects for fundamental research as well as future applied quantum sensing technologies. The first half of the review provides a brief history of droplets and supersolidity in various settings and also discusses the self-binding in binary quantum gases, and the second half of the review summarizes our own recent work in the field, presented at the 2022 FQMT conference in Prague.
Leaf: Modularity for Temporary Sharing in Separation Logic
Authors: Hance Travis , Howell Jon , Padon Oded , Parno Bryan
Published: October 2023

In concurrent verification, separation logic provides a strong story for handling both resources that are owned exclusively and resources that are shared persistently (i.e., forever). However, the situation is more complicated for temporarily shared state, where state might be shared and then later reclaimed as exclusive. We believe that a framework for temporarily-shared state should meet two key goals not adequately met by existing techniques. One, it should allow and encourage users to verify new sharing strategies. Two, it should provide an abstraction where users manipulate shared state in a way agnostic to the means with which it is shared.

We present Leaf, a library in the Iris separation logic which accomplishes both of these goals by introducing a novel operator, which we call guarding, that allows one proposition to represent a shared version of another. We demonstrate that Leaf meets these two goals through a modular case study: we verify a reader-writer lock that supports shared state, and a hash table built on top of it that uses shared state.
Synthesizing Efficient Memoization Algorithms
Authors: Sun Yican , Peng Xuanyu , Xiong Yingfei
Published: October 2023

In this paper, we propose an automated approach to finding correct and efficient memoization algorithms from a given declarative specification. This problem has two major challenges: (i) a memoization algorithm is too large to be handled by conventional program synthesizers; (ii) we need to guarantee the efficiency of the memoization algorithm. To address this challenge, we structure the synthesis of memoization algorithms by introducing the local objective function and the memoization partition function and reduce the synthesis task to two smaller independent program synthesis tasks. Moreover, the number of distinct outputs of the function synthesized in the second synthesis task also decides the efficiency of the synthesized memoization algorithm, and we only need to minimize the number of different output values of the synthesized function. However, the generated synthesis task is still too complex for existing synthesizers. Thus, we propose a novel synthesis algorithm that combines the deductive and inductive methods to solve these tasks. To evaluate our algorithm, we collect 42 real-world benchmarks from Leetcode, the National Olympiad in Informatics in Provinces-Junior (a national-wide algorithmic programming contest in China), and previous approaches. Our approach successfully synhesizes 39/42 problems in a reasonable time, outperforming the baselines.
AtomiS: Data-Centric Synchronization Made Practical
Authors: Paulino Hervé , Almeida Matos Ana , Cederquist Jan , Giunti Marco , Matos João , Ravara António
Published: October 2023

Data-Centric Synchronization (DCS) shifts the reasoning about concurrency restrictions from control structures to data declaration. It is a high-level declarative approach that abstracts away from the actual concurrency control mechanism(s) in use. Despite its advantages, the practical use of DCS is hindered by the fact that it may require many annotations and/or multiple implementations of the same method to cope with differently qualified parameters.

To overcome these limitations, in this paper we present AtomiS, a new DCS approach that requires only qualifying types of parameters and return values in interface definitions, and of fields in class definitions. The latter may also be abstracted away in type parameters, rendering class implementations virtually annotation-free. From this high level specification, a static analysis infers the atomicity constraints that are local to each method, considering valid only the method variants that are consistent with the specification, and performs code generation for all valid variants of each method. The generated code is then the target for automatic injection of concurrency control primitives that are responsible for ensuring the absence of data-races,
atomicity-violations and deadlocks.

We provide a Java implementation and showcase the applicability of AtomiS in real-life code. For the
benchmarks analysed, AtomiS requires fewer annotations than the original number of regions requiring locks, as well as fewer annotations than Atomic Sets (a reference DCS proposal).
Beacons: An End-to-End Compiler Framework for Predicting and Utilizing Dynamic Loop Characteristics
Authors: Mururu Girish , Khan Sharjeel , Chatterjee Bodhisatwa , Chen Chao , Porter Chris , Gavrilovska Ada , Pande Santosh
Published: October 2023

Efficient management of shared resources is a critical problem in high-performance computing (HPC) environments. Existing workload management systems often promote non-sharing of resources among different co-executing applications to achieve performance isolation. Such schemes lead to poor resource utilization and suboptimal process throughput, adversely affecting user productivity. Tackling this problem in a scalable fashion is extremely challenging, since it requires the workload scheduler to possess an in-depth knowledge about various application resource requirements and runtime phases at fine granularities within individual applications.

In this work, we show that
applications’ resource requirements and execution phase behaviour can be captured
in a scalable and lightweight manner at runtime by estimating important program artifacts termed as “
dynamic loop characteristics
”. Specifically,
we propose a solution to the problem of efficient workload scheduling by designing a compiler and runtime cooperative framework that leverages novel loop-based compiler analysis for resource allocation
.

We present
Beacons Framework
, an end-to-end compiler and scheduling framework, that
estimates
dynamic loop characteristics,
encapsulates
them in compiler-instrumented
beacons
in an application, and
broadcasts
them during application runtime, for proactive workload scheduling.
We focus on estimating four important loop characteristics
:
loop trip-count
,
loop timing
,
loop memory footprint
, and
loop data-reuse behaviour
, through a combination of compiler analysis and machine learning.

The novelty of the Beacons Framework also lies in its ability to tackle
irregular loops that exhibit complex control flow with indeterminate loop bounds involving structure fields, aliased variables and function calls
, which are highly prevalent in modern workloads. At the backend, Beacons Framework entails a
proactive workload scheduler that leverages the runtime information to orchestrate aggressive process co-locations, for maximizing resource concurrency, without causing cache thrashing
. Our results show that Beacons Framework can predict different loop characteristics with an accuracy of
85%
to
95%
on average, and the proactive scheduler obtains an average throughput improvement of
1.9x
(up to
3.2x
) over the state-of-the-art schedulers on an Amazon Graviton2 machine on consolidated workloads involving 1000-10000 co-executing processes, across 51 benchmarks.
Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity
Authors: Sano Chuta , Kavanagh Ryan , Pientka Brigitte
Published: October 2023

Session types employ a linear type system that ensures that communication channels cannot be implicitly copied or discarded. As a result, many mechanizations of these systems require modeling channel contexts and carefully ensuring that they treat channels linearly. We demonstrate a technique that localizes linearity conditions as additional predicates embedded within type judgments, which allows us to use structural typing contexts instead of linear ones. This technique is especially relevant when leveraging (weak) higher-order abstract syntax to handle channel mobility and the intricate binding structures that arise in session-typed systems. Following this approach, we mechanize a session-typed system based on classical linear logic and its type preservation proof in the proof assistant Beluga, which uses the logical framework LF as its encoding language. We also prove adequacy for our encoding. This shows the tractability and effectiveness of our approach in modelling substructural systems such as session-typed languages.
Graph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Affordable with Precise Effect Dependencies
Authors: Bračevac Oliver , Wei Guannan , Jia Songlin , Abeysinghe Supun , Jiang Yuxuan , Bao Yuyan , Rompf Tiark
Published: October 2023

Graph-based intermediate representations (IRs) are widely used for powerful compiler optimizations, either interprocedurally in pure functional languages, or intraprocedurally in imperative languages. Yet so far, no suitable graph IR exists for aggressive global optimizations in languages with both effects and higher-order functions: aliasing and indirect control transfers make it difficult to maintain sufficiently granular dependency information for optimizations to be effective. To close this long-standing gap, we propose a novel typed graph IR combining a notion of reachability types with an expressive effect system to compute precise and granular effect dependencies at an affordable cost while supporting local reasoning and separate compilation. Our high-level graph IR imposes lexical structure to represent structured control flow and nesting, enabling aggressive and yet inexpensive code motion and other optimizations for impure higher-order programs. We formalize the new graph IR based on a λ-calculus with a reachability type-and-effect system along with a specification of various optimizations. We present performance case studies for tensor loop fusion, CUDA kernel fusion, symbolic execution of LLVM IR, and SQL query compilation in the Scala LMS compiler framework using the new graph IR. We observe significant speedups of up to 21x.
How Profilers Can Help Navigate Type Migration
Authors: Greenman Ben , Felleisen Matthias , Dimoulas Christos
Published: October 2023

Sound migratory typing envisions a safe and smooth refactoring of untyped code bases to typed ones. However, the cost of enforcing safety with run-time checks is often prohibitively high, thus performance regressions are a likely occurrence. Additional types can often recover performance, but choosing the right components to type is difficult because of the exponential size of the migratory typing lattice. In principal though, migration could be guided by off-the-shelf profiling tools. To examine this hypothesis, this paper follows the rational programmer method and reports on the results of an experiment on tens of thousands of performance-debugging scenarios via seventeen strategies for turning profiler output into an actionable next step. The most effective strategy is the use of deep types to eliminate the most costly boundaries between typed and untyped components; this strategy succeeds in more than 50% of scenarios if two performance degradations are tolerable along the way.
Towards Better Semantics Exploration for Browser Fuzzing
Authors: Zhou Chijin , Zhang Quan , Guo Lihua , Wang Mingzhe , Jiang Yu , Liao Qing , Wu Zhiyong , Li Shanshan , Gu Bin
Published: October 2023

Web browsers exhibit rich semantics that enable a plethora of web-based functionalities. However, these intricate semantics present significant challenges for the implementation and testing of browsers. For example, fuzzing, a widely adopted testing technique, typically relies on handwritten context-free grammars (CFGs) for automatically generating inputs. However, these CFGs fall short in adequately modeling the complex semantics of browsers, resulting in generated inputs that cover only a portion of the semantics and are prone to semantic errors. In this paper, we present SaGe, an automated method that enhances browser fuzzing through the use of production-context sensitive grammars (PCSGs) incorporating semantic information. Our approach begins by extracting a rudimentary CFG from W3C standards and iteratively enhancing it to create a PCSG. The resulting PCSG enables our fuzzer to generate inputs that explore a broader range of browser semantics with a higher proportion of semantically-correct inputs. To evaluate the efficacy of SaGe, we conducted 24-hour fuzzing campaigns on mainstream browsers, including Chrome, Safari, and Firefox. Our approach demonstrated better performance compared to existing browser fuzzers, with a 6.03%-277.80% improvement in edge coverage, a 3.56%-161.71% boost in semantic correctness rate, twice the number of bugs discovered. Moreover, we identified 62 bugs across the three browsers, with 40 confirmed and 10 assigned CVEs.
Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory
Authors: Vindum Simon Friis , Birkedal Lars
Published: October 2023

Weak persistent memory (a.k.a. non-volatile memory) is an emerging technology that offers fast byte-addressable durable main memory.
A wealth of algorithms and libraries has been developed to explore this exciting technology.
As noted by others, this has led to a significant verification gap.
Towards closing this gap, we present Spirea, the first concurrent separation logic for verification of programs under a weak persistent memory model.
Spirea is based on the Iris and Perennial verification frameworks, and by combining features from these logics with novel techniques it supports high-level modular reasoning about crash-safe and thread-safe programs and libraries.
Spirea is fully mechanized in the Coq proof assistant and allows for interactive development of proofs with the Iris Proof Mode.
We use Spirea to verify several challenging examples with modular specifications.
We show how our logic can verify thread-safety and crash-safety of non-blocking durable data structures with null-recovery,
in particular the Treiber stack and the Michael-Scott queue adapted to persistent memory.
This is the first time durable data structures have been verified with a program logic.
An Explanation Method for Models of Code
Authors: Wang Yu , Wang Ke , Wang Linzhang
Published: October 2023

This paper introduces a novel method, called WheaCha, for explaining the predictions of code models. Similar to attribution methods, WheaCha seeks to identify input features that are responsible for a particular prediction that models make. On the other hand, it differs from attribution methods in crucial ways. Specifically, WheaCha separates an input program into "wheat" (i.e., defining features that are the reason for which models predict the label that they predict) and the rest "chaff" for any given prediction. We realize WheaCha in a tool, HuoYan, and use it to explain four prominent code models: code2vec, seq-GNN, GGNN, and CodeBERT. Results show that (1) HuoYan is efficient — taking on average under twenty seconds to compute wheat for an input program in an end-to-end fashion (i.e., including model prediction time); (2) the wheat that all models use to make predictions is predominantly comprised of simple syntactic or even lexical properties (i.e., identifier names); (3) neither the latest explainability methods for code models (i.e., SIVAND and CounterFactual Explanations) nor the most noteworthy attribution methods (i.e., Integrated Gradients and SHAP) can precisely capture wheat. Finally, we set out to demonstrate the usefulness of WheaCha, in particular, we assess if WheaCha’s explanations can help end users to identify defective code models (e.g., trained on mislabeled data or learned spurious correlations from biased data). We find that, with WheaCha, users achieve far higher accuracy in identifying faulty models than SIVAND, CounterFactual Explanations, Integrated Gradients and SHAP.
Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic
Authors: Jung Jaehwang , Lee Janggun , Choi Jaemin , Kim Jaewoo , Park Sunho , Kang Jeehoon
Published: October 2023

Formal verification is an effective method to address the challenge of designing correct and efficient concurrent data structures. But verification efforts often ignore
memory reclamation
, which involves nontrivial synchronization between concurrent accesses and reclamation. When incorrectly implemented, it may lead to critical safety errors such as use-after-free and the ABA problem. Semi-automatic safe memory reclamation schemes such as hazard pointers and RCU encapsulate the complexity of manual memory management in modular interfaces. However, this modularity has not been carried over to formal verification.

We propose modular specifications of hazard pointers and RCU, and formally verify realistic implementations of them in concurrent separation logic. Specifically, we design abstract predicates for hazard pointers that capture the meaning of
validating
the protection of nodes, and those for RCU that support
optimistic traversal
to possibly retired nodes. We demonstrate that the specifications indeed facilitate modular verification in three criteria: compositional verification, general applicability, and easy integration. In doing so, we present the first formal verification of Harris’s list, the Harris-Michael list, the Chase-Lev deque, and RDCSS with reclamation. We report the Coq mechanization of all our results in the Iris separation logic framework.
A Cocktail Approach to Practical Call Graph Construction
Authors: Cai Yuandao , Zhang Charles
Published: October 2023

After decades of research, constructing call graphs for modern C-based software remains either imprecise or inefficient when scaling up to the ever-growing complexity. The main culprit is the difficulty of resolving function pointers, as precise pointer analyses are cubic in nature and become exponential when considering calling contexts. This paper takes a practical stance by first conducting a comprehensive empirical study of function pointer manipulations in the wild. By investigating 5355 indirect calls in five popular open-source systems, we conclude that, instead of the past uniform treatments for function pointers, a cocktail approach can be more effective in “squeezing” the number of difficult pointers to a minimum using a potpourri of cheap methods. In particular, we decompose the costs of constructing highly precise call graphs of big code by tailoring several increasingly precise algorithms and synergizing them into a concerted workflow. As a result, many indirect calls can be precisely resolved in an efficient and principled fashion, thereby reducing the final, expensive refinements. This is, in spirit, similar to the well-known cocktail medical therapy.

The results are encouraging — our implemented prototype called Coral can achieve similar precision versus the previous field-, flow-, and context-sensitive Andersen-style call graph construction, yet scale up to millions of lines of code for the first time, to the best of our knowledge. Moreover, by evaluating the produced call graphs through the lens of downstream clients (i.e., use-after-free detection, thin slicing, and directed grey-box fuzzing), the results show that Coral can dramatically improve their effectiveness for better vulnerability hunting, understanding, and reproduction. More excitingly, we found twelve confirmed bugs (six impacted by indirect calls) in popular systems (e.g., MariaDB), spreading across multiple historical versions.
Complete First-Order Reasoning for Properties of Functional Programs
Authors: Murali Adithya , Peña Lucas , Jhala Ranjit , Madhusudan P.
Published: October 2023

Several practical tools for automatically verifying functional programs (e.g., Liquid Haskell and Leon for Scala programs) rely on a heuristic based on unrolling recursive function definitions followed by quantifier-free reasoning using SMT solvers. We uncover foundational theoretical properties of this heuristic, revealing that it can be generalized and formalized as a technique that is in fact
complete
for reasoning with combined First-Order theories of algebraic datatypes and background theories, where background theories support decidable quantifier-free reasoning. The theory developed in this paper explains the efficacy of these heuristics when they succeed, explain why they fail when they fail, and the precise role that user help plays in making proofs succeed.
Automated Ambiguity Detection in Layout-Sensitive Grammars
Authors: Liu Jiangyi , Zhu Fengmin , He Fei
Published: October 2023

Layout-sensitive grammars have been adopted in many modern programming languages.
In a serious language design phase, the specified syntax—typically a grammar—must be unambiguous.
Although checking ambiguity is undecidable for context-free grammars and (trivially also) layout-sensitive grammars,
ambiguity detection
, on the other hand, is possible and can benefit language designers from
exposing potential design flaws
.

In this paper, we tackle the ambiguity detection problem in layout-sensitive grammars.
Inspired by a previous work on checking the
bounded ambiguity
of context-free grammars via
SAT solving
, we intensively extend their approach to support layout-sensitive grammars but via
SMT solving
to express the ordering and quantitative relations over line/column numbers.
Our key novelty lies in a
reachability
condition, which takes the impact of layout constraints on ambiguity into careful account.
With this condition in hand, we propose an equivalent ambiguity notion called
local ambiguity
for the convenience of SMT encoding.
We translate local ambiguity into an SMT formula and developed a
bounded ambiguity checker
that
automatically
finds a
shortest
nonempty ambiguous sentence (if exists) for a user-input grammar.
The
soundness
and
completeness
of our SMT encoding are mechanized in the Coq proof assistant.
We conducted an evaluation on both grammar fragments and
full
grammars extracted from the language manuals of domain-specific languages like YAML as well as general-purpose languages like Python, which reveals the effectiveness of our approach.
Building Dynamic System Call Sandbox with Partial Order Analysis
Authors: Zhang Quan , Zhou Chijin , Xu Yiwen , Yin Zijing , Wang Mingzhe , Su Zhuo , Sun Chengnian , Jiang Yu , Sun Jiaguang
Published: October 2023

Attack surface reduction is a security technique that secures the operating system by removing the unnecessary code or features of a program. By restricting the system calls that programs can use, the system call sandbox is able to reduce the exposed attack surface of the operating system and prevent attackers from damaging it through vulnerable programs. Ideally, programs should only retain access to system calls they require for normal execution. Many researchers focus on adopting static analysis to automatically restrict the system calls for each program. However, these methods do not adjust the restriction policy along with program execution. Thus, they need to permit all system calls required for program functionalities.

We observe that some system calls, especially security-sensitive ones, are used a few times in certain stages of a program’s execution and then never used again. This motivates us to minimize the set of required system calls dynamically. In this paper, we propose , which gradually disables access to unnecessary system calls throughout the program’s execution. To accomplish this, we utilize partial order analysis to transform the program into a partially ordered graph, which enables efficient identification of the necessary system calls at any given point during program execution. Once a system call is no longer required by the program, can restrict it immediately. To evaluate , we applied it to seven widely-used programs with an average of 615 KLOC, including web servers and databases. With partial order analysis, restricts an average of 23.50, 16.86, and 15.89 more system calls than the state-of-the-art Chestnut, Temporal Specialization, and the configuration-aware sandbox, C2C, respectively. For mitigating malicious exploitations, on average, defeats 83.42% of 1726 exploitation payloads with only a 5.07% overhead.
Resource-Aware Soundness for Big-Step Semantics
Authors: Bianchini Riccardo , Dagnino Francesco , Giannini Paola , Zucca Elena
Published: October 2023

We extend the semantics and type system of a lambda calculus equipped with common constructs to be
resource-aware
. That is, reduction is instrumented to keep track of the usage of resources, and the type system guarantees, besides standard soundness, that for well-typed programs there is a computation where no needed resource gets exhausted. The resource-aware extension is parametric on an arbitrary
grade algebra
, and does not require ad-hoc changes to the underlying language. To this end, the semantics needs to be formalized in big-step style; as a consequence, expressing and proving (resource-aware) soundness is challenging, and is achieved by applying recent techniques based on coinductive reasoning.
MemPerf: Profiling Allocator-Induced Performance Slowdowns
Authors: Zhou Jin , Silvestro Sam , Tang Steven (Jiaxun) , Yang Hanmei , Liu Hongyu , Zeng Guangming , Wu Bo , Liu Cong , Liu Tongping
Published: October 2023

The memory allocator plays a key role in the performance of applications, but none of the existing profilers can pinpoint performance slowdowns caused by a memory allocator. Consequently, programmers may spend time improving application code incorrectly or unnecessarily, achieving low or no performance improvement. This paper designs the first profiler—MemPerf—to identify allocator-induced performance slowdowns without comparing against another allocator. Based on the key observation that an allocator may impact the whole life-cycle of heap objects, including the accesses (or uses) of these objects, MemPerf proposes a life-cycle based detection to identify slowdowns caused by slow memory management operations and slow accesses separately. For the prior one, MemPerf proposes a thread-aware and type-aware performance modeling to identify slow management operations. For slow memory accesses, MemPerf utilizes a top-down approach to identify all possible reasons for slow memory accesses introduced by the allocator, mainly due to cache and TLB misses, and further proposes a unified method to identify them correctly and efficiently. Based on our extensive evaluation, MemPerf reports 98% medium and large allocator-reduced slowdowns (larger than 5%) correctly without reporting any false positives. MemPerf also pinpoints multiple known and unknown design issues in widely-used allocators.
Verifying Indistinguishability of Privacy-Preserving Protocols
Authors: Linvill Kirby , Kaki Gowtham , Wustrow Eric
Published: October 2023

Internet users rely on the protocols they use to protect their private
information including their identity and the websites they visit. Formal
verification of these protocols can detect subtle bugs that compromise these
protections at design time, but is a challenging task as it involves
probabilistic reasoning about random sampling, cryptographic primitives, and
concurrent execution. Existing approaches either reason about symbolic
models of the protocols that sacrifice precision for automation, or reason
about more precise computational models that are harder to automate and
require cryptographic expertise. In this paper we propose a novel approach
to verifying privacy-preserving protocols that is more precise than symbolic
models yet more accessible than computational models. Our approach permits
direct-style
proofs of privacy, as opposed to indirect game-based
proofs in computational models, by formalizing privacy as
indistinguishability
of possible network traces induced by a
protocol. We ease automation by leveraging insights from the distributed
systems verification community to create sound synchronous models of
concurrent protocols. Our verification framework is implemented in F* as a
library we call Waldo. We describe two large case studies of using Waldo
to verify indistinguishability; one on the
Encrypted Client Hello
(ECH) extension of the TLS protocol and another on a
Private
Information Retrieval
(PIR) protocol. We uncover subtle flaws in the TLS
ECH specification that were missed by other models.
How Domain Experts Use an Embedded DSL
Authors: Rennels Lisa , Chasins Sarah E.
Published: October 2023

Programming tools are increasingly integral to research and analysis in myriad domains, including specialized areas with no formal relation to computer science. Embedded domain-specific languages (eDSLs) have the potential to serve these programmers while placing relatively light implementation burdens on language designers. However, barriers to eDSL use reduce their practical value and adoption. In this paper, we aim to deepen our understanding of how programmers use eDSLs and identify user needs to inform future eDSL designs. We performed a contextual inquiry (9 participants) with domain experts using Mimi, an eDSL for climate change economics modeling. A thematic analysis identified five key themes, including: the interaction between the eDSL and the host language has significant and sometimes unexpected impacts on eDSL user experience, and users preferentially engage with domain-specific communities and code templates rather than host language resources. The needs uncovered in our study offer design considerations for future eDSLs and suggest directions for future DSL usability research.
When Concurrency Matters: Behaviour-Oriented Concurrency
Authors: Cheeseman Luke , Parkinson Matthew J. , Clebsch Sylvan , Kogias Marios , Drossopoulou Sophia , Chisnall David , Wrigstad Tobias , Liétar Paul
Published: October 2023

Expressing parallelism and coordination is central for modern concurrent programming. Many mechanisms
exist for expressing both parallelism and coordination. However, the design decisions for these two mechanisms
are tightly intertwined. We believe that the interdependence of these two mechanisms should be recognised
and achieved through a single, powerful primitive. We are not the first to realise this: the prime example
is actor model programming, where parallelism arises through fine-grained decomposition of a program’s
state into actors that are able to execute independently in parallel. However, actor model programming has a
serious pain point: updating multiple actors as a single atomic operation is a challenging task.
We address this pain point by introducing a new concurrency paradigm: Behaviour-Oriented Concurrency
(BoC). In BoC, we are revisiting the fundamental concept of a behaviour to provide a more transactional
concurrency model. BoC enables asynchronously creating atomic and ordered units of work with exclusive
access to a collection of independent resources.
In this paper, we describe BoC informally in terms of examples, which demonstrate the advantages of
exclusive access to several independent resources, as well as the need for ordering. We define it through a
formal model. We demonstrate its practicality by implementing a C++ runtime. We argue its applicability
through the Savina benchmark suite: benchmarks in this suite can be more compactly represented using BoC
in place of Actors, and we observe comparable, if not better, performance.
TASTyTruffle: Just-in-Time Specialization of Parametric Polymorphism
Authors: D'Souza Matt , You James , Lhoták Ondřej , Prokopec Aleksandar
Published: October 2023

Parametric polymorphism enables programmers to express algorithms independently of the types of values that they operate on. The approach used to implement parametric polymorphism can have important performance implications. One popular approach, erasure, uses a uniform representation for generic data, which entails primitive boxing and other indirections that harm performance. Erasure destroys type information that could be used by language implementations to optimize generic code.

We present TASTyTruffle, an implementation for a subset of the Scala programming language. Instead of JVM bytecode, TASTyTruffle interprets Scala's TASTy intermediate representation, a typed representation wherein generic types are not erased. TASTy's precise type information empowers TASTyTruffle to implement generic code more effectively. In particular, it allows TASTyTruffle to reify types as run-time objects that can be passed around. Using reified types, TASTyTruffle supports heterogeneous box-free representations for generic values. TASTyTruffle also uses reified types to specialize generic code, producing monomorphic copies of generic code that can be easily and reliably optimized by its just-in-time (JIT) compiler.

Empirically, TASTyTruffle is competitive with standard JVM implementations on a small set of benchmark programs; when generic code is used with multiple types, TASTyTruffle consistently outperforms the JVM. The precise type information in TASTy enables TASTyTruffle to find additional optimization opportunities that could not be uncovered with erased JVM bytecode.
Turaco: Complexity-Guided Data Sampling for Training Neural Surrogates of Programs
Authors: Renda Alex , Ding Yi , Carbin Michael
Published: October 2023

Programmers and researchers are increasingly developing surrogates of programs, models of a subset of the observable behavior of a given program, to solve a variety of software development challenges. Programmers train surrogates from measurements of the behavior of a program on a dataset of input examples. A key challenge of surrogate construction is determining what training data to use to train a surrogate of a given program.

We present a methodology for sampling datasets to train neural-network-based surrogates of programs. We first characterize the proportion of data to sample from each region of a program's input space (corresponding to different execution paths of the program) based on the complexity of learning a surrogate of the corresponding execution path. We next provide a program analysis to determine the complexity of different paths in a program. We evaluate these results on a range of real-world programs, demonstrating that complexity-guided sampling results in empirical improvements in accuracy.
Inference of Resource Management Specifications
Authors: Shadab Narges , Gharat Pritam , Tiwari Shrey , Ernst Michael D. , Kellogg Martin , Lahiri Shuvendu K. , Lal Akash , Sridharan Manu
Published: October 2023

A resource leak occurs when a program fails to free some finite resource after it is no longer needed. Such leaks are a significant cause of real-world crashes and performance problems. Recent work proposed an approach to prevent resource leaks based on checking resource management specifications. A resource management specification expresses how the program allocates resources, passes them around, and releases them; it also tracks the ownership relationship between objects and resources, and aliasing relationships between objects. While this specify-and-verify approach has several advantages compared to prior techniques, the need to manually write annotations presents a significant barrier to its practical adoption.

This paper presents a novel technique to automatically infer a resource management specification for a program, broadening the applicability of specify-and-check verification for resource leaks. Inference in this domain is challenging because resource management specifications differ significantly in nature from the types that most inference techniques target. Further, for practical effectiveness, we desire a technique that can infer the resource management specification intended by the developer, even in cases when the code does not fully adhere to that specification. We address these challenges through a set of inference rules carefully designed to capture real-world coding patterns, yielding an effective fixed-point-based inference algorithm.

We have implemented our inference algorithm in two different systems, targeting programs written in Java and C#. In an experimental evaluation, our technique inferred 85.5% of the annotations that programmers had written manually for the benchmarks. Further, the verifier issued nearly the same rate of false alarms with the manually-written and automatically-inferred annotations.
Gradual Typing for Effect Handlers
Authors: New Max S. , Giovannini Eric , Licata Daniel R.
Published: October 2023

We present a gradually typed language, GrEff, with effects and handlers that supports migration from unchecked to checked effect typing. This serves as a simple model of the integration of an effect typing discipline with an existing effectful typed language that does not track fine-grained effect information. Our language supports a simple module system to model the programming model of gradual migration from unchecked to checked effect typing in the style of Typed Racket.

The surface language GrEff is given semantics by elaboration to a core language Core GrEff. We equip Core GrEff with an inequational theory for reasoning about the semantic error ordering and desired program equivalences for programming with effects and handlers. We derive an operational semantics for the language from the equations provable in the theory. We then show that the theory is sound by constructing an operational logical relations model to prove the graduality theorem. This extends prior work on embedding-projection pair models of gradual typing to handle effect typing and subtyping.
Synthesizing Specifications
Authors: Park Kanghee , D'Antoni Loris , Reps Thomas
Published: October 2023

Every program should be accompanied by a specification that describes important aspects of the code's behavior, but writing good specifications is often harder than writing the code itself. This paper addresses the problem of synthesizing specifications automatically, guided by user-supplied inputs of two kinds: i) a query posed about a set of function definitions, and ii) a domain-specific language L in which the extracted property is to be expressed (we call properties in the language L-properties). Each of the property is a best L-property for the query: there is no other L-property that is strictly more precise. Furthermore, the set of synthesized L-properties is exhaustive: no more L-properties can be added to it to make the conjunction more precise.
We implemented our method in a tool, Spyro. The ability to modify both the query and L provides a Spyro user with ways to customize the kind of specification to be synthesized. We use this ability to show that Spyro can be used in a variety of applications, such as mining program specifications, performing abstract-domain operations, and synthesizing algebraic properties of program modules.
Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols
Authors: Tamir Orr , Taube Marcelo , McMillan Kenneth L. , Shoham Sharon , Howell Jon , Gueta Guy , Sagiv Mooly
Published: October 2023

Formally verifying infinite-state systems can be a daunting task, especially when it comes to reasoning about quantifiers. In particular, quantifier alternations in conjunction with function symbols can create function cycles that result in infinitely many ground terms, making it difficult for solvers to instantiate quantifiers and causing them to diverge. This can
leave users with no useful information on how to proceed.

To address this issue, we propose an interactive verification methodology that uses a relational abstraction technique to mitigate solver divergence in the presence of quantifiers. This technique abstracts functions in the verification conditions (VCs) as one-to-one relations, which avoids the creation of function cycles and the resulting proliferation of ground terms.

Relational abstraction is sound and guarantees correctness if the solver cannot find counter-models. However, it may also lead to false counterexamples, which can be addressed by refining the abstraction and requiring the existence of corresponding elements.
In the domain of distributed protocols, we can refine the abstraction by diagnosing counterexamples and manually instantiating elements in the range of the original function. If the verification conditions are correct, there always exist finitely many refinement steps that eliminate all spurious counter-models, making the approach complete.

We applied this approach in Ivy to verify the safety properties of consensus protocols and found that: (1) most verification goals can be automatically verified using relational abstraction, while SMT solvers often diverge when given the original VC, (2) only a few manual instantiations were needed, and the counterexamples provided valuable guidance for the user
compared to timeouts produced by the traditional approach, and (3) the technique can be used to derive efficient low-level implementations of tricky algorithms.