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.
Multi-methods are a straightforward extension of traditional (single) dynamic dispatch, which is the core of most object oriented languages. With multi-methods, a method call will select an appropriate implementation based on the values of multiple a
rguments, and not just the first/receiver. Language support for both single and multiple dispatch is typically designed to be used in conjunction with other object oriented features, in particular classes and inheritance. But are these extra features really necessary? M{mu}l is a dynamic language designed to be as simple as possible but still supporting flexible abstraction and polymorphism. M{mu}l provides only two forms of abstraction: (object) identities and (multi) methods. In M{mu}l method calls are dispatched based on the identity of arguments, as well as what other methods are defined on them. In order to keep M{mu}ls design simple, when multiple method definitions are applicable, the most recently defined one is chosen, not the most specific (as is conventional with dynamic dispatch). In this paper we show how by defining methods at runtime, we obtain much of the power of classes and meta object protocols, in particular the ability to dynamically modify the state and behaviour of classes of objects.
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-ti
me 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 programs 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 Moths 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.
Concurrent and parallel programming is difficult due to the presence of memory side-effects, which may introduce data races. Type qualifiers, such as reference capabilities, can remove data races by restricting sharing of mutable data. Unfortunately,
reference capability languages are an all-in or nothing game, i.e., all the types must be annotated with reference capabilities. In this work in progress, we propose to mix the ideas from the reference capability literature with gradual typing, leading to gradual reference capabilities.
Effect systems are used to statically reason about the effects an expression may have when evaluated. In the literature, such effects include various behaviours as diverse as memory accesses and exception throwing. Here we present CallE, an object-or
iented language that takes a flexible approach where effects are just method calls: this works well because ordinary methods often model things like I/O operations, access to global state, or primitive language operations such as thread creation. CallE supports both flexible and fine-grained control over such behaviour, in a way designed to minimise the complexity of annotations. CallEs effect system can be used to prevent OO code from performing privileged operations, such as querying a database, modifying GUI widgets, exiting the program, or performing network communication. It can also be used to ensure determinism, by preventing methods from (indirectly) calling non-deterministic primitives like random number generation or file reading.
In this paper we use pre existing language support for type modifiers and object capabilities to enable a system for sound runtime verification of invariants. Our system guarantees that class invariants hold for all objects involved in execution. Inv
ariants are specified simply as methods whose execution is statically guaranteed to be deterministic and not access any externally mutable state. We automatically call such invariant methods only when objects are created or the state they refer to may have been mutated. Our design restricts the range of expressible invariants but improves upon the usability and performance of our system compared to prior work. In addition, we soundly support mutation, dynamic dispatch, exceptions, and non determinism, while requiring only a modest amount of annotation. We present a case study showing that our system requires a lower annotation burden compared to Spec#, and performs orders of magnitude less runtime invariant checks compared to the widely used `visible state semantics protocols of D, Eiffel. We also formalise our approach and prove that such pre existing type modifier and object capability support is sufficient to ensure its soundness.
Static verification relying on an automated theorem prover can be very slow and brittle: since static verification is undecidable, correct code may not pass a particular static verifier. In this work we use metaprogramming to generate code that is co
rrect by construction. A theorem prover is used only to verify initial traits: units of code that can be used to compose bigger programs. In our work, meta-programming is done by trait composition, which starting from correct code, is guaranteed to produce correct code. We do this by extending conventional traits with pre- and post-conditions for the methods; we also extend the traditional trait composition (+) operator to check the compatibility of contracts. In this way, there is no need to re-verify the produced code. We show how our approach can be applied to the standard power function example, where metaprogramming generates optimised, and correc
