MC
M.A. Costea
info
Please Note
<p>This page displays the records of the person named above and is not linked to a unique person identifier. This record may need to be merged to a profile.</p>
17 records found
1
Rust provides performance, memory safety, and the promise of “fearless concurrency,” owing to its robust ownership system. Rayon has become a widespread library for data parallelism within Rust, enabling programmers to incorporate concurrency into their programs seamlessly.
This work presents the most common Rayon usages across the top 1000 open-source Rust repositories on Github, measured by stargazer count and filtered for usage of Rayon. We perform a manual analysis on 5 repositories, identifying themes within selected instances.
We contextualise these themes to characterize how Rayon is used for complex workloads, where unsafe code is combined with Rayon, and where parallel iterators are insufficient. ...
This work presents the most common Rayon usages across the top 1000 open-source Rust repositories on Github, measured by stargazer count and filtered for usage of Rayon. We perform a manual analysis on 5 repositories, identifying themes within selected instances.
We contextualise these themes to characterize how Rayon is used for complex workloads, where unsafe code is combined with Rayon, and where parallel iterators are insufficient. ...
Rust provides performance, memory safety, and the promise of “fearless concurrency,” owing to its robust ownership system. Rayon has become a widespread library for data parallelism within Rust, enabling programmers to incorporate concurrency into their programs seamlessly.
This work presents the most common Rayon usages across the top 1000 open-source Rust repositories on Github, measured by stargazer count and filtered for usage of Rayon. We perform a manual analysis on 5 repositories, identifying themes within selected instances.
We contextualise these themes to characterize how Rayon is used for complex workloads, where unsafe code is combined with Rayon, and where parallel iterators are insufficient.
This work presents the most common Rayon usages across the top 1000 open-source Rust repositories on Github, measured by stargazer count and filtered for usage of Rayon. We perform a manual analysis on 5 repositories, identifying themes within selected instances.
We contextualise these themes to characterize how Rayon is used for complex workloads, where unsafe code is combined with Rayon, and where parallel iterators are insufficient.
Message Passing in Rust Applications
An exploratory analysis of channel primitives, architectural patterns, and communication roles
Rust promotes message-passing concurrency through channels, yet little is known about how message passing is used in real-world Rust applications. This study investigates message-passing usage in open-source Rust applications through a combination of repository classification and template-guided manual analysis.
Repositories were selected from the Awesome Rust applications collection and classified according to four communication categories. The resulting repositories were then analysed using an automated channel-count analysis to identify message-passing primitives, followed by template-guided manual analysis to identify communication structures and message-passing roles.
The results show that Rust applications employ a diverse range of message-passing primitives and communication patterns. Message passing is commonly organised around dedicated receiving components and is primarily used for data transport, event propagation, and coordination between concurrent tasks. Rather than relying on a single communication pattern, applications frequently combine multiple communication structures and roles within the same codebase.
This work provides an exploratory empirical analysis of message passing in Rust applications and introduces a structured methodology for analysing message-passing usage in software systems. ...
Repositories were selected from the Awesome Rust applications collection and classified according to four communication categories. The resulting repositories were then analysed using an automated channel-count analysis to identify message-passing primitives, followed by template-guided manual analysis to identify communication structures and message-passing roles.
The results show that Rust applications employ a diverse range of message-passing primitives and communication patterns. Message passing is commonly organised around dedicated receiving components and is primarily used for data transport, event propagation, and coordination between concurrent tasks. Rather than relying on a single communication pattern, applications frequently combine multiple communication structures and roles within the same codebase.
This work provides an exploratory empirical analysis of message passing in Rust applications and introduces a structured methodology for analysing message-passing usage in software systems. ...
Rust promotes message-passing concurrency through channels, yet little is known about how message passing is used in real-world Rust applications. This study investigates message-passing usage in open-source Rust applications through a combination of repository classification and template-guided manual analysis.
Repositories were selected from the Awesome Rust applications collection and classified according to four communication categories. The resulting repositories were then analysed using an automated channel-count analysis to identify message-passing primitives, followed by template-guided manual analysis to identify communication structures and message-passing roles.
The results show that Rust applications employ a diverse range of message-passing primitives and communication patterns. Message passing is commonly organised around dedicated receiving components and is primarily used for data transport, event propagation, and coordination between concurrent tasks. Rather than relying on a single communication pattern, applications frequently combine multiple communication structures and roles within the same codebase.
This work provides an exploratory empirical analysis of message passing in Rust applications and introduces a structured methodology for analysing message-passing usage in software systems.
Repositories were selected from the Awesome Rust applications collection and classified according to four communication categories. The resulting repositories were then analysed using an automated channel-count analysis to identify message-passing primitives, followed by template-guided manual analysis to identify communication structures and message-passing roles.
The results show that Rust applications employ a diverse range of message-passing primitives and communication patterns. Message passing is commonly organised around dedicated receiving components and is primarily used for data transport, event propagation, and coordination between concurrent tasks. Rather than relying on a single communication pattern, applications frequently combine multiple communication structures and roles within the same codebase.
This work provides an exploratory empirical analysis of message passing in Rust applications and introduces a structured methodology for analysing message-passing usage in software systems.
Concurrency and Async Practices in Real-World Rust
How are lock-free and atomic-based concurrency techniques used in Rust crates?
Rust provides strong safety guarantees and supports several forms of concurrency, including atomic-based techniques. In this paper, we study how such techniques are used in crates that provide and use atomic-based functionality. We observed that these techniques mainly support communication between threads, shared access to data, and coordination of work. We also observed that they appear at different abstraction levels, from low-level memory management to higher-level data structures. These results help explain how atomic-based concurrency is used in real-world Rust code.
...
Rust provides strong safety guarantees and supports several forms of concurrency, including atomic-based techniques. In this paper, we study how such techniques are used in crates that provide and use atomic-based functionality. We observed that these techniques mainly support communication between threads, shared access to data, and coordination of work. We also observed that they appear at different abstraction levels, from low-level memory management to higher-level data structures. These results help explain how atomic-based concurrency is used in real-world Rust code.
Asynchronous Programming in Rust
An Empirical Analysis on the Usage of Asynchronous Code by Rust Developers
Asynchronous programming in Rust introduces challenges regarding correctness, synchronization and concurrency. Existing literature has focused on uncovering bugs and providing verification techniques to mitigate these. However, further research within this field is still required and to the best of our knowledge, limited empirical data exists analyzing why asynchronous Rust is used in practice and the prominence of different runtimes.
In this paper, we present Rustc-Analysis, an automated analysis tool for discovering and extracting underlying structural information of asynchronous Rust code. We subsequently use this tool to analyze runtime adoption and characterize the functionality provided by asynchronous APIs.
Our analysis shows that asynchronous APIs are mainly used for I/O-related tasks, particularly networking and file-system operations, as well as synchronization between concurrent tasks. Furthermore, we find tokio to be the most widely adopted runtime, followed by futures, async-std and smol. ...
In this paper, we present Rustc-Analysis, an automated analysis tool for discovering and extracting underlying structural information of asynchronous Rust code. We subsequently use this tool to analyze runtime adoption and characterize the functionality provided by asynchronous APIs.
Our analysis shows that asynchronous APIs are mainly used for I/O-related tasks, particularly networking and file-system operations, as well as synchronization between concurrent tasks. Furthermore, we find tokio to be the most widely adopted runtime, followed by futures, async-std and smol. ...
Asynchronous programming in Rust introduces challenges regarding correctness, synchronization and concurrency. Existing literature has focused on uncovering bugs and providing verification techniques to mitigate these. However, further research within this field is still required and to the best of our knowledge, limited empirical data exists analyzing why asynchronous Rust is used in practice and the prominence of different runtimes.
In this paper, we present Rustc-Analysis, an automated analysis tool for discovering and extracting underlying structural information of asynchronous Rust code. We subsequently use this tool to analyze runtime adoption and characterize the functionality provided by asynchronous APIs.
Our analysis shows that asynchronous APIs are mainly used for I/O-related tasks, particularly networking and file-system operations, as well as synchronization between concurrent tasks. Furthermore, we find tokio to be the most widely adopted runtime, followed by futures, async-std and smol.
In this paper, we present Rustc-Analysis, an automated analysis tool for discovering and extracting underlying structural information of asynchronous Rust code. We subsequently use this tool to analyze runtime adoption and characterize the functionality provided by asynchronous APIs.
Our analysis shows that asynchronous APIs are mainly used for I/O-related tasks, particularly networking and file-system operations, as well as synchronization between concurrent tasks. Furthermore, we find tokio to be the most widely adopted runtime, followed by futures, async-std and smol.
Understanding Shared-Memory Concurrency Usage in Rust Systems
A Qualitative Study of Concurrency Primitives, Thread Organisation Models, Workloads, and Functional Roles
Rust provides strong guarantees for memory safety and concurrency correctness, but relatively little is known about how shared-memory concurrency is used in real-world Rust systems. While existing research has largely focused on Rust’s safety guarantees and performance, fewer studies have examined how developers use shared-memory concurrency mechanisms in practice. This work investigates how shared-memory concurrency is used in Rust systems that make extensive use of concurrency. A qualitative thematic analysis was conducted on concurrency-related files from a selection of open-source Rust repositories. The analysis examined the use of shared-memory concurrency primitives, thread organisation models, workload types, functional roles, and implementation trade-offs.
The results show that a small set of primitives, namely Arc, Mutex, and RwLock, accounts for most observed concurrency usage, while specialised primitives appear comparatively rarely. Shared-state concurrency appeared to be the dominant thread organisation model, although actor/message-passing approaches were also commonly used. Across the analysed files, concurrency-related code was primarily used for coordination-heavy responsibilities such as runtime management, resource coordination, event dispatch, request handling, and state management rather than computational work. The findings further show that higher-level architectural patterns frequently rely on shared-memory mechanisms, even when message passing forms the primary organisational model. Several trade-offs were identified between simplicity, scalability, modularity, and coordination complexity. Overall, the study suggests that shared ownership in Rust is used primarily to coordinate access to shared state and resources, and that shared ownership and synchronised access remain foundational despite the availability of other concurrency abstractions. The findings provide insights into how shared-memory concurrency is applied in native Rust systems and provide a foundation for future research on concurrency design practices in Rust software. ...
The results show that a small set of primitives, namely Arc, Mutex, and RwLock, accounts for most observed concurrency usage, while specialised primitives appear comparatively rarely. Shared-state concurrency appeared to be the dominant thread organisation model, although actor/message-passing approaches were also commonly used. Across the analysed files, concurrency-related code was primarily used for coordination-heavy responsibilities such as runtime management, resource coordination, event dispatch, request handling, and state management rather than computational work. The findings further show that higher-level architectural patterns frequently rely on shared-memory mechanisms, even when message passing forms the primary organisational model. Several trade-offs were identified between simplicity, scalability, modularity, and coordination complexity. Overall, the study suggests that shared ownership in Rust is used primarily to coordinate access to shared state and resources, and that shared ownership and synchronised access remain foundational despite the availability of other concurrency abstractions. The findings provide insights into how shared-memory concurrency is applied in native Rust systems and provide a foundation for future research on concurrency design practices in Rust software. ...
Rust provides strong guarantees for memory safety and concurrency correctness, but relatively little is known about how shared-memory concurrency is used in real-world Rust systems. While existing research has largely focused on Rust’s safety guarantees and performance, fewer studies have examined how developers use shared-memory concurrency mechanisms in practice. This work investigates how shared-memory concurrency is used in Rust systems that make extensive use of concurrency. A qualitative thematic analysis was conducted on concurrency-related files from a selection of open-source Rust repositories. The analysis examined the use of shared-memory concurrency primitives, thread organisation models, workload types, functional roles, and implementation trade-offs.
The results show that a small set of primitives, namely Arc, Mutex, and RwLock, accounts for most observed concurrency usage, while specialised primitives appear comparatively rarely. Shared-state concurrency appeared to be the dominant thread organisation model, although actor/message-passing approaches were also commonly used. Across the analysed files, concurrency-related code was primarily used for coordination-heavy responsibilities such as runtime management, resource coordination, event dispatch, request handling, and state management rather than computational work. The findings further show that higher-level architectural patterns frequently rely on shared-memory mechanisms, even when message passing forms the primary organisational model. Several trade-offs were identified between simplicity, scalability, modularity, and coordination complexity. Overall, the study suggests that shared ownership in Rust is used primarily to coordinate access to shared state and resources, and that shared ownership and synchronised access remain foundational despite the availability of other concurrency abstractions. The findings provide insights into how shared-memory concurrency is applied in native Rust systems and provide a foundation for future research on concurrency design practices in Rust software.
The results show that a small set of primitives, namely Arc, Mutex, and RwLock, accounts for most observed concurrency usage, while specialised primitives appear comparatively rarely. Shared-state concurrency appeared to be the dominant thread organisation model, although actor/message-passing approaches were also commonly used. Across the analysed files, concurrency-related code was primarily used for coordination-heavy responsibilities such as runtime management, resource coordination, event dispatch, request handling, and state management rather than computational work. The findings further show that higher-level architectural patterns frequently rely on shared-memory mechanisms, even when message passing forms the primary organisational model. Several trade-offs were identified between simplicity, scalability, modularity, and coordination complexity. Overall, the study suggests that shared ownership in Rust is used primarily to coordinate access to shared state and resources, and that shared ownership and synchronised access remain foundational despite the availability of other concurrency abstractions. The findings provide insights into how shared-memory concurrency is applied in native Rust systems and provide a foundation for future research on concurrency design practices in Rust software.
Rust is a systems programming language that guarantees both performance and Memory Safety through its memory model. With unsafe rust it is possible to opt-out of some security guarantees made by the compiler. However, this comes at the risk of re-introducing memory bugs. While various tools already exist for detecting memory errors in (unsafe) Rust, they are either dynamic or focus on proving the absence of bugs. In this thesis we lay the foundations for a static analysis for Rust that focuses on proving the presence of bugs (Under Approximation) instead of their absence (Over Approximation). We show how we can use a formal framework called incorrectness separation logic (ISL) to show the presence of memory errors in Rust. We add Rust support to Infer, a static analysis tool by Meta that uses ISL to prove the presence of bugs. This is done by translating Rust to a Verification Intermediate Language. Finally, we show that our extension to can be used to detect memory bugs in Rust such as null pointer dereferences, dangling pointer dereferences and use after frees.
Dataset: https://doi.org/10.4121/f0b3b808-51c3-4637-b6ff-3654506da71c ...
Dataset: https://doi.org/10.4121/f0b3b808-51c3-4637-b6ff-3654506da71c ...
Rust is a systems programming language that guarantees both performance and Memory Safety through its memory model. With unsafe rust it is possible to opt-out of some security guarantees made by the compiler. However, this comes at the risk of re-introducing memory bugs. While various tools already exist for detecting memory errors in (unsafe) Rust, they are either dynamic or focus on proving the absence of bugs. In this thesis we lay the foundations for a static analysis for Rust that focuses on proving the presence of bugs (Under Approximation) instead of their absence (Over Approximation). We show how we can use a formal framework called incorrectness separation logic (ISL) to show the presence of memory errors in Rust. We add Rust support to Infer, a static analysis tool by Meta that uses ISL to prove the presence of bugs. This is done by translating Rust to a Verification Intermediate Language. Finally, we show that our extension to can be used to detect memory bugs in Rust such as null pointer dereferences, dangling pointer dereferences and use after frees.
Dataset: https://doi.org/10.4121/f0b3b808-51c3-4637-b6ff-3654506da71c
Dataset: https://doi.org/10.4121/f0b3b808-51c3-4637-b6ff-3654506da71c
Program synthesis is the task of constructing a program that satisfies specified constraints. One popular formulation of program synthesis is example-based synthesis. Here, the synthesizer attempts to find a program in a specified domain that satisfies a set of input-output examples. Enumeration is the most common approach to finding the desired program. However, the exponentially growing search space makes this infeasible. The size of the domain can be largely attributed to its inefficient representation. Often, programs are only syntactically distinguished, meaning programs that behave the same are seen as different. We introduce Context-Sensitive E-Graph Saturation, a novel method that limits the search space to programs that solve at least one of the provided examples. This allows focusing only on programs that behave similarly to the desired one. Crucial is finding contextual equivalences for each example over a generated termset. These equivalences allow generating many solutions for each individual example. A program in the intersection of these programs solves all examples. In experiments on a subset from SyGus SLIA, our method solves the problems that enumeration solves, but not more. These results highlight a trade-off: with a small termset, the discovered equivalences are often too limited to capture the relationships needed to find a universal solution. Conversely, increasing the termset size quickly leads to inefficiency. To address this, we propose a strategy for constructing a more expressive yet small termset, enabling our method to solve a broader range of synthesis problems.
...
Program synthesis is the task of constructing a program that satisfies specified constraints. One popular formulation of program synthesis is example-based synthesis. Here, the synthesizer attempts to find a program in a specified domain that satisfies a set of input-output examples. Enumeration is the most common approach to finding the desired program. However, the exponentially growing search space makes this infeasible. The size of the domain can be largely attributed to its inefficient representation. Often, programs are only syntactically distinguished, meaning programs that behave the same are seen as different. We introduce Context-Sensitive E-Graph Saturation, a novel method that limits the search space to programs that solve at least one of the provided examples. This allows focusing only on programs that behave similarly to the desired one. Crucial is finding contextual equivalences for each example over a generated termset. These equivalences allow generating many solutions for each individual example. A program in the intersection of these programs solves all examples. In experiments on a subset from SyGus SLIA, our method solves the problems that enumeration solves, but not more. These results highlight a trade-off: with a small termset, the discovered equivalences are often too limited to capture the relationships needed to find a universal solution. Conversely, increasing the termset size quickly leads to inefficiency. To address this, we propose a strategy for constructing a more expressive yet small termset, enabling our method to solve a broader range of synthesis problems.
Memory access bugs exist in almost every compiled programming language. To solve this, modern programming languages like Rust use complex variable ownership systems that ensure memory safety. These kinds of ownership systems can be used to distinguish between variables that can only be read and ones that can be safely written to as well. These strict ownership rules are, however, limited when using external libraries. While the Foreign Function Interfaces (FFI) used to show what arguments external functions use can be written with these ownership requirements, enforcing them on the side of the external library is not required, potentially resulting in a discrepancy between what is expected on Rust's side and what happens in the external library.
To solve this problem we propose a novel mechanism for detecting memory safety violations across language boundaries. We implemented it in a tool called MiriPBT: a combination of MIRI, a tool that can enforce ownership rules at runtime, MiriLLI, an extension of MIRI that allows ownership rules to be enforced on the other side of the FFI boundary, and Property Based Testing, which allows us to greatly increase the size of the domain we can test. We use Rust's type system to generate inputs for the PBT and use the runtime checks of MIRI and MiriLLI to check if any ownership rules are violated. Finally we present the result of the PBT in a format an average Rust user can easily understand, helping them resolve any FFI related ownership bugs in their code. ...
To solve this problem we propose a novel mechanism for detecting memory safety violations across language boundaries. We implemented it in a tool called MiriPBT: a combination of MIRI, a tool that can enforce ownership rules at runtime, MiriLLI, an extension of MIRI that allows ownership rules to be enforced on the other side of the FFI boundary, and Property Based Testing, which allows us to greatly increase the size of the domain we can test. We use Rust's type system to generate inputs for the PBT and use the runtime checks of MIRI and MiriLLI to check if any ownership rules are violated. Finally we present the result of the PBT in a format an average Rust user can easily understand, helping them resolve any FFI related ownership bugs in their code. ...
Memory access bugs exist in almost every compiled programming language. To solve this, modern programming languages like Rust use complex variable ownership systems that ensure memory safety. These kinds of ownership systems can be used to distinguish between variables that can only be read and ones that can be safely written to as well. These strict ownership rules are, however, limited when using external libraries. While the Foreign Function Interfaces (FFI) used to show what arguments external functions use can be written with these ownership requirements, enforcing them on the side of the external library is not required, potentially resulting in a discrepancy between what is expected on Rust's side and what happens in the external library.
To solve this problem we propose a novel mechanism for detecting memory safety violations across language boundaries. We implemented it in a tool called MiriPBT: a combination of MIRI, a tool that can enforce ownership rules at runtime, MiriLLI, an extension of MIRI that allows ownership rules to be enforced on the other side of the FFI boundary, and Property Based Testing, which allows us to greatly increase the size of the domain we can test. We use Rust's type system to generate inputs for the PBT and use the runtime checks of MIRI and MiriLLI to check if any ownership rules are violated. Finally we present the result of the PBT in a format an average Rust user can easily understand, helping them resolve any FFI related ownership bugs in their code.
To solve this problem we propose a novel mechanism for detecting memory safety violations across language boundaries. We implemented it in a tool called MiriPBT: a combination of MIRI, a tool that can enforce ownership rules at runtime, MiriLLI, an extension of MIRI that allows ownership rules to be enforced on the other side of the FFI boundary, and Property Based Testing, which allows us to greatly increase the size of the domain we can test. We use Rust's type system to generate inputs for the PBT and use the runtime checks of MIRI and MiriLLI to check if any ownership rules are violated. Finally we present the result of the PBT in a format an average Rust user can easily understand, helping them resolve any FFI related ownership bugs in their code.
Property-Based Testing in Haskell
An Analysis of QuickCheck usage in Open-Source Haskell Projects
Property-Based Testing (PBT) with QuickCheck has become a cornerstone of reliable software development in Haskell, yet there is little systematic understanding of how developers employ it in production quality libraries. In this study, we perform an empirical analysis of QuickCheck usage in nine representative open-source Haskell projects (aeson, attoparsec, containers, hashable, lens, megaparsec, pandoc-type, text and vector). We extract thousands of
QuickCheck properties and manually sample 217 of them to classify property types such as invariants, roundtrip checks, algorithm correctness, and idempotence. We also analyze all extracted properties to identify patterns in generator and shrinking strategies. Our Results show that invariants and test-oracle tests dominate the sampled properties, while custom generators are used in 55.8% of all properties and custom shrinkers in only 25%. We discuss how these patterns vary across different domains (data structures, text processing, optics, hashing) and highlight the tension between default and custom test infrastructure. Finally, we reflect on the implications for tool support, education, and future research particularly automatic generator inference and improved shrinking utilities to lower
the barrier to effective PBT in large codebases. ...
QuickCheck properties and manually sample 217 of them to classify property types such as invariants, roundtrip checks, algorithm correctness, and idempotence. We also analyze all extracted properties to identify patterns in generator and shrinking strategies. Our Results show that invariants and test-oracle tests dominate the sampled properties, while custom generators are used in 55.8% of all properties and custom shrinkers in only 25%. We discuss how these patterns vary across different domains (data structures, text processing, optics, hashing) and highlight the tension between default and custom test infrastructure. Finally, we reflect on the implications for tool support, education, and future research particularly automatic generator inference and improved shrinking utilities to lower
the barrier to effective PBT in large codebases. ...
Property-Based Testing (PBT) with QuickCheck has become a cornerstone of reliable software development in Haskell, yet there is little systematic understanding of how developers employ it in production quality libraries. In this study, we perform an empirical analysis of QuickCheck usage in nine representative open-source Haskell projects (aeson, attoparsec, containers, hashable, lens, megaparsec, pandoc-type, text and vector). We extract thousands of
QuickCheck properties and manually sample 217 of them to classify property types such as invariants, roundtrip checks, algorithm correctness, and idempotence. We also analyze all extracted properties to identify patterns in generator and shrinking strategies. Our Results show that invariants and test-oracle tests dominate the sampled properties, while custom generators are used in 55.8% of all properties and custom shrinkers in only 25%. We discuss how these patterns vary across different domains (data structures, text processing, optics, hashing) and highlight the tension between default and custom test infrastructure. Finally, we reflect on the implications for tool support, education, and future research particularly automatic generator inference and improved shrinking utilities to lower
the barrier to effective PBT in large codebases.
QuickCheck properties and manually sample 217 of them to classify property types such as invariants, roundtrip checks, algorithm correctness, and idempotence. We also analyze all extracted properties to identify patterns in generator and shrinking strategies. Our Results show that invariants and test-oracle tests dominate the sampled properties, while custom generators are used in 55.8% of all properties and custom shrinkers in only 25%. We discuss how these patterns vary across different domains (data structures, text processing, optics, hashing) and highlight the tension between default and custom test infrastructure. Finally, we reflect on the implications for tool support, education, and future research particularly automatic generator inference and improved shrinking utilities to lower
the barrier to effective PBT in large codebases.
Property Based Testing in Rust, How is it Used?
A case study of the ‘quickcheck‘ crate used in open source repositories
Property-based testing (PBT) is a method of verifying software correctness in which a property, a statement about the behavior of the program which should always hold true, is verified with a large number of arbitrary inputs. While it is a powerful method, properties can be complex and fail on obscure inputs, making them difficult to reason about. We qualitatively analyze a large number of property-based tests (PBTs) written with Quickcheck for Rust from public repositories, in order to gather insights about how PBT is utilized in practice. We find that the majority of analyzed PBTs verify by comparing against a known correct implementation, composing inverse operations to form an identity, or asserting a desired contract about a system's state. These findings offer valuable direction to the development of PBT, aiming to tailor PBT frameworks to developer needs and make them more natural to work with.
...
Property-based testing (PBT) is a method of verifying software correctness in which a property, a statement about the behavior of the program which should always hold true, is verified with a large number of arbitrary inputs. While it is a powerful method, properties can be complex and fail on obscure inputs, making them difficult to reason about. We qualitatively analyze a large number of property-based tests (PBTs) written with Quickcheck for Rust from public repositories, in order to gather insights about how PBT is utilized in practice. We find that the majority of analyzed PBTs verify by comparing against a known correct implementation, composing inverse operations to form an identity, or asserting a desired contract about a system's state. These findings offer valuable direction to the development of PBT, aiming to tailor PBT frameworks to developer needs and make them more natural to work with.
Programming Language Tooling for Hylo
Incremental Compilation and Analysis
This paper presents a conceptual model for enabling incremental compilation in Hylo, a modern memory-safe systems programming language currently under development. Drawing from a comparative study of existing incremental compilation techniques, an in-depth analysis of Hylo's front-end architecture, and exploratory experiments, the model categorizes common types of program changes, introduces a scope-aware AST diffing algorithm, and proposes a lightweight dependency tracking mechanism tailored to Hylo's needs.
...
This paper presents a conceptual model for enabling incremental compilation in Hylo, a modern memory-safe systems programming language currently under development. Drawing from a comparative study of existing incremental compilation techniques, an in-depth analysis of Hylo's front-end architecture, and exploratory experiments, the model categorizes common types of program changes, introduces a scope-aware AST diffing algorithm, and proposes a lightweight dependency tracking mechanism tailored to Hylo's needs.
Exploring Property-Based Testing in Java
An Analysis of jqwik Usage in Open-Source Repositories
Property-based testing (PBT) verifies software correctness by checking that specific properties hold across a wide variety of randomly generated inputs. Despite its apparent usefulness, we lack an overview of how PBT is utilized in the Java ecosystem. In this study, we investigated seven repositories using the jqwik framework. We analyzed 84 PBTs to understand the types of properties developers typically test, their use of generators and shrinkers, and the role of PBT in broader testing strategies. Our findings show that PBT remains a small part of most test suites, often representing less than 2% of the total number of tests. Developers tend to focus on mutation, invariant, and round trip as the properties they test, frequently using custom generators combined with filtering but never implementing custom shrinkers. We conclude that property-based testing is not being utilized to its full potential in Java projects and highlight areas for future research, including the impact of filtering, the potential of custom shrinkers, and the overall effectiveness of property-based testing.
...
Property-based testing (PBT) verifies software correctness by checking that specific properties hold across a wide variety of randomly generated inputs. Despite its apparent usefulness, we lack an overview of how PBT is utilized in the Java ecosystem. In this study, we investigated seven repositories using the jqwik framework. We analyzed 84 PBTs to understand the types of properties developers typically test, their use of generators and shrinkers, and the role of PBT in broader testing strategies. Our findings show that PBT remains a small part of most test suites, often representing less than 2% of the total number of tests. Developers tend to focus on mutation, invariant, and round trip as the properties they test, frequently using custom generators combined with filtering but never implementing custom shrinkers. We conclude that property-based testing is not being utilized to its full potential in Java projects and highlight areas for future research, including the impact of filtering, the potential of custom shrinkers, and the overall effectiveness of property-based testing.
Property-Based Testing in Practice using Hypothesis
In-depth study on how developers use Property-Based Testing in Python using Hypothesis
Property-based testing (PBT) allows developers to specify high-level properties that should hold for a range of inputs, which are then automatically generated by the testing framework. Despite its theoretical appeal, PBT is not widely used in the real world. To better understand how PBT is used in practice, we present a qualitative and quantitative study of 87 property-based tests written with the Hypothesis framework in seven widely used Python projects, including cpython, pandas, and jax.
Our analysis reveals that while PBTs are relatively rare in these repositories, they are often simple in structure and highly effective at expressing functional properties. The most common patterns include round-trip checks and comparisons against test oracles, which account for a significant portion of the test suite. We also observed a high rate of custom generator usage (39.1%), but no use of custom shrinking, suggesting strong defaults in Hypothesis. The dataset was variable in stylistic and structural choices, ranging from single-assertion tests to complex hardware-dependent cases.
This study provides new insights into the practical use of PBT in Python, expands on prior quantitative work with qualitative findings, and identifies concrete implications for improving testing frameworks and educational resources. We conclude with recommendations for supporting broader adoption of PBT and outline directions for future research, including cross-language comparison, automated annotation, and temporal analysis of test evolution. ...
Our analysis reveals that while PBTs are relatively rare in these repositories, they are often simple in structure and highly effective at expressing functional properties. The most common patterns include round-trip checks and comparisons against test oracles, which account for a significant portion of the test suite. We also observed a high rate of custom generator usage (39.1%), but no use of custom shrinking, suggesting strong defaults in Hypothesis. The dataset was variable in stylistic and structural choices, ranging from single-assertion tests to complex hardware-dependent cases.
This study provides new insights into the practical use of PBT in Python, expands on prior quantitative work with qualitative findings, and identifies concrete implications for improving testing frameworks and educational resources. We conclude with recommendations for supporting broader adoption of PBT and outline directions for future research, including cross-language comparison, automated annotation, and temporal analysis of test evolution. ...
Property-based testing (PBT) allows developers to specify high-level properties that should hold for a range of inputs, which are then automatically generated by the testing framework. Despite its theoretical appeal, PBT is not widely used in the real world. To better understand how PBT is used in practice, we present a qualitative and quantitative study of 87 property-based tests written with the Hypothesis framework in seven widely used Python projects, including cpython, pandas, and jax.
Our analysis reveals that while PBTs are relatively rare in these repositories, they are often simple in structure and highly effective at expressing functional properties. The most common patterns include round-trip checks and comparisons against test oracles, which account for a significant portion of the test suite. We also observed a high rate of custom generator usage (39.1%), but no use of custom shrinking, suggesting strong defaults in Hypothesis. The dataset was variable in stylistic and structural choices, ranging from single-assertion tests to complex hardware-dependent cases.
This study provides new insights into the practical use of PBT in Python, expands on prior quantitative work with qualitative findings, and identifies concrete implications for improving testing frameworks and educational resources. We conclude with recommendations for supporting broader adoption of PBT and outline directions for future research, including cross-language comparison, automated annotation, and temporal analysis of test evolution.
Our analysis reveals that while PBTs are relatively rare in these repositories, they are often simple in structure and highly effective at expressing functional properties. The most common patterns include round-trip checks and comparisons against test oracles, which account for a significant portion of the test suite. We also observed a high rate of custom generator usage (39.1%), but no use of custom shrinking, suggesting strong defaults in Hypothesis. The dataset was variable in stylistic and structural choices, ranging from single-assertion tests to complex hardware-dependent cases.
This study provides new insights into the practical use of PBT in Python, expands on prior quantitative work with qualitative findings, and identifies concrete implications for improving testing frameworks and educational resources. We conclude with recommendations for supporting broader adoption of PBT and outline directions for future research, including cross-language comparison, automated annotation, and temporal analysis of test evolution.
Debugging Hylo
Providing Debugging Support to a Modern, Natively-Compiled Programming Language
Debugging is a fundamental part of software development, yet adding debugger support to new programming languages remains a complex and underexplored challenge. This report presents the design and implementation of source-level debugging for Hylo, a new systems programming language that emphasises generic programming and mutable value semantics. To achieve this, we extend the Hylo compiler to emit DWARF debug information, enabling seamless integration with the LLDB debugger. Our approach is incremental and guided by the behaviour of the Clang C++ compiler, allowing us to support Hylo core language features, such as variables, functions, user-defined types, and generics. We also identify and analyse key limitations, including challenges in representing Hylo's fine-grained variable lifetimes and projections, enabling evaluation of complex expressions in LLDB, and supporting Hylo's dynamic types (i.e., existentials). Beyond Hylo, this work aims to outline a general, reusable methodology for equipping new programming languages with modern debugging capabilities, improving their usability and adoption.
...
Debugging is a fundamental part of software development, yet adding debugger support to new programming languages remains a complex and underexplored challenge. This report presents the design and implementation of source-level debugging for Hylo, a new systems programming language that emphasises generic programming and mutable value semantics. To achieve this, we extend the Hylo compiler to emit DWARF debug information, enabling seamless integration with the LLDB debugger. Our approach is incremental and guided by the behaviour of the Clang C++ compiler, allowing us to support Hylo core language features, such as variables, functions, user-defined types, and generics. We also identify and analyse key limitations, including challenges in representing Hylo's fine-grained variable lifetimes and projections, enabling evaluation of complex expressions in LLDB, and supporting Hylo's dynamic types (i.e., existentials). Beyond Hylo, this work aims to outline a general, reusable methodology for equipping new programming languages with modern debugging capabilities, improving their usability and adoption.
High-Fidelity C Interoperability in Hylo
A Principled Design for Safe and Idiomatic C Bindings
Interoperability with C is critical for new systems languages, yet achieving a high-fidelity bridge requires navigating a complex space of trade-offs between usability, portability, and maintainability. Beyond mastering platform-specific ABIs and C dialects, a robust tool must decipher C's "semantic dialects"—programming conventions where syntax alone is insufficient to determine intent, such as an enum representing a set of mutually exclusive cases, a collection of combinable bitflags, or simply a group of named integer constants. These idioms defy rigid, one-size-fits-all translation.
This paper presents a principled technical design for a C interoperability layer for Hylo that addresses these challenges. We propose an architecture that leverages Clang for high-fidelity parsing and correct ABI handling, and a semantic mapping framework based on sensible defaults with developer-driven customization. This approach allows ambiguous C constructs to be mapped to the most appropriate and idiomatic Hylo representation, balancing automation with developer control. The result is a complete roadmap for a powerful and usable interoperability solution. ...
This paper presents a principled technical design for a C interoperability layer for Hylo that addresses these challenges. We propose an architecture that leverages Clang for high-fidelity parsing and correct ABI handling, and a semantic mapping framework based on sensible defaults with developer-driven customization. This approach allows ambiguous C constructs to be mapped to the most appropriate and idiomatic Hylo representation, balancing automation with developer control. The result is a complete roadmap for a powerful and usable interoperability solution. ...
Interoperability with C is critical for new systems languages, yet achieving a high-fidelity bridge requires navigating a complex space of trade-offs between usability, portability, and maintainability. Beyond mastering platform-specific ABIs and C dialects, a robust tool must decipher C's "semantic dialects"—programming conventions where syntax alone is insufficient to determine intent, such as an enum representing a set of mutually exclusive cases, a collection of combinable bitflags, or simply a group of named integer constants. These idioms defy rigid, one-size-fits-all translation.
This paper presents a principled technical design for a C interoperability layer for Hylo that addresses these challenges. We propose an architecture that leverages Clang for high-fidelity parsing and correct ABI handling, and a semantic mapping framework based on sensible defaults with developer-driven customization. This approach allows ambiguous C constructs to be mapped to the most appropriate and idiomatic Hylo representation, balancing automation with developer control. The result is a complete roadmap for a powerful and usable interoperability solution.
This paper presents a principled technical design for a C interoperability layer for Hylo that addresses these challenges. We propose an architecture that leverages Clang for high-fidelity parsing and correct ABI handling, and a semantic mapping framework based on sensible defaults with developer-driven customization. This approach allows ambiguous C constructs to be mapped to the most appropriate and idiomatic Hylo representation, balancing automation with developer control. The result is a complete roadmap for a powerful and usable interoperability solution.
The Statix meta-language is a domain-specific language that is used to describe specifications for type systems using high-level declarative inference rules. Type checkers
can be automatically generated from these rules, saving one from the burden of writing
it manually. One of the problems with these generated type checkers is performance;
handwritten type checkers usually outperform the generated ones. Statix uses the formalism of scope graphs to represent name binding, and querying these scope graphs is
known to be the main performance bottleneck. Improving the performance of queries
means improving the performance of the type checkers generated by Statix.
In this thesis, we propose a memoised variant of the current state-of-the-art query
resolution algorithm that memoises data encountered during graph traversal, reducing
future queries to a cache lookup. We also identify common patterns in real-world scope
graphs and link those to the name binding structure that created them. We construct a
synthetic dataset with these patterns that is used to evaluate query resolution algorithms
with microbenchmarks. This gives us more granular information on what name binding
structures benefit most, if at all, from memoisation.
The results of these benchmarks are the performance differences between the memoised algorithm and the current state-of-the-art algorithm per identified pattern. They
show that our proposed algorithm breaks even in terms of performance after only two
queries for most patterns. Furthermore, we demonstrate that our proposed algorithm
and the current state-of-the-art provide identical efficacy. The tradeoffs are twofold: the
cache increases the memory usage of query resolution significantly and the query resolution parameters were tweaked to make caching possible, but less versatile. The changed
query parameters’ limitations should only be theoretical however, the Statix specification
for Java 1.5 has 23 out of 25 fully compatible queries. ...
can be automatically generated from these rules, saving one from the burden of writing
it manually. One of the problems with these generated type checkers is performance;
handwritten type checkers usually outperform the generated ones. Statix uses the formalism of scope graphs to represent name binding, and querying these scope graphs is
known to be the main performance bottleneck. Improving the performance of queries
means improving the performance of the type checkers generated by Statix.
In this thesis, we propose a memoised variant of the current state-of-the-art query
resolution algorithm that memoises data encountered during graph traversal, reducing
future queries to a cache lookup. We also identify common patterns in real-world scope
graphs and link those to the name binding structure that created them. We construct a
synthetic dataset with these patterns that is used to evaluate query resolution algorithms
with microbenchmarks. This gives us more granular information on what name binding
structures benefit most, if at all, from memoisation.
The results of these benchmarks are the performance differences between the memoised algorithm and the current state-of-the-art algorithm per identified pattern. They
show that our proposed algorithm breaks even in terms of performance after only two
queries for most patterns. Furthermore, we demonstrate that our proposed algorithm
and the current state-of-the-art provide identical efficacy. The tradeoffs are twofold: the
cache increases the memory usage of query resolution significantly and the query resolution parameters were tweaked to make caching possible, but less versatile. The changed
query parameters’ limitations should only be theoretical however, the Statix specification
for Java 1.5 has 23 out of 25 fully compatible queries. ...
The Statix meta-language is a domain-specific language that is used to describe specifications for type systems using high-level declarative inference rules. Type checkers
can be automatically generated from these rules, saving one from the burden of writing
it manually. One of the problems with these generated type checkers is performance;
handwritten type checkers usually outperform the generated ones. Statix uses the formalism of scope graphs to represent name binding, and querying these scope graphs is
known to be the main performance bottleneck. Improving the performance of queries
means improving the performance of the type checkers generated by Statix.
In this thesis, we propose a memoised variant of the current state-of-the-art query
resolution algorithm that memoises data encountered during graph traversal, reducing
future queries to a cache lookup. We also identify common patterns in real-world scope
graphs and link those to the name binding structure that created them. We construct a
synthetic dataset with these patterns that is used to evaluate query resolution algorithms
with microbenchmarks. This gives us more granular information on what name binding
structures benefit most, if at all, from memoisation.
The results of these benchmarks are the performance differences between the memoised algorithm and the current state-of-the-art algorithm per identified pattern. They
show that our proposed algorithm breaks even in terms of performance after only two
queries for most patterns. Furthermore, we demonstrate that our proposed algorithm
and the current state-of-the-art provide identical efficacy. The tradeoffs are twofold: the
cache increases the memory usage of query resolution significantly and the query resolution parameters were tweaked to make caching possible, but less versatile. The changed
query parameters’ limitations should only be theoretical however, the Statix specification
for Java 1.5 has 23 out of 25 fully compatible queries.
can be automatically generated from these rules, saving one from the burden of writing
it manually. One of the problems with these generated type checkers is performance;
handwritten type checkers usually outperform the generated ones. Statix uses the formalism of scope graphs to represent name binding, and querying these scope graphs is
known to be the main performance bottleneck. Improving the performance of queries
means improving the performance of the type checkers generated by Statix.
In this thesis, we propose a memoised variant of the current state-of-the-art query
resolution algorithm that memoises data encountered during graph traversal, reducing
future queries to a cache lookup. We also identify common patterns in real-world scope
graphs and link those to the name binding structure that created them. We construct a
synthetic dataset with these patterns that is used to evaluate query resolution algorithms
with microbenchmarks. This gives us more granular information on what name binding
structures benefit most, if at all, from memoisation.
The results of these benchmarks are the performance differences between the memoised algorithm and the current state-of-the-art algorithm per identified pattern. They
show that our proposed algorithm breaks even in terms of performance after only two
queries for most patterns. Furthermore, we demonstrate that our proposed algorithm
and the current state-of-the-art provide identical efficacy. The tradeoffs are twofold: the
cache increases the memory usage of query resolution significantly and the query resolution parameters were tweaked to make caching possible, but less versatile. The changed
query parameters’ limitations should only be theoretical however, the Statix specification
for Java 1.5 has 23 out of 25 fully compatible queries.