bluuebunny/crossref_metadata_2025 huggingface dataset:
Disentanglement with Futures, State, and Interaction
Authors: Arora Jatin , Muller Stefan K. , Acar Umut A.
Published: January 2024

Recent work has proposed a memory property for parallel programs,
called disentanglement, and showed that it is pervasive in a variety
of programs, written in different languages, ranging from C/C++ to
Parallel ML, and showed that it can be exploited to improve
the performance of parallel functional programs.
All existing work on disentanglement, however, considers the
"fork/join" model for parallelism and does not apply to "futures",
the more powerful approach to parallelism.
This is not surprising:
fork/join parallel programs exhibit a reasonably strict dependency
structure (e.g., series-parallel DAGs), which disentanglement exploits.
In contrast, with futures, parallel computations become first-class
values of the language, and thus can be created, and passed between
functions calls or stored in memory, just like other ordinary values,
resulting in complex dependency structures, especially in the
presence of mutable state.
For example, parallel programs with futures can have deadlocks, which
is impossible with fork-join parallelism.

In this paper, we are interested in the theoretical question of
whether disentanglement may be extended beyond fork/join parallelism,
and specifically to futures.
We consider a functional language with futures, Input/Output (I/O),
and mutable state (references) and show that a broad range of programs
written in this language are disentangled.
We start by formalizing disentanglement for futures and proving that
purely functional programs written in this language are disentangled.
We then generalize this result in three directions.
First, we consider state (effects) and prove that stateful programs
are disentangled if they are race free.
Second, we show that race freedom is sufficient but not a necessary
condition and non-deterministic programs, e.g. those that use atomic
read-modify-operations and some non-deterministic combinators, may
also be disentangled.
Third, we prove that disentangled task-parallel programs written with
futures are free of deadlocks, which arise due to interactions between
state and the rich dependencies that can be expressed with futures.
Taken together, these results show that disentanglement generalizes to
parallel programs with futures and, thus, the benefits of disentanglement
may go well beyond fork-join parallelism.
Solving Infinite-State Games via Acceleration
Authors: Heim Philippe , Dimitrova Rayna
Published: January 2024

Two-player graph games have found numerous applications, most notably in the synthesis of reactive systems from temporal specifications, but also in verification. The relevance of infinite-state systems in these areas has lead to significant attention towards developing techniques for solving infinite-state games.

We propose novel symbolic semi-algorithms for solving infinite-state games with temporal winning conditions. The novelty of our approach lies in the introduction of an acceleration technique that enhances fixpoint-based game-solving methods and helps to avoid divergence. Classical fixpoint-based algorithms, when applied to infinite-state games, are bound to diverge in many cases, since they iteratively compute the set of states from which one player has a winning strategy. Our proposed approach can lead to convergence in cases where existing algorithms require an infinite number of iterations. This is achieved by acceleration: computing an infinite set of states from which a simpler sub-strategy can be iterated an unbounded number of times in order to win the game. Ours is the first method for solving infinite-state games to employ acceleration. Thanks to this, it is able to outperform state-of-the-art techniques on a range of benchmarks, as evidenced by our evaluation of a prototype implementation.
Guided Equality Saturation
Authors: Kœhler Thomas , Goens Andrés , Bhat Siddharth , Grosser Tobias , Trinder Phil , Steuwer Michel
Published: January 2024

Rewriting is a principled term transformation technique with uses across theorem
proving and compilation.
In theorem proving, each rewrite is a proof step; in compilation, rewrites optimize a program term.
While developing rewrite sequences manually is possible, this process does not
scale to larger rewrite sequences. Automated rewriting
techniques, like greedy simplification or equality saturation, work well
without requiring human input.
Yet, they do not scale to large search spaces, limiting the complexity of tasks where automated rewriting is effective,
and meaning that just a small increase in term size or rewrite length may result in failure.

This paper proposes a semi-automatic rewriting technique as a means to scale rewriting by allowing
human insight at key decision points.
Specifically, we propose
guided equality saturation
that embraces human guidance when fully automated equality saturation does not scale.
The rewriting is split into two simpler automatic equality saturation steps: from the original term to a human-provided intermediate
guide
, and from the guide to the target. Complex rewriting tasks may require multiple guides, resulting in a sequence of equality saturation steps.
A guide can be a complete term, or a
sketch
containing undefined elements that are instantiated by the equality saturation search.
Such sketches may be far more concise than complete terms.

We demonstrate the generality and effectiveness of guided equality saturation using two case studies.
First, we integrate guided equality saturation in the Lean 4 proof assistant.
Proofs are written in the style of textbook proof sketches, as a series of calculations omitting details and skipping steps.
These proofs conclude in less than a second instead of minutes when compared to unguided equality saturation, and can
find complex proofs that previously had to be done manually.
Second, in the compiler of the Rise array language, where unguided equality saturation fails to perform optimizations within an hour and using 60 GB of memory, guided equality saturation performs the same optimizations with at most 3 guides, within seconds using less than 1 GB memory.
A Formalization of Core Why3 in Coq
Authors: Cohen Joshua M. , Johnson-Freyd Philip
Published: January 2024

