Deductive Derivation of Parallel Programs
Published 27 August 2007
Peter Pepper
Citations15
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
This paper explores possibilities for adapting a rigorous and formal methodology for program development to the derivation of parallel programs, with particular emphasis on two questions: How can the partitioning of the data space be expressed on a high and abstract level.
Abstract
The idea of a rigorous and formal methodology for program development has been successfully applied to sequential programs. In this paper we explore possibilities for adapting this methodology to the derivation of parallel programs. Particular emphasis is given to two questions: How can the partitioning of the data space be expressed on a high and abstract level? Which kinds of functional forms do lead in a natural way to parallel implementations?
Keywords
Computer Science
Journal of the Operational Research SocietyIntroduction to Algorithms
16,942 Citations1991V. J. Rayward‐Smith, Thomas H. Cormen +2 more
The Science of Programming
1,430 Citations1981David Gries
Describes basic programming principles and their step-by- step applications and shows how to apply them to real-world problems.
ACM Transactions on Programming Languages and SystemsA Distributed Algorithm for Minimum-Weight Spanning Trees
1,137 Citations1983Robert G. Gallager, P.A. Humblet +1 more
A distributed algorithm is presented that constructs the minimum-weight spanning tree in a connected undirected graph with distinct edge weights that can be initiated spontaneously at any node or at any subset of nodes.
CERN Document Server (European Organization for Nuclear Research)Algorithmic skeletons : structured management of parallel computation
876 Citations1989Murray Cole
This book introduces a new approach to the design and implementation of software systems which will help users of large scale parallel systems coordinate many concurrent activities toward a single goal and proposes a selection of independent algorithmic skeletons which describes the structure of a particular style of algorithm.
Lecture notes in computer scienceParallel programming using skeleton functions
275 Citations1993John Darlington, A. J. Field +5 more
Performance will be generally poor unless the issue of resource allocation is addressed explicitly, diminishing the advantage of using a functional language in the first place.
Algorithmic Language and Program Development
137 Citations1982Friedrich L. Bauer, H. Woessner
This chapter discusses the construction of Routines, a type of programming language, and some of the techniques used to design and implement these systems.
Lecture notes in computer sciencePerfect pipelining: A new loop parallelization technique
125 Citations1988Alex Aiken, Alexandru Nicolau
A new transformation is presented, Perfect Pipelining, that bridges the gap between fine- and coarse-grain transformations while retaining the desirable features of both and is accomplished even in the presence of conditional branches and resource constraints.
Theoretical Computer ScienceA theory for nondeterminism, parallelism, communication, and concurrency
102 Citations1986Manfred Broy
The presented language allows to treat the basic semantic notions of nondeterminism, parallelism, communication, and concurrency for multiprogramming in a completely formal, applicative framework and provides a semantic theory for networks of loosely coupled, nondeterministic, communicating, stream processing functions.
ACM Transactions on Programming Languages and SystemsOptimal parallel generation of a computation tree form
74 Citations1985Ilan Bar‐On, Uzi Vishkin
Given a general arithmetic expression, a computation binary tree representation in O(n) time using n processors on a concurrent-read, exclusive-write, parallel random-access machine is found.
Constructive Methods in Computing Science
57 Citations1989Manfred Broy
The notion of propositions as types within the context of Per Martin-LM's theory of types is explained and the relationship between constructive and classical logic is also discussed.
ACM Transactions on Programming Languages and SystemsAn exercise in the formal derivation of parallel programs: maximum flows in graphs
23 Citations1990Edgar Knapp
A new method is applied for the development of parallel programs to the problem of finding maximum flows in graphs that uses predicate transformer semantics to define a set of basic operators for the specification and verification of programs.
Parallel-program transformation using a metalanguage
22 Citations1991Jaehyung Yang, Young-il Choo
This paper describes how program transformation using a rnetalanguage can be an effective methodology for developim~gcorrect and efficient parallel programs.
Optimal schedules for parallel prefix computation with bounded resources
21 Citations1991Alexandru Nicolau, Haigeng Wang
This work shows optimal schedules for parallel pre x computation with a xed number of resources p 2 for a pre x of size N p(p + 1)=2, and presents a pipelined form of optimal schedules with d2N=( p + 1)e + d(p 1)= 2e 1 time, which takes a constant overhead of d( p 1)+1 time more than the optimal schedules.
Science of Computer ProgrammingThe derivation of graph marking algorithms from distributed termination detection protocols
20 Citations1988Gérard Tel, Richard B. Tan +1 more
It is shown that on-the-fly garbage collection algorithms can be obtained by transforming distributed termination detection protocols and this approach leads to a novel and insightful derivation of, e.g., the concurrent garbage collectiongorithms of Dijkstra et al. and of Hudak and Keller.
Acta InformaticaOn parsing arithmetic expressions in a multiprocessing environment
18 Citations1982Fran�ois Baccelli, Thierry Fleury
Some decomposition of the parsing of the sentences of context-free grammars into sequences of independant sub-tasks is proposed, for which this decomposition provides an efficient parser for a multiprocessing environment.
Workshops in computingGenerating Efficient Portable Code for a Strict Applicative Language
16 Citations1992Wolfram Schulte, Wolfgang Grieskamp
The overall style of code generation for the strict applicative language OPAL is discussed, which uses an optimized variant of the classical reference counting scheme, resulting in a residual garbage collector and the capability to perform run-time-detected selective update on recursive data structures.
Programming with (Finite) Mappings
10 Citations1991Peter Pepper, Bernhard Möller
A unified view of “mappings” is presented, abstracting from their appearance as “routines” or “map-like data structures”, which is able to develop algorithms at a very high level of abstraction, without losing the potential of implementing them efficiently in terms of arrays and loops.
Lecture notes in computer scienceLiterate program derivation: A case study
6 Citations2005Peter Pepper
This paper attempts to combine the principal ideas of literate programming with the concepts of formal program development, based on algebraic specifications and transformations, using the sublinear string-searching algorithm of Boyer and Moore (1977) as an illustrating example.
ACM SIGPLAN NoticesParallel-program transformation using a metalanguage
5 Citations1991Jaehyung Yang, Young-il Choo
ACM SIGPLAN NoticesOptimal schedules for parallel prefix computation with bounded resources
4 Citations1991Alexandru Nicolau, Haigeng Wang
Lecture notes in computer scienceInterleaving partitions of systolic algorithms for programming distributed memory multiprocessors
3 Citations1991A. Fernández, J. M. Liabería +2 more
A systematic method for mapping systolizable problems onto Distributed Memory Multiprocessors permits to increase the granularity of the parallel algorithm reducing in this way the communication requirements.