Iterative program optimization is known to be able to adapt more easily to particular programs and target hardware than model-based approaches. An approach is to generate random program transformations and evaluate their profitability by applying them and benchmarking the transformed program on the target hardware. This procedure’s large computational effort impairs its practicality tremendously, though. To address this limitation, we pursue the guidance of a genetic algorithm for program optimization via feedback from surrogate performance models. We train the models on program transformations that were evaluated during previous iterative optimizations. Our representation of programs and program transformations refers to the polyhedron model. The representation is particularly meaningful for an optimization of loop programs that profit a from coarse-grained parallelization for execution on modern multicore-CPUs. Our evaluation reveals that surrogate performance models can be used to speed up the optimization of loop programs. We demonstrate that we can reduce the benchmarking effort required for an iterative optimization and degrade the resulting speedups by an average of 15%.

Performance optimization of stencil codes requires data locality improvements. The polyhedron model for loop transformation is well suited for such optimizations with established techniques, such as the PLuTo algorithm and diamond tiling. However, in the domain of our project ExaStencils, stencil codes, it fails to yield optimal results. As an alternative, we propose a new, optimized, multi-dimensional polyhedral search space exploration and demonstrate its effectiveness: we obtain better results than existing approaches in several cases. We also propose how to specialize the search for the domain of stencil codes, which dramatically reduces the exploration effort without significantly impairing performance.

The purpose of a domain-specific language (DSL) is to enable the application programmer to specify a problem, or an abstract algorithm description, in his/her domain of expertise without being burdened by implementation details. The ideal scenario is that the implementation detail is added in an automatic process of program translation and code generation. The approach of domain-specific program generation has lately received increasing attention in the area of computational science and engineering. In this paper, we introduce the new code generation framework Athariac. Its goal is to support the quick implementation of a language processing and program optimization platform for a given DSL based on stepwise term rewriting. We demonstrate the framework's use on our DSL ExaSlang for the specification and optimization of multigrid solvers. On this example, we provide evidence of Athariac's potential for making domain-specific software engineering more productive.

Summary SPIRAL is an autotuning, program generation, and code synthesis system that offers a fully automatic generation of highly optimized target codes, customized for the specific execution platform at hand. Initially, SPIRAL was targeted at problem domains in digital signal processing, later also at basic linear algebra. We open SPIRAL up to a new, practically relevant and challenging domain: multigrid solvers. SPIRAL is driven by algebraic transformation rules. We specify a set of such rules for a simple multigrid solver with a Richardson smoother for a discretized square 2D Poisson equation with Dirichlet boundary conditions. We present the target code that SPIRAL generates in static single‐assignment form and discuss its performance. While this example required no changes of or extensions to the SPIRAL system, more complex multigrid solvers may require small adaptations.

Here, stencil codes are compute-intensive algorithms, in which data points arranged in a large grid are being recomputed repeatedly from the values of data points in a predefined neighborhood. This fixed neighborhood pattern is called a stencil. Stencils codes see wide-spread use in computing the discrete solutions of partial differential equations and systems composed of such equations.

This special issue of Concurrency and Computation: Practice and Experience contains revised and extended versions of selected papers presented at the conference Euro-Par 2016.Euro-Par-the European Conference on Parallel Computing-is an annual series of international conferences dedicated to the promotion and advancement of all aspects of parallel and distributed computing.Euro-Par covers a wide spectrum of topics from algorithms and theory to software technology and hardware-related issues, with application areas ranging from scientific to mobile and cloud computing.The major part of the Euro-Par audience consists of researchers in academic institutions, government laboratories, and industrial organisations.Euro-Par 2016, the 22nd conference in the Euro-Par series, was held in Grenoble, France.It was organised by Inria, Université Grenoble-Alpes, and IUT 2 Grenoble.Twelve broad topics were defined and advertised, covering a large variety of aspects of parallel and distributed computing.The call for papers attracted a total of 176 submissions.The submitted papers were reviewed at least 3 and, in most cases, 4 or even more times (4 reviews on average).A total of 47 papers were finally accepted for publication.This makes a global acceptance rate of 26.7 %.The authors of accepted papers came from 20 countries, with the 4 main contributing countries-France, the United States, Germany, and Spain-accounting for a bit more than half of them.Compared to the conference version, this framework is enhanced further with the availability of customized CUDA kernels and a multiple-GPU implementation with almost linear scalability.The reviewers appreciated the high quality and scientific soundness of the treatise.Concluding this preface, we would like to thank Prof Geoffrey Fox, editor-in-chief of Concurrency and Computation: Practice and Experience, for his support of this special issue.We

