Michael D. Bond

dblp:36/2453 · DBLP profile ↗
← Back
46ranked-venue papers
10as first author
10since 2021 · last 2026
0000-0002-8971-4944ORCID · verified

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 39 · 9 first-author · 8 since 2021Systems, architecture and hardware · 13 · 4 first-author · 1 since 2021Databases, data management, data science and information retrieval · 1 · 1 since 2021
YearPublicationVenuePosition
2026 &inator: Correct, Precise C-to-Rust Interface Translation
abstract
Automatically translating system software from C to Rust is an appealing but challenging problem, as it requires whole-program reasoning to satisfy Rust’s ownership and borrowing discipline. A key enabling step in whole-program translation is interface translation , which produces Rust declarations for the C program’s top-level declarations (i.e., structs and function signatures), enabling modular and incremental code translation. This paper introduces correct, precise C-to-Rust interface translation, called &inator . &inator employs a novel constraint-based formulation of semantic equivalence and type correctness including borrow-checking rules to produce a Rust interface that is correct (i.e., the interface admits a semantics-preserving implementation in safe Rust) and precise (i.e., it uses the simplest, least costly types). Our results show &inator produces correct, precise Rust interfaces for real C programs, but support for certain C features and scaling to large programs are challenges left for future work. This work advances the state of the art by being the first correct, precise approach to C-to-Rust interface translation.
Ayden Coughlin, Michael D. Bond
Proc. ACM Program. Lang.3
2025 Carapace: Static-Dynamic Information Flow Control in Rust
abstract
Fine-grained information flow control (IFC) ensures confidentiality and integrity at the programming language level by ensuring that high-secrecy values do not affect low-secrecy values and that low-integrity values do not affect high-integrity values. However, prior support for fine-grained IFC is impractical: It either analyzes programs using whole-program static analysis, detecting false IFC violations; or it extends the language and compiler, thwarting adoption. Recent work called Cocoon demonstrates how to provide fine-grained IFC for Rust programs without modifying the language or compiler, but it is limited to static secrecy labels, and its case studies are limited. This paper introduces an approach called Carapace that employs Cocoon’s core approach and supports both static and dynamic IFC and supports both secrecy and integrity. We demonstrate Carapace using three case studies involving real applications and comprehensive security policies. An evaluation shows that applications can be retrofitted to use Carapace with relatively few changes, while incurring negligible run-time overhead in most cases. Carapace advances the state of the art by being the first hybrid static—dynamic IFC that works with an off-the-shelf language—Rust—and its unmodified compiler.
Vincent Beardsley, Chris Xiong, Ada Lamba, Michael D. Bond
Proc. ACM Program. Lang.4
2024 IsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly Isolated Data Store Applications
abstract
Distributed data stores typically provide weak isolation levels, which are efficient but can lead to unserializable behaviors, which are hard for programmers to understand and often result in errors. This paper presents the first dynamic predictive analysis for data store applications under weak isolation levels, called IsoPredict . Given an observed serializable execution of a data store application, IsoPredict generates and solves SMT constraints to find an unserializable execution that is a feasible execution of the application. IsoPredict introduces novel techniques that handle divergent application behavior; solve mutually recursive sets of constraints; and balance coverage, precision, and performance. An evaluation on four transactional data store benchmarks shows that IsoPredict often predicts unserializable behaviors, 99 % of which are feasible.
Chujun Geng, Spyros Blanas, Michael D. Bond, Yang Wang 0009
Proc. ACM Program. Lang.3
2024 Cocoon: Static Information Flow Control in Rust
abstract
Information flow control (IFC) provides confidentiality by enforcing noninterference, which ensures that high-secrecy values cannot affect low-secrecy values. Prior work introduces fine-grained IFC approaches that modify the programming language and use non-standard compilation tools, impose run-time overhead, or report false secrecy leaks—all of which hinder adoption. This paper presents Cocoon, a Rust library for static type-based IFC that uses the unmodified Rust language and compiler. The key insight of Cocoon lies in leveraging Rust’s type system and procedural macros to establish an effect system that enforces noninterference. A performance evaluation shows that using Cocoon increases compile time but has no impact on application performance. To demonstrate Cocoon’s utility, we retrofitted two popular Rust programs, the Spotify TUI client and Mozilla’s Servo browser engine, to use Cocoon to enforce limited confidentiality policies
Ada Lamba, Max Taylor, Vincent Beardsley, Jacob Bambeck, Michael D. Bond, Zhiqiang Lin 0001
Proc. ACM Program. Lang.5
2023 Developer's Responsibility or Database's Responsibility? Rethinking Concurrency Control in Databases
Chaoyi Cheng, Mingzhe Han, Spyros Blanas, Michael D. Bond, Yang Wang 0009
CIDR5
2022 Cape: compiler-aided program transformation for HTM-based cache side-channel defense
abstract
Cache side-channel attacks pose real threats to computer system security. Prior work called Cloak leverages commodity hardware transactional memory (HTM) to protect sensitive data and code from cache side-channel attacks. However, Cloak requires tedious and error-prone manual modifications to vulnerable software by programmers. This paper presents Cape, a compiler analysis and transformation that soundly and automatically protects programs from cache side-channel attacks using Cloak’s defense. An evaluation shows that Cape provides protection that is as strong as Cloak’s, while performing competitively with Cloak.
Michael D. Bond, Yinqian Zhang
CC2
2022 Distilling the Real Cost of Production Garbage Collectors
abstract
Despite the long history of garbage collection (GC) and its prevalence in modern programming languages, there is surprisingly little clarity about its true cost. Without understanding their cost, crucial tradeoffs made by garbage collectors (GCs) go unnoticed. This can lead to misguided design constraints and evaluation criteria used by GC researchers and users, hindering the development of high-performance, low-cost GCs. In this paper, we develop a methodology that allows us to empirically estimate the cost of GC for any given set of metrics. This fundamental quantification has eluded the research community, even when using modern, well-established methodologies. By distilling out the explicitly identifiable GC cost, we estimate the intrinsic application execution cost using different GCs. The minimum distilled cost forms a baseline. Subtracting this baseline from the total execution costs, we can then place an empirical lower bound on the absolute costs of different GCs. Using this methodology, we study five production GCs in OpenJDK 17, a high-performance Java runtime. We measure the cost of these collectors, and expose their respective key performance tradeoffs. We find that with a modestly sized heap, production GCs incur substantial overheads across a diverse suite of modern benchmarks, spending at least 7-82% more wall-clock time and 6-92% more CPU cycles relative to the baseline cost. We show that these costs can be masked by concurrency and generous provisioning of memory/compute. In addition, we find that newer low-pause GCs are significantly more expensive than older GCs, and, surprisingly, sometimes deliver worse application latency than stop-the-world GCs. Our findings reaffirm that GC is by no means a solved problem and that a low-cost, low-latency GC remains elusive. We recommend adopting the distillation methodology together with a wider range of cost metrics for future GC evaluations. This will not only help the community more comprehensively understand the performance characteristics of different GCs, but also reveal opportunities for future GC optimizations.
Zixian Cai, Steve Blackburn, Michael D. Bond, Martin Maas 0001
ISPASS3
2022 Mako: a low-pause, high-throughput evacuating collector for memory-disaggregated datacenters
abstract
Resource disaggregation has gained much traction as an emerging datacenter architecture, as it improves resource utilization and simplifies hardware adoption. Under resource disaggregation, different types of resources (memory, CPUs, etc.) are disaggregated into dedicated servers connected by high-speed network fabrics. Memory disaggregation brings efficiency challenges to concurrent garbage collection (GC), which is widely used for latency-sensitive cloud applications, because GC and mutator threads simultaneously run and constantly compete for memory and swap resources.
Chenxi Wang 0005, Yifan Qiao 0002, Michael D. Bond, Steve Blackburn, Miryung Kim, Guoqing Harry Xu
PLDI5
2021 Finding heterogeneous-unsafe configuration parameters in cloud systems
abstract
With the increasing prevalence of heterogeneous hardware and the increasing need for online reconfiguration, there is increasing demand for heterogeneous configurations. However, allowing different nodes to have different configurations may cause errors when these nodes communicate, even if the configuration of each node uses valid values.
Sixiang Ma, Michael D. Bond, Yang Wang 0009
EuroSys3
2021 Understanding and utilizing hardware transactional memory capacity
abstract
Hardware transactional memory (HTM) provides a simpler programming model than lock-based synchronization. However, HTM has limits that mean that transactions may suffer costly capacity aborts. Understanding HTM capacity is therefore critical. Unfortunately, crucial implementation details are undisclosed. In practice HTM capacity can manifest in puzzling ways. It is therefore unsurprising that the literature reports results that appear to be highly contradictory, reporting capacities that vary by nearly three orders of magnitude. We conduct an in-depth study into the causes of HTM capacity aborts using four generations of Intel's Transactional Synchronization Extensions (TSX). We identify the apparent contradictions among prior work, and shed new light on the causes of HTM capacity aborts. In doing so, we reconcile the apparent contradictions. We focus on how replacement policies and the status of the cache can affect HTM capacity.
Zixian Cai, Steve Blackburn, Michael D. Bond
ISMM3
2020 Peacenik: Architecture Support for Not Failing under Fail-Stop Memory Consistency
abstract
Modern shared-memory systems have erroneous, undefined behavior for programs that are not well synchronized. A promising solution is to provide fail-stop memory consistency, which ensures well-defined behavior for all programs. While fail-stop consistency avoids undefined behavior, it can lead to unexpected failures, imperiling performance or progress. This paper presents architecture support called Peacenik that avoids failures in the context of fail-stop memory consistency. We demonstrate Peacenik by applying Peacenik's general mechanisms to two existing architectures that provide fail-stop consistency. A simulation-based evaluation shows that Peacenik eliminates nearly all of the high costs of fail-stop behavior incurred by the baseline architectures, demonstrating how to get the benefits of fail-stop consistency without incurring most or all of its costs.
Swarnendu Biswas, Vignesh Balaji, Michael D. Bond, Brandon Lucia
ASPLOS4
2020 Semeru: A Memory-Disaggregated Managed Runtime
Chenxi Wang 0005, Yuanqi Li, Zhenyuan Ruan, Khanh Nguyen 0001, Michael D. Bond, Ravi Netravali, Miryung Kim, Guoqing Harry Xu
OSDI7
2020 Crafty: efficient, HTM-compatible persistent transactions
abstract
Byte-addressable persistent memory, such as Intel/Micron 3D XPoint, is an emerging technology that bridges the gap between volatile memory and persistent storage. Data in persistent memory survives crashes and restarts; however, it is challenging to ensure that this data is consistent after failures. Existing approaches incur significant performance costs to ensure crash consistency.
Kaan Genç, Michael D. Bond, Guoqing Harry Xu
PLDI2
2020 SmartTrack: efficient predictive race detection
abstract
Widely used data race detectors, including the state-of-the-art FastTrack algorithm, incur performance costs that are acceptable for regular in-house testing, but miss races detectable from the analyzed execution. Predictive analyses detect more data races in an analyzed execution than FastTrack detects, but at significantly higher performance cost.
Jake Roemer, Kaan Genç, Michael D. Bond
PLDI3
2019 Rethinking Support for Region Conflict Exceptions
abstract
Current shared-memory systems provide well-defined execution semantics only for data-race-free executions. A state-of-the-art technique called Conflict Exceptions (CE) extends M(O) ESI-based coherence to provide defined semantics to all program executions. However, CE incurs significant performance costs because of its need to frequently access metadata in memory. In this work, we explore designs for practical architecture support for region conflict exceptions. First, we propose an on-chip metadata cache called access information memory (AIM) to reduce memory accesses in CE. The extended design is called CE+. In spite of the AIM, CE+ stresses or saturates the on-chip interconnect and the off-chip memory network bandwidth because of its reliance on eager write-invalidation-based coherence. We explore whether detecting conflicts is potentially better suited to cache coherence based on release consistency and self-invalidation, rather than M(O) ESI-based coherence. We realize this insight in a novel architecture design called ARC. Our evaluation shows that CE+ improves the run-time performance and energy usage over CE for several applications across different core counts, but can suffer performance penalties from network saturation. ARC generally outperforms CE, and is competitive with CE+ on average while stressing the on-chip interconnect and off-chip memory network much less, showing that coherence based on release consistency and self-invalidation is well suited to detecting region conflicts.
Swarnendu Biswas, Michael D. Bond, Brandon Lucia
IPDPS3
2019 Dependence-aware, unbounded sound predictive race detection
abstract
Data races are a real problem for parallel software, yet hard to detect. Sound predictive analysis observes a program execution and detects data races that exist in some other, unobserved execution. However, existing predictive analyses miss races because they do not scale to full program executions or do not precisely incorporate data and control dependence. This paper introduces two novel, sound predictive approaches that incorporate data and control dependence and handle full program executions. An evaluation using real, large Java programs shows that these approaches detect more data races than the closest related approaches, thus advancing the state of the art in sound predictive race detection.
Kaan Genç, Jake Roemer, Yufan Xu 0001, Michael D. Bond
Proc. ACM Program. Lang.4
2018 High-coverage, unbounded sound predictive race detection
abstract
Dynamic program analysis can predict data races knowable from an observed execution, but existing predictive analyses either miss races or cannot analyze full program executions. This paper presents Vindicator, a novel, sound (no false races) predictive approach that finds more data races than existing predictive approaches. Vindicator achieves high coverage by using a new, efficient analysis that finds all possible predictable races but may detect false races. Vindicator ensures soundness using a novel algorithm that checks each potential race to determine whether it is a true predictable race. An evaluation using large Java programs shows that Vindicator finds hard-to-detect predictable races that existing sound predictive analyses miss, at a comparable performance cost.
Jake Roemer, Kaan Genç, Michael D. Bond
PLDI3
2017 Lightweight data race detection for production runs
Swarnendu Biswas, Man Cao, Minjia Zhang, Michael D. Bond, Benjamin P. Wood
CC4
2017 Legato: end-to-end bounded region serializability using commodity hardware transactional memory
Aritra Sengupta, Man Cao, Michael D. Bond, Milind Kulkarni 0001
CGO3
2017 Avoiding consistency exceptions under strong memory models
abstract
Shared-memory languages and systems generally provide weak or undefined semantics for executions with data races. Prior work has proposed memory consistency models that ensure well-defined, easy-to-understand semantics based on region serializability (RS), but the resulting system may throw a consistency exception in the presence of a data race. Consistency exceptions can occur unexpectedly even in well-tested programs, hurting availability and thus limiting the practicality of RS-based memory models.
Minjia Zhang, Swarnendu Biswas, Michael D. Bond
ISMM3
2017 POSTER: On the Problem of Consistency Exceptions in the Context of Strong Memory Models
abstract
This work considers the problem of availability for memory models that throw consistency exceptions. We define a new memory model called RIx based on isolation of synchronization-free regions and a new approach called Avalon that provides RIx. Our evaluation shows that Avalon and RIx substantially reduce consistency exceptions, by 1-3 orders of magnitude and sometimes eliminate them completely. Furthermore, our exploration provides new, compelling points in the performance-availability tradeoff space.
Minjia Zhang, Swarnendu Biswas, Michael D. Bond
PPoPP3
2017 Instrumentation bias for dynamic data race detection
abstract
This paper presents Fast Instrumentation Bias (FIB), a sound and complete dynamic data race detection algorithm that improves performance by reducing or eliminating the costs of analysis atomicity. In addition to checking for errors in target programs, dynamic data race detectors must introduce synchronization to guard against metadata races that may corrupt analysis state and compromise soundness or completeness. Pessimistic analysis synchronization can account for nontrivial performance overhead in a data race detector. The core contribution of FIB is a novel cooperative ownership-based synchronization protocol whose states and transitions are derived purely from preexisting analysis metadata and logic in a standard data race detection algorithm. By exploiting work already done by the analysis, FIB ensures atomicity of dynamic analysis actions with zero additional time or space cost in the common case. Analysis of temporally thread-local or read-shared accesses completes safely with no synchronization. Uncommon write-sharing transitions require synchronous cross-thread coordination to ensure common cases may proceed synchronization-free. We implemented FIB in the Jikes RVM Java virtual machine. Experimental evaluation shows that FIB eliminates nearly all instrumentation atomicity costs on programs where data often experience windows of thread-local access. Adaptive extensions to the ownership policy effectively eliminate high coordination costs of the core ownership protocol on programs with high rates of serialized sharing. FIB outperforms a naive pessimistic synchronization scheme by 50% on average. Compared to a tuned optimistic metadata synchronization scheme based on conventional fine-grained atomic compare-and-swap operations, FIB is competitive overall, and up to 17% faster on some programs. Overall, FIB effectively exploits latent analysis and program invariants to bring strong integrity guarantees to an otherwise unsynchronized data race detection algorithm at minimal cost.
Benjamin P. Wood, Man Cao, Michael D. Bond, Dan Grossman
Proc. ACM Program. Lang.3
2016 Relaxed dependence tracking for parallel runtime support
abstract
It is notoriously difficult to achieve both correctness and scalability for many shared-memory parallel programs. To improve correctness and scalability, researchers have developed various kinds of parallel runtime support such as multithreaded record & replay and software transactional memory. Existing forms of runtime support slow programs significantly in order to track an execution's cross-thread dependences accurately. This paper investigates the potential for runtime support to hide latency introduced by dependence tracking, by tracking dependences in a relaxed way---meaning that not all dependences are tracked accurately. The key challenge in relaxing dependence tracking is preserving both the program's semantics and the runtime support's guarantees. We present an approach called relaxed dependence tracking (RT) and demonstrate its potential by building two types of RT-based runtime support. Our evaluation shows that RT hides much of the latency incurred by dependence tracking, although RT-based runtime support incurs costs and complexity in order to handle relaxed dependence information. By demonstrating how to relax dependence tracking to hide latency while preserving correctness, this work shows the potential for addressing a key cost of dependence tracking, thus advancing knowledge in the design of parallel runtime support.
Minjia Zhang, Swarnendu Biswas, Michael D. Bond
CC3
2016 Prescient memory: exposing weak memory model behavior by looking into the future
abstract
Shared-memory parallel programs are hard to get right. A major challenge is that language and hardware memory models allow unexpected, erroneous behaviors for executions containing data races. Researchers have introduced dynamic analyses that expose weak memory model behaviors, but these approaches cannot expose behaviors due to loading a "future value" -- a value written by a program store that executes after the program load that uses the value. This paper presents prescient memory (PM), a novel dynamic analysis that exposes behaviors due to future values. PM speculatively returns a future value at a program load, and tries to validate the speculative value at a later store. To enable PM to expose behaviors due to future values in real application executions, we introduce a novel approach that increases the chances of using and successfully validating future values, by profiling and predicting future values and guiding execution. Experiments show that our approach is able to uncover a few previously unknown behaviors due to future values in benchmarked versions of real applications. Overall, PM overcomes a key limitation of existing approaches, broadening the scope of program behaviors that dynamic analyses can expose.
Man Cao, Jake Roemer, Aritra Sengupta, Michael D. Bond
ISMM4
2016 Drinking from both glasses: combining pessimistic and optimistic tracking of cross-thread dependences
abstract
It is notoriously challenging to develop parallel software systems that are both scalable and correct. Runtime support for parallelism---such as multithreaded record & replay, data race detectors, transactional memory, and enforcement of stronger memory models---helps achieve these goals, but existing commodity solutions slow programs substantially in order to track (i.e., detect or control) an execution's cross-thread dependences accurately. Prior work tracks cross-thread dependences either "pessimistically," slowing every program access, or "optimistically," allowing for lightweight instrumentation of most accesses but dramatically slowing accesses involved in cross-thread dependences.
Man Cao, Minjia Zhang, Aritra Sengupta, Michael D. Bond
PPoPP4
2015 Hybrid Static: Dynamic Analysis for Statically Bounded Region Serializability
abstract
Data races are common. They are difficult to detect, avoid, or eliminate, and programmers sometimes introduce them intentionally. However, shared-memory programs with data races have unexpected, erroneous behaviors. Intentional and unintentional data races lead to atomicity and sequential consistency (SC) violations, and they make it more difficult to understand, test, and verify software. Existing approaches for providing stronger guarantees for racy executions add high run-time overhead and/or rely on custom hardware. This paper shows how to provide stronger semantics for racy programs while providing relatively good performance on commodity systems. A novel hybrid static--dynamic analysis called \emph{EnfoRSer} provides end-to-end support for a memory model called \emph{statically bounded region serializability} (SBRS) that is not only stronger than weak memory models but is strictly stronger than SC. EnfoRSer uses static compiler analysis to transform regions, and dynamic analysis to detect and resolve conflicts at run time. By demonstrating commodity support for a reasonably strong memory model with reasonable overheads, we show its potential as an always-on execution model.
Aritra Sengupta, Swarnendu Biswas, Minjia Zhang, Michael D. Bond, Milind Kulkarni 0001
ASPLOS4
2015 Valor: efficient, software-only region conflict exceptions
abstract
Data races complicate programming language semantics, and a data race is often a bug. Existing techniques detect data races and define their semantics by detecting conflicts between synchronization-free regions (SFRs). However, such techniques either modify hardware or slow programs dramatically, preventing always-on use today. This paper describes Valor, a sound, precise, software-only region conflict detection analysis that achieves high performance by eliminating the costly analysis on each read operation that prior approaches require. Valor instead logs a region's reads and lazily detects conflicts for logged reads when the region ends. As a comparison, we have also developed FastRCD, a conflict detector that leverages the epoch optimization strategy of the FastTrack data race detector. We evaluate Valor, FastRCD, and FastTrack, showing that Valor dramatically outperforms FastRCD and FastTrack. Valor is the first region conflict detector to provide strong semantic guarantees for racy program executions with under 2X slowdown. Overall, Valor advances the state of the art in always-on support for strong behavioral guarantees for data races.
Swarnendu Biswas, Minjia Zhang, Michael D. Bond, Brandon Lucia
OOPSLA3
2015 Low-overhead software transactional memory with progress guarantees and strong semantics
abstract
Software transactional memory offers an appealing alternative to locks by improving programmability, reliability, and scalability. However, existing STMs are impractical because they add high instrumentation costs and often provide weak progress guarantees and/or semantics. This paper introduces a novel STM called LarkTM that provides three significant features. (1) Its instrumentation adds low overhead except when accesses actually conflict, enabling low single-thread overhead and scaling well on low-contention workloads. (2) It uses eager concurrency control mechanisms, yet naturally supports flexible conflict resolution, enabling strong progress guarantees. (3) It naturally provides strong atomicity semantics at low cost. LarkTM's design works well for low-contention workloads, but adds significant overhead under higher contention, so we design an adaptive version of LarkTM that uses alternative concurrency control for high-contention objects. An implementation and evaluation in a Java virtual machine show that the basic and adaptive versions of LarkTM not only provide low single-thread overhead, but their multithreaded performance compares favorably with existing high-performance STMs.
Minjia Zhang, Jipeng Huang, Man Cao, Michael D. Bond
PPoPP4
2014 DoubleChecker: efficient sound and precise atomicity checking
abstract
Atomicity is a key correctness property that allows programmers to reason about code regions in isolation. However, programs often fail to enforce atomicity correctly, leading to atomicity violations that are difficult to detect. Dynamic program analysis can detect atomicity violations based on an atomicity specification, but existing approaches slow programs substantially.
Swarnendu Biswas, Jipeng Huang, Aritra Sengupta, Michael D. Bond
PLDI4
2014 Practical Fine-Grained Information Flow Control Using Laminar
abstract
Decentralized Information Flow Control (DIFC) is a promising model for writing programs with powerful, end-to-end security guarantees. Current DIFC systems that run on commodity hardware can be broadly categorized into two types: language-level and operating system-level DIFC. Language solutions provide no guarantees against security violations on system resources such as files and sockets. Operating system solutions mediate accesses to system resources but are either inefficient or imprecise at monitoring the flow of information through fine-grained program data structures. This article describes Laminar, the first system to implement DIFC using a unified set of abstractions for OS resources and heap-allocated objects. Programmers express security policies by labeling data with secrecy and integrity labels and access the labeled data in security methods . Laminar enforces the security policies specified by the labels at runtime. Laminar is implemented using a modified Java virtual machine and a new Linux security module. This article shows that security methods ease incremental deployment and limit dynamic security checks by retrofitting DIFC policies on four application case studies. Replacing the applications' ad hoc security policies changes less than 10% of the code and incurs performance overheads from 5% to 56%. Compared to prior DIFC systems, Laminar supports a more general class of multithreaded DIFC programs efficiently and integrates language and OS abstractions.
Donald E. Porter, Michael D. Bond, Indrajit Roy 0001, Kathryn S. McKinley, Emmett Witchel
ACM Trans. Program. Lang. Syst.2
2013 OCTET: capturing and controlling cross-thread dependences efficiently
abstract
Parallel programming is essential for reaping the benefits of parallel hardware, but it is notoriously difficult to develop and debug reliable, scalable software systems. One key challenge is that modern languages and systems provide poor support for ensuring concurrency correctness properties - atomicity, sequential consistency, and multithreaded determinism - because all existing approaches are impractical. Dynamic, software-based approaches slow programs by up to an order of magnitude because capturing and controlling cross-thread dependences (i.e., conflicting accesses to shared memory) requires synchronization at virtually every access to potentially shared memory.
Michael D. Bond, Milind Kulkarni 0001, Man Cao, Minjia Zhang, Meisam Fathi Salmi, Swarnendu Biswas, Aritra Sengupta, Jipeng Huang
OOPSLA1
2013 Efficient context sensitivity for dynamic analyses via calling context uptrees and customized memory management
abstract
State-of-the-art dynamic bug detectors such as data race and memory leak detectors report program locations that are likely causes of bugs. However, programmers need more than static program locations to understand the behavior of increasingly complex and concurrent software. Dynamic calling context provides additional information, but it is expensive to record calling context frequently, e.g., at every read and write. Context-sensitive dynamic analyses can build and maintain a calling context tree (CCT) to track calling context--but in order to reuse existing nodes, CCT-based approaches require an expensive lookup.
Jipeng Huang, Michael D. Bond
OOPSLA2
2011 A security policy oracle: detecting security holes using multiple API implementations
abstract
Even experienced developers struggle to implement security policies correctly. For example, despite 15 years of development, standard Java libraries still suffer from missing and incorrectly applied permission checks, which enable untrusted applications to execute native calls or modify private class variables without authorization. Previous techniques for static verification of authorization enforcement rely on manually specified policies or attempt to infer the policy by code-mining. Neither approach guarantees that the policy used for verification is correct.
Michael D. Bond, Kathryn S. McKinley, Vitaly Shmatikov
PLDI2
2011 LeakChaser: helping programmers narrow down causes of memory leaks
abstract
In large programs written in managed languages such as Java and C#, holding unnecessary references often results in memory leaks and bloat, degrading significantly their run-time performance and scalability. Despite the existence of many leak detectors for such languages, these detectors often target low-level objects; as a result, their reports contain many false warnings and lack sufficient semantic information to help diagnose problems. This paper introduces a specification-based technique called LeakChaser that can not only capture precisely the unnecessary references leading to leaks, but also explain, with high-level semantics, why these references become unnecessary.
Guoqing Harry Xu, Michael D. Bond, Atanas Rountev
PLDI2
2010 Breadcrumbs: efficient context sensitivity for dynamic bug detection analyses
abstract
Calling context--the set of active methods on the stack--is critical for understanding the dynamic behavior of large programs. Dynamic program analysis tools, however, are almost exclusively context insensitive because of the prohibitive cost of representing calling contexts at run time. Deployable dynamic analyses, in particular, have been limited to reporting only static program locations.
Michael D. Bond, Graham Z. Baker, Samuel Z. Guyer
PLDI1
2010 PACER: proportional detection of data races
abstract
Data races indicate serious concurrency bugs such as order, atomicity, and sequential consistency violations. Races are difficult to find and fix, often manifesting only after deployment. The frequency and unpredictability of these bugs will only increase as software adds parallelism to exploit multicore hardware. Unfortunately, sound and precise race detectors slow programs by factors of eight or more and do not scale to large numbers of threads.
Michael D. Bond, Katherine E. Coons, Kathryn S. McKinley
PLDI1
2009 Leak pruning
abstract
Managed languages improve programmer productivity with type safety and garbage collection, which eliminate memory errors such as dangling pointers, double frees, and buffer overflows. However, because garbage collection uses reachability to over-approximate live objects, programs may still leak memory if programmers forget to eliminate the last reference to an object that will not be used again. Leaks slow programs by increasing collector workload and frequency. Growing leaks eventually crash programs.
Michael D. Bond, Kathryn S. McKinley
ASPLOS1
2009 Laminar: practical fine-grained decentralized information flow control
abstract
Decentralized information flow control (DIFC) is a promising model for writing programs with powerful, end-to-end security guarantees. Current DIFC systems that run on commodity hardware can be broadly categorized into two types: language-level and operating system-level DIFC. Language level solutions provide no guarantees against security violations on system resources, like files and sockets. Operating system solutions can mediate accesses to system resources, but are inefficient at monitoring the flow of information through fine-grained program data structures.
Indrajit Roy 0001, Donald E. Porter, Michael D. Bond, Kathryn S. McKinley, Emmett Witchel
PLDI3
2008 Tolerating memory leaks
abstract
Type safety and garbage collection in managed languages eliminate memory errors such as dangling pointers, double frees, and leaks of unreachable objects. Unfortunately, a program still leaks memory if it maintains references to objects it will never use again. Leaked objects decrease program locality and increase garbage collection frequency and workload. A growing leak will eventually exhaust memory and crash the program.
Michael D. Bond, Kathryn S. McKinley
OOPSLA1
2007 Correcting the Dynamic Call Graph Using Control-Flow Constraints
Byeongcheol Lee, Kevin Resnick, Michael D. Bond, Kathryn S. McKinley
CC3
2007 Probabilistic calling context
abstract
Calling context enhances program understanding and dynamic analyses by providing a rich representation of program location. Compared to imperative programs, object-oriented programs use more interprocedural and less intraprocedural control flow, increasing the importance of context sensitivity for analysis. However, prior online methods for computing calling context, such as stack-walking or maintaining the current location in a calling context tree, are expensive in time and space. This paper introduces a new online approach called probabilistic calling context (PCC) that continuously maintains a probabilistically unique value representing the current calling context. For millions of unique contexts, a 32-bit PCC value has few conflicts. Computing the PCC value adds 3% average overhead to a Java virtual machine. PCC is well-suited to clients that detect new or anomalous behavior since PCC values from training and production runs can be compared easily to detect new context-sensitive behavior; clients that query the PCC value at every system call, Java utility call, and Java API call add 0-9% overhead on average. PCC adds space overhead proportional to the distinct contexts stored by the client (one word per context). Our results indicate PCC is efficient and accurate enough to use in deployed software for residual testing, bug detection, and intrusion detection.
Michael D. Bond, Kathryn S. McKinley
OOPSLA1
2007 Tracking bad apples: reporting the origin of null and undefined value errors
abstract
Programs sometimes crash due to unusable values, for example, when Java and C# programs dereference null pointers and when C and C++ programs use undefined values to affect program behavior. A stack trace produced on such a crash identifies the effect of the unusable value, not its cause, and is often not much help to the programmer.
Michael D. Bond, Nicholas Nethercote, Stephen W. Kent, Samuel Z. Guyer, Kathryn S. McKinley
OOPSLA1
2006 Bell: bit-encoding online memory leak detection
abstract
Memory leaks compromise availability and security by crippling performance and crashing programs. Leaks are difficult to diagnose because they have no immediate symptoms. Online leak detection tools benefit from storing and reporting per-object sites (e.g., allocation sites) for potentially leaking objects. In programs with many small objects, per-object sites add high space overhead, limiting their use in production environments.This paper introduces Bit-Encoding Leak Location (Bell), a statistical approach that encodes per-object sites to a single bit per object. A bit loses information about a site, but given sufficient objects that use the site and a known, finite set of possible sites, Bell uses brute-force decoding to recover the site with high accuracy.We use this approach to encode object allocation and last-use sites in Sleigh, a new leak detection tool. Sleigh detects stale objects (objects unused for a long time) and uses Bell decoding to report their allocation and last-use sites. Our implementation steals four unused bits in the object header and thus incurs no per-object space overhead. Sleigh's instrumentation adds 29% execution time overhead, which adaptive profiling reduces to 11%. Sleigh's output is directly useful for finding and fixing leaks in SPEC JBB2000 and Eclipse, although sufficiently many objects must leak before Bell decoding can report sites with confidence. Bell is suitable for other leak detection approaches that store per-object sites, and for other problems amenable to statistical per-object metadata.
Michael D. Bond, Kathryn S. McKinley
ASPLOS1
2005 Practical Path Profiling for Dynamic Optimizers
abstract
Modern processors are hungry for instructions. To satisfy them, compilers need to find and optimize execution paths across multiple basic blocks. Path profiles provide this context, but their high overhead has so far limited their use by dynamic compilers. We present new techniques for low overhead online practical path profiling (PPP). Following targeted path profiling (TPP), PPP uses an edge profile to simplify path profile instrumentation (profile-guided profiling). PPP improves over prior work by (1) reducing the amount of profiling instrumentation on cold paths and paths that the edge profile predicts well and (2) reducing the cost of the remaining instrumentation. Experiments in an ahead-of-time compiler perform edge profile-guided inlining and unrolling prior to path profiling instrumentation. These transformations are faithful to staged optimization, and create longer, harder to predict paths. We introduce the branch-flow metric to measure path flow as a function of branch decisions, rather than weighting all paths equally as in prior work. On SPEC2000, PPP maintains high accuracy and coverage, but has only 5% overhead on average (ranging from -3% to 13%), making it appealing for use by dynamic compilers.
Michael D. Bond, Kathryn S. McKinley
CGO1
2005 Continuous Path and Edge Profiling
abstract
Micro architectures increasingly rely on dynamic optimization to improve performance in ways that are difficult or impossible for ahead-of-time compilers. Dynamic optimizers in turn require continuous, portable, low cost, and accurate control-flow profiles to inform their decisions, but prior approaches have struggled to meet these goals simultaneously. This paper presents PEP, a hybrid instrumentation and sampling approach for continuous path and edge profiling that is efficient, accurate, and portable. PEP uses a subset of Ball-Larus path profiling to identify paths with low overhead, and uses sampling to mitigate the expense of storing paths. PEP further reduces overhead by using profiling to guide instrumentation placement. PEP improves profile accuracy with a modified version of Arnold-Grove sampling. The resulting system has 1.2% average and 4.3% maximum overhead, 94% path profile accuracy, and 96% edge profile accuracy on a set of Java benchmarks
Michael D. Bond, Kathryn S. McKinley
MICRO1
2004 Targeted Path Profiling: Lower Overhead Path Profiling for Staged Dynamic Optimization Systems
abstract
We present a technique for reducing the overhead of collecting path profiles in the context of a dynamic optimizer. The key idea to our approach, called targeted path profiling (TPP), is to use an edge profile to simplify the collection of a path profile. This notion of profile-guided profiling is a natural fit for dynamic optimizers, which typically optimize the code in a series of stages. TPP is an extension to the Ball-Lams efficient path profiling algorithm. Its increased efficiency comes from two sources: (i) reducing the number of potential paths by not enumerating paths with cold edges, allowing array accesses to be substituted for more expensive hash table lookups, and (ii) not instrumenting regions where paths can be unambiguously derived from an edge profile. Our results suggest that on average the overhead of profile collection can be reduced by half (SPEC95) to almost two-thirds (SPEC2000) relative to the Ball-Larus algorithm with minimal impact on the information collected.
Rahul Joshi, Michael D. Bond, Craig B. Zilles
CGO2