Implicit parallel programming models typically give less parallelism control to the programmer, but require less specialised expertise. Explicit parallel models, on the other hand, give much greater parallelism control, but can require significant expertise from the programmer. In this paper, we introduce a novel semi-implicit parallel model, called Elysium, for Idris. Elysium therefore demonstrates semi-explicit parallelism for an emerging class of languages known as dependently-typed languages. These dependently-typed languages encourage safer software via their ability to express strong logical guarantees, in the form of proofs, directly in code. Our semi-implicit approach is based on a process model that uses dependent types to guarantee parallelism properties. We demonstrate how we can use this semi-implicit process model to build common algorithmic skeletons, including farms, pipelines and divide and conquer skeletons. We evaluate our process skeleton approach on a number of examples, achieving speedups of up to 22 on a 28-core machine.

Dependent types provide users with the tools to embody specifications in types, with implementations carrying proofs that the specifications are met. One approach to developing programs in a dependently typed language develops such programs by enriching simply typed programs through a process of refactoring.

Algorithmic skeletons are an effective, pattern-based approach for parallelising software. However, despite implementations for a range of languages and paradigms, there is currently no support for dependently-typed languages, such as Idris, Agda and Coq. Such languages promote safer software via the ability to express logical properties and specifications, along with their proofs, directly in code. In this paper, we present pi-par, a prototype dependently-typed language based on Idris, with message-passing concurrency and built-in Pipeline and Task Farm skeletons. We evaluate pi-par on a series of standard Task Farm and Pipeline examples, achieving speedups of up to 23.35 × on a 28-core machine.

Refactoring is a common task in writing and maintaining software. Refactoring tools are available for a wide variety of programming languages, and they are intended to transform source code without altering the functional behaviour of the software being refactored. However, even though most refactoring tools are designed with this criterion in mind, and programmers expect it, their implementations do not provide formal guarantees of correctness. To address this limitation, we propose a methodology for extending refactoring implementations with correctness guarantees. Our approach leverages dependently-typed languages and techniques to guard refactoring implementations with proofs of conformance to formal specifications. We illustrate our proposed methodology using a renaming refactoring that includes correctness guarantees as an integral part of its implementation.

Non-functional properties, such as energy, time, and security (ETS) are becoming increasingly important in Cyber-Physical Systems (CPS) programming. This article describes TeamPlay, a research project funded under the EU Horizon 2020 programme between January 2018 and June 2021. TeamPlay aimed to provide the system designer with a toolchain for developing embedded applications where ETS properties are first-class citizens, allowing the developer to reflect directly on energy, time and security properties at the source code level. In this paper we give an overview of the TeamPlay methodology, introduce the challenges and solutions of our approach and summarise the results achieved. Overall, applying our TeamPlay methodology led to an improvement of up to 18% performance and 52% energy usage over traditional approaches.

Cyber attacks become more and more prevalent every day. One type of cyber attack is known as a side channel attack, where attackers exploit information leakage from the physical execution of a program, e.g. timing or power leakage, to uncover secret information, such as encryption keys or other sensitive data. There have been various attempts at addressing the problem of preventing side-channel attacks, often relying on various measures to decrease the discernibility of several code variants or code paths. Most techniques require a high-degree of expertise by the developer, who often employs ad hoc, hand-crafted code-patching in an attempt to make it more secure. In this paper, we take a different approach: building on the idea of ladderisation, inspired by Montgomery Ladders. We present a semi-automatic tool-supported technique, aimed at the non-specialised developer, which refactors (a class of) C programs into functionally (and even algorithmically) equivalent counterparts with improved security properties. Our approach provides refactorings that transform the source code into its ladderised equivalent, driven by an underlying verified rewrite system, based on dependent types. Our rewrite system automatically finds rewritings of selected C expressions, facilitating the production of their equivalent ladderised counterparts for a subset of C. We demonstrate our approach on a number of representative examples from the cryptographic domain, showing increased security.

This paper presents COMPROF and COMPLACE, a novel profiling tool and thread placement technique for shared-memory architectures that requires no recompilation or user intervention. We use dynamic binary instrumentation to intercept memory operations and estimate inter-thread communication overhead, deriving (and possibly visualising) a communication graph of data-sharing between threads. We then use this graph to map threads to cores in order to optimise memory traffic through the memory system. Different paths through a system’s memory hierarchy have different latency, throughput and energy properties, COMPLACE exploits this heterogeneity to provide automatic performance and energy improvements for multithreaded programs. We demonstrate COMPLACE on the NAS Parallel Benchmark (NPB) suite where, using our technique, we are able to achieve improvements of up to 12% in the execution time and up to 10% in the energy consumption (compared to default Linux scheduling) while not requiring any modification or recompilation of the application code.

SummaryThis 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.

Parallel patterns are a high-level programming paradigm that enables non-experts in parallelism to develop structured parallel programs that are maintainable, adaptive, and portable whilst achieving good performance on a variety of parallel systems. However, there still exists a large base of legacy-parallel code developed using ad-hoc methods and incorporating low-level parallel/concurrency libraries such as pthreads without any parallel patterns in the fundamental design. This code would benefit from being restructured and rewritten into pattern-based code. However, the process of rewriting the code is laborious and error-prone, due to typical concurrency and pthreading code being closely intertwined throughout the business logic of the program. In this paper, we present a new software restoration methodology, to transform legacy-parallel programs implemented using pthreads into structured farm and pipeline patterned equivalents. We demonstrate our restoration technique on a number of benchmarks, allowing the introduction of patterned farm and pipeline parallelism in the resulting code; we record improvements in cyclomatic complexity and speedups on a number of representative benchmarks.