The polyhedron model is a powerful model to identify and apply systematically loop transformations that improve data locality (e.g., via tiling) and enable parallelization. In the polyhedron model, a loop transformation is, essentially, represented as an affine function. Well-established algorithms for the discovery of promising transformations are based on performance models. These algorithms have the drawback of not being easily adaptable to the characteristics of a specific program or target hardware. An iterative search for promising loop transformations is more easily adaptable and can help to learn better models. We present an iterative optimization method in the polyhedron model that targets tiling and parallelization. The method enables either a sampling of the search space of legal loop transformations at random or a more directed search via a genetic algorithm. For the latter, we propose a set of novel, tailored reproduction operators. We evaluate our approach against existing iterative and model-driven optimization strategies. We compare the convergence rate of our genetic algorithm to that of random exploration. Our approach of iterative optimization outperforms existing optimization techniques in that it finds loop transformations that yield significantly higher performance. If well configured, then random exploration turns out to be very effective and reduces the need for a genetic algorithm.

This special issue of Concurrency and Computation: Practice and Experience contains revised and extended versions of selected papers presented at the conference Euro-Par 2015.Euro-Par-the European Conference on Parallel Computing-is an annual series of international conferences dedicated to the promotion and advancement of all aspects of parallel and distributed computing.Euro-Par covers a wide spectrum of topics from algorithms and theory to software technology and hardware-related issues, with application areas ranging from scientific to mobile and cloud computing.The major part of the Euro-Par audience consists of researchers in academic institutions, government laboratories and industrial organisations.Euro-Par 2015, the 21st conference in the Euro-Par series, was held in Vienna, Austria.It was organised by the Research Group for Parallel Computing of the Vienna University of Technology (TU Wien).Thirteen broad topics were defined and advertised, covering a large variety of aspects of parallel and distributed computing.The call for papers attracted a total of 190 submissions.The submitted papers were reviewed at least three and, in most cases, four or even more times (four reviews on average).A total of 51 papers were finally accepted for publication.This makes a global acceptance rate of 27 %.The authors of accepted papers came from 21 countries, with the four main contributing countries-the United States, France, Spain and Germany-accounting for a bit more than half of them.Based on the results of the reviews and a majority opinion of the respective topic programme committees, a number of papers were recommended for this special issue.The authors were contacted at the conference and invited to submit revised and extended versions of their papers.These new versions were reviewed independently by three reviewers; two had previously reviewed the conference version, the third had not.Eventually, four papers were accepted for publication.This year, two Euro-Par topics are represented-both covering methods of programming modern computer architectures.Topic 13 on Accelerator Computing is represented with three papers.The paper Performance optimization of sparse matrix-vector multiplication for multi-component PDE-based applications using GPUs, authored by Ahmad Abdelfattah, Hatem Ltaief, David Keyes and Jack Dongarra [1], describes the implementation of a single-GPU and multi-GPU kernel for block-sparse matrix-vector multiplication, a problem that appears in the discretisation of partial differential equations with many dependent variables.The performance of the kernel is measured on a subset of the Florida Sparse Matrix Collection.Especially noted by the reviewers was the uniform interface that applies to a wide range of problem sizes via tunable parameters.This makes it perform efficiently on a wide range of GPU architectures running CUDA.The paper Fast parallel skew and prefix-doubling suffix array construction on the GPU, authored by Leyuan Wang, Sean Baxter and John D. Owens [2], proposes a hybrid GPU implementation of known algorithms for constructing suffix arrays of a string that fits the given GPU architecture best.One highlight pointed out in the reviews is a highly efficient segmented sorting primitive, which is also valuable as independent result.The paper Performance and portability of accelerated lattice Boltzmann applications with OpenACC, authored by Enrico Calore, Jiri Kraus, Sebastiano Fabio Schifano and Raffaele Tripiccione [3], reports on a performance study based on a simple performance model of an OpenACCbased lattice Boltzmann implementation on three different architectures: an NVIDIA GPU, an AMD GPU and a multi-core CPU.The practical relevance of this work was particularly appreciated.