Intermediate verification languages like Why3 and Boogie have made it much easier to build program verifiers, transforming the process into a logic compilation problem rather than a proof automation one.
Why3 in particular implements a rich logic for program specification with polymorphism, algebraic data types, recursive functions and predicates, and inductive predicates; it translates this logic to over a dozen solvers and proof assistants.
Accordingly, it serves as a backend for many tools, including Frama-C, EasyCrypt, and GNATProve for Ada SPARK.
But how can we be sure that these tools are correct?
The alternate foundational approach, taken by tools like VST and CakeML, provides strong guarantees by implementing the entire toolchain in a proof assistant, but these tools are harder to build and cannot directly take advantage of SMT solver automation.
As a first step toward enabling automated tools with similar foundational guarantees, we give a formal semantics in Coq for the logic fragment of Why3.
We show that our semantics are useful by giving a correct-by-construction natural deduction proof system for this logic, using this proof system to verify parts of Why3's standard library, and proving sound two of Why3's transformations used to convert terms and formulas into the simpler logics supported by the backend solvers.
Probabilistic Programming Interfaces for Random Graphs: Markov Categories, Graphons, and Nominal Sets
Authors: Ackerman Nate , Freer Cameron E. , Kaddar Younesse , Karwowski Jacek , Moss Sean , Roy Daniel , Staton Sam , Yang Hongseok
Published: January 2024

We study semantic models of probabilistic programming languages over graphs, and establish a connection to graphons from graph theory and combinatorics. We show that every well-behaved equational theory for our graph probabilistic programming language corresponds to a graphon, and conversely, every graphon arises in this way.

We provide three constructions for showing that every graphon arises from an equational theory. The first is an abstract construction, using Markov categories and monoidal indeterminates. The second and third are more concrete. The second is in terms of traditional measure theoretic probability, which covers 'black-and-white' graphons. The third is in terms of probability monads on the nominal sets of Gabbay and Pitts. Specifically, we use a variation of nominal sets induced by the theory of graphs, which covers Erdős-Rényi graphons. In this way, we build new models of graph probabilistic programming from graphons.
Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures
Authors: Randone Francesca , Bortolussi Luca , Incerto Emilio , Tribastone Mirco
Published: January 2024

Computing the posterior distribution of a probabilistic program is a hard task for which no one-fit-for-all solution exists. We propose Gaussian Semantics, which approximates the exact probabilistic semantics of a bounded program by means of Gaussian mixtures. It is parametrized by a map that associates each program location with the moment order to be matched in the approximation. We provide two main contributions. The first is a universal approximation theorem stating that, under mild conditions, Gaussian Semantics can approximate the exact semantics arbitrarily closely. The second is an approximation that matches up to second-order moments analytically in face of the generally difficult problem of matching moments of Gaussian mixtures with arbitrary moment order. We test our second-order Gaussian approximation (SOGA) on a number of case studies from the literature. We show that it can provide accurate estimates in models not supported by other approximation methods or when exact symbolic techniques fail because of complex expressions or non-simplified integrals. On two notable classes of problems, namely collaborative filtering and programs involving mixtures of continuous and discrete distributions, we show that SOGA significantly outperforms alternative techniques in terms of accuracy and computational time.
How Hard Is Weak-Memory Testing?
Authors: Chakraborty Soham , Krishna Shankara Narayanan , Mathur Umang , Pavlogiannis Andreas
Published: January 2024

Weak-memory models are standard formal specifications of concurrency across hardware, programming languages, and distributed systems. A fundamental computational problem is
consistency testing
: is the observed execution of a concurrent program in alignment with the specification of the underlying system? The problem has been studied extensively across Sequential Consistency (SC) and weak memory, and proven to be NP-complete when some aspect of the input (e.g., number of threads/memory locations) is unbounded. This unboundedness has left a natural question open: are there efficient
parameterized
algorithms for testing?

The main contribution of this paper is a deep hardness result for consistency testing under many popular weak-memory models: the problem remains NP-complete even in its
bounded
setting, where candidate executions contain a bounded number of threads, memory locations, and values. This hardness spreads across several Release-Acquire variants of C11, a popular variant of its Relaxed fragment, popular Causal Consistency models, and the POWER architecture. To our knowledge, this is the first result that fully exposes the hardness of weak-memory testing and proves that the problem
admits no parameterization
under standard input parameters. It also yields a computational separation of these models from SC, x86-TSO, PSO, and Relaxed, for which bounded consistency testing is either known (for SC), or shown here (for the rest), to be in polynomial time.
Ill-Typed Programs Don’t Evaluate
Authors: Ramsay Steven , Walpole Charlie
Published: January 2024

