arXiv subjects

Ivan Beschastnikh

Publications and source records attributed to Ivan Beschastnikh.

At least 19 recordsLinked to original sources

arXiv2026

Specula: Scaling formal specifications for autonomous model checking of system code

Specula is a push-button agentic system that generates high-quality formal specifications for large, complex system code and uses the specifications for highly effective model checking and bug finding. Specula employs large language model (LLM) based coding agents to autonomously develop TLA+ specifications, including invariants that describe correctness properties of the target system and formal models that describe the system implementation with the right level of abstractions. Specula is fully autonomous and thus eliminates the barrier of applying formal methods to real-world system code (as in traditional human-centric approaches). Meanwhile, Specula addresses limitations of LLM-driven techniques like reward hacking and hallucinations through self-evolving loops that iteratively improve specification quality by enabling the agents to deepen their understanding of system code and its behaviors. We have used Specula to check 48 open-source system projects; Specula found 249 bugs including many deep bugs that are hard to find by existing approaches. Specula has been used by several companies and is maintained at https://github.com/specula-org/Specula.

cs.SE↗

arXiv2026

Uber's Failover Architecture: Reconciling Reliability and Efficiency in Hyperscale Microservice Infrastructure

Operating a global, real-time platform at Uber's scale requires infrastructure that is both resilient and cost-efficient. Historically, reliability was ensured through a costly 2x capacity model--each service provisioned to handle global traffic independently across two regions--leaving half the fleet idle. We present Uber's Failover Architecture (UFA), which replaces the uniform 2x model with a differentiated architecture aligned to business criticality. Critical services retain failover guarantees, while non-critical services opportunistically use failover buffer capacity reserved for critical services during steady state. During rare "full-peak" failovers, non-critical services are selectively preempted and rapidly restored, with differentiated Service-Level Agreements (SLAs) using on-demand capacity. Automated safeguards, including dependency analysis and regression gates, ensure critical services continue to function even while non-critical services are unavailable. The quantitative impact is significant: UFA reduces steady-state provisioning from 2x to 1.3x, raising utilization from ~20% to ~30% while sustaining 99.97% availability. To date, UFA has hardened over 4,000 unsafe dependencies, eliminated over one million CPU cores from a baseline of about four million cores.

cs.DC↗

arXiv2026

Trace Validation of Unmodified Concurrent Systems with OmniLink

Concurrent systems are notoriously difficult to validate: subtle bugs may only manifest under rare thread interleavings, and existing tools often require intrusive instrumentation or unrealistic execution models. We present OmniLink, a new methodology for validating concurrent implementations against high-level specifications in TLA+. Unlike prior TLA+ based approaches which use a technique called trace validation, OmniLink treats system events as black boxes with a timebox in which they occurred and a meaning in TLA+, solving for a logical total order of actions. Unlike prior approaches based on linearizability checking, which already solves for total orders of actions with timeboxes, OmniLink uses a flexible specification language, and offers a different linearizability checking method based on off-the-shelf model checking. OmniLink offers different features compared existing linearizability checking tools, and we show that it outperforms the state of the art on large scale validation tasks. Our evaluation validates WiredTiger, a state-of-the-art industrial database storage layer, as well as Balanced Augmented Tree (BAT), a state-of-the art lock-free data structure from the research community, and ConcurrentQueue, a popular lock-free queue featuring aggressive performance optimizations. We use OmniLink to improve WiredTiger's existing TLA+ model, as well as develop new TLA+ models that closely match the behavior of the modeled systems, including non-linearizable behaviors. OmniLink is able to find known bugs injected into the systems under test, as well as help discover two previously unknown bugs (1 in BAT, 1 in ConcurrentQueue), which we have confirmed with the authors of those systems.

cs.SE↗

arXiv2025

HYDRA: Breaking the Global Ordering Barrier in Multi-BFT Consensus