Today, many software systems are configurable with conditional compilation. Just like any software system, configurable systems need to be refactored in their evolution, but their inherent variability induces an additional dimension of complexity that is not addressed well by current academic and industrial refactoring engines. To improve the state of the art, we propose a variability-aware refactoring approach that relies on a canonical variability representation and recent work on variability-aware analysis. The goal is to preserve the behavior of all variants of a configurable system, without compromising general applicability and scalability. To demonstrate practicality, we developed Morpheus, a sound, variability-aware refactoring engine for C code with preprocessor directives. We applied Morpheus to three substantial real-world systems (Busybox, OpenSSL, and SQLite) showing that it scales reasonably well, despite of its heavy reliance on satisfiability solvers. By extending a standard approach of testing refactoring engines with support for variability, we provide evidence for the correctness of the refactorings implemented.

SUMMARY MapReduce frameworks allow programmers to write distributed, data‐parallel programs that operate on multisets. These frameworks offer considerable flexibility to support various kinds of programs and data. To understand the essence of the programming model better and to provide a rigorous foundation for optimizations, we present an abstract, functional model of MapReduce along with a number of customization options. We demonstrate that the MapReduce programming model can also represent programs that operate on lists, which differ from multisets in that the order of elements matters. Along with the functional model, we offer a cost model that allows programmers to estimate and compare the performance of MapReduce programs. Based on the cost model, we introduce two transformation rules aiming at performance optimization of MapReduce programs, which also demonstrates the usefulness of our model. In an exploratory study, we assess the impact of applying these rules to two applications. The functional model and the cost model provide insights at a proper level of abstraction into why the optimization works. Copyright © 2014 John Wiley & Sons, Ltd.