We introduce two-sided type systems, which are sequent calculi for typing formulas. Two-sided type systems allow for hypothetical reasoning over the typing of compound program expressions, and the refutation of typing formulas. By incorporating a type of all values, these type systems support more refined notions of well-typing and ill-typing, guaranteeing both that well-typed programs don't go wrong and that ill-typed programs don't evaluate - that is, reach a value. This makes two-sided type systems suitable for incorrectness reasoning in higher-order program verification, which we illustrate through an application to precise data-flow typing in a language with constructors and pattern matching. Finally, we investigate the internalisation of the meta-level negation in the system as a complement operator on types. This motivates an alternative semantics for the typing judgement, which guarantees that ill-typed programs don't evaluate, but in which well-typed programs may yet go wrong.
Total Type Error Localization and Recovery with Holes
Authors: Zhao Eric , Maroof Raef , Dukkipati Anand , Blinn Andrew , Pan Zhiyi , Omar Cyrus
Published: January 2024

Type systems typically only define the conditions under which an expression is well-typed, leaving ill-typed expressions formally meaningless. This approach is insufficient as the basis for language servers driving modern programming environments, which are expected to recover from simultaneously localized errors and continue to provide a variety of downstream semantic services. This paper addresses this problem, contributing the first comprehensive formal account of total type error localization and recovery: the marked lambda calculus. In particular, we define a gradual type system for expressions with marked errors, which operate as non-empty holes, together with a total procedure for marking arbitrary unmarked expressions. We mechanize the metatheory of the marked lambda calculus in Agda and implement it, scaled up, as the new basis for Hazel, a full-scale live functional programming environment with, uniquely, no meaningless editor states.

The marked lambda calculus is bidirectionally typed, so localization decisions are systematically predictable based on a local flow of typing information. Constraint-based type inference can bring more distant information to bear in discovering inconsistencies but this notoriously complicates error localization. We approach this problem by deploying constraint solving as a type-hole-filling layer atop this gradual bidirectionally typed core. Errors arising from inconsistent unification constraints are localized exclusively to type and expression holes, i.e. the system identifies unfillable holes using a system of traced provenances, rather than localized in an ad hoc manner to particular expressions. The user can then interactively shift these errors to particular downstream expressions by selecting from suggested partially consistent type hole fillings, which returns control back to the bidirectional system. We implement this type hole inference system in Hazel.
Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations
Authors: Ding Yuantian , Qiu Xiaokang
Published: January 2024

Syntax-guided synthesis has been a prevalent theme in various computer-aided programming systems. However, the domain of bit-vector synthesis poses several unique challenges that have not yet been sufficiently addressed and resolved. In this paper, we propose a novel synthesis approach that incorporates a distinct enumeration strategy based on various factors. Technically, this approach weighs in subexpression recurrence by term-graph-based enumeration, avoids useless candidates by example-guided filtration, prioritizes valuable components identified by large language models. This approach also incorporates a bottom-up deduction step to enhance the enumeration algorithm by considering subproblems that contribute to the deductive resolution. We implement all the enhanced enumeration techniques in our SyGuS solver DryadSynth, which outperforms state-of-the-art solvers in terms of the number of solved problems, execution time, and solution size. Notably, DryadSynth successfully solved 31 synthesis problems for the first time, including 5 renowned Hacker's Delight problems.
Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules
Authors: Zhang Ling , Wang Yuting , Wu Jinhua , Koenig Jérémie , Shao Zhong
Published: January 2024

Verified compilation of open modules (i.e., modules whose functionality depends on other modules) provides a foundation for end-to-end verification of modular programs ubiquitous in contemporary software. However, despite intensive investigation in this topic for decades,the proposed approaches are still difficult to use in practice as they rely on assumptions about the internal working of compilers which make it difficult for external users to apply the verification results. We propose an approach to verified compositional compilation without such assumptions in the setting of verifying compilation of heterogeneous modules written in first-order languages supporting global memory and pointers. Our approach is based on the memory model of CompCert and a new discovery that a Kripke relation with a notion of memory protection can serve as a uniform and composable semantic interface for the compiler passes. By absorbing the rely-guarantee conditions on memory evolution for all compiler passes into this Kripke Memory Relation and by piggybacking requirements on compiler optimizations onto it, we get compositional correctness theorems for realistic optimizing compilers as refinements that directly relate native semantics of open modules and that are ignorant of intermediate compilation processes. Such direct refinements support all the compositionality and adequacy properties essential for verified compilation of open modules. We have applied this approach to the full compilation chain of CompCert with its Clight source language and demonstrated that our compiler correctness theorem is open to composition and intuitive to use with reduced verification complexity through end-to-end verification of non-trivial heterogeneous modules that may freely invoke each other (e.g.,mutually recursively).
Polynomial Time and Dependent Types
Authors: Atkey Robert
Published: January 2024

We combine dependent types with linear type systems that soundly and completely capture polynomial time computation. We explore two systems for capturing polynomial time: one system that disallows construction of iterable data, and one, based on the LFPL system of Martin Hofmann, that controls construction via a payment method. Both of these are extended to full dependent types via Quantitative Type Theory, allowing for arbitrary computation in types alongside guaranteed polynomial time computation in terms. We prove the soundness of the systems using a realisability technique due to Dal Lago and Hofmann.

