An official website of the United States government
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
-
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
-
In Computer Science (CS) education, instructors use office hours for one-on-one help-seeking. Prior work has shown that traditional in-person office hours may be underutilized. In response many instructors are adding or transitioning to virtual office hours. Our research focuses on comparing in-person and online office hours to investigate differences between performance, interaction time, and the characteristics of the students who utilize in-person and virtual office hours. We analyze a rich dataset covering two semesters of a CS2 course which used in-person office hours in Fall 2019 and virtual office hours in Fall 2020. Our data covers students' use of office hours, the nature of their questions, and the time spent receiving help as well as demographic and attitude data. Our results show no relationship between student's attendance in office hours and class performance. However we found that female students attended office hours more frequently, as did students with a fixed mindset in computing, and those with weaker skills in transferring theory to practice. We also found that students with low confidence in or low enjoyment toward CS were more active in virtual office hours. Finally, we observed a significant correlation between students attending virtual office hours and an increased interest in CS study; while students attending in-person office hours tend to show an increase in their growth mindset.more » « less
-
Merkle, Larry; Doyle, Maureen; Sheard, Judithe; Soh, Leen-Kiat; Dorn, Brian (Ed.)In Computer Science (CS) education, instructors use office hours for one-on-one help-seeking. Prior work has shown that traditional in-person office hours may be underutilized. In response many instructors are adding or transitioning to virtual office hours. Our research focuses on comparing in-person and online office hours to investigate differences between performance, interaction time, and the characteristics of the students who utilize in-person and virtual office hours. We analyze a rich dataset covering two semesters of a CS2 course which used in-person office hours in Fall 2019 and virtual office hours in Fall 2020. Our data covers students' use of office hours, the nature of their questions, and the time spent receiving help as well as demographic and attitude data. Our results show no relationship between student's attendance in office hours and class performance. However we found that female students attended office hours more frequently, as did students with a fixed mindset in computing, and those with weaker skills in transferring theory to practice. We also found that students with low confidence in or low enjoyment toward CS were more active in virtual office hours. Finally, we observed a significant correlation between students attending virtual office hours and an increased interest in CS study; while students attending in-person office hours tend to show an increase in their growth mindset.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/10.1145/3510003.3510107
