Behaviour-oriented concurrency (BoC) is a recently established programming model in which programmers define concurrent operations that execute atomically across multiple isolated resources. This allows for expressive interactions but introduces complex causal dependencies determined by dynamic resource overlap. Previous work defines the causal guarantees of BoC operationally, but mixes intended design constraints with incidental implementation details, leading to unintended causal orders. BoC is now being implemented across multiple languages and runtimes, all relying on the operational descriptions of causality. This paper develops an axiomatic model of BoC executions that makes the intrinsic orders explicit and derives the intended causal relation from their interaction. Using a set of representative programs and candidate executions, we motivate the design of this causal relation. We then prove that a representative minimal core calculus for BoC is sound with respect to this axiomatic model. Together, these results provide an implementation-independent foundation for reasoning about BoC causality across runtimes, schedulers and optimisation decisions.

In today’s complex software, internal trusted code is tightly intertwined with external untrusted code. To reason about internal code, programmers must reason about the potential effects of calls to external code, even though that code is not trusted and may not even be available. The effects of external calls can be limited if internal code is programmed defensively, limiting potential effects by limiting access to the capabilities necessary to cause those effects. This paper addresses the specification and verification of internal code that relies on encapsulation and object capabilities to limit the effects of external calls. We propose new assertions for access to capabilities, new specifications for limiting effects, and a Hoare logic to verify that a module satisfies its specification, even while making external calls. We illustrate the approach though a running example with mechanised proofs, and prove soundness of the Hoare logic.

Verona is a concurrent object-oriented programming language that organises all the objects in a program into a forest of isolated regions. Memory is managed locally for each region, so programmers can control a program's memory use by adjusting objects' partition into regions, and by setting each region's memory management strategy. A thread can only mutate (allocate, deallocate) objects within one active region---its "window of mutability". Memory management costs are localised to the active region, ensuring overheads can be predicted and controlled. Moving the mutability window between regions is explicit, so code can be executed wherever it is required, yet programs remain in control of memory use. An ownership type system based on reference capabilities enforces region isolation, controlling aliasing within and between regions, yet supporting objects moving between regions and threads. Data accesses never need expensive atomic operations, and are always thread-safe.

Expressing parallelism and coordination is central for modern concurrent programming. Many mechanisms exist for expressing both parallelism and coordination. However, the design decisions for these two mechanisms are tightly intertwined. We believe that the interdependence of these two mechanisms should be recognised and achieved through a single, powerful primitive. We are not the first to realise this: the prime example is actor model programming, where parallelism arises through fine-grained decomposition of a program’s state into actors that are able to execute independently in parallel. However, actor model programming has a serious pain point: updating multiple actors as a single atomic operation is a challenging task. We address this pain point by introducing a new concurrency paradigm: Behaviour-Oriented Concurrency (BoC). In BoC, we are revisiting the fundamental concept of a behaviour to provide a more transactional concurrency model. BoC enables asynchronously creating atomic and ordered units of work with exclusive access to a collection of independent resources. In this paper, we describe BoC informally in terms of examples, which demonstrate the advantages of exclusive access to several independent resources, as well as the need for ordering. We define it through a formal model. We demonstrate its practicality by implementing a C++ runtime. We argue its applicability through the Savina benchmark suite: benchmarks in this suite can be more compactly represented using BoC in place of Actors, and we observe comparable, if not better, performance.

Robust modules guarantee to do only what they are supposed to do – even in the presence of untrusted malicious clients, and considering not just the direct behaviour of individual methods, but also the emergent behaviour from calls to more than one method. Necessity is a language for specifying robustness, based on novel necessity operators capturing temporal implication, and a proof logic that derives explicit robustness specifications from functional specifications. Soundness and an exemplar proof are mechanised in Coq.

A cyber–cyber digital twin is a simulation of a software system. By contrast, a cyber–physical digital twin is a simulation of a non-software (physical) system. Although cyber–physical digital twins have received a lot of recent attention, their cyber–cyber counterparts have been comparatively overlooked. In this paper we show how the unique properties of cyber–cyber digital twins open up exciting opportunities for research and development. Like all digital twins, the cyber–cyber digital twin is both informed by and informs the behaviour of the twin it simulates. It is therefore a software system that simulates another software system, making it conceptually truly a twin, blurring the distinction between the simulated and the simulator. Cyber–cyber digital twins can be twins of other cyber–cyber digital twins, leading to a hierarchy of twins. As we shall see, these apparently philosophical observations have practical ramifications for the design, implementation and deployment of digital twins at Facebook.

