ORCID Profile
0000-0003-1442-5387
Current Organisation
Universiteit Utrecht
Does something not look right? The information on this page has been harvested from data sources that may not be up to date. We continue to work with information providers to improve coverage and quality. To report an issue, use the Feedback Form.
Publisher: Springer Berlin Heidelberg
Date: 1996
DOI: 10.1007/BFB0027796
Publisher: Springer Berlin Heidelberg
Date: 1998
DOI: 10.1007/BFB0057920
Publisher: Springer Berlin Heidelberg
Date: 2006
DOI: 10.1007/11758525_122
Publisher: ACM
Date: 25-03-2016
Publisher: Springer Berlin Heidelberg
Date: 2001
Publisher: Association for Computing Machinery (ACM)
Date: 25-09-2013
Abstract: Purely functional, embedded array programs are a good match for SIMD hardware, such as GPUs. However, the naive compilation of such programs quickly leads to both code explosion and an excessive use of intermediate data structures. The resulting slow-down is not acceptable on target hardware that is usually chosen to achieve high performance. In this paper, we discuss two optimisation techniques, sharing recovery and array fusion, that tackle code explosion and eliminate superfluous intermediate structures. Both techniques are well known from other contexts, but they present unique challenges for an embedded language compiled for execution on a GPU. We present novel methods for implementing sharing recovery and array fusion, and demonstrate their effectiveness on a set of benchmarks.
Publisher: ACM
Date: 12-01-2005
Publisher: Association for Computing Machinery (ACM)
Date: 12-09-2005
Abstract: Haskell programmers often use a multi-parameter type class in which one or more type parameters are functionally dependent on the first. Although such functional dependencies have proved quite popular in practice, they express the programmer's intent somewhat indirectly. Developing earlier work on associated data types , we propose to add functionally dependent types as type synonyms to type-class bodies. These associated type synonyms constitute an interesting new alternative to explicit functional dependencies.
Publisher: ACM
Date: 23-01-2011
Publisher: Association for Computing Machinery (ACM)
Date: 09-09-2012
Abstract: Existing approaches to higher-order vectorisation , also known as flattening nested data parallelism , do not preserve the asymptotic work complexity of the source program. Straightforward ex les, such as sparse matrix-vector multiplication, can suffer a severe blow-up in both time and space, which limits the practicality of this method. We discuss why this problem arises, identify the mis-handling of index space transforms as the root cause, and present a solution using a refined representation of nested arrays. We have implemented this solution in Data Parallel Haskell (DPH) and present benchmarks showing that realistic programs, which used to suffer the blow-up, now have the correct asymptotic work complexity. In some cases, the asymptotic complexity of the vectorised program is even better than the original.
Publisher: ACM
Date: 22-09-2011
Publisher: ACM
Date: 25-09-2013
Publisher: ACM
Date: 23-09-2013
Publisher: Association for Computing Machinery (ACM)
Date: 12-01-2005
Abstract: Haskell's type classes allow ad-hoc overloading, or type-indexing, of functions . A natural generalisation is to allow type-indexing of data types as well. It turns out that this idea directly supports a powerful form of abstraction called associated types , which are available in C++ using traits classes. Associated types are useful in many applications, especially for self-optimising libraries that adapt their data representations and algorithms in a type-directed manner.In this paper, we introduce and motivate associated types as a rather natural generalisation of Haskell's existing type classes. Formally, we present a type system that includes a type-directed translation into an explicitly typed target language akin to System F the existence of this translation ensures that the addition of associated data types to an existing Haskell compiler only requires changes to the front end.
Publisher: Association for Computing Machinery (ACM)
Date: 15-05-2014
Abstract: File systems are too important, and current ones are too buggy, to remain unverified. Yet the most successful verification methods for functional correctness remain too expensive for current file system implementations-we need verified correctness but at reasonable cost. This paper presents our vision and ongoing work to achieve this goal for a new high-performance flash file system, called BilbyFs. BilbyFs is carefully designed to be highly modular, so it can be verified against a high-level functional specification one component at a time. This modular implementation is captured in a set of domain specific languages from which we produce the design-level specification, as well as its optimised C implementation. Importantly, we also automatically generate the proof linking these two artefacts. The combination of these features dramatically reduces verification effort. Verified file systems are now within reach for the first time.
Publisher: ACM
Date: 09-09-2012
Publisher: ACM
Date: 03-11-2014
Publisher: Springer Berlin Heidelberg
Date: 2004
Publisher: Wiley
Date: 21-08-2007
Publisher: Association for Computing Machinery (ACM)
Date: 09-01-2023
DOI: 10.1145/3571240
Abstract: Systems programmers need fine-grained control over the memory layout of data structures, both to produce performant code and to comply with well-defined interfaces imposed by existing code, standardised protocols or hardware. Code that manipulates these low-level representations in memory is hard to get right. Traditionally, this problem is addressed by the implementation of tedious marshalling code to convert between compiler-selected data representations and the desired compact data formats. Such marshalling code is error-prone and can lead to a significant runtime overhead due to excessive copying. While there are many languages and systems that address the correctness issue, by automating the generation and, in some cases, the verification of the marshalling code, the performance overhead introduced by the marshalling code remains. In particular for systems code, this overhead can be prohibitive. In this work, we address both the correctness and the performance problems. We present a data layout description language and data refinement framework, called Dargent, which allows programmers to declaratively specify how algebraic data types are laid out in memory. Our solution is applied to the Cogent language, but the general ideas behind our solution are applicable to other settings. The Dargent framework generates C code that manipulates data directly with the desired memory layout, while retaining the formal proof that this generated C code is correct with respect to the functional semantics. This added expressivity removes the need for implementing and verifying marshalling code, which eliminates copying, smoothens interoperability with surrounding systems, and increases the trustworthiness of the overall system.
Publisher: Association for Computing Machinery (ACM)
Date: 22-09-2011
Abstract: Stencil convolution is a fundamental building block of many scientific and image processing algorithms. We present a declarative approach to writing such convolutions in Haskell that is both efficient at runtime and implicitly parallel. To achieve this we extend our prior work on the Repa array library with two new features: partitioned and cursored arrays. Combined with careful management of the interaction between GHC and its back-end code generator LLVM, we achieve performance comparable to the standard OpenCV library.
Publisher: Springer International Publishing
Date: 2022
Publisher: Association for Computing Machinery (ACM)
Date: 13-09-2012
Abstract: We present a refined approach to parallel array fusion that uses indexed types to specify the internal representation of each array. Our approach aids the client programmer in reasoning about the performance of their program in terms of the source code. It also makes the intermediate code easier to transform at compile-time, resulting in faster compilation and more reliable runtimes. We demonstrate how our new approach improves both the clarity and performance of several end-user written programs, including a fluid flow solver and an interpolator for volumetric data.
Publisher: ACM
Date: 28-10-2017
Publisher: Elsevier BV
Date: 04-2004
Publisher: Association for Computing Machinery (ACM)
Date: 13-09-2012
Abstract: Flattening nested parallelism is a vectorising code transform that converts irregular nested parallelism into flat data parallelism. Although the result has good asymptotic performance, flattening thoroughly restructures the code. Many intermediate data structures and traversals are introduced, which may or may not be eliminated by subsequent optimisation. We present a novel program analysis to identify parts of the program where flattening would only introduce overhead, without appropriate gain. We present empirical evidence that avoiding vectorisation in these cases leads to more efficient programs than if we had applied vectorisation and then relied on array fusion to eliminate intermediates from the resulting code.
Publisher: Elsevier BV
Date: 06-2019
Publisher: IEEE Comput. Soc
Date: 1997
Publisher: Institute of Electrical and Electronics Engineers (IEEE)
Date: 15-03-2018
Publisher: World Scientific Pub Co Pte Lt
Date: 06-2002
DOI: 10.1142/S0129626402000951
Abstract: We discuss a language-based cost model for array programs built on the notions of work complexity and parallel depth. The programs operate over data structures comprising nested arrays and recursive product-sum types. In a purely functional setting, such programs can be implemented by way of the flattening transformation that converts codes over nested arrays into vectorised code over flat arrays. Flat arrays lend themselves to a particularly efficient implementation on standard hardware, but the overall efficiency of the approach depends on the flattening transformation preserving the asymptotic complexity of the nested array codes. Blelloch has characterised a class of first-order array programs, called contained programs, for which flattening preserves the asymptotic depth complexity. However, his result is restricted to programs processing only arrays and tuples. In the present paper, we extend Blelloch's result to array programs processing data structures containing arrays as well as arbitrary recursive product-sum types. Moreover, we replace the notion of containment by the more general concept of fold programs.
Publisher: ACM
Date: 23-08-2021
Publisher: Association for Computing Machinery (ACM)
Date: 27-09-2010
Abstract: We present a novel approach to regular, multi-dimensional arrays in Haskell. The main highlights of our approach are that it (1) is purely functional, (2) supports reuse through shape polymorphism, (3) avoids unnecessary intermediate structures rather than relying on subsequent loop fusion, and (4) supports transparent parallelisation. We show how to embed two forms of shape polymorphism into Haskell's type system using type classes and type families. In particular, we discuss the generalisation of regular array transformations to arrays of higher rank, and introduce a type-safe specification of array slices. We discuss the runtime performance of our approach for three standard array algorithms. We achieve absolute performance comparable to handwritten C code. At the same time, our implementation scales well up to 8 processor cores.
Publisher: Springer International Publishing
Date: 2020
Publisher: The Royal Society
Date: 04-09-2017
Abstract: We present recent work on building and scaling trustworthy systems with formal, machine-checkable proof from the ground up, including the operating system kernel, at the level of binary machine code. We first give a brief overview of the seL4 microkernel verification and how it can be used to build verified systems. We then show two complementary techniques for scaling these methods to larger systems: proof engineering, to estimate verification effort and code roof co-generation, for scalable development of provably trustworthy applications. This article is part of the themed issue ‘Verified trustworthy software systems’.
Publisher: Association for Computing Machinery (ACM)
Date: 09-2000
Abstract: This paper generalises the flattening transformation---a technique for the efficient implementation of nested data parallelism---and reconciles it with main stream functional programming. Nested data parallelism is significantly more expressive and convenient to use than the flat data parallelism typically used in conventional parallel languages like High Performance Fortran and C*. The flattening transformation of Blelloch and Sabot is a key technique for the efficient implementation of nested parallelism via flat parallelism, but originally it was severely restricted, as it did not permit general sum types, recursive types, higher-order functions, and separate compilation. Subsequent work, including some of our own, generalised the transformation and allowed higher-order functions and recursive types. In this paper, we take the final step of generalising flattening to cover the full range of types available in modern languages like Haskell and ML furthermore, we enable the use of separate compilation. In addition, we present a completely new formulation of the transformation, which is based on the standard lambda calculus notation, and replace a previously ad-hoc transformation step by a systematic generic programming technique. First experiments demonstrate the efficiency of our approach.
Publisher: Springer International Publishing
Date: 2018
Publisher: Springer International Publishing
Date: 2022
Publisher: Springer Berlin Heidelberg
Date: 1999
DOI: 10.1007/BFB0097892
Publisher: Association for Computing Machinery (ACM)
Date: 10-2001
Abstract: This paper introduces a new approach to optimizing array algorithms in functional languages. We are specifically aiming at an efficient implementation of irregular array algorithms that are hard to implement in conventional array languages such as Fortran. We optimize the storage layout of arrays containing complex data structures and reduce the running time of functions operating on these arrays by means of equational program transformations. In particular, this paper discusses a novel form of combinator loop fusion, which by removing intermediate structures optimizes the use of the memory hierarchy. We identify a combinator named loop P that provides a general scheme for iterating over an array and that in conjunction with an array constructor replicate P is sufficient to express a wide range of array algorithms. On this basis, we define equational transformation rules that combine traversals of loop P and replicate P as well as sequences of applications of loop P into a single loop P traversal. Our approach naturally generalizes to a parallel implementation and includes facilities for optimizing load balancing and communication. A prototype implementation based on the rewrite rule pragma of the Glasgow Haskell Compiler is significantly faster than standard Haskell arrays and approaches the speed of hand coded C for simple ex les.
Publisher: Cambridge University Press (CUP)
Date: 2004
DOI: 10.1017/S0956796803004805
Abstract: We argue that teaching purely functional programming as such in freshman courses is detrimental to both the curriculum as well as to promoting the paradigm. Instead, we need to focus on the more general aims of teaching elementary techniques of programming and essential concepts of computing. We support this viewpoint with experience gained during several semesters of teaching large first-year classes (up to 600 students) in Haskell. These classes consisted of computer science students as well as students from other disciplines. We have systematically gathered student feedback by conducting surveys after each semester. This article contributes an approach to the use of modern functional languages in first year courses and, based on this, advocates the use of functional languages in this setting.
Publisher: ACM
Date: 13-09-2012
Publisher: Springer International Publishing
Date: 2016
Publisher: Institute of Electrical and Electronics Engineers (IEEE)
Date: 2020
Publisher: ACM
Date: 03-09-2014
Publisher: Springer International Publishing
Date: 2014
Publisher: Institute of Electrical and Electronics Engineers (IEEE)
Date: 15-03-2018
Publisher: ACM
Date: 27-09-2010
Start Date: 2016
End Date: 2018
Funder: Australian Research Council
View Funded ActivityStart Date: 2002
End Date: 2004
Funder: Australian Research Council
View Funded ActivityStart Date: 2006
End Date: 2008
Funder: Australian Research Council
View Funded ActivityStart Date: 2009
End Date: 2011
Funder: Australian Research Council
View Funded Activity