This special issue of Concurrency and Computation: Practice and Experience contains revised and extended versions of selected papers presented at the conference Euro-Par 2014.Euro-Par-the European Conference on Parallel Computing-is an annual series of international conferences dedicated to the promotion and advancement of all aspects of parallel and distributed computing.Euro-Par covers a wide spectrum of topics from algorithms and theory to software technology and hardware-related issues, with application areas ranging from scientific to mobile and cloud computing.The major part of the Euro-Par audience consists of researchers in academic institutions, government laboratories and industrial organisations.Euro-Par 2014, the 20th conference in the Euro-Par series, was held in Porto, Portugal.It was organised by the Computer Science Department of the Faculty of Sciences of the University of Porto.Fifteen broad topics were defined and advertised, covering a large variety of aspects of parallel and distributed computing.The call for papers attracted a total of 267 submissions.The submitted papers were reviewed at least three, and in most cases, four, times (4.02 on average).A total of 68 papers were finally accepted for publication.This makes a global acceptance rate of 25.5%.The authors of accepted papers came from 29 countries, with the four main contributing countries-France, the United States, Spain and Germany-accounting for about 55% of them.Based on the results of the reviews and a majority opinion of the respective topic programme committees, several papers were recommended for a special journal issue.The authors were contacted at the conference and invited to submit revised and extended versions of their papers.These new versions were reviewed independently by three reviewers; two had previously reviewed the conference version, the third had not.Eventually, four papers were accepted for publication.They cover the following four Euro-Par topics: Performance Prediction and Evaluation, Distributed Systems and Algorithms, Theory and Algorithms for Parallel Computation and High-Performance and Scientific Applications.Topic 2 on Performance Prediction and Evaluation contributes the paper Performance prediction of dynamic task-based runtime system for heterogeneous multi-core architectures authored by Luka Stanisic, Samuel Thibault, Arnaud Legrand, Brice Videau and Jean-François Méhaut [1].They address the challenge of deciding, with high accuracy and low effort, what computations to offload onto accelerators on a heterogeneous execution platform.Their coarse-grain hybrid simulation/emulation of StarPU ‡ on SimGrid, a versatile simulator for distributed systems, yields performance predictions of dense linear algebra applications in a matter of seconds and with an accuracy of within a few percent.The reviewers appreciated particularly the volume of experimental results and analysis on a wide range of heterogeneous platforms.Topic 8 on Distributed Systems and Algorithms is represented by the paper A comparative study of spanning tree and gossip protocols for aggregation authored by Lehel Nyers and Márk Jelasity [2].The authors provide a carefully designed comparative study of two paradigms for distributed aggregation queries, like average and sum: gossiping and tree algorithms.With a demonstration suite covering different practical topologies and scenarios, they identify the dominating distinguishing influences and do away with stereotypes such as 'gossip is slow and expensive' and 'trees are fragile and complicated'.The reviewers valued the experimental framework as an effective decision tool for choosing between the two paradigms.Topic 12 on Theory and Algorithms for Parallel Computation contributes the paper On constructing DAG-schedules with large AREAs authored by Scott T.

International audience

Present-day automatic optimization relies on powerful static (i.e., compile-time) analysis and transformation methods. One popular platform for automatic optimization is the polyhedron model. Yet, after several decades of development, there remains a lack of empirical evidence of the model's benefits for real-world software systems. We report on an empirical study in which we analyzed a set of popular software systems, distributed across various application domains. We found that polyhedral analysis at compile time often lacks the information necessary to exploit the potential for optimization of a program's execution. However, when conducted also at run time, polyhedral analysis shows greater relevance for real-world applications. On average, the share of the execution time amenable to polyhedral optimization is increased by a factor of nearly 3. Based on our experimental results, we discuss the merits and potential of polyhedral optimization at compile time and run time.

The advent of variability management and generator technology enables users to derive individual variants from a variable code base based on a selection of desired configuration options. This approach gives rise to the generation of possibly billions of variants that, however, cannot be efficiently analyzed for errors with classic analysis techniques. To address this issue, researchers and practitioners usually apply sampling heuristics. While sampling reduces the analysis effort significantly, the information obtained is necessarily incomplete and it is unknown whether sampling heuristics scale to billions of variants. Recently, researchers have begun to develop variability-aware analyses that analyze the variable code base directly exploiting the similarities among individual variants to reduce analysis effort. However, while being promising, so far, variability-aware analyses have been applied mostly only to small academic systems. To learn about the mutual strengths and weaknesses of variability-aware and sampling-based analyses of software systems, we compared the two strategies by means of two concrete analysis implementations (type checking and liveness analysis), applied them to three subject systems: Busybox, the x86 Linux kernel, and OpenSSL. Our key finding is that variability-aware analysis outperforms most sampling heuristics with respect to analysis time while preserving completeness.

International audience

International audience

