러스트(Rust) 소유권(Ownership) 타입에 대한 개념적 모델

Introduction Background A Concept Inventory for Ownership A Conceptual Model for Ownership Evaluation Related Work General Discussion Acknowledgments Originally Published References Footnotes Abstract Programmers learning Rust struggle to understand ownership types, Rust’s core mechanism for ensuring memory safety without garbage collection. This paper describes our process of systematically designing a pedagogy for ownership types. First, we studied Rust developers’ misconceptions of ownership to create the Ownership Inventory, a new instrument for measuring a person’s knowledge of ownership. We found that Rust learners could not connect Rust’s static and dynamic semantics, such as determining why an ill-typed program would (or would not) exhibit undefined behavior. Second, we created a conceptual model of Rust’s semantics that explains borrow checking in terms of flow-sensitive permissions on paths into memory. Third, we implemented a Rust compiler plug-in that visualizes programs under the model. Fourth, we integrated the permissions model and visualizations into a broader pedagogy of ownership by writing a new ownership chapter for The Rust Programming Language , a popular Rust textbook. Fifth, we evaluated an initial deployment of our pedagogy against the original version, using reader responses to the Ownership Inventory as a point of comparison. Thus far, the new pedagogy has improved learner scores on the Ownership Inventory by an average of 9% (N= 342, d= 0.56). 1. Introduction Ownership is a programming discipline for managing the aliasing and mutation of data, enforced statically through ownership types. The flagship programming language for ownership is Rust, which empowers programmers to write memory-safe code without garbage collection. Rust’s ownership model synthesizes several ideas from programming language research, such as linear logic, 9 class-based alias management, 6 and region-based memory management. 10 Developers cannot use languages like C and C++ to build memory-safe systems at scale, 19 so the software industry is turning toward Rust. For example, Google’s Android team has thus far found zero memory vulnerabilities in 1.5 million lines of Rust code. 24 This rosy picture of tech transfer belies a persistent obstacle: teaching Rust to prospective users, especially about ownership. Over the last four years, studies have found that Rust learners struggle to fix ownership type errors, 28 and users self-report that ownership is among their biggest barriers to learning Rust. 23 To wit: Advances in the technical factors of type systems require commensurate advances in the human factors of type systems. Our work started with the question: How can we systematically design a pedagogy for ownership types? Today, popular pedagogies for advanced type systems are driven by experts’ intuitions about how people learn, as well as by intuitions about what makes type systems difficult to understand. As practicing (computer) scientists, we wanted to approach pedagogic design through scientific principles: grounding the pedagogy in observations about the struggles of Rust learners, and then evaluating the pedagogy by its effects on learning outcomes. This paper describes how we put these principles into practice: We ran a formative user study to identify misconceptions about ownership types held by Rust learners ( Section 3 ). We designed a new instrument for evaluating understanding of ownership, the Ownership Inventory, by drawing tasks from commonly reported Rust issues on StackOverflow. We studied N = 36 Rust learners trying to solve Ownership Inventory problems. We found that learners can generally identify the surface-level reason for why a program is ill-typed with respect to ownership. However, learners do not understand what undefined behavior (if any) would occur if an ill-typed program were executed. This misunderstanding is reflected in inefficient and incorrect strategies used to fix ownership errors. We developed a conceptual model of ownership types to address these misconceptions ( Section 4 ). The conceptual model represents the aspects of Rust’s static and dynamic semantics that are relevant to ownership while abstracting other details. The model provides learners a foundation to understand essential concepts such as undefined behavior and the incompleteness of Rust’s ownership type-checker, or “borrow checker.” We implemented tools to execute Rust programs under the conceptual model, generating traces which we visualize to illustrate how the model applies to concrete examples. We wrote a new chapter on ownership for a popular Rust textbook, The Rust Programming Language ( TRPL ), 12 using this conceptual model with these visualizations. We A/B tested our pedagogy against the TRPL baseline ( Section 5 ). We set up and advertised a public website that hosts our TRPL fork. We measured learning outcomes with two kinds of quizzes: simpler comprehension questions about the conceptual model, and more difficult multiple-choice versions of the Ownership Inventory. Learners could correctly answer comprehension questions with 72% accuracy. Our initial deployment improved the average Inventory score from 48% to 57% ( N = 342, p < 0.001, d = 0.56). 2. Background If you, the reader, are not familiar with Rust or ownership, then it’s important to understand the basics to understand this paper’s contributions. One contribution is exactly an explanation of the basics of ownership. We will therefore give a brief exposition of Rust in the form of a heavily abbreviated version of the actual pedagogy we developed for Rust learners. Later sections will refer back to explain the design rationale of the concepts and diagrams mentioned here. 2.1 Ownership. Rust is a systems programming language, most similar in its aims and scope to C++. Rust contains many standard imperative language features, such as mutable variables, conditionals, arrays, loops, structs, and functions. Rust manages memory through a system of compile-time checks known as ownership , as opposed to runtime checks (garbage collection) or manual checks (malloc/free). The basic idea is that heap allocations are owned by a variable, and allocations are freed when their owner goes out of scope, unless the owner moves ownership to another variable. This concept is illustrated in Figure 1 . The goal of ownership is to ensure memory safety, or more generally, to prevent undefined behavior . Undefined behavior means runtime operations without semantics under the Rust language specification, such as dereferencing a null pointer or pretending a string is a boolean. To prevent undefined behavior, the Rust compiler enforces several rules. First, data always has exactly one owner. Second, data is only deallocated on behalf of its owner. Third, data can only be accessed through its owner (except through references, discussed next). These rules prevent situations such as double-frees or use after-frees as shown in Figure 2 . 2.2 Borrowing. To allow accessing data without owning it, Rust provides non-owning pointers called references. References borrow data owned by another variable. Those references can be either immutable (created by & ) or mutable (created by &mut ). Figure 3 shows an example of creating an immutable reference to a piece of a string, and creating a mutable reference to pass to a helper function. Rust enforces safety with references through the concept of permissions. Permissions describe the kinds of operations one can do to data; they come and go based on which owners and references are in use at any given time. Specifically, Rust tracks three permission: readable ( R ), writable ( W ), or ownable ( O ). Figure 4 shows one example of how permissions change over the course of a program. Each operation expects certain permissions from its inputs. For example, getting the length of a vector requires R . Pushing an element to a vector requires W . Deallocating a vector requ