The vast gap between CPU and RAM speed means that on modern architectures, developers need to carefully consider data placement in memory to exploit spatial and temporal cache locality and use CPU caches effectively. To that extent, developers have devised various strategies regarding data placement; for objects that should be close in memory, a contiguous pool of objects is allocated and then new instances are constructed inside it; an array of objects is clustered into multiple arrays, each holding the values of a specific field of the objects. Such data placements, however, have to be performed manually, hence readability, maintainability, memory safety, and key OO concepts such as encapsulation and object identity need to be sacrificed and the business logic needs to be modified accordingly. We propose a language extension, SHAPES, which aims to offer developers high-level fine-grained control over data placement, whilst retaining memory safety and the look-and-feel of OO. SHAPES extends an OO language with the concepts of pools and layouts: Developers declare pools that contain objects of a specific type and specify the pool’s layout. A layout specifies how objects in a pool are laid out in memory. That is, it dictates how the values of the fields of the pool’s objects are grouped together into clusters. Objects stored in pools behave identically to ordinary, standalone objects; the type system allows the code to be oblivious to the layout being used. This means that the business logic is completely decoupled from any placement concerns and the developer need not deviate from the spirit of OO to better utilise the cache. In this paper, we present the features of SHAPES, as well as the design rationale behind each feature. We then showcase the merit of SHAPES through a sequence of case studies; we claim that, compared to the manual pooling and clustering of objects, we can observe improvement in readability and maintainability, and comparable (i.e., on par or better) performance. We also present SHAPES^h, an OO calculus which models the SHAPES ideas, we formalise the type system, and prove soundness. The SHAPES^h type system uses ideas from Ownership Types [Clarke et al., 2013] and Java Generics [Gosling et al., 2014]: In SHAPES^h, pools are part of the types; SHAPES^h class and type definitions are enriched with pool parameters. Moreover, class pool parameters are enriched with bounds, which is what allows the business logic of SHAPES to be oblivious to the layout being used. SHAPES^h types also enforce pool uniformity and homogeneity. A pool is uniform if it contains objects of the same class only; a pool is homogeneous if the corresponding fields of all its objects point to objects in the same pool. These properties allow for more efficient implementation. For performance considerations, we also designed SHAPES^l, an untyped, unsafe low-level language with no explicit support for objects or pools. We argue that it is possible to translate SHAPES^l into existing low-level intermediate representations, such as LLVM [Lattner and Adve, 2004], present the translation of SHAPES^h into SHAPES^l, and show its soundness. Thus, we expect SHAPES to offer developers more fine-grained control over data placement, without sacrificing memory safety or the OO look-and-feel.

Functional specifications describe what program components can do: the sufficient conditions to invoke components’ operations. They allow us to reason about the use of components in a closed world setting, where components interact with known client code, and where the client code must establish the appropriate pre-conditions before calling into a component. Sufficient conditions are not enough to reason about the use of components in an open world setting, where components interact with external code, possibly of unknown provenance, and where components may evolve over time. In this open world setting, we must also consider the necessary conditions, i. e. what are the conditions without which an effect will not happen. In this paper we propose the $${\mathcal {C}}$$ hainmail specification language for writing holistic specifications that focus on necessary conditions (as well as sufficient conditions). We give a formal semantics for $${\mathcal {C}}$$ hainmail, and discuss several examples. The core of $${\mathcal {C}}$$ hainmail has been mechanised in the Coq proof assistant.

snmalloc is an implementation of malloc aimed at workloads in which objects are typically deallocated by a different thread than the one that had allocated them. We use the term producer/consumer for such workloads. snmalloc uses a novel message passing scheme which returns deallocated objects to the originating allocator in batches without taking any locks. It also uses a novel bump pointer-free list data structure with which just 64-bits of meta-data are sufficient for each 64 KiB slab. On such producer/consumer benchmarks our approach performs better than existing allocators. Snmalloc is available at https://github.com/Microsoft/snmalloc.