Multi-Byzantine Fault Tolerant (Multi-BFT) consensus, which runs multiple BFT instances in parallel, has recently emerged as a promising approach to overcome the leader bottleneck in classical BFT protocols. However, existing designs rely on a global ordering layer to serialize blocks across instances, an intuitive yet costly mechanism that constrains scalability, amplifies failure propagation, and complicates deployment. In this paper, we challenge this conventional wisdom. We present HYDRA, the first Multi-BFT consensus framework that eliminates global ordering altogether. HYDRA introduces an object-centric execution model that partitions transactions by their accessed objects, enabling concurrent yet deterministic execution across instances. To ensure consistency, HYDRA combines lightweight lock-based coordination with a deadlock resolution mechanism, achieving both scalability and correctness. We implement HYDRA and evaluate it on up to 128 replicas in both LAN and WAN environments. Experimental results show HYDRA outperforms several state-of-the-art Multi-BFT protocols in the presence of a straggler. These results demonstrate strong consistency and high performance by removing global ordering, opening a new direction toward scalable Multi-BFT consensus design.

cs.DC↗

arXiv2025

Cracking CodeWhisperer: Analyzing Developers' Interactions and Patterns During Programming Tasks

The use of AI code-generation tools is becoming increasingly common, making it important to understand how software developers are adopting these tools. In this study, we investigate how developers engage with Amazon's CodeWhisperer, an LLM-based code-generation tool. We conducted two user studies with two groups of 10 participants each, interacting with CodeWhisperer - the first to understand which interactions were critical to capture and the second to collect low-level interaction data using a custom telemetry plugin. Our mixed-methods analysis identified four behavioral patterns: 1) incremental code refinement, 2) explicit instruction using natural language comments, 3) baseline structuring with model suggestions, and 4) integrative use with external sources. We provide a comprehensive analysis of these patterns .

cs.SE↗

arXiv2025

SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems

Formal models are essential to specifying large, complex computer systems and verifying their correctness, but are notoriously expensive to write and maintain. Recent advances in generative AI show promise in generating certain forms of specifications. However, existing work mostly targets small code, not complete systems. It is unclear whether AI can deal with realistic system artifacts, as this requires abstracting their complex behavioral properties into formal models. We present SysMoBench, a benchmark that evaluates AI's ability to formally model large, complex systems. We focus on concurrent and distributed systems, which are keystones of today's critical computing infrastructures, encompassing operating systems and cloud infrastructure. We use TLA+, the de facto specification language for concurrent and distributed systems, though the benchmark can be extended to other specification languages. We address the primary challenge of evaluating AI-generated models by automating metrics like syntactic and runtime correctness, conformance to system code, and invariant correctness. SysMoBench currently includes eleven diverse system artifacts: the Raft implementation of Etcd and Redis, the leader election of ZooKeeper, the Spinlock, Mutex, and Ringbuffer in Asterinas OS, etc., with more being added. SysMoBench enables us to understand the capabilities and limitations of today's LLMs and agents, putting tools in this area on a firm footing and opening up promising new research directions.

cs.AI↗

arXiv2025

Toward Inclusive AI-Driven Development: Exploring Gender Differences in Code Generation Tool Interactions

The increasing reliance on Code Generation Tools (CGTs), such as Claude Code and GitHub Copilot, is revamping programming workflows and raising critical questions about fairness and inclusivity in human-AI collaboration. While CGTs offer potential productivity enhancements, their effectiveness across diverse user groups have not been sufficiently investigated. We hypothesized that developers' interactions with CGTs vary based on gender, influencing task outcomes and cognitive load, as prior research suggests that gender differences can affect technology use and cognitive processing. This study employed a mixed-subjects design with 39 participants, evenly divided by gender for a counterbalanced design. Participants completed two programming tasks of medium to high difficulty using two distinct treatments: only CGT assistance and only internet access. Task orders and conditions were counterbalanced to mitigate order effects. We collected cognitive load surveys, screen recordings, and task performance metrics such as completion time, code correctness, and CGT interaction behaviors. Our results indicate no statistically significant gender differences in cognitive load or performance outcomes when using CGTs compared to Internet-based workflows. CGTs reduce intrinsic and extraneous cognitive load compared to Internet based workflows, but the reduction was not statistically significantly. However, CGTs improved advanced code correctness. Our results suggest that CGTs can lower cognitive load and enhance performance on complex coding tasks without significantly affecting core correctness or completion time. These findings highlight how CGT usage can reduce cognitive burden and support more equitable programming experiences across users.

