Imperial College London

ProfessorSophiaDrossopoulou

Faculty of EngineeringDepartment of Computing

Professor of Programming Languages
 
 
 
//

Contact

 

+44 (0)20 7594 8368s.drossopoulou Website

 
 
//

Location

 

559Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Publication Type
Year
to

140 results found

Tasos A, Franco J, Drossopoulou S, Wrigstad T, Eisenbach Set 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.

Journal article

Drossopoulou S, Noble J, MacKay J, Eisenbach Set 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.

Conference paper

Drossopoulou S, Noble J, Mackay J, Eisenbach Set 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

Software

Blessing S, Fernandez-Reyes K, Yang AM, Drossopoulou S, Wrigstad Tet al., 2019, Run, actor, run towards cross-actor language benchmarking, Pages: 41-50

The actor paradigm supports the natural expression of concurrency. It has inspired the development of several actor-based languages, whose adoption depends, to a large extent, on the runtime characteristics (i.e., the performance and scaling behaviour) of programs written in these languages. This paper investigates the relative runtime characteristics of Akka, CAF and Pony, based on the Savina benchmarks. We observe that the scaling of many of the Savina benchmarks does not reflect their categorization (into essentially sequential, concurrent and parallel), that many programs have similar runtime characteristics, and that their runtime behaviour may drastically change nature (e.g., go from essentially sequential to parallel) by tweaking some parameters. These observations lead to our proposal of a single benchmark program which we designed so that through tweaking of some knobs (we hope) we can simulate most of the programs of the Savina suite.

Conference paper

Liétar P, Butler T, Clebsch S, Drossopoulou S, Franco J, Parkinson MJ, Swamis A, Wintersteiger CM, Chisnall Det 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.

Conference paper

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.

Thesis dissertation

Tasos A, Franco J, Wrigstad T, Drossopoulou S, Eisenbach Set 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.

Conference paper

Vicente Franco J, Clebsch S, Drossopoulou S, Vitek J, Wrigstad Tet 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.

Conference paper

Vicente Franco J, Clebsch S, Drossopoulou S, Vitek J, Wrigstad Tet 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.

Conference paper

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.

Conference paper

Franco J, Hagelin M, Wrigstad T, Drossopoulou S, Eisenbach Set 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.

Conference paper

Blessing S, Clebsch S, Drossopoulou S, 2017, Tree topologies for causal message delivery, Pages: 1-10

Causal message delivery, i.e. the requirement that messages are delivered in an order respecting their causal (logical) dependencies, is often mandated in the distributed setting. So far, causal message delivery has been implemented by augmenting messages with meta data information that allows the receiver (or the platform) to re-order, and if necessary hold back, messages upon receipt before processing. We propose that causal message delivery can be achieved by construction, simply by organizing the nodes of the distributed application into a tree topology, and without the need for any meta data in the messages. We present our ideas informally through an example application and then develop a formal model and prove that causal message delivery is preserved in tree-based networks.

Conference paper

Clebsch S, Franco J, Drossopoulou S, Mingkun Yang A, Wrigstad T, Vitek Jet 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.

Conference paper

Wood T, Drossopoulou S, Lahiri SK, Eisenbach Set 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.

Conference paper

Drossopoulou S, Noble J, Miller MS, Murray Tet 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.

Conference paper

Certezeanu R, Drossopoulou S, Egelund-Muller B, Leino KRM, Sivarajan S, Wheelhouse Met 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.

Book chapter

Franco J, Drossopoulou S, 2016, Behavioural types for non-uniform memory accesses, Publisher: OPEN PUBL ASSOC, Pages: 109-120, ISSN: 2075-2180

Conference paper

Clebsch S, Drossopoulou S, Blessing S, McNeil Aet 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.

Conference paper

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.

Conference paper

Drossopoulou S, Noble J, 2014, How to Break the Bank -- Semantics of Capability Policies, Integrated Formal Methods, ISSN: 0302-9743

Conference paper

Boer F, Einar Broch J, Clarke D, Drossopoulou S, Yoshida N, Wrigstad Tet al., 2014, Scaling Future Software: The Manycore Challenge, ERCIM News, Vol: 2014

Journal article

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

Conference paper

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.

Conference paper

Drossopoulou S, Noble J, 2014, Rationally reconstructing the Escrow Example, Formal Techniques for Java Programs, Publisher: ACM

Conference paper

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.

Conference paper

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

Journal article

Drossopoulou S, Clebsch S, 2013, Fully Concurrent garbage Collection for Actors in Many-Core Mashines, OOPSLA

Conference paper

Cameron N, Drossopoulou S, 2013, Understanding Ownership Types with Dependent Types, Aliasing in Object-Oriented Programming, Editors: Clarke, Noble, Wrigstad

Book chapter

Cameron N, Drossopoulou S, 2013, Understanding Ownership Types with Dependent Types, Aliasing in Object-Oriented Programming, Editors: Clarke, Noble, Wrigstag, Publisher: Springer, LNCS

Book chapter

Drossopoulou S, Noble J, 2013, The Need for Capability Policies, FTfJP

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 ver- sions 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 method- ologies cannot adequately capture all aspects of the capability poli- cies required to support object-capability systems. We outline inormally the features that such security policies should support, and we demonstrate (also informally) how we can reason that examples satisfy the capability policies.

Conference paper

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.

Request URL: http://wlsprd.imperial.ac.uk:80/respub/WEB-INF/jsp/search-html.jsp Request URI: /respub/WEB-INF/jsp/search-html.jsp Query String: respub-action=search.html&id=00001716&limit=30&person=true