Our long-term goal is to combine the extensional reasoning of type theory with intensional reasoning about the resources intrinsically consumed by programs. This paper is a step along this path, which we hope will lead both to practical systems for reasoning about programs’ resource usage, and to theoretical use as a form of
synthetic computational complexity theory
.
Internal Parametricity, without an Interval
Authors: Altenkirch Thorsten , Chamoun Yorgo , Kaposi Ambrus , Shulman Michael
Published: January 2024

Parametricity is a property of the syntax of type theory implying,
e.g., that there is only one function having the type of the
polymorphic identity function. Parametricity is usually proven
externally, and does not hold internally. Internalising it is
difficult because once there is a term witnessing parametricity, it
also has to be parametric itself and this results in the appearance
of higher dimensional cubes. In previous theories with internal
parametricity, either an explicit syntax for higher cubes is present
or the theory is extended with a new sort for the interval. In this
paper we present a type theory with internal parametricity which is
a simple extension of Martin-Löf type theory: there are a few new
type formers, term formers and equations. Geometry is not explicit
in this syntax, but emergent: the new operations and equations only
refer to objects up to dimension 3. We show that this theory is
modelled by presheaves over the BCH cube category. Fibrancy
conditions are not needed because we use span-based rather than
relational parametricity. We define a gluing model for this theory
implying that external parametricity and canonicity hold. The theory
can be seen as a special case of a new kind of modal type theory,
and it is the simplest setting in which the computational properties
of higher observational type theory can be demonstrated.
Explicit Effects and Effect Constraints in ReML
Authors: Elsman Martin
Published: January 2024

An important aspect of building robust systems that execute on dedicated hardware and perhaps in constrained environments is to control and manage the effects performed by program code.

We present ReML, a higher-order statically-typed functional language, which allows programmers to be explicit about the effects performed by program code and in particular effects related to memory management. Allowing programmers to be explicit about effects, the regions in which values reside, and the constraints under which code execute, makes programs robust to changes in the program source code and to compiler updates, including compiler optimisations.

ReML is integrated with a polymorphic inference system that builds on top of region-inference, as it is implemented in the MLKit, a Standard ML compiler that uses region-based memory management as its primary memory management scheme.
Indexed Types for a Statically Safe WebAssembly
Authors: Geller Adam T. , Frank Justin , Bowman William J.
Published: January 2024

We present Wasm-prechk, a superset of WebAssembly (Wasm) that uses indexed types to express and check simple constraints over program values. This additional static reasoning enables safely removing dynamic safety checks from Wasm, such as memory bounds checks. We implement Wasm-prechk as an extension of the Wasmtime compiler and runtime, evaluate the run-time and compile-time performance of Wasm-prechk vs WebAssembly configurations with explicit dynamic checks, and find an average run-time performance gain of 1.71x faster in the widely used PolyBenchC benchmark suite, for a small overhead in binary size (7.18% larger) and type-checking time (1.4% slower). We also prove type and memory safety of Wasm-prechk, prove Wasm safely embeds into Wasm-prechk ensuring backwards compatibility, prove Wasm-prechk type-erases to Wasm, and discuss design and implementation trade-offs.
A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability
Authors: Jayanti Prasad , Jayanti Siddhartha , Yavuz Ugur , Hernandez Lizzie
Published: January 2024

We introduce simple,
universal
,
sound
, and
complete
proof methods for producing machine-verifiable proofs of linearizability and strong linearizability. Universality means that our method works for any object type; soundness means that an algorithm can be proved correct by our method only if it is linearizable (resp. strong linearizable); and completeness means that any linearizable (resp. strong linearizable) implementation can be proved so using our method. We demonstrate the simplicity and power of our method by producing proofs of linearizability for the Herlihy-Wing queue and Jayanti’s single-scanner snapshot, as well as a proof of strong linearizability of the Jayanti-Tarjan union-find object. All three of these proofs are machine-verified by TLAPS (the TLA+ Proof System).
On Model-Checking Higher-Order Effectful Programs
Authors: Dal Lago Ugo , Ghyselen Alexis
Published: January 2024

Model-checking is one of the most powerful techniques for verifying systems and programs, which since the pioneering results by Knapik et al., Ong, and Kobayashi, is known to be applicable to functional programs with higher-order types against properties expressed by formulas of monadic second-order logic. What happens when the program in question, in addition to higher-order functions, also exhibits algebraic effects such as probabilistic choice or global store? The results in the literature range from those, mostly positive, about nondeterministic effects, to those about probabilistic effects, in the presence of which even mere reachability becomes undecidable. This work takes a fresh and general look at the problem, first of all showing that there is an elegant and natural way of viewing higher-order programs producing algebraic effects as ordinary higher-order recursion schemes. We then move on to consider effect handlers, showing that in their presence the model checking problem is bound to be undecidable in the general case, while it stays decidable when handlers have a simple syntactic form, still sufficient to capture so-called generic effects. Along the way, we hint at how a general specification language could look like, this way justifying some of the results in the literature, and deriving new ones.
Efficient Matching of Regular Expressions with Lookaround Assertions
Authors: Mamouras Konstantinos , Chattopadhyay Agnishom
Published: January 2024