cs.SE↗

arXiv2025

FedFetch: Faster Federated Learning with Adaptive Downstream Prefetching

Federated learning (FL) is a machine learning paradigm that facilitates massively distributed model training with end-user data on edge devices directed by a central server. However, the large number of heterogeneous clients in FL deployments leads to a communication bottleneck between the server and the clients. This bottleneck is made worse by straggling clients, any one of which will further slow down training. To tackle these challenges, researchers have proposed techniques like client sampling and update compression. These techniques work well in isolation but combine poorly in the downstream, server-to-client direction. This is because unselected clients have outdated local model states and need to synchronize these states with the server first. We introduce FedFetch, a strategy to mitigate the download time overhead caused by combining client sampling and compression techniques. FedFetch achieves this with an efficient prefetch schedule for clients to prefetch model states multiple rounds before a stated training round. We empirically show that adding FedFetch to communication efficient FL techniques reduces end-to-end training time by 1.26$\times$ and download time by 4.49$\times$ across compression techniques with heterogeneous client settings. Our implementation is available at https://github.com/DistributedML/FedFetch

cs.LG↗

arXiv2024

Orthrus: Accelerating Multi-BFT Consensus through Concurrent Partial Ordering of Transactions (Extended Version)

Multi-Byzantine Fault Tolerant (Multi-BFT) consensus allows multiple consensus instances to run in parallel, resolving the leader bottleneck problem inherent in classic BFT consensus. However, the global ordering of Multi-BFT consensus enforces a strict serialized sequence of transactions, imposing additional confirmation latency and also limiting concurrency. In this paper, we introduce Orthrus, a Multi-BFT protocol that accelerates transaction confirmation through partial ordering while reserving global ordering for transactions requiring stricter sequencing. To this end, Orthrus strategically partitions transactions to maximize concurrency and ensure consistency. Additionally, it incorporates an escrow mechanism to manage interactions between partially and globally ordered transactions. We evaluated Orthrus through extensive experiments in realistic settings, deploying 128 replicas in WAN and LAN environments. Our findings demonstrate latency reductions of up to 87% in WAN compared to existing Multi-BFT protocols.

cs.DC↗

arXiv2024

Ladon: High-Performance Multi-BFT Consensus via Dynamic Global Ordering (Extended Version)

Multi-BFT consensus runs multiple leader-based consensus instances in parallel, circumventing the leader bottleneck of a single instance. However, it contains an Achilles' heel: the need to globally order output blocks across instances. Deriving this global ordering is challenging because it must cope with different rates at which blocks are produced by instances. Prior Multi-BFT designs assign each block a global index before creation, leading to poor performance. We propose Ladon, a high-performance Multi-BFT protocol that allows varying instance block rates. Our key idea is to order blocks across instances dynamically, which eliminates blocking on slow instances. We achieve dynamic global ordering by assigning monotonic ranks to blocks. We pipeline rank coordination with the consensus process to reduce protocol overhead and combine aggregate signatures with rank information to reduce message complexity. Ladon's dynamic ordering enables blocks to be globally ordered according to their generation, which respects inter-block causality. We implemented and evaluated Ladon by integrating it with both PBFT and HotStuff protocols. Our evaluation shows that Ladon-PBFT (resp., Ladon-HotStuff) improves the peak throughput of the prior art by $\approx$8x (resp., 2x) and reduces latency by $\approx$62% (resp., 23%), when deployed with one straggling replica (out of 128 replicas) in a WAN setting.

cs.DC↗

arXiv2024

Crystallizing Schemas with Teleoscope: Thematic Curation of Large Text Corpora on Reddit

Large text corpora, such as Reddit posts, have become an increasingly prevalent site of qualitative inquiry. However, most large text corpora are intractable for qualitative researchers. Instead, teams rely on statistical subsampling to reduce corpora to a manageable size for qualitative analysis. While previous work for navigating large corpora involves visualizing the dataset at the corpus-level using high-level statistical summaries, few systems offer the ability to curate data using an interpretivist approach. To address this, we developed Teleoscope, a web-based interface designed to scaffold iterative, interactive, and reflexive refinement of a large corpus, in a process we call thematic curation. Across three deployments, we learned that Teleoscope supports serendipitous discovery of new keywords, results in greater feelings of confidence in search saturation, and aids collaborative discussion of alternative curation pathways. Teleoscope empowers researchers to stay "close to the data" in order to make qualitative workflows methodologically coherent with large text corpora.