Superimposition is a composition technique that has been applied successfully in many areas of software development. Although superimposition is a general-purpose concept, it has been (re)invented and implemented individually for various kinds of software artifacts. We unify languages and tools that rely on superimposition by using the language-independent model of feature structure trees (FSTs). On the basis of the FST model, we propose a general approach to the composition of software artifacts written in different languages. Furthermore, we offer a supporting framework and tool chain, called FEATUREHOUSE. We use attribute grammars to automate the integration of additional languages. In particular, we have integrated Java, C#, C, Haskell, Alloy, and JavaCC. A substantial number of case studies demonstrate the practicality and scalability of our approach and reveal insights into the properties that a language must have in order to be ready for superimposition. We discuss perspectives of our approach and demonstrate how we extended FEATUREHOUSE with support for XML languages (in particular, XHTML, XMI/UML, and Ant) and alternative composition approaches (in particular, aspect weaving). Rounding off our previous work, we provide here a holistic view of the FEATUREHOUSE approach based on rich experience with numerous languages and case studies and reflections on several years of research.

Software-merging techniques face the challenge of finding a balance between precision and performance. In practice, developers use unstructured-merge (i.e., line-based) tools, which are fast but imprecise. In academia, many approaches incorporate information on the structure of the artifacts being merged. While this increases precision in conflict detection and resolution, it can induce severe performance penalties. Striving for a proper balance between precision and performance, we propose a structured-merge approach with auto-tuning. In a nutshell, we tune the merge process on-line by switching between unstructured and structured merge, depending on the presence of conflicts. We implemented a corresponding merge tool for Java, called JDime. Our experiments with 8 real-world Java projects, involving 72 merge scenarios with over 17 million lines of code, demonstrate that our approach indeed hits a sweet spot: While largely maintaining a precision that is superior to the one of unstructured merge, structured merge with auto-tuning is up to 12 times faster than purely structured merge, 5 times on average.

An ongoing problem in revision control systems is how to resolve conflicts in a merge of independently developed revisions. Unstructured revision control systems are purely text-based and solve conflicts based on textual similarity. Structured revision control systems are tailored to specific languages and use language-specific knowledge for conflict resolution. We propose semistructured revision control systems that inherit the strengths of both: the generality of unstructured systems and the expressiveness of structured systems. The idea is to provide structural information of the underlying software artifacts --- declaratively, in the form of annotated grammars. This way, a wide variety of languages can be supported and the information provided can assist in the automatic resolution of two classes of conflicts: ordering conflicts and semantic conflicts. The former can be resolved independently of the language and the latter using specific conflict handlers. We have been developing a tool that supports semistructured merge and conducted an empirical study on 24 software projects developed in Java, C#, and Python comprising 180 merge scenarios. We found that semistructured merge reduces the number of conflicts in 60% of the sample merge scenarios by, on average, 34%, compared to unstructured merge. We found also that renaming is challenging in that it can increase the number of conflicts during semistructured merge, and that a combination of unstructured and semistructured merge is a pragmatic way to go.

Abstract Preface for the special issue on Euro‐Par 2009. Copyright © 2010 John Wiley & Sons, Ltd.