Regular expressions have been extended with lookaround assertions, which are subdivided into lookahead and lookbehind assertions. These constructs are used to refine when a match for a pattern occurs in the input text based on the surrounding context. Current implementation techniques for lookaround involve backtracking search, which can give rise to running time that is super-linear in the length of input text. In this paper, we first consider a formal mathematical semantics for lookaround, which complements the commonly used operational understanding of lookaround in terms of a backtracking implementation. Our formal semantics allows us to establish several equational properties for simplifying lookaround assertions. Additionally, we propose a new algorithm for matching regular expressions with lookaround that has time complexity
O
(
m
·
n
), where
m
is the size of the regular expression and
n
is the length of the input text. The algorithm works by evaluating lookaround assertions in a bottom-up manner. Our algorithm makes use of a new notion of nondeterministic finite automata (NFAs), which we call oracle-NFAs. These automata are augmented with epsilon-transitions that are guarded by oracle queries that provide the truth values of lookaround assertions at every position in the text. We provide an implementation of our algorithm that incorporates three performance optimizations for reducing the work performed and memory used. We present an experimental comparison against PCRE and Java’s regex library, which are state-of-the-art regex engines that support lookaround assertions. Our experimental results show that, in contrast to PCRE and Java, our implementation does not suffer from super-linear running time and is several times faster.
Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs
Authors: Batz Kevin , Biskup Tom Jannik , Katoen Joost-Pieter , Winkler Tobias
Published: January 2024

We consider imperative programs that involve both randomization and pure nondeterminism. The central question is how to find a strategy resolving the pure nondeterminism such that the so-obtained determinized program satisfies a given quantitative specification, i.e., bounds on expected outcomes such as the expected final value of a program variable or the probability to terminate in a given set of states. We show how memoryless and deterministic (MD) strategies can be obtained in a semi-automatic fashion using deductive verification techniques. For loop-free programs, the MD strategies resulting from our weakest precondition-style framework are correct by construction. This extends to loopy programs, provided the loops are equipped with suitable loop invariants - just like in program verification. We show how our technique relates to the well-studied problem of obtaining strategies in countably infinite Markov decision processes with reachability-reward objectives. Finally, we apply our technique to several case studies.
A Novel Cross-Domain Recommendation with Evolution Learning
Authors: Chen Yi-Cheng , Lee Wang-Chien
Published: January 2024

In this “info-plosion” era, recommendation systems (or recommenders) play a significant role in finding interesting items in the surge of online digital activities and e-commerce. Several techniques have been widely applied for recommendation systems, but the cold-start and sparsity problems remain a major challenge. The cold-start problem occurs when generating recommendations for new users and items without sufficient information. Sparsity refers to the problem of having a large amount of users and items but with few transactions or interactions. In this article, a novel cross-domain recommendation model, Cross-Domain Evolution Learning Recommendation (abbreviated as CD-ELR), is developed to communicate the information from different domains in order to tackle the cold-start and sparsity issues by integrating matrix factorization and recurrent neural network. We introduce an evolutionary concept to describe the preference variation of users over time. Furthermore, several optimization methods are developed for combining the domain features for precision recommendation. Experimental results show that CD-ELR outperforms existing state-of-the-art recommendation baselines. Finally, we conduct experiments on several real-world datasets to demonstrate the practicability of the proposed CD-ELR.
Distributed Experimental Design Networks
Authors: Li Yuanyuan
Published: January 2024

As edge computing capabilities increase, model learning deployments in a heterogeneous edge environment have emerged. We consider an experimental design network, as introduced by Liu et al., in which network routing and rate allocation is designed to aid the transfer of data from sensors to heterogeneous learners. We generalize this setting by considering heterogeneous noisy Gaussian sources, incorporating multicast, but also-crucially-distributed algorithms in this setting. From a technical standpoint, we show that, assuming Gaussian sensor sources still yields an continuous DR-submodular experimental design objective. We also propose a distributed Frank-Wolfe algorithm yielding allocations within a 1-1/e factor from the optimal. Numerical evaluations show that our proposed algorithm outperforms competitors w.r.t. both objective maximization and model learning quality.
An End-to-End Benchmarking Tool for Analyzing the Hardware-Software Implications of Multi-modal DNNs
Authors: Huang Tianhao , Zhu Xiaozhi , Niu Mo
Published: January 2024

Abstract-Multi-modal deep neural networks (DNNs) have become increasingly pervasive in many machine learning application domains due to their superior accuracy by fusing various modalities together. However, multi-modal DNNs present many unique characteristics such as multi-stage execution, frequent synchronization and high heterogeneity, which are not well understood in the system and architecture community. In this article, we first present and characterize a set of multi-modal DNN workloads of different sizes from five domains and measure metrics like accuracy to ensure the availability of these applications from the algorithm perspective. We then explore their important hardwaresoftware implications from system and architecture aspects by conducting an in-depth analysis on the unique hardware-software characteristics of multimodal DNNs. We hope that our work can help guide future hardware-software design and optimization for efficient inference of multi-modal DNN applications on both cloud and edge computing platforms.
Foreword from Chair of 2023 ACM SIGMETRICS Doctoral Dissertation Award Committee
Authors: Ayesta Urtzi
Published: January 2024

