123 results found
Kiss C, Field A, Eisenbach S, et al., Higher-Order Type-Level Programming in Haskell, International Conference on Functional Programming, Publisher: ACM
Type family applications in Haskell must be fully saturated. This means that all type-level functions haveto be first-order, leading to code that is both messy and longwinded. In this paper we detail an extension toGHC that removes this restriction. We augment Haskell’s existing type arrow,→, with anunmatchablearrow,↠, that supports partial application of type families without compromising soundness. A soundness proof isprovided. We show how the techniques described can lead to substantial code-size reduction (circa 80%) inthe type-level logic of commonly-used type-level libraries whilst simultaneously improving code quality and readability.
Schrans F, Hails D, Harkness A, et al., 2019, Flint for safer smart contracts, Publisher: arXiv
The Ethereum blockchain platform supports the execution of decentralisedapplications or smart contracts. These typically hold and transfer digitalcurrency to other parties on the platform; however, they have been subject tonumerous attacks due to the unintentional introduction of bugs. Over a billiondollars worth of currency has been stolen since its release in July 2015. Assmart contracts cannot be updated after deployment, it is imperative that theprogramming language supports the development of robust contracts. We propose Flint, a new statically-typed programming language specificallydesigned for writing robust smart contracts. Flint's features enforce thewriting of safe and predictable code. To encourage good practices, we introduceprotection blocks. Protection blocks restrict who can run code and when (usingtypestate) it can be executed. To prevent vulnerabilities relating to theunintentional loss of currency, Flint Asset traits provide safe atomicoperations, ensuring the state of contracts is always consistent. Writes tostate are restricted, simplifying reasoning about smart contracts.
Tasos A, Franco J, Wrigstad T, et al., 2018, Extending SHAPES for SIMD architectures: An approach to native support for struct of arrays in languages, Pages: 23-27
© 2018 Copyright held by the owner/author(s). Publication rights licensed to Association for Computing Machinery. 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.
Schrans F, Eisenbach S, Drossopoulou S, 2018, Writing safe smart contracts in flint, Pages: 218-219
© 2018 Copyright held by the owner/author(s). 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, 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.
Wood T, Drossopoulou S, Lahiri SK, et al., Modular verification of procedure equivalence in the presence of memory allocation, European Symposium on Programming
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.
Gudka K, Harris T, Eisenbach S, 2012, Lock inference in the presence of large libraries, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol: 7313 LNCS, Pages: 308-332, ISSN: 0302-9743
Atomic sections can be implemented using lock inference. For lock inference to be practically useful, it is crucial that large libraries be analysed. However, libraries are challenging for static analysis, due to their cyclomatic complexity. Existing approaches either ignore libraries, require library implementers to annotate which locks to take or only consider accesses performed upto one level deep in library call chains. Thus, some library accesses may go unprotected, leading to atomicity violations that atomic sections are supposed to eliminate. We present a lock inference approach for Java that analyses library methods in full. We achieve this by (i) formulating lock inference as an Interprocedural Distributive Environment dataflow problem, (ii) using a graph representation for summary information and (iii) applying a number of optimisations to our implementation to reduce space-time requirements and locks inferred. We demonstrate the scalability of our approach by analysing the entire GNU Classpath library comprising 122KLOC. © 2012 Springer-Verlag Berlin Heidelberg.
Sonnex W, Drossopoulou S, Eisenbach S, 2012, Zeno: An automated prover for properties of recursive data structures, 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Publisher: Springer Berlin Heidelberg, Pages: 407-421, ISSN: 0302-9743
Most functional programs rely heavily on recursively defined structures and pattern matching thereupon. Proving properties of such programs often requires a proof by induction, which many theorem provers have difficulty addressing. In this paper we present Zeno, a new tool for the automatic verification of simple properties of functional programs. We define a minimal functional language along with a subset of first order logic in which to express properties to be proven. Zeno constructs a proof tree by iteratively reducing the goal into an equivalent conjunction of several simpler sub-goals, terminating when all leaves are trivially true. Building this tree requires the exploration of many alternatives and we give sophisticated techniques for the reduction of this search space through the analysis of function definitions. We provide a comparison with the rippling based tool IsaPlanner and the industrial strength tool ACL2s. Using a test suite from the IsaPlanner website we found that Zeno could prove strictly more properties than either, and in as good times.
Martins P, McCann J, Eisenbach S, 2012, The Environment as an Argument, Practical Aspects of Declarative Languages, Publisher: Springer Berlin Heidelberg, Pages: 48-62
Gudka K, Harris T, Eisenbach S, 2012, Lock Inference in the Presence of Large Libraries, European Conference on Object-Oriented Programming, Publisher: Springer, Pages: 308-332, ISSN: 0302-9743
Atomic sections can be implemented using lock inference. For the implementation of lock inference to be practically useful, it is crucial that large libraries be analysed. Large libraries are challenging for static analysis, due to their cyclomatic complexity.Existing approaches either ignore libraries, require library implementers to annotate which locks to take or only consider accesses performed upto one level deep in library call chains. As a result, some accesses performed within the library may go unprotected, leading to atomicity violations that atomic sections are supposed to eliminate.We present a lock inference approach for Java that analyses library methods in full. We achieve this by (i) formulating lock inference as an Interprocedural Distributive Environment dataflow problem, (ii) using a graph representation for summary information and (iii) applying a number of optimisations to our implementation to reduce space-time requirements. We evaluate the effects of each optimisation and show that propagating only new dataflow information gives the biggest speed up whilst also reducing memory usage. We identify and remove many locks for thread-local and internal objects via simple analyses. We demonstrate the scalability of our approach by analysing the entire GNU Classpath library comprising 122KLOC.
Canfora G, Dalcher D, Raffo D, et al., 2011, In memory of Manny Lehman, 'Father of Software Evolution', JOURNAL OF SOFTWARE MAINTENANCE AND EVOLUTION-RESEARCH AND PRACTICE, Vol: 23, Pages: 137-144, ISSN: 1532-060X
Allwood T, Cadar C, Eisenbach S, 2011, High Coverage Testing of Haskell Programs, International Symposium on Software Testing and Analysis, Publisher: ACM, Pages: 375-385
This paper presents Irulan, a fully automatic tool designed to perform systematic gray-box unit testing of Haskell libraries. Through automatic code generation and execution, Irulan checks if there are any possible uses of a library's API that cause uncaught exceptions to be thrown. If such cases are found, Irulan returns a Haskell expression that triggers the error, to help programmers debug and fix their code. Irulan supports (and takes advantage of) the most important features of the Haskell language, such as lazy evaluation and polymorphism. In addition, it uses various exploration strategies and caching to more effectively explore the state space of the programs under testing. We evaluate Irulan on over 50 benchmarks from the nofib suite and show that it can effectively generate high-coverage test suites and find errors in these programs.
Allwood TOR, Eisenbach S, 2010, Strengthening the zipper, Electronic Notes in Theoretical Computer Science, Vol: 253, Pages: 3-18, ISSN: 1571-0661
The zipper is a well known design pattern for providing a cursor-like interface to a data structure. However, the classic treatise by Huet only scratches the surface of some of its potential applications. In this paper we take inspiration from Huet, and describe a library suitable as an underpinning for structured editors. We consider a zipper structure that is suitable for traversing heterogeneous data types, encoding routes to other places in the tree (for bookmark or quick-jump functionality), expressing lexically bound information using contexts, and traversals for rendering a program indicating where the cursor is currently focused. © 2010 Elsevier B.V. All rights reserved.
Plociniczak H, Eisenbach S, 2010, JErlang: Erlang with Joins, COORDINATION 2010, Publisher: Springer, Pages: 61-75
Erlang is an industrially successful functional language that uses the Actor model for concurrency. It supports the message-passing paradigm by providing pattern-matching over received messages. Unfortunately coding synchronisation between multiple processes is not straightforward. To overcome this limitation we designed and implemented JErlang, a Join-Calculus inspired extension to Erlang. We provide a rich set of language features with our joins. We present implementation details of our two alternative solutions, a library and an altered VM. Our optimisations provide JErlang with good performance.
Allwood T, Peyton Jones S, Eisenbach S, 2009, Finding the needle: Stack Traces for GHC, Haskell'09, Pages: 129-140
Even Haskell programs can occasionally go wrong. Programs calling head on an empty list, and incomplete patterns in function definitions can cause program crashes, reporting little more than the precise location where error was ultimately called. Being told that one application of the head function in your program went wrong, without knowing which use of head went wrong can be infuriating.\r\n\r\nWe present our work on adding the ability to get stack traces out of GHC, for example that our crashing head was used during the evaluation of foo, which was called during the evaluation of bar, during the evaluation of main. We provide a transformation that converts GHC Core programs into ones that pass a stack around, and a stack library that ensures bounded heap usage despite the highly recursive nature of Haskell. We call our extension to GHC StackTrace.
Schaeffer Filho A, Lupu E, Sloman M, et al., 2009, Verification of Policy-based Self-Managed Cell Interactions Using Alloy, IEEE International Symposium on Policies for Distributed Systems and Networks (Policy), Publisher: IEEE, Pages: 37-40
Self-Managed Cells (SMCs) define an infrastructure for building ubiquitous computing applications. An SMC consists of an autonomous administrative domain based on a policy-driven feedback control-loop. SMCs are able to interact with each other and compose with other SMCs to form larger autonomous components. In this paper we present a formal specification of an SMC's behaviour for the analysis and verification of its operation in collaborations of SMCs. These collaborations typically involve SMCs originated from different administrative authorities, and the definition of a formal model has helped us to verify the correctness of their operation when SMCs are composed or federated.
Petrounias A, Eisenbach S, 2009, Fairness for Chorded Languages, Coordination'09, Publisher: Springer
Joins or chords is a concurrency construct that seems to fit well with the object oriented paradigm. Chorded languages are presented with implicit assumptions regarding the fair treatment of processes by the scheduler. We define weak and strong fairness for the Small Chorded Object-Oriented Language (l SCHOOL) which allows the classification of executions as fair. We investigate the liveness behaviour of programs and establish worst-case behaviours in terms of scheduling delays. \r\n\r\nWe discover that weak fairness, although giving the scheduler implementer greater freedom in selecting the next process which is to be executed, is harder to implement than strong fairness; strong fairness benefits from a straightforward implementation, however, imposes many more constraints and limits the selection function of a scheduler. \r\n\r\n
Alpay E, Cutler PS, Eisenbach S, et al., 2009, Changing the Marks Based Culture of Learning through Peer Assisted Tutorials, Washington, DC, 2009 ASEE Annual Conference, Publisher: Taylor and Francis Group, Pages: 17-32
We describe and evaluate an approach to student learning that aims to instil a culture of formative assessment based on peer-assisted learning. The idea is for suitably qualified undergraduates to assist in the running of weekly first-year tutorials. They mark submitted work, provide written and verbal feedback and lead problem solving discussions during tutorials. However, contrary to normal practice, the marks they award do not contribute to the students' year total; all tutorial work becomes essentially voluntary. We report results from a pilot implementation of the scheme over a 12-month period in an engineering department at a leading academic institution. The scheme was such that a comparative and triangulated assessment was possible amongst the students and tutor team. Results show no discernible degradation in student attendance, submission rates and performance in either the weekly exercises or end of year examinations. Important benefits to the peer tutors are also found.
Ayres J, Eisenbach S, 2009, Stage: Python with Actors, International Workshop on Multicore Software Engineering (IWMSE)
Programmers hoping to exploit multi-core processors must split their applications into threads suitable for independent, concurrent execution. The lock-based concurrency of many existing languages is clumsy and error prone -- a barrier to writing fast and correct concurrent code.\r\n\r\nThe Actor model exudes concurrency -- each entity in the model (an Actor) executes concurrently. Interaction is restricted to message passing which prevents many of the errors associated with shared mutable state and locking, the common alternative. By favouring message passing over method calling the Actor model makes distribution straightforward. \r\n\r\nEarly Actor-based languages enjoyed only moderate success, probably because they were before their time. More recent Actor languages have enjoyed greater success, the most successful being Erlang, but the language is functional; a paradigm unfamiliar to many programmers. There is a need for a language that presents a familiar and fast encoding of the Actor model. In this paper we present Stage, our mobile Actor language based on Python.
Schaeffer Filho A, Lupu E, Sloman M, et al., 2009, Verification of Policy-based Self-Managed Cell Interactions Using Alloy
Self-Managed Cells (SMCs) define an infrastructure for building ubiquitous computing applications. An SMC consists of an autonomous administrative domain based on a policy-driven feedback control-loop. SMCs are able to interact with each other and compose with other SMCs to form larger autonomous components. In this paper we present a formal specification of an SMC's behaviour for the analysis and verification of its operation in collaborations of SMCs. These collaborations typically involve SMCs originated from different administrative authorities, and the definition of a formal model has helped us to verify the correctness of their operation when SMCs are composed or federated. The formal specification also enables a better characterisation of the integrity constraints that must be preserved during SMC operation.
Giachino E, Sackman M, Drossopoulou S, et al., 2009, Softly safely spoken: Role playing for Session Types, Places'09
Session types have made much progress at permitting programs be statically verified concordant with a specified protocol. However, it is difficult to build abstractions of, or encapsulate Session types, thus limiting their flexibility. Global session types add further constraints to communication, by permitting the order of exchanges amongst many participants to be specified. The cost is that the number of participants is statically fixed. \r\n\r\nWe introduce Roles in which, similarly to global session types, the number of roles and the conversations involving roles are statically known, but participants can dynamically join and leave roles and the number of participants within a role is not statically known. Statically defined roles which conform to a specified conversation can be dynamically instantiated, participants can be members of multiple roles simultaneously and can participate in multiple conversations concurrently. \r\n\r\n
Sackman M, Eisenbach S, 2009, Safely Speaking in Tongues: Statically Checking Domain Specific Languages in Haskell, Workshop on Language Descriptions Tools and Applications (LDTA) 2009, Pages: 34-51
Allwood TOR, Eisenbach S, 2009, CLASE: Cursor Library for A Structured Editor, ACM SIGPLAN NOTICES, Vol: 44, Pages: 123-124, ISSN: 0362-1340
Allwood T, Eisenbach S, 2009, Strengthening the Zipper, Workshop on Language Descriptions Tools and Applications (LDTA) 2009, Pages: 2-17
The "zipper" is a well known design pattern for providing a cursor-like interface to a data structure. However, the classic treatise by Huet only scratches the surface of some of its potential applications. In this paper we take inspiration from Huet, and describe a library suitable as an underpinning for structured editors. We consider a zipper structure that is suitable for traversing heterogeneous data types, encoding routes to other places in the tree (for bookmark or quick-jump functionality), expressing lexically bound information using contexts, and traversals for rendering a program indicating where the cursor is currently focused.
Aplay E, Cutler P, Eisenbach S, et al., 2009, Changing the Marks Based Culture of Learning through Peer Assisted Tutorials, 2009 ASEE Annual Conference & Exposition, Publisher: American Society for Engineering Education, Pages: 1-24
We describe and evaluate an approach to student learning that aims to instil a culture of formative assessment based on peer-assisted self learning, instead of a marks-based culture in which learning effort is rewarded with marks that contribute to the student's degree. The idea is for suitably qualified third- and fourth-year undergraduates to assist in the running of weekly first-year tutorials. They mark submitted work, provide written and verbal feedback on the students' performance and lead problem solving discussions during tutorials. However, contrary to normal practice, the marks they award do not contribute to the students' year total; all tutorial work becomes essentially voluntary. We report results from a pilot implementation of the scheme over a 12-month period in an engineering department at a leading academic institution. The set-up of the scheme was such that a comparative and triangulated assessment was possible amongst the students and tutor team. There was no\r\ndiscernible degradation in student attendance, submission rates and performance in either the weekly exercises or end of year examinations. Further analysis demonstrates that this type of peer-assisted learning improves some key aspects of student learning, and provides important benefits to the senior peers in terms of their own personal development. We conclude that the scheme provides an excellent alternative to traditional learning methods whilst substantially reducing the investment in academic staff time.\r\n
Petrounias A, Drossopoulou S, Eisenbach S, 2008, A Featherweight Model for Chorded Languages, Publisher: Imperial College, Department of Computing
Chords are a concurrency mechanism of object-oriented languages inspired by the join of the Join-Calculus. We present SCHOOL, the Small Chorded Object-Oriented Language, a featherweight model which aims to capture the essence of the concurrent behaviours of chords. Our model serves as a generalisation of chorded behaviours found in existing experimental languages such as Polyphonic C-sharp. Furthermore, we study the interaction of chords with fields by extending SCHOOL to include fields, resulting in fSCHOOL. Fields are orthogonal to chords in terms of concurrent behaviours. We show that adding fields to SCHOOL does not change its expressiveness by means of an encoding between the two languages.
Sackman M, Eisenbach S, 2008, Errors for the Common Man: Hiding the unintelligable in Haskell, Publisher: Department of Computing, Imperial College
If a library designer takes full advantage of HaskellÆs rich type system and type-level programming capabilities, then the resulting library will frequently inflict huge and unhelpful error messages on the library user. These error messages are typically in terms of the library and do not refer to the call-site of the library by the library user, nor provide any guidance to the user as to how to fix the error. \r\n\r\nThe increasing appetite for programmable type-level computation makes this a critical issue, as the advantages and capabilities of type-level computation are nullified if useful error messages cannot be returned to the user. \r\n\r\nWe present a novel technique that neatly side-steps the default error messages and allows the library programmer to control the generation of error messages that are statically returned to the user. Thus with this technique, there is no longer any drawback to using the full power of HaskellÆs type system. \r\n\r\n
Drossopoulou S, Eisenbach S, Cunningham D, 2008, Lock Inference Proven Correct, FTfJP, Pages: 24-35
With the introduction of multi-core CPUs, multi-threaded programming is becoming significantly more popular. Unfortunately, it is difficult for programmers to ensure their code is correct because current languages are too low-level.\r\n\r\nAtomic sections are a recent language primitive that expose a higher level interface to programmers. Thus they make concurrent programming more straightforward. Atomic sections can be compiled using transactional memory or lock inference, but ensuring correctness and good performance is a challenge. Transactional memory has problems with IO and contention, whereas lock inference algorithms are often too imprecise which translates to a loss of parallelism at runtime.\r\n\r\nWe define a lock inference algorithm that has good precision. We give the operational semantics of a model OO language, and define a notion of correctness for our algorithm. We then prove correctness using Isabelle/HOL.\r\n
Sackman M, Eisenbach S, 2008, Session Types in Haskell: Updating Message Passing for the 21st Century
Session Types allow plans of conversation between two concurrent processes to be treated as types. Type checking then ensures that communication between processes is safe: i.e. it obeys the protocol specified by the session type. Thus Session Types offer a means to establish conformance to protocols in both distributed applications and multi-threaded programming.\r\n\r\nWe incorporate Session Types into Haskell as a tool for concurrent programming. Our implementation, which is a standard Haskell library, presents a monadic API to the programmer. Using the library looks and feels very much like normal monadic computation and thus there is a shallow learning curve for the Haskell programmer. Our implementation lifts the invariants and properties of Session Types into Haskell's rich type system. This allows our implementation to statically verify the use of the communication primitives provided without an additional type checker, preprocessor or modification to the compiler.\r\n\r\nOur implementation supports multiple concurrent communication channels, individual processes can interleave actions across any number of open channels, and channels themselves can be sent and received. New channels can be created between pre-existing processes as well as to newly created processes. Communication is asynchronous and fully polymorphic. To our knowledge, no other implementation of Session Types is available in any language which matches our library in terms of functionality and supported features. We describe the key aspects of our implementation and demonstrate, through a running example, its usage and flexibility.
Allwood T, Eisenbach S, 2008, CLASE: Cursor Library for A Structured Editor
The ``zipper'' is a well known design pattern for providing a cursor-like interface to a data structure. However, the classic treatise by Huet only scratches the surface of some of the potential applications of the zipper. In this paper we take inspiration from Huet, and build a library suitable as an underpinning for a structured editor for programming languages. We consider a zipper structure that is suitable for traversing heterogeneous data types, encoding routes to other places in the tree (for bookmark or quick-jump functionality), expressing lexically bound information using contexts, and traversals for rendering a program indicating where the cursor is currently focused in the whole.
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.