cs.HC↗

arXiv2023

Empirical Study on Transformer-based Techniques for Software Engineering

Many Transformer-based pre-trained models for code have been developed and applied to code-related tasks. In this paper, we review the existing literature, examine the suitability of model architectures for different tasks, and look at the generalization ability of models on different datasets, and their resource consumption. We examine three very representative pre-trained models for code: CodeBERT, CodeGPT, and CodeT5, and conduct experiments on the top-4 most targeted software engineering tasks that we found in our literature survey: Code Summarization, Bug Fixing, Bug Detection, and Code Search. In our study, we showcase the capability of decoder-only models (CodeGPT) for specific generation tasks under state-of-the-art evaluation metrics and contest the common belief that the encoder-decoder architecture is optimal for general-purpose coding tasks. Additionally, we found that the most frequently used models are not necessarily the most suitable for certain applications and the developers' needs are not adequately addressed by current research. As well, we found that the benchmark and frequent dataset for Bug Fixing and Code Summarization both fail to enable models to generalize onto other datasets for the same task (the frequent dataset refers to the dataset with the highest frequency used in literature other than the benchmark). We use statistical testing to support our conclusions from experiments. Finally, CodeBERT is highly efficient for understanding tasks, whereas CodeT5's efficiency for generation tasks is in doubt, as the highest resource consumption does not guarantee a consistent better performance on different metrics. We also discuss the numerous practical issues in advancing future research on transformer-based models for code-related tasks.

cs.SE↗

arXiv2023

Scalable Data Point Valuation in Decentralized Learning

Existing research on data valuation in federated and swarm learning focuses on valuing client contributions and works best when data across clients is independent and identically distributed (IID). In practice, data is rarely distributed IID. We develop an approach called DDVal for decentralized data valuation, capable of valuing individual data points in federated and swarm learning. DDVal is based on sharing deep features and approximating Shapley values through a k-nearest neighbor approximation method. This allows for novel applications, for example, to simultaneously reward institutions and individuals for providing data to a decentralized machine learning task. The valuation of data points through DDVal allows to also draw hierarchical conclusions on the contribution of institutions, and we empirically show that the accuracy of DDVal in estimating institutional contributions is higher than existing Shapley value approximation methods for federated learning. Specifically, it reaches a cosine similarity in approximating Shapley values of 99.969 % in both, IID and non-IID data distributions across institutions, compared with 99.301 % and 97.250 % for the best state of the art methods. DDVal scales with the number of data points instead of the number of clients, and has a loglinear complexity. This scales more favorably than existing approaches with an exponential complexity. We show that DDVal is especially efficient in data distribution scenarios with many clients that have few data points - for example, more than 16 clients with 8,000 data points each. By integrating DDVal into a decentralized system, we show that it is not only suitable for centralized federated learning, but also decentralized swarm learning, which aligns well with the research on emerging internet technologies such as web3 to reward users for providing data to algorithms.

cs.LG↗

arXiv2022

GlueFL: Reconciling Client Sampling and Model Masking for Bandwidth Efficient Federated Learning

Federated learning (FL) is an effective technique to directly involve edge devices in machine learning training while preserving client privacy. However, the substantial communication overhead of FL makes training challenging when edge devices have limited network bandwidth. Existing work to optimize FL bandwidth overlooks downstream transmission and does not account for FL client sampling. In this paper we propose GlueFL, a framework that incorporates new client sampling and model compression algorithms to mitigate low download bandwidths of FL clients. GlueFL prioritizes recently used clients and bounds the number of changed positions in compression masks in each round. Across three popular FL datasets and three state-of-the-art strategies, GlueFL reduces downstream client bandwidth by 27% on average and reduces training time by 29% on average.

cs.LG↗

arXiv2022

Scaling Blockchain Consensus via a Robust Shared Mempool