The ACM SIGMETRICS Doctoral Dissertation Award recognizes outstanding thesis research by doctoral candidates in the field of performance evaluation analysis of computer systems. Nominations for the 2023 award were sought from all faculty with graduating Ph.D. students working in performance evaluation, broadly understood. The award winners were determined by a review committee composed by researchers working in different sub-fields of performance evaluation: Urtzi Ayesta (CNRS & Ikerbasque, chair), Giuliano Casale (Imperial College London), Kristy Gardner (Amherst College), Daniel Sadoc Menasche (Federal University of Rio de Janeiro), Neil Walton (Durham University) and Weina Wang (Carnegie Mellon University).
Optimal Scheduling in Multiserver Queues
Authors: Grosof Isaac
Published: January 2024

Scheduling theory is a key tool for reducing latency (i.e. response time) in queueing systems. Scheduling, i.e. choosing the order in which to serve jobs, can reduce response time by an order of magnitude with no additional resources. Scheduling theory is well-developed in single-server systems, where one job is processed at a time. However, little is known about scheduling in multiserver systems, where many jobs are processed at once. Results are especially limited in stochastic multiserver scheduling theory. Today's datacenters have thousands of servers, and scheduling theory is unable to analyze such systems.
Data Freshness in Information-update Systems: Modeling, Scheduling, and Tradeoffs
Authors: Liu Zhongdong
Published: January 2024

Brief Biography: Zhongdong Liu is a final-year Ph.D. student in the Department of Computer Science at Virginia Tech. He received his B.S. degree in Mathematics and Applied Mathematics with honors from Northeast Forestry University in 2016. His research interests are in the modeling, analysis, control, and optimization of complex network systems. His specific area of focus lies in analyzing and improving data freshness within real-time applications and services through the development of efficient scheduling algorithms. Zhongdong's research has been featured in notable publications, including IEEE INFOCOM, Proceedings of ICCCN (as an invited paper), IEEE Internet of Things Journal, and IEEE/ACM Transactions on Networking.
Data-Rich Causal Inference
Authors: Shah Abhin
Published: January 2024

Brief Biography: Abhin Shah is a final-year Ph.D. student in the department of Electrical Engineering and Computer Science atMIT, where he is a recipient ofMIT's Jacobs Presidential Fellowship. He has interned with Google Research (2021) and IBM Research (2020).
Timely Inference over Networks
Authors: Chowdhury Shisher Md Kamran
Published: January 2024

Brief Biography: Md Kamran Chowdhury Shisher is a final-year Ph.D. candidate in the Department of Electrical and Computer Engineering at Auburn University, Auburn, AL, USA. He expects to graduate by May 2024. His Ph.D. works are advised by Yin Sun. Shisher's research interests include Information Freshness, Wireless Networks, Semantic Communications, and Machine Learning. His Ph.D. works focus on designing low-complexity optimal scheduling algorithms for remote inference systems. He also developed an information-theoretic tool to analyze the impact of freshness on the performance of real-time applications. He received his M.Sc. degree in Electrical Engineering at Auburn University in 2022. He completed his B.Sc. in Electrical and Electronic Engineering from the Bangladesh University of Engineering and Technology in 2017.
Synthesize of Ni0.75Zn0.25Fe2O4 Spinel Oxide as a Working Electrode for Formaldehyde Electrochemical Gas Sensors
Authors: Zhu Lecheng , Wei Lei , Cheng Keyu , Li Kun , Rong Qian , Zhang Chuanhui , Yu Yi , Wang Chunchang , Guo Youmin
Published: January 2024

Gas sensor with yttrium stabilized zirconia film in electrochemistry have been rapidly applied in the monitoring of toxic and harmful gases, and nickel spinel ferrite (NFO) is one of the most studied working electrodes. However, the sensing performance to formaldehyde (HCHO) is quiet poor. In this work, the sol-gel method was used to prepare Zn-doped NFO (Ni0.75Zn0.25Fe2O4) oxide, and the Zn-doped NFO was applied as the working electrode of the electrochemical gas sensor of HCHO. The phase structure, micromorphology, and surface area of the prepared Ni0.75Zn0.25Fe2O4 oxide were evaluated for the working electrode. The results showed that when the operating temperature reached 480 °C, the sensor with Ni0.75Zn0.25Fe2O4 as the working electrode achieved high response value of −17 mV to 5 ppm HCHO, and the response/recovery time was 28/20 s. The polarization curve was further performed to validate the mechanism of the observed sensing behavior. Meanwhile, the response signal of the fabricated sensor increased logarithmically with the log (HCHO) in the investigated range of 1–5 ppm, and the corresponding sensitivity reached −29.08 mV/decade.
Modulation of the Cobalt Content in Ti3C2T
x
by Molten Salt Method for Hydrogen Evolution Reaction
Authors: Wang Ya , Gao Zihan , Zhang Xiuqing , Shen Miao
Published: January 2024

