-
RustMC: Extending the GenMC stateless model checker to Rust
Authors:
Oliver Pearce,
Julien Lange,
Dan O'Keeffe
Abstract:
RustMC is a stateless model checker that enables verification of concurrent Rust programs. As both Rust and C/C++ compile to LLVM IR, RustMC builds on GenMC which provides a verification framework for LLVM IR. This enables the automatic verification of Rust code and any C/C++ dependencies. This tool paper presents the key challenges we addressed to extend GenMC. These challenges arise from Rust's…
▽ More
RustMC is a stateless model checker that enables verification of concurrent Rust programs. As both Rust and C/C++ compile to LLVM IR, RustMC builds on GenMC which provides a verification framework for LLVM IR. This enables the automatic verification of Rust code and any C/C++ dependencies. This tool paper presents the key challenges we addressed to extend GenMC. These challenges arise from Rust's unique compilation strategy and include intercepting threading operations, handling memory intrinsics and uninitialized accesses. Through case studies adapted from real-world programs, we demonstrate RustMC's effectiveness at finding concurrency bugs stemming from unsafe Rust code, FFI calls to C/C++, and incorrect use of atomic operations.
△ Less
Submitted 10 February, 2025;
originally announced February 2025.
-
A Tale of Two Models: Understanding Data Workers' Internal and External Representations of Complex Data
Authors:
Connor Scully-Allison,
Katy Williams,
Stephanie Brink,
Olga Pearce,
Katherine E. Isaacs
Abstract:
Data workers may have a a different mental model of their data that the one reified in code. Understanding the organization of their data is necessary for analyzing data, be it through scripting, visualization or abstract thought. More complicated organizations, such as tables with attached hierarchies, may tax people's ability to think about and interact with data. To better understand and ultima…
▽ More
Data workers may have a a different mental model of their data that the one reified in code. Understanding the organization of their data is necessary for analyzing data, be it through scripting, visualization or abstract thought. More complicated organizations, such as tables with attached hierarchies, may tax people's ability to think about and interact with data. To better understand and ultimately design for these situations, we conduct a study across a team of ten people working with the same reified data model. Through interviews and sketching, we probed their conception of the data model and developed themes through reflexive data analysis. Participants had diverse data models that differed from the reified data model, even among team members who had designed the model, resulting in parallel hazards limiting their ability to reason about the data. From these observations, we suggest potential design interventions for data analysis processes and tools.
△ Less
Submitted 21 January, 2025; v1 submitted 16 January, 2025;
originally announced January 2025.
-
MPI Implementation Profiling for Better Application Performance
Authors:
Riley Shipley,
Garrett Hooten,
David Boehme,
Derek Schafer,
Anthony Skjellum,
Olga Pearce
Abstract:
While application profiling has been a mainstay in the HPC community for years, profiling of MPI and other communication middleware has not received the same degree of exploration. This paper adds to the discussion of MPI profiling, contributing two general-purpose profiling methods as well as practical applications of these methods to an existing implementation. The ability to detect performance…
▽ More
While application profiling has been a mainstay in the HPC community for years, profiling of MPI and other communication middleware has not received the same degree of exploration. This paper adds to the discussion of MPI profiling, contributing two general-purpose profiling methods as well as practical applications of these methods to an existing implementation. The ability to detect performance defects in MPI codes using these methods increases the potential of further research and development in communication optimization.
△ Less
Submitted 19 February, 2024;
originally announced February 2024.
-
Design Concerns for Integrated Scripting and Interactive Visualization in Notebook Environments
Authors:
Connor Scully-Allison,
Ian Lumsden,
Katy Williams,
Jesse Bartels,
Michela Taufer,
Stephanie Brink,
Abhinav Bhatele,
Olga Pearce,
Katherine E. Isaacs
Abstract:
Interactive visualization can support fluid exploration but is often limited to predetermined tasks. Scripting can support a vast range of queries but may be more cumbersome for free-form exploration. Embedding interactive visualization in scripting environments, such as computational notebooks, provides an opportunity to leverage the strengths of both direct manipulation and scripting. We investi…
▽ More
Interactive visualization can support fluid exploration but is often limited to predetermined tasks. Scripting can support a vast range of queries but may be more cumbersome for free-form exploration. Embedding interactive visualization in scripting environments, such as computational notebooks, provides an opportunity to leverage the strengths of both direct manipulation and scripting. We investigate interactive visualization design methodology, choices, and strategies under this paradigm through a design study of calling context trees used in performance analysis, a field which exemplifies typical exploratory data analysis workflows with Big Data and hard to define problems. We first produce a formal task analysis assigning tasks to graphical or scripting contexts based on their specificity, frequency, and suitability. We then design a notebook-embedded interactive visualization and validate it with intended users. In a follow-up study, we present participants with multiple graphical and scripting interaction modes to elicit feedback about notebook-embedded visualization design, finding consensus in support of the interaction model. We report and reflect on observations regarding the process and design implications for combining visualization and scripting in notebooks.
△ Less
Submitted 16 October, 2024; v1 submitted 9 May, 2022;
originally announced May 2022.