ORCA is a garbage collection protocol for actor-based programs. Multiple actors may mutate the heap while the collector is running without any dedicated synchronisation. ORCA is applicable to any actor language whose type system prevents data races and which supports causal message delivery. We present a model of ORCA which is parametric to the host language and its type system. We describe the interplay between the host language and the collector. We give invariants preserved by ORCA , and prove its soundness and completeness.

ORCA is a concurrent and parallel garbage collector for actor programs, which does not require any STW steps, or synchronization mechanisms, and that has been designed to support zero-copy message passing and sharing of mutable data. ORCA is part of a runtime for actor-based languages, which was co-designed with the Pony programming language, and in particular, with its data race free type system. By co-designing an actor language with its runtime, it was possible to exploit certain language properties in order to optimize performance of garbage collection. Namely, ORCA relies on the guarantees of absence of race conditions in order to avoid read/write barriers, and it leverages the actor message passing, for synchronization among actors. In this paper we briefly describe Pony and its type system. We use pseudo-code in order to introduce how ORCA allocates and deallocates objects, how it shares mutable data without requiring barriers upon data mutation, and how can immutability be used to further optimize garbage collection. Moreover, we discuss the advantages of co-designing an actor language with its runtime, and we demonstrate that ORCA can be implemented in a performant and scalable way through a set of micro-benchmarks, including a comparison with other well-known collectors.

The Escrow Exchange Contract has been used as a case study of building up complex and trustworthy systems from basic object capabilities, in the context of concurrent and distributed programming. In this short paper we present a Rational Reconstruction of the Escrow Exchange Contract case study, expressed in Grace, concentrating on the most essential issues of trustworthiness, and ignoring issues to do with distribution or more complex protocols. We then use our notation for capability policies to specify the key features of the reconstructed case study.

The object-capability model is one of the industry standards adopted for the implementation of security policies for web-based software. Object-capabilities in various forms are supported by programming languages such as E, Joe-E, Newspeak, Grace, and the newer versions of Javascript. Unfortunately, code written using capabilities tends to concentrate on the low-level mechanism rather than the high-level policy.

Disposal of dead actors in actor-model languages is as important as disposal of unreachable objects in object-oriented languages. In current practice, programmers are required to either manually terminate actors, or they have to rely on garbage collection systems that monitor actor mutation through write barriers, thread coordination through locks etc. These techniques, however, prevent the collector from being fully concurrent.

Chalice is a verification tool for object-based concurrent programs. It supports verification of functional properties of the programs as well as providing a deadlock prevention mechanism. It is built on Implicit Dynamic Frames, fractional permissions and permission transfer.

The definitive version can be found at : http://onlinelibrary.wiley.com/ Copyright Wiley [Full text of this article is not available in the UHRA]

Ownership is a powerful concept to structure the object store and to control aliasing and modifications of objects. This article presents an ownership type system for a Java-like programming language with generic types. Like our earlier Universe type system, Generic Universe Types structure the heap hierarchically. In contrast to earlier work, we separate the enforcement of an ownership topology from an encapsulation system. The topological system uses an existential modifier to express that no ownership information is available statically. On top of the topological system, we build an encapsulation system that enforces the owner-as-modifier discipline. This discipline does not restrict aliasing, but requires modifications of an object to be initiated by its owner. This allows owner objects to control state changes of owned objects—for instance, to maintain invariants. Separating the topological system from the encapsulation system allows for a cleaner formalization, separation of concerns, and simpler reuse of the individual systems in different contexts.

Wildcard types enrich the types expressible in Java, and extend the set of typeable Java programs. Syntactic models and proofs of soundness for type systems related to Java wildcards have been suggested in the past, however, the semantics of wildcards has not yet been studied.

Wildcards are an often confusing part of the Java type system: the behaviour of wildcard types is not fully specified by subtyping, due to wildcard capture, and the rules for type checking are often misunderstood. Their very formulation seems somehow 'different' from the rest of the Java type system, which is based on a simple, nominal hierarchy.

Existing ownership type systems require objects to have precisely one primary owner, organizing the heap into an ownership tree. Unfortunately, a tree structure is too restrictive for many programs, and prevents many common design patterns where multiple objects interact.