Exploring non-noble catalysts with highly efficient activity to replace noble metal is a problem that needs to be solved in electrocatalytic water splitting. Herein, Ti3C2T
x
MXene with different functional groups was prepared. The results showed that the substitution of F by Cl terminal groups can improve the electrocatalytic activity in hydrogen evolution reaction (HER). Further introduction of Co on the surface of Ti3C2T
x
MXene can largely reduced the overpotential from 542 mV to 318 mV at 10 mA cm−2, which can be attributed to the Ti-O-Co bond to accelerate the electron/ion migration. The content of Co in Ti3C2T
x
could be modulated by simply changing the etching time. This work suggests that Co anchored on Ti3C2T
x
helps to promote the hydrogen production process.
Simultaneous Electrochemical Quantification of Favipiravir and Molnupiravir as Antiviral Drugs for the Treatment of COVID-19 by Using a Glassy Carbon Electrode Modified by Pd/Co-Mn-MOF-74
Authors: Mahdavi Nejad Ehsan
Published: January 2024

An electrochemical monitoring of Favipiravir (Favi) and Molnupiravir (Moln) as effective drugs for the treatment of COVID-19 was conducted for the first time in the presented research. A modification of the glassy carbon electrode (GCE) with Metal–organic frameworks (MOFs) was applied for the determination process by using the Square Wave Voltammetry (SWV) technique. Transmission electron microscopy (TEM), Fourier Transform Infrared (FTIR), the Energy Dispersive X-ray (EDX) and, X-ray Diffraction (XRD) techniques applied to check the characterization of synthesized Modified-MOFs. In Britton–Robinson buffer solutions (BR) with pH = 7, two well-defined peaks appeared on the Pd/Co-Mn-MOF-74/GCE for 10 μM Moln and Favi were 423 and 1143 mV while the oxidation currents were 32.6 and 18.4 μA, respectively. The detection limit for Moln and Favi were calculated based on 3 Signal/Noise as 0.002 and 0.003 μM, respectively. The ability of the Pd/Co-Mn-MOF-74/GCE was checked by monitoring the Moln and Favi in urine and blood and comparing the obtained data with HPLC data. The obtained data were in good agreement with each other which demonstrates that the presented method was one of the best analytical methods for the monitoring of Moln and Favi in the laboratory.
Effect of Engineered Cracks in Catalyst Layers on PEMFC Catalyst Layer Durability
Authors: Lee ChungHyuk , Komini Babu Siddharth , Patterson Brian M. , Reeves Kimberly S. , Yu Haoran , Cullen David A. , Mukundan Rangachary , Borup Rod L. , Spendelow Jacob S.
Published: January 2024

Proton exchange membrane fuel cells (PEMFCs) are expected to play a pivotal role in decarbonizing the transportation sector, and particularly heavy-duty vehicles (HDVs). However, improvements in durability are needed for PEMFCs to compete with state-of-the-art power sources for HDVs. Here, we examine how catalyst layer (CL) cracks that are engineered affect the CL durability by using patterned silicon templates to control the CL crack density at the micrometer scale. Electrochemical analyses show that the initial PEMFC performance is relatively unaffected by crack density, but the performance after durability testing was strongly affected. Specifically, CLs with high crack density showed higher performance relative to CLs without cracks after application of a carbon corrosion accelerated stress test. Electrochemical analyses coupled with X-ray computed tomography and scanning transmission electron microscopy with energy dispersive X-ray spectroscopy showed that the cracks provide shorter oxygen diffusion pathways to reaction sites, leading to decreased oxygen transport resistance. Additionally, we observed that the catalyst durability is unaffected by cracks. Our results provide a mechanistic explanation of the role of cracks in CL durability.
The cardiomyocyte origins of diastolic dysfunction: cellular components of myocardial “stiffness”
Authors: Janssens Johannes V. , Raaijmakers Antonia J. A. , Weeks Kate L. , Bell James R. , Mellor Kimberley M. , Curl Claire L. , Delbridge Lea M. D.
Published: January 2024