This special issue of Concurrency and Computation: Practice and Experience contains revised and extended versions of selected papers presented at the Euro-Par 2010 conference.Euro-Par-the European Conference on Parallel Computing-is an annual series of international conferences dedicated to the promotion and the advancement of all aspects of parallel and distributed computing.Euro-Par covers a wide spectrum of topics from algorithms and theory to software technology and hardware-related issues, with application areas ranging from scientific to mobile and cloud computing.The main audience of Euro-Par are the researchers in academic institutions, government laboratories, and industrial organizations.Euro-Par 2010, the 16th conference in the Euro-Par series, was organized by the Institute for High Performance Computing and Networking of the Italian National Research Council and was held at the Hotel Continental Terme on the Italian island of Ischia, in the Naples Bay.Fourteen broad topics were defined and advertised, covering a large variety of aspects of parallel and distributed computing.The call for papers attracted a total of 256 submissions.The submitted papers were reviewed at least three and, in many cases, four times.A total of 90 papers were finally accepted for publication.This makes a global acceptance rate of 35%.The authors of the accepted papers come from 24 countries, with the four main contributing countries-USA, France, Spain, and Germany-accounting for about 55% of the authors.The distribution of authors followed the pattern typical for a Euro-Par conference: of the 10 authors, this year, six have been academic researchers, three PhD students, and one from industry.The topical distribution of the papers in the proceedings of Euro-Par 2010 reflects the current trends in the field of parallel and distributed computing: 18 of 90 papers are devoted to the relatively new topic Multicore and Manycore Programming.This figure was 11 in 2009 and was even lower in 2008 when the subject was part of the topic High-Performance Architectures and Compilers.On the other hand, the well-established Euro-Par topics such as Support Tools and Environments or Scheduling and Load-Balancing, for instance, have remained quite stable throughout the years.These figures demonstrate that the topic structure of Euro-Par has the flexibility to adapt to current trends in a wide spectrum of research areas.With its topic structure, Euro-Par has been filling two complementary rôles: as a regular meeting place for established communities and as a place to develop new communities.In recent years, the latter rôle has been strengthened by the introduction of satellite workshops, at which researchers can meet initially and form a new community that later settles and flourishes in other fora.In 2010, the number of satellite workshops was higher than ever before, 11, and we strive to have it grow further, maintaining the Euro-Par claim of being the wide-spectrum conference on parallelism in Europe.Returning to the spread of papers in 2010, based on the results of the reviews and a majority opinion of the topic program committees, several papers were recommended for a special journal issue.The authors were contacted at the conference and invited to submit revised and extended versions of their papers.These new versions were reviewed independently by three reviewers; two had also reviewed the conference version, the third had not.Eventually, eight papers were accepted for publication.

Over 30 years ago, the preprocessor cpp was developed to extend the programming language C by lightweight metaprogramming capabilities. Despite its error-proneness and low abstraction level, the preprocessor is still widely used in present-day software projects to implement variable software. However, not much is known about how cpp is employed to implement variability. To address this issue, we have analyzed forty open-source software projects written in C. Specifically, we answer the following questions: How does program size influence variability? How complex are extensions made via cpp's variability mechanisms? At which level of granularity are extensions applied? Which types of extension occur? These questions revive earlier discussions on program comprehension and refactoring in the context of the preprocessor. To provide answers, we introduce several metrics measuring the variability, complexity, granularity, and types of extension applied by preprocessor directives. Based on the collected data, we suggest alternative implementation techniques. Our data set is a rich source for rethinking language design and tool support.

Feature-oriented software development (FOSD) aims at the construction, customization, and synthesis of large-scale software systems. We propose a novel software design paradigm, called feature-oriented design, that takes the distinguishing characteristics of FOSD into account, especially the clean and consistent mapping between features and their implementations as well as the tendency of features to interact inadvertently. We extend the lightweight modeling language Alloy with support for feature-oriented design and call the extension Feature Alloy. By means of an implementation and four case studies, we demonstrate how feature-oriented design with Feature Alloy facilitates separation of concerns, variability, and reuse of models of individual features and helps defining and detecting semantic dependences and interactions between features.

Superimposition is a composition technique that has been applied successfully in many areas of software development. Although superimposition is a general-purpose concept, it has been (re)invented and implemented individually for various kinds of software artifacts. We unify languages and tools that rely on superimposition by using the language-independent model of feature structure trees (FSTs). On the basis of the FST model, we propose a general approach to the composition of software artifacts written in different languages, Furthermore, we offer a supporting framework and tool chain, called FEATUREHOUSE. We use attribute grammars to automate the integration of additional languages, in particular, we have integrated Java, C#, C, Haskell, JavaCC, and XML. Several case studies demonstrate the practicality and scalability of our approach and reveal insights into the properties a language must have in order to be ready for superimposition.

Abstract Preface for the special issue on Euro‐Par 2007. Copyright © 2009 John Wiley & Sons, Ltd.

