This article introduces a novel system for deriving upper bounds on the heap-space requirements of functional programs with garbage collection. The space cost model is based on a perfect garbage collector that immediately deallocates memory cells when they become unreachable. Heap-space bounds are derived using type-based automatic amortized resource analysis (AARA), a template-based technique that efficiently reduces bound inference to linear programming. The first technical contribution of the work is a new operational cost semantics that models a perfect garbage collector. The second technical contribution is an extension of AARA to take into account automatic deallocation. A key observation is that deallocation of a perfect collector can be modeled with destructive pattern matching if data structures are used in a linear way. However, the analysis uses destructive pattern matching to accurately model deallocation even if data is shared. The soundness of the extended AARA with respect to the new cost semantics is proven in two parts via an intermediate linear cost semantics. The analysis and the cost semantics have been implemented as an extension to Resource Aware ML (RaML). An experimental evaluation shows that the system is able to derive tight symbolic heap-space bounds for common algorithms. Often the bounds are asymptotic improvements over bounds that RaML derives without taking into account garbage collection.
more »
« less
Garbage collection makes rust easier to use: a randomized controlled trial of the bronze garbage collector
Rust is a general-purpose programming language that is both type-and memory-safe. Rust does not use a garbage collector, but rather achieves these properties through a sophisticated, but complex, type system. Doing so makes Rust very efficient, but makes Rust relatively hard to learn and use. We designed Bronze, an optional, library-based garbage collector for Rust. To see whether Bronze could make Rust more usable, we conducted a randomized controlled trial with volunteers from a 633--person class, collecting data from 428 students in total. We found that for a task that required managing complex aliasing, Bronze users were more likely to complete the task in the time available, and those who did so required only about a third as much time (4 hours vs. 12 hours). We found no significant difference in total time, even though Bronze users re-did the task without Bronze afterward. Surveys indicated that ownership, borrowing, and lifetimes were primary causes of the challenges that users faced when using Rust.
more »
« less
- Award ID(s):
- 1801545
- PAR ID:
- 10357741
- Date Published:
- Journal Name:
- ICSE '22: Proceedings of the 44th International Conference on Software Engineering
- Page Range / eLocation ID:
- 1021 to 1032
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Garbage collectors provide memory safety, an important step toward program correctness. However, correctness of the collector itself can be challenging to establish, given both the style in which such systems are written and the weakly-ordered memory accesses of modern hardware. One way to maximize benefits is to use a framework in which effort can be focused on the correctness of small, modular critical components from which various collectors may be composed. Full proof of correctness is likely impractical, so we propose to gain a degree of confidence in collector correctness by applying model checking to critical kernels within a garbage collection framework. We further envisage a model framework, paralleling the framework nature of the collector, in hope that it will be easy to create new models for new collectors. We describe here a prototype model structure, and present results of model checking both stop-the-world and snapshot-at-the-beginning concurrent marking. We found useful regularities of model structure, and that models could be checked within possible time and space budgets on capable servers. This suggests that collectors built in a modular style might be model checked, and further that it may be worthwhile to develop a model checking framework with a domain-specific language from which to generate those models.more » « less
-
more » « less
Abstract Stem rust is an important disease of wheat that can be controlled using resistance genes. The gene
SuSr-D1 identified in cultivar ‘Canthatch’ suppresses stem rust resistance.SuSr-D1 mutants are resistant to several races of stem rust that are virulent on wild-type plants. Here we identifySuSr-D1 by sequencing flow-sorted chromosomes, mutagenesis, and map-based cloning. The gene encodes Med15, a subunit of the Mediator Complex, a conserved protein complex in eukaryotes that regulates expression of protein-coding genes. Nonsense mutations in Med15b.D result in expression of stem rust resistance. Time-course RNAseq analysis show a significant reduction or complete loss of differential gene expression at 24 h post inoculation inmed15b.D mutants, suggesting that transcriptional reprogramming at this time point is not required for immunity to stem rust. Suppression is a common phenomenon and this study provides novel insight into suppression of rust resistance in wheat. -
We introduce Flux, which shows how logical refinements can work hand in glove with Rust's ownership mechanisms to yield ergonomic type-based verification of low-level pointer manipulating programs. First, we design a novel refined type system for Rust that indexes mutable locations, with pure (immutable) values that can appear in refinements, and then exploits Rust's ownership mechanisms to abstract sub-structural reasoning about locations within Rust's polymorphic type constructors, while supporting strong updates. We formalize the crucial dependency upon Rust's strong aliasing guarantees by exploiting the Stacked Borrows aliasing model to prove that "well-borrowed evaluations of well-typed programs do not get stuck". Second, we implement our type system in Flux, a plug-in to the Rust compiler that exploits the factoring of complex invariants into types and refinements to efficiently synthesize loop annotations-including complex quantified invariants describing the contents of containers-via liquid inference. Third, we evaluate Flux with a benchmark suite of vector manipulating programs and parts of a previously verified secure sandboxing library to demonstrate the advantages of refinement types over program logics as implemented in the state-of-the-art Prusti verifier. While Prusti's more expressive program logic can, in general, verify deep functional correctness specifications, for the lightweight but ubiquitous and important verification use-cases covered by our benchmarks, liquid typing makes verification ergonomic by slashing specification lines by a factor of two, verification time by an order of magnitude, and annotation overhead from up to 24% of code size (average 14%), to nothing at all.more » « less
-
more » « less
Summary Urbanization and other human modifications of the landscape may indirectly affect disease dynamics by altering host behavior in ways that influence pathogen transmission. Few opportunities arise to investigate behaviorally mediated effects of human habitat modification in natural host–pathogen systems, but we provide a potential example of this phenomenon in banded mongooses (
Mungos mungo ), a social mammal. Our banded mongoose study population in Botswana is endemically infected with a novelMycobacterium tuberculosis complex pathogen,M. mungi , that primarily invades the mongoose host through the nasal planum and breaks in the skin. In this system, several study troops have access to human garbage sites and other modified landscapes for foraging. Banded mongooses in our study site (N = 4 troops, ~130 individuals) had significantly higher within‐troop aggression levels when foraging in garbage compared to other foraging habitats. Second, monthly rates of aggression were a significant predictor of monthly number of injuries in troops. Finally, injured individuals had a 75% incidence of clinical tuberculosis (TB ) compared to a 0% incidence in visibly uninjured mongooses during the study period. Our data suggest that mongoose troops that forage in garbage may be at greater risk of acquiringTB by incurring injuries that may allow for pathogen invasion. Our study suggests the need to consider the indirect effects of garbage on behavior and wildlife health when developing waste management approaches in human‐modified areas.
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/10.1145/3510003.3510107
