122 results found
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, Pages: 148-167
© 2017 Copyright held by the owner/author(s). 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, Drossopolou S, Lahiri SK, et al., 2017, Modular verification of procedure equivalence in the presence of memory allocation, Pages: 937-963, ISSN: 0302-9743
© Springer-Verlag GmbH Germany 2017. For most high level languages, two procedures are equivalent if they transform a pair of isomorphic stores to isomorphic stores. However, tools for modular checking of such equivalence impose a stronger check where isomorphism is strengthened to equality of stores. This results in the inability to prove many interesting program pairs with recursion and dynamic memory allocation. In this work, we present RIE, a methodology to modularly establish equivalence of procedures in the presence of memory allocation, cyclic data structures and recursion. Our technique addresses the need for finding witnesses to isomorphism with angelic allocation, supports reasoning about equivalent procedures calls when the stores are only locally isomorphic, 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.
Martins PM, McCann JA, Eisenbach S, 2012, The environment as an argument: Context-aware functional programming, Pages: 48-62, ISSN: 0302-9743
Context-awareness as defined in the setting of Ubiquitous Computing  is all about expressing the dependency of a specific computation upon some implicit piece of information. The manipulation and expression of such dependencies may thus be neatly encapsulated in a language where computations are first-class values. Perhaps surprisingly however, context-aware programming has not been explored in a functional setting, where first-class computations and higher-order functions are commonplace. In this paper we present an embedded domain-specific language (EDSL) for constructing context-aware applications in the functional programming language Haskell. © 2012 Springer-Verlag.
Gudka K, Harris T, Eisenbach S, 2012, Lock Inference in the Presence of Large Libraries, 26th European Conference on Object-Oriented Programming (ECOOP), Publisher: SPRINGER-VERLAG BERLIN, Pages: 308-332, ISSN: 0302-9743
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-VERLAG BERLIN, Pages: 407-421, ISSN: 0302-9743
Allwood T, Cadar C, Eisenbach S, 2011, High coverage testing of Haskell programs, Pages: 375-385
This paper presents a new lightweight technique for automatically generating high coverage test suites for Haskell library code. Our approach combines four main features to increase test coverage: (1) automatically inferring the constructors and functions needed to generate test data; (2) using needed narrowing to take advantage of Haskell's lazy evaluation semantics; (3) inspecting elements inside returned data structures through the use of case statements, and (4) efficiently handling polymorphism by lazily instantiating all possible instances. We have implemented this technique in IRULAN, a fully automatic tool for systematic black-box unit testing of Haskell library code. We have designed IRULAN to generate high coverage test suites and detect common programming errors in the process. We have applied IRULAN to over 50 programs from the spectral and real suites of the nofib benchmark and show that it can effectively generate high-coverage test suites - exhibiting 70.83% coverage for spectral and 59.78% coverage for real - and find errors in these programs. Our techniques are general enough to be useful for several other types of testing, and we also discuss our experience of using IRULAN for property and regression testing. © 2011 ACM.
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 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.
Alpay E, Cutler PS, Eisenbach S, et al., 2010, Changing the marks-based culture of learning through peer-assisted tutorials, Pages: 17-32, ISSN: 0304-3797
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'end-of-year total; all tutorialwork 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 among 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. © 2010 SEFI.
Plociniczak H, Eisenbach S, 2010, JErlang: Erlang with Joins, 12th International Conference on Coordination Models and Languages (COORDINATION 2010), Publisher: SPRINGER-VERLAG BERLIN, Pages: 61-+, ISSN: 0302-9743
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.
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
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
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
Filho AES, Lupu EC, Sloman M, et al., 2009, Verification of Policy-Based Self-Managed Cell Interactions Using Alloy., Publisher: IEEE Computer Society, Pages: 37-40
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.
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.
Cunningham D, Gudka K, Eisenbach S, 2008, Keep off the grass: Locking the right path for atomicity, 17th International Conference on Compiler Construction, Publisher: SPRINGER-VERLAG BERLIN, Pages: 276-290, ISSN: 0302-9743
Allwood TOR, Eisenbach S, 2008, CLASS: Cursor Library for A Structured Editor, 1st ACM SIGPLAN Haskell Symposium, Publisher: ASSOC COMPUTING MACHINERY, Pages: 123-124
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.