Feature-oriented programming (FOP) is a paradigm that incorporates programming language technology, program generation techniques, and stepwise refinement. In their GPCE'07 paper, Thaker et al. suggest the development of a type system for FOP to guarantee safe feature composition, i.e, to guarantee the absence of type errors during feature composition. We present such a type system along with a calculus for a simple feature-oriented, Java-like language, called Feature Featherweight Java (FFJ). Furthermore, we explore four extensions of FFJ and how they affect type soundness.

Feature oriented refactoring (FOR) is the process of decomposinga program into features, where a feature is an increment in programfunctionality. We develop a theory of FOR that relates code refac-toring to algebraic factoring. Our theory explains relationshipsbetween features and their implementing modules, and why fea-tures in different programs of a product-line can have differentimplementations. We describe a tool and refactoring methodologybased on our theory, and present a validating case study.

Aspect-oriented programming is a promising paradigm that challenges traditional notions of program modularity. Despite its increasing acceptance, aspects have been documented to suffer limited reuse, hard to predict behavior, and difficult modular reasoning. We develop an algebraic model that relates aspects to program transformations and uncovers aspect composition as a significant source of the problems mentioned. We propose an alternative model of composition that eliminates these problems, preserves the power of aspects, and lays an algebraic foundation on which to build and understand AOP tools.

Abstract Tiling is a well‐known technique for sequential compiler optimization, as well as for automatic program parallelization. However, in the context of parallelization, tiling should not be considered as a stand‐alone technique, but should be applied after a dedicated parallelization phase, in our case after space–time mapping. We show how tiling can benefit from space–time mapping, and we derive an algorithm for computing tiles which can minimize the number of communication startups, taking the number of physically available processors into account. We also present how the use of a simple cost model reduces real execution time. Copyright © 2004 John Wiley & Sons, Ltd.

We present a hierarchical classification of specializations of the divide-and-conquer paradigm. The aim is to identify a subclass of divide-and-conquer algorithms with an efficient parallel implementation which can be viewed as a static space-time mapping. The specializations impose a balanced call tree, a fixed degree of the problem division, and elementwise operations. The correctness of our compile-time transformations is proved by equational reasoning in Haskell; recursion and iteration are handled by induction. We demonstrate the practicality of the skeleton by some examples, one of which is Strassen's matrix multiplication.

Abstract An SPMD parallel implementation schema for divide-and-conquer specifications is proposed and derived by formal refinement (transformation) of the specification schema. The specification is in the form of a mutually recursive functional definition. In a first phase, a parallel functional program schema is constructed which consists of a communication tree and a functional program that is shared by all nodes of the tree. The fact that this phase proceeds by semantics-preserving transformations in the Bird-Meertens formalism of higher-order functions guarantees the correctness of the resulting functional implementation. A second phase yields an imperative distributed message-passing implementation of this schema. The derivation process is illustrated with an example: a two-dimensional numerical integration algorithm.

Abstract A scheme is presented which transforms systolic programs with a two-dimensional structure to one dimension. The elementary steps of the transformation are justified by theorems in the theory of communicating sequential processes and the scheme is demonstrated with an example in occam: matrix composition/decomposition.

Abstract An experiment of a mechanical code generation for a programmable systolic computer is reported. Two‐dimensional systolic arrays are automatically reduced to one dimension, and code is generated for the one‐dimensional processor array Warp. The technique is demonstrated with two examples: matrix multiplication and LU decomposition.

Our concern is the mechanical certification of transformations of sequential program executions into parallel executions with equivalent semantics. The objective of such transformations is to accelerate the execution of programs. The result reported here is a mechanically certified theorem of optimality. We present a transformation which applies to every program in a particular programming language, the language of sorting networks. This transformation transforms the sequential execution of any sorting network into an execution which is as fast or faster than any other transformation which applies to every sorting network. The theorem is stated formally in a mechanized logic.