No Arabic abstract
Rust is a systems programming language that guarantees memory safety without the need for a garbage collector by statically tracking ownership and borrowing events. The associated rules are subtle and unique among industry programming languages, which can make learning Rust more challenging. Motivated by the challenges that Rust learners face, we are developing RustViz, a tool that allows teachers to generate an interactive timeline depicting ownership and borrowing events for each variable in a Rust code example. These visualizations are intended to help Rust learners develop an understanding of ownership and borrowing by example. This paper introduces RustViz by example, shows how teachers can use it to generate visualizations, describes learning goals, and proposes a study designed to evaluate RustViz based on these learning goals.
Ownership is the concept of tracking aliases and mutations to data, useful for both memory safety and system design. The Rust programming language implements ownership via the borrow checker, a static analyzer that extends the core type system. The borrow checker is a notorious learning barrier for new Rust users. In this paper, I focus on the gap between understanding ownership in theory versus its implementation in the borrow checker. As a sound and incomplete analysis, compiler errors may arise from either ownership-unsound behavior or limitations of the analyzer. Understanding this distinction is essential for fixing ownership errors. But how are users actually supposed to make the correct inference? Drawing on my experience with using and teaching Rust, I explore the many challenges in interpreting and responding to ownership errors. I also suggest educational and automated interventions that could improve the usability of ownership.
Just-in-time (JIT) compilers are used by many modern programming systems in order to improve performance. Bugs in JIT compilers provide exploitable security vulnerabilities and debugging them is difficult as they are large, complex, and dynamic. Current debugging and visualization tools deal with static code and are not suitable in this domain. We describe a new approach for simplifying the large and complex intermediate representation, generated by a JIT compiler and visualize it with a metro map metaphor to aid developers in debugging.
Linearizability is a commonly accepted notion of correctness for libraries of concurrent algorithms. Unfortunately, it assumes a complete isolation between a library and its client, with interactions limited to passing values of a given data type. This is inappropriate for common programming languages, where libraries and their clients can communicate via the heap, transferring the ownership of data structures, and can even run in a shared address space without any memory protection. In this paper, we present the first definition of linearizability that lifts this limitation and establish an Abstraction Theorem: while proving a property of a client of a concurrent library, we can soundly replace the library by its abstract implementation related to the original one by our generalisation of linearizability. This allows abstracting from the details of the library implementation while reasoning about the client. We also prove that linearizability with ownership transfer can be derived from the classical one if the library does not access some of data structures transferred to it by the client.
A prominent goal of neuroimaging studies is mapping the human brain, in order to identify and delineate functionally-meaningful regions and elucidate their roles in cognitive behaviors. These brain regions are typically represented by atlases that capture general trends over large populations. Despite being indispensable to neuroimaging experts, population-level atlases do not capture individual differences in functional organization. In this work, we present an interactive visualization method, PRAGMA, that allows domain experts to derive scan-specific parcellations from established atlases. PRAGMA features a user-driven, hierarchical clustering scheme for defining temporally correlated parcels in varying granularity. The visualization design supports the user in making decisions on how to perform clustering, namely when to expand, collapse, or merge parcels. This is accomplished through a set of linked and coordinated views for understanding the users current hierarchy, assessing intra-cluster variation, and relating parcellations to an established atlas. We assess the effectiveness of PRAGMA through a user study with four neuroimaging domain experts, where our results show that PRAGMA shows the potential to enable exploration of individualized and state-specific brain parcellations and to offer interesting insights into functional brain networks.
In many upper-division lab courses, instructors implement multiweek student-led projects. During such projects, students may design and carry out experiments, collect and analyze data, document and report their findings, and collaborate closely with peers and mentors. To better understand cognitive, social, and affective aspects of projects, we conducted an exploratory investigation of student ownership of projects. Ownership is a complex construct that refers to, e.g., students willingness and ability to make strategic decisions about their project. Using data collected through surveys and interviews with students and instructors at five institutions, we developed a preliminary model for student ownership of projects. Our model describes student interactions with the project during three phases: choice of topic, execution of experiment, and synthesis of results. Herein, we explicate our model and demonstrate that it maps well onto students and instructors conceptions of ownership and ideas presented in prior literature.