There is a resurgence of interest in Byzantine fault-tolerant (BFT) systems due to blockchains. However, leader-based BFT consensus protocols used by permissioned blockchains have limited scalability and robustness. To alleviate the leader bottleneck in BFT consensus, we introduce Stratus, a robust shared mempool protocol that decouples transaction distribution from consensus. Our idea is to have replicas disseminate transactions in a distributed manner and have the leader only propose transaction ids. Stratus uses a provably available broadcast (PAB) protocol to ensure the availability of the referenced transactions. We implemented and evaluated Stratus by integrating it with state-of-the-art BFT-based blockchain protocols and evaluated these protocols in both LAN and WAN settings. Our results show that Stratus-based protocols achieve up to $5\sim20\times$ more throughput than their native counterparts in a network with hundreds of replicas. In addition, the performance of Stratus degrades gracefully in the presence of network asynchrony, Byzantine attackers, and unbalanced workloads. Our design provides easy-to-use APIs so that other BFT systems suffering from leader bottlenecks can use Stratus.

cs.DC↗

arXiv2022

Gridiron: A Technique for Augmenting Cloud Workloads with Network Bandwidth Requirements

Cloud applications use more than just server resources, they also require networking resources. We propose a new technique to model network bandwidth demand of networked cloud applications. Our technique, Gridiron, augments VM workload traces from Azure cloud with network bandwidth requirements. The key to the Gridiron technique is to derive inter-VM network bandwidth requirements using Amdahl's second law. As a case study, we use Gridiron to generate realistic traces with network bandwidth demands for a distributed machine learning training application. Workloads generated with Gridiron allow datacenter operators to estimate the network bandwidth demands of cloud applications and enable more realistic cloud resource scheduler evaluation.

cs.DC↗

arXiv2021

One Bad Apple Spoils the Bunch: Transaction DoS in MimbleWimble Blockchains

As adoption of blockchain-based systems grows, more attention is being given to privacy of these systems. Early systems like BitCoin provided few privacy features. As a result, systems with strong privacy guarantees, including Monero, Zcash, and MimbleWimble have been developed. Compared to BitCoin, these cryptocurrencies are much less understood. In this paper, we focus on MimbleWimble, which uses the Dandelion++ protocol for private transaction relay and transaction aggregation to provide transaction content privacy. We find that in combination these two features make MimbleWimble susceptible to a new type of denial-of-service attacks. We design, prototype, and evaluate this attack on the Beam network using a private test network and a network simulator. We find that by controlling only 10% of the network nodes, the adversary can prevent over 45% of all transactions from ending up in the blockchain. We also discuss several potential approaches for mitigating this attack.

cs.CR↗

arXiv2021

Generalizing Neural Networks by Reflecting Deviating Data in Production

Trained with a sufficiently large training and testing dataset, Deep Neural Networks (DNNs) are expected to generalize. However, inputs may deviate from the training dataset distribution in real deployments. This is a fundamental issue with using a finite dataset. Even worse, real inputs may change over time from the expected distribution. Taken together, these issues may lead deployed DNNs to mis-predict in production. In this work, we present a runtime approach that mitigates DNN mis-predictions caused by the unexpected runtime inputs to the DNN. In contrast to previous work that considers the structure and parameters of the DNN itself, our approach treats the DNN as a blackbox and focuses on the inputs to the DNN. Our approach has two steps. First, it recognizes and distinguishes "unseen" semantically-preserving inputs. For this we use a distribution analyzer based on the distance metric learned by a Siamese network. Second, our approach transforms those unexpected inputs into inputs from the training set that are identified as having similar semantics. We call this process input reflection and formulate it as a search problem over the embedding space on the training set. This embedding space is learned by a Quadruplet network as an auxiliary model for the subject model to improve the generalization. We implemented a tool called InputReflector based on the above two-step approach and evaluated it with experiments on three DNN models trained on CIFAR-10, MNIST, and FMINST image datasets. The results show that InputReflector can effectively distinguish inputs that retain semantics of the distribution (e.g., blurred, brightened, contrasted, and zoomed images) and out-of-distribution inputs from normal inputs.

cs.LG↗