-
The Fearless Journey [Draft]
Authors:
Nick Webster,
Marco Servetto,
Michael Homer
Abstract:
Existing minimal Object-Oriented models (OO), like Featherweight Java (FJ), are valuable for modelling programs and designing new programming languages and tools. However, their utility in develo** real-world programs is limited. We introduce the 'Fearless Heart', a novel object calculus preserving FJ's minimal and extensible nature while being more suited for constructing complex, real-world ap…
▽ More
Existing minimal Object-Oriented models (OO), like Featherweight Java (FJ), are valuable for modelling programs and designing new programming languages and tools. However, their utility in develo** real-world programs is limited. We introduce the 'Fearless Heart', a novel object calculus preserving FJ's minimal and extensible nature while being more suited for constructing complex, real-world applications.
To illustrate the extensibility of the Fearless Heart, we extend it with Reference Capabilities (RC), creating R-Fearless. It supports mutability and other side effects while retaining the reasoning advantages of functional programming and gaining support for features that are well-known to be enabled by RC, like automatic parallelism, caching and invariants. R-Fearless is still minimal enough to allow further extensions. It is an ideal foundation for constructing both practical systems and formal models.
△ Less
Submitted 12 May, 2024; v1 submitted 10 May, 2024;
originally announced May 2024.
-
CrashJS: A NodeJS Benchmark for Automated Crash Reproduction
Authors:
Philip Oliver,
Jens Dietrich,
Craig Anslow,
Michael Homer
Abstract:
Software bugs often lead to software crashes, which cost US companies upwards of $2.08 trillion annually. Automated Crash Reproduction (ACR) aims to generate unit tests that successfully reproduce a crash. The goal of ACR is to aid developers with debugging, providing them with another tool to locate where a bug is in a program. The main approach ACR currently takes is to replicate a stack trace f…
▽ More
Software bugs often lead to software crashes, which cost US companies upwards of $2.08 trillion annually. Automated Crash Reproduction (ACR) aims to generate unit tests that successfully reproduce a crash. The goal of ACR is to aid developers with debugging, providing them with another tool to locate where a bug is in a program. The main approach ACR currently takes is to replicate a stack trace from an error thrown within a program. Currently, ACR has been developed for C, Java, and Python, but there are no tools targeting JavaScript programs. To aid the development of JavaScript ACR tools, we propose CrashJS: a benchmark dataset of 453 Node.js crashes from several sources. CrashJS includes a mix of real-world and synthesised tests, multiple projects, and different levels of complexity for both crashes and target programs.
△ Less
Submitted 9 May, 2024;
originally announced May 2024.
-
Dala: A Simple Capability-Based Dynamic Language Design For Data Race-Freedom
Authors:
Kiko Fernandez-Reyes,
Isaac Oscar Gariano,
James Noble,
Erin Greenwood-Thessman,
Michael Homer,
Tobias Wrigstad
Abstract:
Dynamic languages like Erlang, Clojure, JavaScript, and E adopted data-race freedom by design. To enforce data-race freedom, these languages either deep copy objects during actor (thread) communication or proxy back to their owning thread. We present Dala, a simple programming model that ensures data-race freedom while supporting efficient inter-thread communication. Dala is a dynamic, concurrent,…
▽ More
Dynamic languages like Erlang, Clojure, JavaScript, and E adopted data-race freedom by design. To enforce data-race freedom, these languages either deep copy objects during actor (thread) communication or proxy back to their owning thread. We present Dala, a simple programming model that ensures data-race freedom while supporting efficient inter-thread communication. Dala is a dynamic, concurrent, capability-based language that relies on three core capabilities: immutable values can be shared freely; isolated mutable objects can be transferred between threads but not aliased; local objects can be aliased within their owning thread but not dereferenced by other threads. Objects with capabilities can co-exist with unsafe objects, that are unchecked and may suffer data races, without compromising the safety of safe objects. We present a formal model of Dala, prove data race-freedom and state and prove a dynamic gradual guarantee. These theorems guarantee data race-freedom when using safe capabilities and show that the addition of capabilities is semantics preserving modulo permission and cast errors.
△ Less
Submitted 15 September, 2021;
originally announced September 2021.
-
A Partial Reproduction of A Guided Genetic Algorithm for Automated Crash Reproduction
Authors:
Philip Oliver,
Michael Homer,
Jens Dietrich,
Craig Anslow
Abstract:
This paper is a partial reproduction of work by Soltani et al. which presented EvoCrash, a tool for replicating software failures in Java by reproducing stack traces. EvoCrash uses a guided genetic algorithm to generate JUnit test cases capable of reproducing failures more reliably than existing coverage-based solutions. In this paper, we present the findings of our reproduction of the initial stu…
▽ More
This paper is a partial reproduction of work by Soltani et al. which presented EvoCrash, a tool for replicating software failures in Java by reproducing stack traces. EvoCrash uses a guided genetic algorithm to generate JUnit test cases capable of reproducing failures more reliably than existing coverage-based solutions. In this paper, we present the findings of our reproduction of the initial study exploring the effectiveness of EvoCrash and comparison to three existing solutions: STAR, JCHARMING, and MuCrash. We further explored the capabilities of EvoCrash on different programs to check for selection bias. We found that we can reproduce the crashes covered by EvoCrash in the original study while reproducing two additional crashes not reported as reproduced. We also find that EvoCrash was unsuccessful in reproducing several crashes from the JCHARMING paper, which were excluded from the original study. Both EvoCrash and JCHARMING could reproduce 73\% of the crashes from the JCHARMING paper. We found that there was potentially some selection bias in the dataset for EvoCrash. We also found that some crashes had been reported as non-reproducible even when EvoCrash could reproduce them. We suggest this may be due to EvoCrash becoming stuck in a local optimum.
△ Less
Submitted 1 August, 2021; v1 submitted 25 July, 2021;
originally announced July 2021.
-
Which of My Transient Type Checks Are Not (Almost) Free?
Authors:
Isaac Oscar Gariano,
Richard Roberts,
Stefan Marr,
Michael Homer,
James Noble
Abstract:
One form of type checking used in gradually typed language is transient type checking: whenever an object 'flows' through code with a type annotation, the object is dynamically checked to ensure it has the methods required by the annotation. Just-in-time compilation and optimisation in virtual machines can eliminate much of the overhead of run-time transient type checks. Unfortunately this optimis…
▽ More
One form of type checking used in gradually typed language is transient type checking: whenever an object 'flows' through code with a type annotation, the object is dynamically checked to ensure it has the methods required by the annotation. Just-in-time compilation and optimisation in virtual machines can eliminate much of the overhead of run-time transient type checks. Unfortunately this optimisation is not uniform: some type checks will significantly decrease, or even increase, a program's performance.
In this paper, we refine the so called "Takikawa" protocol, and use it to identify which type annotations have the greatest effects on performance. In particular, we show how graphing the performance of such benchmarks when varying which type annotations are present in the source code can be used to discern potential patterns in performance. We demonstrate our approach by testing the Moth virtual machine: for many of the benchmarks where Moth's transient type checking impacts performance, we have been able to identify one or two specific type annotations that are the likely cause. Without these type annotations, the performance impact of transient type checking becomes negligible.
Using our technique programmers can optimise programs by removing expensive type checks, and VM engineers can identify new opportunities for compiler optimisation.
△ Less
Submitted 12 September, 2019;
originally announced September 2019.
-
Transient Typechecks are (Almost) Free
Authors:
Richard Roberts,
Stefan Marr,
Michael Homer,
James Noble
Abstract:
Transient gradual ty** imposes run-time type tests that typically cause a linear slowdown in programs' performance. This performance impact discourages the use of type annotations because adding types to a program makes the program slower. A virtual machine can employ standard just-in-time optimizations to reduce the overhead of transient checks to near zero. These optimizations can give gradual…
▽ More
Transient gradual ty** imposes run-time type tests that typically cause a linear slowdown in programs' performance. This performance impact discourages the use of type annotations because adding types to a program makes the program slower. A virtual machine can employ standard just-in-time optimizations to reduce the overhead of transient checks to near zero. These optimizations can give gradually-typed languages performance comparable to state-of-the-art dynamic languages, so programmers can add types to their code without affecting their programs' performance.
△ Less
Submitted 18 February, 2019; v1 submitted 2 July, 2018;
originally announced July 2018.