We present a translation from Fickle , a small object-oriented language allowing objects to change their class at runtime, into Java. The translation is provenly correct in the sense that it preserves the static and dynamic semantics. Moreover, it is compatible with separate compilation, since the translation of a Fickle class does not depend on the implementation of used classes. Based on the formal system, we have developed an implementation. The translation turned out to be a more subtle problem than we expected. In this article, we discuss four possible approaches we considered for the design of the translation and to justify our choice, we present formally the translation and proof of preservation of the static and dynamic semantics, and discuss the prototype implementation. Moreover, we outline an alternative translation based on generics that avoids most of the casts (but not all) needed in the previous translation. The language Fickle has undergone and is still undergoing several phases of development. In this article we are discussing the translation of Fickle II .

We define compositional compilation as the ability to typecheck source code fragments in isolation, generate We define compositional compilation as the ability to typecheck source code fragments in isolation, generate corresponding binaries,and link together fragments whose mutual assumptions are satisfied, without reinspecting the code. Even though compositional compilation is a highly desirable feature, in Java-like languages it can hardly be achieved. This is due to the fact that the bytecode generated for a fragment (say, a class) is not uniquely determined by its source code, but also depends on the compilation context.We propose a way to obtain compositional compilation for Java, by introducing a polymorphic form of bytecode containing type variables (ranging over class names) and equipped with a set of constraints involving type variables. Thus, polymorphic bytecode provides a representation for all the (standard) bytecode that can be obtained by replacing type variables with classes satisfying the associated constraints.We illustrate our proposal by developing a typing and a linking algorithm. The typing algorithm compiles a class in isolation generating the corresponding polymorphic bytecode fragment and constraints on the classes it depends on. The linking algorithm takes a collection of polymorphic bytecode fragments, checks their mutual consistency, and possibly simplifies and specializes them. In particular, linking a self-contained collection of fragments either fails, or produces standard bytecode (the same as would have been produced by standard compilation of all fragments).

Ownership types provide a statically enforceable notion of object-level encapsulation. We extend ownership types with computational effects to support reasoning about object-oriented programs. The ensuing system provides both access control and effects reporting. Based on this type system, we codify two formal systems for reasoning about aliasing and the disjointness of computational effects. The first can be used to prove that evaluation of two expressions will never lead to aliases, while the latter can be used to show the non-interference of two expressions.

Reclassification changes the class membership of an object at run-time while retaining its identity. We suggest language features for object reclassification, which extend an imperative, typed, class-based, object-oriented language.We present our proposal through the language Fickle ⋄⋄ . The imperative features, combined with the requirement for a static and safe type system, provided the main challenges. We develop a type and effect system for Fickle ⋄⋄ and prove its soundness with respect to the operational semantics. In particular, even though objects may be reclassified across classes with different members, there will never be an attempt to access nonexisting members.

We propose a calculus describing compilation and linking in terms of operations on fragments, i.e. compilation units, without reference to their specific contents. We believe this calculus faithfully reflects the situation within modern programming systems. Binary compatibility in Java prescribes conditions under which modification of fragments does not necessitate recompilation of importing fragments. We apply our calculus to formalize binary compatibility, and demonstrate that several interpretations of the language specification are possible, each with different ramifications. We choose a particular interpretation, justify our choice, formulate and prove properties important for language designers and code library developers.

Separate compilation allows the decomposition of programs into units that may be compiled separately, and linked into an executable. Traditionally, separate compilation was equivalent to the compilation of all units together, and modification and re-compilation of one unit required re-compilation of all importing units.Java suggests a more flexible framework, in which the linker checks the integrity of the binaries to be combined. Certain source code modifications, such as addition of methods to classes, are defined as binary compatible. The language description guarantees that binaries of types (i.e. classes or interfaces) modified in binary compatible ways may be re-compiled and linked with the binaries of types that imported and were compiled using the earlier versions of the modified types.However, this is not always the case: some of the changes considered by Java as binary compatible do not guarantee successful linking and execution. In this paper we study the concepts around binary compatibility. We suggest a formalization of the requirement of safe linking and execution without re-compilation, investigate alternatives, demonstrate several of its properties, and propose a more restricted definition of binary compatible changes. Finally, we prove for a substantial subset of Java, that this restricted definition guarantees error-free linking and execution.

This paper describes the integrated engineering study scheme, based around a set of 4 year MEng programmes of study, established by Imperial College. The paper outlines the rationale for the scheme and gives an account of its constituent programmes of study and the curriculum. The organisation and pattern of teaching, student workload and assessment methods are discussed. A detailed comparison of the scheme with the proposals and recommendations of the important model curricula are given.