Demo Data from VLDB 2026 / reviewers in the wild / expert
Kevin Hammond
dblp:35/4224
· DBLP profile ↗
48ranked-venue papers
4as first author
2since 2021 · last 2026
0000-0002-4326-4562ORCID · corroborated
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 21 · 2 first-author · 1 since 2021Systems, architecture and hardware · 16 · 2 first-author · 1 since 2021Theory of computation · 5Artificial intelligence and machine learning · 3Applied, interdisciplinary, general and emerging computing · 1
Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.
| Software engineering, system software, and programming languages
3 papers |
Program analysis · 80% Programming languages and type systems · 20% | |
| Computer architecture, parallel and distributed computing, and storage systems
2 papers |
Parallel and multicore computing · 64% Energy-efficient computing · 36% |
Topics — the 12 heaviest of 15, each with the papers that count most for it
| Topic | Weight | Papers | Last | Evidence papers |
|---|---|---|---|---|
Program analysis › resource analysis
amortized analysis |
0.2 | 2 | 2010 | Static determination of quantitative resource usage for higher-order programs · POPL 2010 "Carbon Credits" for Resource-Bounded Computations Using Amortised Analysis · FM 2009 |
Program analysis
type-based analysis |
0.1 | 1 | 2010 | Static determination of quantitative resource usage for higher-order programs · POPL 2010 |
Programming languages and type systems › type systems › substructural type systems
linear types |
0.0 | 1 | 2010 | Static determination of quantitative resource usage for higher-order programs · POPL 2010 |
Programming languages and type systems › type inference
hindley-milner type inference |
0.0 | 1 | 1996 | Type Classes in Haskell · ACM Trans. Program. Lang. Syst. 1996 |
Programming languages and type systems › type systems › polymorphism
type classes |
0.0 | 1 | 1996 | Type Classes in Haskell · ACM Trans. Program. Lang. Syst. 1996 |
Programming languages and type systems
type inference |
0.0 | 1 | 1996 | Type Classes in Haskell · ACM Trans. Program. Lang. Syst. 1996 |
Programming languages and type systems
type systems |
0.0 | 1 | 1996 | Type Classes in Haskell · ACM Trans. Program. Lang. Syst. 1996 |
Parallel and multicore computing › parallel programming runtimes
message-driven runtime |
0.0 | 1 | 1996 | GUM: A Portable Parallel Implementation of Haskell · PLDI 1996 |
Parallel and multicore computing › parallel computing › parallel programming languages
parallel functional programming |
0.0 | 1 | 1996 | GUM: A Portable Parallel Implementation of Haskell · PLDI 1996 |
Parallel and multicore computing
parallel programming runtimes |
0.0 | 1 | 1996 | GUM: A Portable Parallel Implementation of Haskell · PLDI 1996 |
Programming languages and type systems
functional programming |
0.0 | 1 | 1996 | Type Classes in Haskell · ACM Trans. Program. Lang. Syst. 1996 |
Programming languages and type systems › functional language
haskell |
0.0 | 1 | 1996 | Type Classes in Haskell · ACM Trans. Program. Lang. Syst. 1996 |
Methods — techniques the papers use, named apart from their topics
amortised analysis · 0.2type inference · 0.1amortized analysis · 0.1second-order lambda calculus · 0.0message passing · 0.0PVM · 0.0
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2026 | Algebraic reasoning for timeliness-guided system design
Seyed Hossein Haeri, Peter Van Roy, Heinrich Apfelmus, Peter Thompson 0002, Neil Davies 0001, Magne Haveraaen, Mikhail Barash, Kevin Hammond, James Chapman 0001, Artjoms Sinkarovs |
J. Log. Algebraic Methods Program. | 8 |
| 2021 | Refactoring for introducing and tuning parallelism for heterogeneous multicore machines in ErlangabstractSummary This paper presents semi‐automatic software refactorings to introduce and tune structured parallelism in sequential Erlang code, as well as to generate code for running computations on GPUs and possibly other accelerators. Our refactorings are based on the lapedo framework for programming heterogeneous multi‐core systems in Erlang. lapedo is based on the PaRTE refactoring tool and also contains (1) a set of hybrid skeletons that target both CPU and GPU processors, (2) novel refactorings for introducing and tuning parallelism, and (3) a tool to generate the GPU offloading and scheduling code in Erlang, which is used as a component of hybrid skeletons. We demonstrate, on four realistic use‐case applications, that we are able to refactor sequential code and produce heterogeneous parallel versions that can achieve significant and scalable speedups of up to 220 over the original sequential Erlang program on a 24‐core machine with a GPU. Vladimir Janjic, Christopher Brown 0002, Adam D. Barwell, Kevin Hammond |
Concurr. Comput. Pract. Exp. | 4 |
| 2019 | Proof-Carrying Plans
Christopher Schwaab, Ekaterina Komendantskaya, Alasdair Hill, Frantisek Farka, Ronald P. A. Petrick, Joe B. Wells, Kevin Hammond |
PADL | 7 |
| 2019 | Learning-Based Dynamic Pinning of Parallelized Applications in Many-Core SystemsabstractThis paper introduces a learning-based framework for dynamic placement of threads of parallel applications to the cores of Non-Uniform Memory Access (NUMA) architectures. Adaptation takes place in two levels, where at the first level each thread independently decides on which group of cores (NUMA node) it will execute, and on the second level it decides to which particular core from the group it will be pinned. Naturally, these two adaptation levels run on different time-scales: a low-frequency switching for the NUMA-node adaptation, and a high-frequency switching for the CPU-node level adaptation. In addition, the learning dynamics have been designed to handle measurement noise and rapid variations in the performance of the threads. The advantage of the proposed learning scheme is the ability to easily incorporate any multi-objective criterion and easily adapt to performance variations during runtime. Our objective is to demonstrate that this framework is appropriate for supervising parallel processes and intervening with respect to better resource allocation. Under the multi-objective criterion of maximizing total completed instructions per second (i.e., both computational and memory-access instructions), we compare the performance of the proposed scheme with the Linux operating system scheduler. We have observed that performance improvement could be significant especially under limited availability of resources and under irregular memory-access patterns. Georgios C. Chasparis, Michael Rossbory, Vladimir Janjic, Kevin Hammond |
PDP | 4 |
| 2019 | Extending the "Open-Closed Principle" to Automated Algorithm ConfigurationabstractMetaheuristics are an effective and diverse class of optimization algorithms: a means of obtaining solutions of acceptable quality for otherwise intractable problems. The selection, construction, and configuration of a metaheuristic for a given problem has historically been a manually intensive process based on experience, experimentation, and reasoning by metaphor. More recently, there has been interest in automating the process of algorithm configuration. In this article, we identify shared state as an inhibitor of progress for such automation. To solve this problem, we introduce the Automated Open-Closed Principle (AOCP), which stipulates design requirements for unintrusive reuse of algorithm frameworks and automated assembly of algorithms from an extensible palette of components. We demonstrate how the AOCP enables a greater degree of automation than previously possible via an example implementation. Jerry Swan, Steven Adriænsen, Adam D. Barwell, Kevin Hammond, David Robert White |
Evol. Comput. | 4 |
| 2018 | Special issue on Parallel and distributed computing based on the functional programming paradigmabstractOver a decade after the beginning of the multicore revolution, researchers and industry are still struggling with problems related to using concurrent hardware. Discovering or developing proper means for creating efficient, scalable, and adaptable software for multicore and multimode computers is still an open and a very important problem. Great efforts are made to solve problems related to the efficiency of resource utilization,1-3 monitoring and failure handling,4, 5 and, most importantly, development of highly concurrent systems.6-8 In addition to much work on adapting existing imperative technologies to the new challenges, we can observe a very interesting trend toward using the functional paradigm. The concepts of functional programming languages are very well suited to concurrent systems. Referential transparency, lazy evaluation, control over side-effects, immutable variables, and functions as first-class citizens help define maintainable and scalable solutions to the basic problems of parallel computing. The advantages of such an approach are clearly visible in HPC environments, where massively parallel solutions are needed. Providing novel services and solutions for the complex real-life problems of modern societies creates a growing demand for very fast solutions to computationally demanding problems. For example, planning complex urban road systems requires gathering results from large-scale simulations,9, 10 which are only feasible using massive parallelization. Similarly, in real-time scheduling tasks, complex optimization problems have to be solved within a single second.11, 12 Such challenges can greatly benefit from technologies based on the functional paradigm, which simplify the development process and lower the barrier for utilizing modern HPC hardware. In this special section, we have three interesting papers focusing on different issues arising in highly concurrent and distributed systems. They all adopt the functional paradigm and show its potential to solve problems of efficient utilization of available hardware. The first paper, authored by Krzywicki et al,8 tackles concurrent computations expressed using the agent paradigm. The paper introduces a new formal description of the execution model for agent-based computing systems in the form of an adaptive dataflow decoupled from the domain-specific semantics of the computation. The authors have shown that the execution models studied in previous work can be unified in this common model. The parameters of the model, such as queuing policies and granularity of the data in the flow are analyzed. Several queueing alternatives are benchmarked to demonstrate how they affect the efficiency of the computation. Using the example of a multi-agent evolutionary optimization problem solver, the new approach is shown to outperform the classic one. This proposed model is well suited to functional languages and can be easily mapped onto different classes of hardware—from simple single-core computers to distributed environments. The second paper, authored by Berenyi et al,3 focuses on linear algebraic expressions, stating that they are the essence of many computationally intensive problems, including scientific simulations and machine learning applications. However, translating high-level formulations of these expressions to efficient machine-level representations is far from trivial: developers should be assisted by automatic optimization tools so that they can focus their attention on high-level problems rather than low-level details. The tractability of these optimizations is highly dependent on the choice of the primitive constructs in terms of which the computations are expressed. In this work, the authors propose describing operations on multi-dimensional arrays using a selection of higher-order functions, inspired by functional programming, and present rewrite rules for these that can optimize them automatically for modern hierarchical and heterogeneous architectures. Using this formalism, the authors systematically construct and analyze different subdivisions and permutations of the dense matrix multiplication problem. The final paper, authored by Ciolczyk et al,5 focuses on the problem of tracing agent-based systems at large scale. At scale, assuming of course that the system considered is distributed, there are situations where processing messages within one of the actors fails—often due to failures that had occurred earlier in the system. Tracking down the origin of the failure can be difficult since existing monitoring tools only provide ways to collect metrics and statistical information about system execution. In this paper, the authors describe a new tool for tracing distributed actor systems—the Akka Tracing Tool—which allows users to generate a trace graph of messages. To address the distributed nature of the environment, the authors propose an efficient data collection mechanism based on the one-way replication technique implemented in CouchDB—a popular document database. The tool was evaluated in a distributed environment of up to 50 nodes, set up in the Amazon Web Services computing cloud, on a real application: car traffic simulation. The overhead measured when tracing all messages was between 39% to 45% on average. The library also proved to be scalable with respect to the number of nodes in the actor system and to be user-friendly. Thanks to these properties, the authors expect that the tool can simplify finding errors and speed up the development process of actor systems. The renaissance of the functional paradigm is a fact—languages like Haskell and Erlang find more and more industrial applications, and functional concepts are being introduced into classic object-oriented technologies such as Java and .NET. While this trend may not result in a complete paradigm-shift, “paradigm-mix” is already well established. The concepts inspired by functional approach help in building highly concurrent systems in various technologies. Nevertheless, many problems of massive parallelism still remain open. We believe that the work presented in this special section is a valuable step toward methods for building efficient, scalable, and robust software for modern multicore and multimode hardware platforms. Wojciech Turek, Aleksander Byrski, John Hughes 0001, Kevin Hammond, Marek Zaionc |
Concurr. Comput. Pract. Exp. | 4 |
| 2018 | Finding parallel functional pearls: Automatic parallel recursion scheme detection in Haskell functions via anti-unification
Adam D. Barwell, Christopher Brown 0002, Kevin Hammond |
Future Gener. Comput. Syst. | 3 |
| 2018 | Special section on functional paradigm for high performance computing
Aleksander Byrski, Katarzyna Rycerz, John Hughes 0001, Kevin Hammond |
Future Gener. Comput. Syst. | 4 |
| 2018 | Automatically deriving cost models for structured parallel processes using hylomorphisms
David Castro-Perez, Kevin Hammond, Susmit Sarkar, Yasir Alguwaifli |
Future Gener. Comput. Syst. | 2 |
| 2018 | Reengineering for parallelism in heterogeneous parallel platforms
José Daniel García, Kevin Hammond, Lutz Schubert |
J. Supercomput. | 2 |
| 2018 | Proof-relevant Horn Clauses for Dependent Type Inference and Term SynthesisabstractAbstract First-order resolution has been used for type inference for many years, including in Hindley-Milner type inference, type-classes, and constrained data types. Dependent types are a new trend in functional languages. In this paper, we show that proof-relevant first-order resolution can play an important role in automating type inference and term synthesis for dependently typed languages. We propose a calculus that translates type inference and term synthesis problems in a dependently typed language to a logic program and a goal in the proof-relevant first-order Horn clause logic. The computed answer substitution and proof term then provide a solution to the given type inference and term synthesis problem. We prove the decidability and soundness of our method. Frantisek Farka, Ekaterina Komendantskaya, Kevin Hammond |
Theory Pract. Log. Program. | 3 |
| 2017 | Type-Based Cost Analysis for Lazy Functional Languages
Steffen Jost, Pedro B. Vasconcelos, Mário Florido, Kevin Hammond |
J. Autom. Reason. | 4 |
| 2016 | Kindergarten cop: dynamic nursery resizing for GHCabstractGenerational garbage collectors are among the most popular garbage collectors used in programming language runtime systems. Their performance is known to depend heavily on choosing the appropriate size of the area where new objects are allocated (the nursery). In imperative languages, it is usual to make the nursery as large as possible, within the limits imposed by the heap size. Functional languages, however, have quite different memory be- haviour. In this paper, we study the effect that the nursery size has on the performance of lazy functional programs, through the interplay between cache locality and the frequency of collections. We demonstrate that, in contrast with imperative programs, having large nurseries is not always the best solution. Based on these re- sults, we propose two novel algorithms for dynamic nursery resiz- ing that aim to achieve a compromise between good cache locality and the frequency of garbage collections. We present an implemen- tation of these algorithms in the state-of-the-art GHC compiler for the functional language Haskell, and evaluate them using an exten- sive benchmark suite. In the best case, we demonstrate a reduction in total execution times of up to 88.5%, or an 8.7 overall speedup, compared to using the production GHC garbage collector. On aver- age, our technique gives an improvement of 9.3% in overall perfor- mance across a standard suite of 63 benchmarks for the production GHC compiler. Henrique Ferreiro, Laura M. Castro, Vladimir Janjic, Kevin Hammond |
CC | 4 |
| 2016 | Farms, pipes, streams and reforestation: reasoning about structured parallel processes using types and hylomorphismsabstractThe increasing importance of parallelism has motivated the creation of better abstractions for writing parallel software, including structured parallelism using nested algorithmic skeletons. Such approaches provide high-level abstractions that avoid common problems, such as race conditions, and often allow strong cost models to be defined. However, choosing a combination of algorithmic skeletons that yields good parallel speedups for a program on some specific parallel architecture remains a difficult task. In order to achieve this, it is necessary to simultaneously reason both about the costs of different parallel structures and about the semantic equivalences between them. This paper presents a new type-based mechanism that enables strong static reasoning about these properties. We exploit well-known properties of a very general recursion pattern, hylomorphisms, and give a denotational semantics for structured parallel processes in terms of these hylomorphisms. Using our approach, it is possible to determine formally whether it is possible to introduce a desired parallel structure into a program without altering its functional behaviour, and also to choose a version of that parallel structure that minimises some given cost model. David Castro-Perez, Kevin Hammond, Susmit Sarkar |
ICFP | 2 |
| 2016 | Coinductive Soundness of Corecursive Type Class Resolution
Frantisek Farka, Ekaterina Komendantskaya, Kevin Hammond |
LOPSTR | 3 |
| 2016 | RPL: A Domain-Specific Language for Designing and Implementing Parallel C++ ApplicationsabstractParallelising sequential applications is usually a very hard job, due to many different ways in which an application can be parallelised and a large number of programming models (each with its own advantages and disadvantages) that can be used. In this paper, we describe a method to semi-automatically generate and evaluate different parallelisations of the same application, allowing programmers to find the best parallelisation without significant manual reengineering of the code. We describe a novel, high-level domain-specific language, Refactoring Pattern Language (RPL), that is used to represent the parallel structure of an application and to capture its extra-functional properties (such as service time). We then describe a set of RPL rewrite rules that can be used to generate alternative, but semantically equivalent, parallel structures (parallelisations) of the same application. We also describe the RPL Shell that can be used to evaluate these parallelisations, in terms of the desired extra-functional properties. Finally, we describe a set of C++ refactorings, targeting OpenMP, Intel TBB and FastFlow parallel programming models, that semi-automatically apply the desired parallelisation to the application's source code, therefore giving a parallel version of the code. We demonstrate how the RPL and the refactoring rules can be used to derive efficient parallelisations of two realistic C++ use cases (Image Convolution and Ant Colony Optimisation). Vladimir Janjic, Christopher Brown 0002, Kenneth MacKenzie, Kevin Hammond, Marco Danelutto, Marco Aldinucci, José Daniel García |
PDP | 4 |
| 2016 | HPC-GAP: engineering a 21st-century high-performance computer algebra systemabstractSummary Symbolic computation has underpinned a number of key advances in Mathematics and Computer Science. Applications are typically large and potentially highly parallel, making them good candidates for parallel execution at a variety of scales from multi‐core to high‐performance computing systems. However, much existing work on parallel computing is based around numeric rather than symbolic computations. In particular, symbolic computing presents particular problems in terms of varying granularity and irregular task sizes that do not match conventional approaches to parallelisation. It also presents problems in terms of the structure of the algorithms and data. This paper describes a new implementation of the free open‐source GAP computational algebra system that places parallelism at the heart of the design, dealing with the key scalability and cross‐platform portability problems. We provide three system layers that deal with the three most important classes of hardware: individual shared memory multi‐core nodes, mid‐scale distributed clusters of (multi‐core) nodes and full‐blown high‐performance computing systems, comprising large‐scale tightly connected networks of multi‐core nodes. This requires us to develop new cross‐layer programming abstractions in the form of new domain‐specific skeletons that allow us to seamlessly target different hardware levels. Our results show that, using our approach, we can achieve good scalability and speedups for two realistic exemplars, on high‐performance systems comprising up to 32000 cores, as well as on ubiquitous multi‐core systems and distributed clusters. The work reported here paves the way towards full‐scale exploitation of symbolic computation by high‐performance computing systems, and we demonstrate the potential with two major case studies. © 2016 The Authors.Concurrency and Computation: Practice and ExperiencePublished by John Wiley & Sons Ltd. Reimer Behrends, Kevin Hammond, Vladimir Janjic, Olexandr Konovalov, Steve Linton, Hans-Wolfgang Loidl, Patrick Maier 0001, Philip W. Trinder |
Concurr. Comput. Pract. Exp. | 2 |
| 2016 | PAEAN: Portable and scalable runtime support for parallel Haskell dialectsabstractAbstract Over time, several competing approaches to parallel Haskell programming have emerged. Different approaches support parallelism at various different scales, ranging from small multicores to massively parallel high-performance computing systems. They also provide varying degrees of control, ranging from completely implicit approaches to ones providing full programmer control. Most current designs assume a shared memory model at the programmer, implementation and hardware levels. This is, however, becoming increasingly divorced from the reality at the hardware level. It also imposes significant unwanted runtime overheads in the form of garbage collection synchronisation etc. What is needed is an easy way to abstract over the implementation and hardware levels, while presenting a simple parallelism model to the programmer. The PArallEl shAred Nothing runtime system design aims to provide a portable and high-level shared-nothing implementation platform for parallel Haskell dialects. It abstracts over major issues such as work distribution and data serialisation, consolidating existing, successful designs into a single framework. It also provides an optional virtual shared-memory programming abstraction for (possibly) shared-nothing parallel machines, such as modern multicore/manycore architectures or cluster/cloud computing systems. It builds on, unifies and extends, existing well-developed support for shared-memory parallelism that is provided by the widely used GHC Haskell compiler. This paper summarises the state-of-the-art in shared-nothing parallel Haskell implementations, introduces the PArallEl shAred Nothing abstractions, shows how they can be used to implement three distinct parallel Haskell dialects, and demonstrates that good scalability can be obtained on recent parallel machines. Jost Berthold, Hans-Wolfgang Loidl, Kevin Hammond |
J. Funct. Program. | 3 |
| 2015 | Type-Based Allocation Analysis for Co-recursion in Lazy Functional Languages
Pedro B. Vasconcelos, Steffen Jost, Mário Florido, Kevin Hammond |
ESOP | 4 |
| 2014 | Agricultural Reform: More Efficient Farming Using Advanced Parallel Refactoring ToolsabstractModern multicore systems offer huge computing potential. Exploiting large parallel systems is still a very challenging task, however, especially as many software developers still use overly-sequential programming models. refactoring tool support that allows the programmer to introduce and tune parallelism in an easy and effective way, exploiting high-level parallel patterns such as farms and pipelines. Using our approach, we achieve speedups of up to 21 on a 24-core shared-memory system for a number of realistic use-cases. Christopher Brown 0002, Vladimir Janjic, Kevin Hammond, Holger Schöner, Kamran Idrees, Colin W. Glass |
PDP | 3 |
| 2013 | Mapping parallel programs to heterogeneous CPU/GPU architectures using a Monte Carlo Tree SearchabstractThe single core processor, which has dominated for over 30 years, is now obsolete with recent trends increasing towards parallel systems, demanding a huge shift in programming techniques and practices. Moreover, we are rapidly moving towards an age where almost all programming will be targeting parallel systems. Parallel hardware is rapidly evolving, with large heterogeneous systems, typically comprising a mixture of CPUs and GPUs, becoming the mainstream. Additionally, with this increasing heterogeneity comes increasing complexity: not only does the programmer have to worry about where and how to express the parallelism, they must also express an efficient mapping of resources to the available system. This generally requires in-depth expert knowledge that most application programmers do not have. In this paper we describe a new technique that derives, automatically, optimal mappings for an application onto a heterogeneous architecture, using a Monte Carlo Tree Search algorithm. Our technique exploits high-level design patterns, targeting a set of well-specified parallel skeletons. We demonstrate that our MCTS on a convolution example obtained speedups that are within 5% of the speedups achieved by a hand-tuned version of the same application. Mehdi Goli 0001, John A. W. McCall, Christopher Brown 0002, Vladimir Janjic, Kevin Hammond |
IEEE Congress on Evolutionary Computation | 5 |
| 2013 | How to be a Successful Thief - Feudal Work Stealing for Irregular Divide-and-Conquer Applications on Heterogeneous Distributed Systems
Vladimir Janjic, Kevin Hammond |
Euro-Par | 2 |
| 2013 | Resource analyses for parallel and distributed coordinationabstractSUMMARY Predicting the resources that are consumed by a program component is crucial for many parallel or distributed systems. In this context, the main resources of interest are execution time, space and communication/synchronisation costs. There has recently been significant progress in resource analysis technology, notably in type‐based analyses and abstract interpretation. At the same time, parallel and distributed computing are becoming increasingly important. This paper synthesises progress in both areas to survey the state‐of‐the‐art in resource analysis for parallel and distributed computing. We articulate a general model of resource analysis and describe parallel/distributed resource analysis together with the relationship to sequential analysis. We use three parallel or distributed resource analyses as examples and provide a critical evaluation of the analyses. We investigate why the chosen analysis is effective for each application and identify general principles governing why the resource analysis is effective. Copyright © 2011 John Wiley & Sons, Ltd. Philip W. Trinder, M. I. Cole, Kevin Hammond, Hans-Wolfgang Loidl, Greg J. Michaelson |
Concurr. Comput. Pract. Exp. | 3 |
| 2013 | Easy composition of symbolic computation software using SCSCP: A new Lingua Franca for symbolic computation
Steve Linton, Kevin Hammond, Olexandr Konovalov, Christopher Brown 0002, Philip W. Trinder, Hans-Wolfgang Loidl, Peter Horn, Dan Roozemond |
J. Symb. Comput. | 2 |
| 2012 | Code-level timing analysis of embedded software: emsoft'12 invited talk session outlineabstractEmbedded systems are often business- or safety-critical, with strict timing requirements that have to be met for the information-processing. Code-level timing analysis (used to analyse software running on some given hardware w.r.t. its timing properties) is an indispensable technique for ascertaining whether or not these requirements are met. However, recent developments in hardware, especially multi-core processors, and in software organisation render analysis increasingly more difficult, thus challenging the evolution of timing analysis techniques. This special session aims to give an overview over the current state of the art and the future challenges w.r.t. code-level timing analysis and introduces TACLe, a recently started EU-funded networking activity targeting these challenges. Heiko Falk, Kevin Hammond, Kim G. Larsen, Björn Lisper, Stefan M. Petters |
EMSOFT | 2 |
| 2012 | Using Load Information in Work-Stealing on Distributed Systems with Non-uniform Communication Latencies
Vladimir Janjic, Kevin Hammond |
Euro-Par | 2 |
| 2012 | Automatic amortised analysis of dynamic memory allocation for lazy functional programsabstractThis paper describes the first successful attempt, of which we are aware, to define an automatic, type-based static analysis of resource bounds for lazy functional programs. Our analysis uses the automatic amortisation approach developed by Hofmann and Jost, which was previously restricted to eager evaluation. In this paper, we extend this work to a lazy setting by capturing the costs of unevaluated expressions in type annotations and by amortising the payment of these costs using a notion of lazy potential. We present our analysis as a proof system for predicting heap allocations of a minimal functional language (including higher-order functions and recursive data types) and define a formal cost model based on Launchbury's natural semantics for lazy evaluation. We prove the soundness of our analysis with respect to the cost model. Our approach is illustrated by a number of representative and non-trivial examples that have been analysed using a prototype implementation of our analysis. Hugo R. Simões, Pedro B. Vasconcelos, Mário Florido, Steffen Jost, Kevin Hammond |
ICFP | 5 |
| 2012 | Resource-Safe Systems Programming with Embedded Domain Specific Languages
Edwin C. Brady, Kevin Hammond |
PADL | 2 |
| 2012 | Introduction to the Special Issue on Automatic Program Generation for Embedded Systems
Kevin Hammond, Paul H. J. Kelly |
Sci. Comput. Program. | 1 |
| 2010 | Granularity-Aware Work-Stealing for Computationally-Uniform GridsabstractGood scheduling is important for ensuring effective use of Grid resources, while maximising parallel performance. In this paper, we show how a basic "Random-Stealing'' load balancing algorithm for computational Grids can be improved by using information about the task granularity of parallel programs. We propose several strategies (SSL, SLL and LLL) for using granularity information to improve load balancing, presenting results both from simulations and from a real implementation (the Grid-GUM Runtime System for Parallel Haskell). We assume a common model of task creation which subsumes both master/worker and data-parallel programming paradigms under a task-stealing work distribution strategy. Overall, we achieve improvement in runtime of up to 19.4% for irregular problems in the real implementation, and up to 40% for the simulations (typical improvements of more that 15% for irregular programs, and from 5-10% for regular ones). Our results show that, for computationally-uniform Grids, advanced load balancing methods that exploit granularity information generally have the greatest impact on reducing the runtimes of irregular parallel programs. Moreover, the more irregular the program is, the better the improvements that can be achieved. Vladimir Janjic, Kevin Hammond |
CCGRID | 2 |
| 2010 | Scrapping your inefficient engine: using partial evaluation to improve domain-specific language implementationabstractPartial evaluation aims to improve the efficiency of a program by specialising it with respect to some known inputs. In this paper, we show that partial evaluation can be an effective and, unusually, easy to use technique for the efficient implementation of embedded domain-specific languages. We achieve this by exploiting dependent types and by following some simple rules in the definition of the interpreter for the domain-specific language. We present experimental evidence that partial evaluation of programs in domain-specific languages can yield efficient residual programs whose performance is competitive with their Java and C equivalents and which are also, through the use of dependent types, verifiably resource-safe. Using our technique, it follows that a verifiably correct and resource-safe program can also be an efficient program Edwin C. Brady, Kevin Hammond |
ICFP | 2 |
| 2010 | Easy composition of symbolic computation software: a new lingua franca for symbolic computationabstractWe present the results of the first four years of the European research project SCIEnce (www.symbolic-computation.org), which aims to provide key infrastructure for symbolic computation research. A primary outcome of the project is that we have developed a new way of combining computer algebra systems using the Symbolic Computation Software Composability Protocol (SCSCP), in which both protocol messages and data are encoded in the OpenMath format. We describe SCSCP middleware and APIs, outline some implementations for various Computer Algebra Systems (CAS), and show how SCSCP-compliant components may be combined to solve scientific problems that can not be solved within a single CAS, or may be organised into a system for distributed parallel computations. Steve Linton, Kevin Hammond, Olexandr Konovalov, Abdallah Al Zain, Philip W. Trinder, Peter Horn, Dan Roozemond |
ISSAC | 2 |
| 2010 | Static determination of quantitative resource usage for higher-order programsabstractWe describe a new automatic static analysis for determining upper-bound functions on the use of quantitative resources for strict, higher-order, polymorphic, recursive programs dealing with possibly-aliased data. Our analysis is a variant of Tarjan's manual amortised cost analysis technique. We use a type-based approach, exploiting linearity to allow inference, and place a new emphasis on the number of references to a data object. The bounds we infer depend on the sizes of the various inputs to a program. They thus expose the impact of specific inputs on the overall cost behaviour. Steffen Jost, Kevin Hammond, Hans-Wolfgang Loidl, Martin Hofmann 0001 |
POPL | 2 |
| 2010 | Correct-by-Construction Concurrency: Using Dependent Types to Verify Implementations of Effectful Resource Usage ProtocolsabstractIn the modern, multi-threaded, multi-core programming environment, correctly managing system resources, including locks and shared variables, can be especially difficult and errorprone. A simple mistake, such as forgetting to release a lock, can have major consequences on the correct operation of a program, by, for example, inducing deadlock, often at a time and location that is isolated from the original error. In this paper, we propose a new type-based approach to resource management, based on the use of dependent types to construct a Domain-Specific Embedded Language (DSEL) whose typing rules directly enforce the formal program properties that we require. In this way, we ensure strong static guarantees of correctness-by-construction, without requiring the development of a new special-purpose type system or the associated special-purpose soundness proofs. We also reduce the need for “over-serialisation”, the overly-conservative use of locks that often occurs in manually constructed software, where formal guarantees cannot be exploited. We illustrate our approach by implementing a DSEL for concurrent programming and demonstrate its applicability with reference to an example based on simple bank account transactions. Edwin C. Brady, Kevin Hammond |
Fundam. Informaticae | 2 |
| 2009 | "Carbon Credits" for Resource-Bounded Computations Using Amortised Analysis
Steffen Jost, Hans-Wolfgang Loidl, Kevin Hammond, Norman Scaife, Martin Hofmann 0001 |
FM | 3 |
| 2008 | Parallelism without Pain: Orchestrating Computational Algebra Components into a High-Performance Parallel SystemabstractThis paper describes a very high-level approach that aims to orchestrate sequential components written using high-level domain-specific programming into high-performance parallel applications. By achieving this goal, we hope to make parallel programming more accessible to experts in mathematics, engineering and other domains. A key feature of our approach is that parallelism is achieved without any modification to the underlying sequential computational algebra systems, or to the user-level components: rather, all orchestration is performed at an outer level, with sequential components linked through a standard communication protocol, the Symbolic Computing Software Composability Protocol, SCSCP. Despite the generality of our approach, our results show that we are able to achieve very good, and even, in some cases, super-linear, speedups on clusters of commodity workstations: up to a factor of 33.4 on a 28-processor cluster. We are, moreover, able to parallelise a wider variety of problem, and achieve higher performance than typical specialist parallel computational algebra implementations. Abdallah Al Zain, Philip W. Trinder, Kevin Hammond, Olexandr Konovalov, Steve Linton, Jost Berthold |
ISPA | 3 |
| 2007 | SymGrid: A Framework for Symbolic Computation on the Grid
Kevin Hammond, Abdallah Al Zain, Gene Cooperman, Dana Petcu, Philip W. Trinder |
Euro-Par | 1 |
| 2007 | Generic Access to Web and Grid-based Symbolic Computing Services: the SymGrid-Services FrameworkabstractModern grid and Web technologies provide straightforward access to applications and services running on remote resources. The user (which may be a software developer or even an application) should be able to discover such a service and dynamically load an interface to interact with it. While some software systems support either fully or partially automatic creation of client software to access Web services, fewer support grid services in the same way. This paper introduces a new system that automatically generates client software to allow access to both grid and Web services. Although designed as a stand-alone tool for accessing any Web or grid service, we demonstrate its usefulness in the context of the SymGrid framework for grid-based symbolic computations. Alexandru Cârstea, Marc Frîncu, Georgiana Macariu, Dana Petcu, Kevin Hammond |
ISPDC | 5 |
| 2006 | A verified staged interpreter is a verified compilerabstractDependent types and multi-stage programming have both been used, separately, in programming language design and implementation. Each technique has its own advantages --- with dependent types, we can verify aspects of interpreters and compilers such as type safety and stack invariants. Multi-stage programming, on the other hand, can give the implementor access to underlying compiler technology; a staged interpreter is a translator. In this paper, we investigate the combination of these techniques. We implement an interpreter for a simply typed lambda calculus, using dependent types to guarantee correctness properties by construction. We give explicit proofs of these correctness properties, then add staging annotations to generate a translator from the interpreter. In this way, we have constructed a verified compiler from a verified staged interpreter. We illustrate the application of the technique by considering a simple staged interpreter that provides guarantees for some simple resource bound properties, as might be found in a domain specific language for real-time embedded systems. Edwin C. Brady, Kevin Hammond |
GPCE | 2 |
| 2003 | Hume: A Domain-Specific Language for Real-Time Embedded Systems
Kevin Hammond, Greg J. Michaelson |
GPCE | 1 |
| 2002 | Parallel Programming: Models, Methods and Programming Languages
Kevin Hammond |
Euro-Par | 1 |
| 2000 | The Multi-architecture Performance of the Parallel Functional Language GP H (Research Note)
Philip W. Trinder, Hans-Wolfgang Loidl, Ed. Barry Jr., Kei Davis, Kevin Hammond, Ulrike Klusik, Simon L. Peyton Jones, Álvaro J. Rebón Portillo |
Euro-Par | 5 |
| 1999 | Engineering parallel symbolic programs in GPHabstractWe investigate the claim that functional languages offer low-cost parallelism in the context of symbolic programs on modest parallel architectures. In our investigation we present the first comparative study of the construction of large applications in a parallel functional language, in our case in Glasgow Parallel Haskell (GPH). The applications cover a range of application areas, use several parallel programming paradigms, and are measured on two very different parallel architectures. On the applications level the most significant result is that we are able to achieve modest wall-clock speedups (between factors of 2 and 10) over the optimised sequential versions for all but one of the programs. Speedups are obtained even for programs that were not written with the intention of being parallelised. These gains are achieved with a relatively small programmer-effort. One reason for the relative ease of parallelisation is the use of evaluation strategies, a new parallel programming technique that separates the algorithm from the co-ordination of parallel behaviour. On the language level we show that the combination of lazy and parallel evaluation is useful for achieving a high level of abstraction. In particular we can describe top-level parallelism, and also preserve module abstraction by describing parallelism over the data structures provided at the module interface (‘data-oriented parallelism’). Furthermore, we find that the determinism of the language is helpful, as is the largely implicit nature of parallelism in GPH. Copyright © 1999 John Wiley & Sons, Ltd. Hans-Wolfgang Loidl, Philip W. Trinder, Kevin Hammond, Sahalu B. Junaidu, Richard G. Morgan, Simon L. Peyton Jones |
Concurr. Pract. Exp. | 3 |
| 1998 | Algorithms + Strategy = ParallelismabstractThe process of writing large parallel programs is complicated by the need to specify both the parallel behaviour of the program and the algorithm that is to be used to compute its result. This paper introduces evaluation strategies : lazy higher-order functions that control the parallel evaluation of non-strict functional languages. Using evaluation strategies, it is possible to achieve a clean separation between algorithmic and behavioural code. The result is enhanced clarity and shorter parallel programs. Evaluation strategies are a very general concept: this paper shows how they can be used to model a wide range of commonly used programming paradigms, including divide-and-conquer parallelism, pipeline parallelism, producer/consumer parallelism, and data-oriented parallelism. Because they are based on unrestricted higher-order functions, they can also capture irregular parallel structures. Evaluation strategies are not just of theoretical interest: they have evolved out of our experience in parallelising several large-scale parallel applications, where they have proved invaluable in helping to manage the complexities of parallel behaviour. Some of these applications are described in detail here. The largest application we have studied to date, Lolita, is a 40,000 line natural language engineering system. Initial results show that for these programs we can achieve acceptable parallel performance, for relatively little programming effort. Philip W. Trinder, Kevin Hammond, Hans-Wolfgang Loidl, Simon L. Peyton Jones |
J. Funct. Program. | 2 |
| 1996 | GUM: A Portable Parallel Implementation of HaskellabstractGUM is a portable, parallel implementation of the Haskell functional language. Despite sustained research interest in parallel functional programming, GUM is one of the first such systems to be made publicly available.GUM is message-based, and portability is facilitated by using the PVM communications harness that is available on many multi-processors. As a result, GUM is available for both shared-memory (Sun SPARCserver multiprocessors) and distributed-memory (networks of workstations) architectures. The high message-latency of distributed machines is ameliorated by sending messages asynchronously, and by sending large packets of related data in each message.Initial performance figures demonstrate absolute speedups relative to the best sequential compiler technology. To improve the performance of a parallel Haskell program GUM provides tools for monitoring and visualising the behaviour of threads and of processors during execution. Philip W. Trinder, Kevin Hammond, James S. Mattson Jr., Andrew S. Partridge, Simon L. Peyton Jones |
PLDI | 2 |
| 1996 | Benchmarking Implementations of Functional Languages with 'Pseudoknot', a Float-Intensive BenchmarkabstractAbstract Over 25 implementations of different functional languages are benchmarked using the same program, a floating-point intensive application taken from molecular biology. The principal aspects studied are compile time and execution time for the various implementations that were benchmarked. An important consideration is how the program can be modified and tuned to obtain maximal performance on each language implementation. With few exceptions, the compilers take a significant amount of time to compile this program, though most compilers were faster than the then current GNU C compiler (GCC version 2.5.8). Compilers that generate C or Lisp are often slower than those that generate native code directly: the cost of compiling the intermediate form is normally a large fraction of the total compilation time. There is no clear distinction between the runtime performance of eager and lazy implementations when appropriate annotations are used: lazy implementations have clearly come of age when it comes to implementing largely strict applications, such as the Pseudoknot program. The speed of C can be approached by some implementations, but to achieve this performance, special measures such as strictness annotations are required by non-strict implementations. The benchmark results have to be interpreted with care. Firstly, a benchmark based on a single program cannot cover a wide spectrum of ‘typical’ applications. Secondly, the compilers vary in the kind and level of optimisations offered, so the effort required to obtain an optimal version of the program is similarly varied. Pieter H. Hartel, Marc Feeley, Martin Helmut Alt, Lennart Augustsson, Marcel Beemster, Emmanuel Chailloux, Christine H. Flood, Wolfgang Grieskamp, John H. G. van Groningen, Kevin Hammond, Bogumil Hausman, Melody Y. Ivory, Richard E. Jones, Jasper Kamperman, Peter Lee 0001, Xavier Leroy, Rafael Dueire Lins, Sandra Loosemore, Niklas Röjemo, Manuel Serrano, Jean-Pierre Talpin, Jon Thackray, Pum Walters, Pierre Weis, Peter Wentworth |
J. Funct. Program. | 11 |
| 1996 | Type Classes in HaskellabstractThis article defines a set of type inference rules for resolving overloading introduced by type classes, as used in the functional programming language Haskell. Programs including type classes are transformed into ones which may be typed by standard Hindley-Milner inference rules. In contrast to other work on type classes, the rules presented here relate directly to Haskell programs. An innovative aspect of this work is the use of second-order lambda calculus to record type information in the transformed program. Cordelia V. Hall, Kevin Hammond, Simon L. Peyton Jones, Philip Wadler |
ACM Trans. Program. Lang. Syst. | 2 |
| 1994 | Type Classes in Haskell
Cordelia V. Hall, Kevin Hammond, Simon L. Peyton Jones, Philip Wadler |
ESOP | 2 |