The impaired ability of the heart to relax and stretch to accommodate venous return is generally understood to represent a state of “diastolic dysfunction” and often described using the all-purpose noun “stiffness.” Despite the now common qualitative usage of this term in fields of cardiac patho/physiology, the specific quantitative concept of stiffness as a molecular and biophysical entity with real practical interpretation in healthy and diseased hearts is sometimes obscure. The focus of this review is to characterize the concept of cardiomyocyte stiffness and to develop interpretation of “stiffness” attributes at the cellular and molecular levels. Here, we consider “stiffness”-related terminology interpretation and make links between cardiomyocyte stiffness and aspects of functional and structural cardiac performance. We discuss cross bridge-derived stiffness sources, considering the contributions of diastolic myofilament activation and impaired relaxation. This includes commentary relating to the role of cardiomyocyte Ca2+ flux and Ca2+ levels in diastole, the troponin-tropomyosin complex role as a Ca2+ effector in diastole, the myosin ADP dissociation rate as a modulator of cross bridge attachment and regulation of cross-bridge attachment by myosin binding protein C. We also discuss non-cross bridge-derived stiffness sources, including the titin sarcomeric spring protein, microtubule and intermediate filaments, and cytoskeletal extracellular matrix interactions. As the prevalence of conditions involving diastolic heart failure has escalated, a more sophisticated understanding of the molecular, cellular, and tissue determinants of cardiomyocyte stiffness offers potential to develop imaging and molecular intervention tools.
Interpretation of field and LEAP potentials recorded from cardiomyocyte monolayers
Authors: Ernault Auriane C. , Al-Shama Rushd F. M. , Li Jiuru , Devalla Harsha D. , de Groot Joris R. , Coronel Ruben , Vigmond Edward , Boukens Bastiaan J.
Published: January 2024

We present a physiological basis for the interpretation of multielectrode array-derived, extracellular, electrical signals.
Noninvasive analysis of contractility during identical maturations revealed two phenotypes in ventricular but not in atrial iPSC-CM
Authors: Rapöhn Marcel , Cyganek Lukas , Voigt Niels , Hasenfuß Gerd , Lehnart Stephan E. , Wegener Jörg W.
Published: January 2024

Differentiation of induced pluripotent stem cells (iPSCs) into iPSC-derived cardiomyocytes (iPSC-CMs) exhibits a high variability in mature parameters. Here, we monitored noninvasively contractile parameters of iPSC-CM during full-time differentiation using a smartphone device. Our results show that parallel maturations of iPSCs into ventricular iPSC-CMs, but not into atrial iPSC-CMs, resulted in two distinct subpopulations of iPSC-CMs. These findings suggest that our cost-effective method may help to compare iPSC-CMs at the same maturation level.
Intraoperative Touch Imprint Cytology of Brain Neoplasms: A Useful High‐Diagnostic Tool in 93 Consecutive Cases; Differential Diagnoses, Pitfalls, and Traps
Authors: Koyuncuer Ali
Published: January 2024

Introduction. Intraoperative cytological examination of central nervous system (CNS) lesions was first introduced in 1920 by Eisenhardt and Cushing for rapid evaluation of neurosurgical specimens and to guide surgical treatment. It is recognized that this method not only confirms the adequacy of biopsy in CNS samples but also indicates the presence and preliminary diagnosis of lesional tissue. Methods. A total of 93 patients who underwent touch imprint cytology (TIC) for CNS tumors or lesions between 2018 and 2023 were included in the study. All cases were correlated with the final histopathological diagnosis, and pitfalls and difficulties encountered with discrepancies were noted. Result. The most common primary CNS tumors were gliomas and meningiomas, while secondary (metastatic) tumors were predominantly lung, breast, and gastrointestinal system carcinomas. Sensitivity, specificity, positive predictive value, and negative predictive value for diagnosis with TIC were 94.1%, 100%, and 61.5%, respectively. Final histopathological diagnosis by TIC was made in 88 cases (94.6%) and the discrepancy was found in 5 cases (5.37%). Three of the five discrepancies (3.2%) were haematolymphoid malignancies (two lymphomas and one plasma cell neoplasia), one glioblastoma, and one hemangioblastoma case. Conclusion. TIC is a fast, safe, and inexpensive diagnostic tool used during intraoperative neuropathology consultation. Awareness of the pitfalls of using this method during intraoperative consultation will enable high‐diagnostic accuracy.
The Digital Self-Efficacy Scale: Adaptation and Validation of Its Spanish Version
Authors: Paredes-Aguirre Milton , Campoverde Aguirre Ronald , Hernandez-Pozas Olivia , Ayala Yarid , Barriga Medina Holger
Published: January 2024

The importance of Digital Self-Efficacy is likely to grow as digital technology becomes increasingly widespread. To succeed in today’s digital world, it is essential for people to have a strong belief in their ability to effectively use digital technologies. Therefore, it is necessary for researchers to have adequate instruments to measure them in different populations. The Digital Self-Efficacy Scale offers an innovative technology-independent approach. It provides a multidimensional assessment grounded in the DigComp framework, allowing adaptability and facilitating comparison across diverse demographics. This study examined the validity and reliability of the Spanish-adapted version of the Digital Self-Efficacy for Equatorian workers. The results from a sample of 471 participants, with a gender-balanced distribution (43.74% female and 55.41% male) and a mean age of 34 years, showed that this translated 19-item scale is a valid and reliable measure of this construct. Nomological network analysis with SEM showed that Digital Self-Efficacy had a positive and significant association with task-technology fit and the use of technology. This suggests that workers with higher levels of Digital Self-Efficacy are more likely to use technology effectively and efficiently and that they are more likely to find technology that is a good fit for their tasks.