The Generic Reusable Parallel Pattern Interface (GrPPI) is a very useful abstraction over different parallel pattern libraries, allowing the programmer to write generic patterned parallel code that can easily be compiled to different backends such as FastFlow, OpenMP, Intel TBB and C++ threads. However, rewriting legacy code to use GrPPI still involves code transformations that can be highly non-trivial, especially for programmers who are not experts in parallelism. This paper describes software refactorings to semi-automatically introduce instances of GrPPI patterns into sequential C++ code, as well as safety checking static analysis mechanisms which verify that introducing patterns into the code does not introduce concurrency-related bugs such as race conditions. We demonstrate the refactorings and safety-checking mechanisms on four simple benchmark applications, showing that we are able to obtain, with little effort, GrPPI-based parallel versions that accomplish good speedups (comparable to those of manually-produced parallel versions) using different pattern backends.

This paper presents a new technique for introducing and tuning parallelism for heterogeneous shared-memory systems (comprising a mixture of CPUs and GPUs), using a combination of algorithmic skeletons (such as farms and pipelines), Monte–Carlo tree search for deriving mappings of tasks to available hardware resources, and refactoring tool support for applying the patterns and mappings in an easy and effective way. Using our approach, we demonstrate easily obtainable, significant and scalable speedups on a number of case studies showing speedups of up to 41 over the sequential code on a 24-core machine with one GPU. We also demonstrate that the speedups obtained by mappings derived by the MCTS algorithm are within 5–15% of the best-obtained manual parallelisation.

Parallel pattern libraries offer a strong combination of abstraction and performance. However, discovering places in sequential code where parallel patterns should be introduced is still highly non-trivial, often requiring expert manual analysis and profiling. We present a hybrid discovery technique to detect instances of parallel patterns in sequential code. This employs both static and dynamic trace-based analysis, together with hotspot detection. We evaluate our pattern discovery mechanism on a number of representative benchmarks. We evaluate the performance of the resulting parallelised benchmarks on a 24core parallel machine.

Funding: European Union’s Horizon 2020 research and innovation programme under grant agreement No 779882.

Systems with non-functional requirements, such as Energy, Time and Security (ETS), are of increasing importance due to the proliferation of embedded devices with limited resources such as drones, wireless sensors, and tablet computers. Currently, however, there are little to no programmer supported methodologies or frameworks to allow them to reason about ETS properties in their source code. Drive is one such existing framework supporting the developer by lifting non-functional properties to the source-level through the Contract Specification Language (CSL), allowing non-functional properties to be first-class citizens, and supporting programmer-written code-level contracts to guarantee the non-functional specifications of the program are met. In this paper, we extend the Drive system by providing rigorous implementations of the underlying proof-engine, modeling the specification of the annotations and assertions from CSL for a representative subset of C, called Imp. We define both an improved abstract interpretation that automatically derives proofs of assertions, and define inference algorithms for the derivation of both abstract interpretations and the context over which the interpretation is indexed. We use the dependently-typed programming language, Idris, to give a formal definition, and implementation, of our abstract interpretation. Finally, we show our well-formed abstract interpretation over some representative exemplars demonstrating provable assertions of ETS.

Energy, Time and Security (ETS) properties of programs are becoming increasingly prioritised by developers, especially where applications are running on ETS sensitive systems, such as embedded devices or the Internet of Things. Moreover, developers currently lack tools and language properties to allow them to reason about ETS. In this paper, we introduce a new contract specification framework, called Drive, which allows a developer to reason about ETS or other non-functional properties of their programs as first-class properties of the language. Furthermore, we introduce a contract specification language, allowing developers to reason about these first-class ETS properties by expressing contracts that are proved correct by an underlying formal type system. Finally, we show our contract framework over a number of representable examples, demonstrating provable worst-case ETS properties.

This paper describes a new technique for identifying potentially parallelisable code structures in functional programs. Higher-order functions enable simple and easily understood abstractions that can be used to implement a variety of common recursion schemes, such as maps and folds over traversable data structures. Many of these recursion schemes have natural parallel implementations in the form of algorithmic skeletons. This paper presents a technique that detects instances of potentially parallelisable recursion schemes in Haskell 98 functions. Unusually, we exploit anti-unification to expose these recursion schemes from source-level definitions whose structures match a recursion scheme, but which are not necessarily written directly in terms of maps, folds, etc. This allows us to automatically introduce parallelism, without requiring the programmer to structure their code a priori in terms of specific higher-order functions. We have implemented our approach in the Haskell refactoring tool, HaRe, and demonstrated its use on a range of common benchmarking examples. Using our technique, we show that recursion schemes can be easily detected, that parallel implementations can be easily introduced, and that we can achieve real parallel speedups (up to 23.79x the sequential performance on 28 physical cores, or 32.93x the sequential performance with hyper-threading enabled). (C) 2017 Elsevier B.V. All rights reserved.

Evolutionary multi-agent systems (EMAS) play a critical role in many artificial intelligence applications that are in use today. In this paper, we present a new generic skeleton in Erlang for parallel EMAS computations. The skeleton enables us to capture a wide variety of concrete evolutionary computations that can exploit the same underlying parallel implementation. We demonstrate the use of our skeleton on two different evolutionary computing applications: (1) computing the minimum of the Rastrigin function; and (2) solving an urban traffic optimisation problem. We show that we can obtain very good speedups (up to 142.44 $$\times $$ the sequential performance) on a variety of different parallel hardware, while requiring very little parallelisation effort.