Publications
147 results found
Drossopoulou S, Eisenbach S, 2022, Java is type safe -- probably, Departmental Technical Report: 96/8, Publisher: Department of Computing, Imperial College London
Amidst rocketing numbers of enthusiastic Java programmers and internet applet users, there is growing concern about the security of executing Java code produced by external, unknown sources. Rather than waiting to find out empirically what damage Java programs do, we aim to examine first the language and then the environment, looking for points of weakness. A proof of the soundness of the Java type system is a first, necessary step towards demonstrating which Java programs won't compromise computer security.We consider a type safe subset of Java describing primitive types, classes, inheritance, instance variables and methods, interfaces, shadowing, dynamic method binding, object creation, null and arrays. We argue that for this subset the type system is sound, by proving that program execution preserves the types, up to subclasses/subinterfaces.
Tasos A, Franco J, Drossopoulou S, et al., 2020, Reshape your layouts, not your programs: A safe language extension for better cache locality, Science of Computer Programming, Vol: 197, ISSN: 0167-6423
The vast divide between the speed of CPU and RAM means that effective use of CPU caches is often a prerequisite for high performance on modern architectures. Hence, developers need to consider how to place data in memory so as to exploit spatial locality and achieve high memory bandwidth. Such manual memory optimisations are common in unmanaged languages (e.g. C, C++), but they sacrifice readability, maintainability, memory safety, and object abstraction. In managed languages, such as Java and C#, where the runtime abstracts away the memory from the developer, such optimisations are almost impossible.We present a language extension called SHAPES, which aims to offer developers more fine-grained control over the placement of data, without sacrificing memory safety or object abstraction. In SHAPES, programmers group related objects into pools, and specify how objects are laid out in these pools. Classes and types are annotated by pool parameters, which allow placement aspects to be changed orthogonally to the code that operates on the objects in the pool. These design decisions disentangle business logic and memory concerns.We give a formal model of SHAPES, present its type and memory safety model, and present its translation to a low-level language. We argue why we expect this translation to be efficient in terms of runtime representation of objects and access to their fields. We argue that SHAPES can be incorporated into existing managed and unmanaged language runtimes and fit well with garbage collection.
Drossopoulou S, Noble J, MacKay J, et al., 2020, Holistic specifications for robust programs, International Conference on Fundamental Approaches to Software Engineering, Publisher: Springer Verlag, ISSN: 0302-9743
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, wherecomponents 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 \emph{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 possible external code. \emph{necessary} conditions, i.e, what are the conditions without which an effect will not happen. In this paper we propose the Chainmail specification language for writing {holistic specifications that focus on necessary conditions (as well as sufficient conditions). We give a formal semantics for \Chainmail, and discuss several examples. The core of \Chainmail has been mechanised in the Coq proof assistant.
Drossopoulou S, Noble J, Mackay J, et al., 2020, Holisitic specifications for robust programs - Coq model
A Coq formalism of the core of the Chainmail specification language, along with an underlying language, Loo.This Coq formalism has been developed as part of the associated paper: Holistic Specifications for Robust Programs (https://arxiv.org/abs/2002.08334), to be published at FASE 2020
Liétar P, Butler T, Clebsch S, et al., 2019, snmalloc: a message passing allocator, Proceedings of the 2019 ACM SIGPLAN International Symposium on Memory Management, Publisher: ACM, Pages: 122-135
snmalloc is an implementation of malloc aimed at work- loads 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 struc- ture 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.
Blessing S, Fernandez-Reyes K, Yang AM, et al., 2019, Run, Actor, Run Towards Cross-Actor Language Benchmarking, 9th ACM SIGPLAN International Workshop on Programming Based on Actors, Agents, and Decentralized Control (AGERE), Publisher: ASSOC COMPUTING MACHINERY, Pages: 41-50
- Author Web Link
- Cite
- Citations: 1
Vicente Franco JP, 2018, Orca: Ownership and Reference Count Collection for Actors
Orca is a novel garbage collection protocol for actor-based, object-oriented programming languages for multicore machines. It supports fully concurrent garbage collection, where an actor can trigger garbage collection at any time without synchronising with any other actor. It does so while supporting copy-less message passing and sharing of mutable state. By leveraging a type system’s guarantees of actor isolation, Orca can perform GC fully concurrently, without any form of barrier synchronisation in mutator threads, as commonly found in state-of-the-art concurrent collectors. Although Orca has been successfully implemented in Pony and in Encore, it had never been evaluated nor proven correct. Indeed, these are the two main contributions of this thesis. In this thesis, we model Orca and prove that it will never collect reachable objects (i.e., execution of programs managed by Orca will never result in dangling pointers) and that it will eventually deallocate all unreachable objects (i.e., execution of programs managed by Orca will never result in memory leaks). We model Orca in three steps: firstly, we define a set of requirements that must be ensured by the host language; secondly, assuming these requirements are in place, we model all the garbage collection related operations atomically; and thirdly, we extend our model to take into consideration that, in fact, in a fully concurrent system every instruction is interleaved with the execution of other operations. Moreover, we evaluate Orca’s performance by measuring scalability, footprint, responsiveness and its overhead in the execution of a program. We perform this evaluation in the context of Pony, the language with which Orca was co-designed, and compare it against the JVM, BEAM and Boehm-Demers-Weiser.
Tasos A, Franco J, Wrigstad T, et al., 2018, Extending SHAPES for SIMD architectures, Proceedings of the 13th Workshop on Implementation, Compilation, Optimization of Object-Oriented Languages, Programs and Systems, Publisher: ACM Press, Pages: 1-7
SIMD (Single Instruction, Multiple Data) instruction sets are ubiquitous on modern hardware, but rarely used in software projects. A major reason for this is that efficient SIMD code requires data to be laid out in memory in an unconventional manner, forcing developers to explicitly refactor their code and data structures in order to make use of SIMD.In previous work, we proposed SHAPES, an abstract layout specification for enabling memory optimisations for managed, object-oriented languages. In this paper, we explain how, by extending SHAPES with well-known constructs from the literature, which are not specific to SIMD, we can extend SHAPES to compile programs to use SIMD instructions.The resulting language (sketch) seems able to exploit SIMD capabilities without sacrificing ease of development.
Vicente Franco J, Clebsch S, Drossopoulou S, et al., 2018, Soundness of a concurrent collector for actors, 27th European Symposium on Programming (ESOP), Publisher: Springer, Pages: 885-911
ORCA is a fully concurrent garbage collection protocol foractor-based programs. Multiple actors may mutate the heap while thecollector is running without any dedicated synchronization. ORCA isapplicable to any actor language whose type system prevents data racesand which supports causal message delivery. We present a model ofORCA which is parametric to the host language and its type system. Wedescribe the interplay between the host language and the collector. Wegive eight invariants preserved by the protocol, and prove its soundnessand completeness.
Vicente Franco J, Clebsch S, Drossopoulou S, et al., 2018, Correctness of a concurrent object collector for actor languages, 27th European Symposium on Programming, Publisher: Springer
ORCAis a garbage collection protocol for actor-based pro-grams. Multiple actors may mutate the heap while the collector is run-ning without any dedicated synchronisation.ORCAis applicable to anyactor language whose type system prevents data races and which sup-ports causal message delivery. We present a model ofORCAwhich isparametric to the host language and its type system. We describe theinterplay between the host language and the collector. We give invariantspreserved byORCA, and prove its soundness and completeness.
Schrans F, Eisenbach S, Drossopoulou S, 2018, Writing safe smart contracts in flint, Pages: 218-219
Blockchain-based platforms such as Ethereum support the execution of versatile decentralized applications, known as smart contracts. These typically hold and transfer digital currency (e.g., Ether) to other parties on the platform. Contracts have been subject to numerous attacks, losing hundreds of millions of dollars (in Ether). We propose Flint, a new type-safe, capabilities-secure, contractoriented programming language specifically designed for writing robust smart contracts. To help programmers reason about access control of functions, Flint programmers use caller capabilities. To prevent vulnerabilities relating to the unintentional loss of currency, transfers of assets in Flint are performed through safe atomic operations, inspired by linear type theory.
Franco J, Clebsch S, Drossopoulou S, et al., 2018, Soundness of a concurrent collector for actors (extended version), Departmental Technical Report: 18/1, Publisher: Department of Computing, Imperial College London
ORCA is a garbage collection protocol for actor-based programs.Multiple actors may mutate the heap while the collector is runningwithout any dedicated synchronisation. ORCA is applicable to anyactor language whose type system prevents data races and which supportscausal message delivery. We present a model of ORCA which isparametric to the host language and its type system. We describe theinterplay between the host language and the collector. We give invariantspreserved by ORCA, and prove its soundness and completeness.
Franco J, Hagelin M, Wrigstad T, et al., 2017, You can have it all: Abstraction and good cache performance, 2017 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, co-located with SPLASH 2017, Publisher: ACM, Pages: 148-167
On current architectures, the optimisation of an application's performance often involves data being stored according to access affinity - what is accessed together should be stored together, rather than logical affinity - what belongs together logically stays together. Such low level techniques lead to faster, but more error prone code, and end up tangling the program's logic with low-level data layout details. Our vision, which we call SHAPES - Safe, High-level, Abstractions for oPtimisation of mEmory cacheS - is that the layout of a data structure should be defined only once, upon instantiation, and the remainder of the code should be layout agnostic. This enables performance improvements while also guaranteeing memory safety, and supports the separation of program logic from low level concerns. In this paper we investigate how this vision can be supported by extending a programming language. We describe the core language features supporting this vision: classes can be customized to support different layouts, and layout information is carried around in types; the remaining source code is layout-unaware and the compiler emits layout-aware code. We then discuss our SHAPES implementation through a prototype library, which we also used for preliminary evaluations. Finally, we discuss how the core could be expanded so as to deliver SHAPES's full potential: the incorporation of compacting garbage collection, ad hoc polymorphism and late binding, synchronization of representations of different collections, support for dynamic change of representation, etc.
Clebsch S, Franco J, Drossopoulou S, et al., 2017, Orca: GC and type system co-design for actor languages, OOPSLA 2017, Publisher: Association for Computing Machinery, Pages: 72:1-72:28, ISSN: 2475-1421
ORCA is a concurrent and parallel garbage collector for actor programs,which does not require any stop-the-world steps, or synchronisationmechanisms, and which has been designed to support zero-copy message passing and sharing of mutable data. \ORCA is part of the runtime of the actor-based language Pony. Pony's runtime was co-designed with the Pony language. This co-design allowed us to exploit certain language properties in order to optimise performance of garbage collection. Namely, ORCA relies on the absence of race conditions in order to avoid read/write barriers, and itleverages actor message passing for synchronisation among actors. Thispaper describes Pony, its type system, and the ORCA garbage collection algorithm.An evaluation of the performance of ORCA suggests that it is fast and scalable for idiomatic workloads.
Wood T, Drossopoulou S, Lahiri SK, et al., 2017, Modular verification of procedure equivalence in the presence of memory allocation, European Symposium on Programming, Publisher: Springer Verlag, ISSN: 0302-9743
For most high level languages, two procedures are equivalentif they transform a pair of isomorphic stores to isomorphic stores. How-ever, tools for modular checking of such equivalence impose a strongercheck where isomorphism is strengthened to equality of stores. This re-sults in the inability to prove many interesting program pairs with re-cursion and dynamic memory allocation.In this work, we present RIE, a methodology to modularly establishequivalence of procedures in the presence of memory allocation, cyclicdata structures and recursion. Our technique addresses the need for find-ing witnesses to isomorphism with angelic allocation, supports reasoningabout equivalent procedures calls when the stores are only locally iso-morphic, and reasoning about changes in the order of procedure calls.We have implemented RIE by encoding it in the Boogie program verifier.We describe the encoding and prove its soundness.
Blessing S, Clebsch S, Drossopoulou S, 2017, Tree Topologies for Causal Message Delivery, 7th ACM SIGPLAN International Workshop on Programming Based on Actors, Agents, and Decentralized Control (AGERE), Publisher: ASSOC COMPUTING MACHINERY, Pages: 1-10
- Author Web Link
- Cite
- Citations: 4
Drossopoulou S, Noble J, Miller MS, et al., 2016, Permission and authority revisited towards a formalisation
Miller's notions of permissions and authority are foundational to the analysis of object-capability programming. Informal definitions of these concepts were given in Miller's thesis. In this paper we propose precise definitions for permissions and authority, based on a small object-oriented calculus. We quantify their bounds (current, eventual, behavioural, topological), and delineate the relationships between these definitions.
Certezeanu R, Drossopoulou S, Egelund-Muller B, et al., 2016, Quicksort Revisited: Verifying Alternative Versions of Quicksort, Theory and Practice of Formal Methods: Essays Dedicated to Frank de Boeron the Occasion of His 60th Birthday, Publisher: Springer International Publishing, Pages: 407-426, ISBN: 9783319307336
We verify the correctness of a recursive version of Tony Hoare’s quicksort algorithm using the Hoare-logic based verification tool Dafny. We then develop a non-standard, iterative version which is based on a stack of pivot-locations rather than the standard stack of ranges. We outline an incomplete Dafny proof for the latter.
Franco J, Drossopoulou S, 2016, Behavioural types for non-uniform memory accesses, 8th International Workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software (PLACES), Publisher: OPEN PUBL ASSOC, Pages: 109-120, ISSN: 2075-2180
- Author Web Link
- Cite
- Citations: 5
Clebsch S, Drossopoulou S, Blessing S, et al., 2015, Deny capabilities for safe, fast actors, Pages: 1-12
Combining the actor-model with shared memory for performance is efficient but can introduce data-races. Existing approaches to static data-race freedom are based on uniqueness and immutability, but lack flexibility and high performance implementations. Our approach, based on deny properties, allows reading, writing and traversing unique references, introduces a new form of write uniqueness, and guarantees atomic behaviours.
Drossopoulou S, Noble J, Miller MS, 2015, Swapsies on the internet: First steps towards reasoning about risk and trust in an open world, Pages: 2-15
Contemporary open systems use components developed by many different parties, linked together dynamically in unforeseen constellations. Code needs to live up to strict security specifications: it has to ensure the correct functioning of its objects when they collaborate with external objects which may be malicious. In this paper we propose specifications that model risk and trust in such open systems. We specify Miller, Van Cutsem, and Tulloh's escrow exchange example, and discuss the meaning of such a specification. We argue informally that the code satisfies its specification.
Drossopoulou S, Noble J, 2014, How to Break the Bank -- Semantics of Capability Policies, Integrated Formal Methods, ISSN: 0302-9743
Boer F, Einar Broch J, Clarke D, et al., 2014, Scaling Future Software: The Manycore Challenge, ERCIM News, Vol: 2014
Franco J, Drossopoulou S, Yoshida N, 2014, Calculating communication costs with Sessions Types and Sizes, Pages: 50-57, ISSN: 2190-6807
We present a small object-oriented language with communication primitives. The language allows the assignment of binary session types to communication channels in order to govern the interaction between different objects and to statically calculate communication costs. Class declarations are annotated with size information in order to determine the cost of sending and receiving objects. This paper describes our first steps in the creation of a session-based, object-oriented language for communication optimization purposes.
Drossopoulou S, Noble J, 2014, Rationally reconstructing the Escrow Example, Formal Techniques for Java Programs, Publisher: ACM
Drossopoulou S, Noble J, 2014, How to Break the Bank: Semantics of Capability Policies, 11th International Conference on Integrated Formal Methods (IFM), Publisher: SPRINGER INTERNATIONAL PUBLISHING AG, Pages: 18-35, ISSN: 0302-9743
- Author Web Link
- Cite
- Citations: 1
Drossopoulou S, Noble J, 2013, The need for capability policies position paper
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. In this position paper, we argue that current specification methodologies cannot adequately capture all aspects of the capability policies required to support object-capability systems. We outline informally the features that such security policies should support, and we demonstrate (also informally) how we can reason that examples satisfy the capability policies.
Clebsch S, Drossopoulou S, 2013, Fully Concurrent Garbage Collection of Actors on Many-Core Machines, ACM SIGPLAN NOTICES, Vol: 48, Pages: 553-570, ISSN: 0362-1340
- Author Web Link
- Cite
- Citations: 9
Drossopoulou S, Clebsch S, 2013, Fully Concurrent garbage Collection for Actors in Many-Core Mashines, OOPSLA
Cameron N, Drossopoulou S, 2013, Understanding Ownership Types with Dependent Types, Aliasing in Object-Oriented Programming, Editors: Clarke, Noble, Wrigstad
This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.