Speculative evaluation in lazy functional languagesSpeculative evaluation is a technique for extracting parallelism from a program by beginning the evaluation of some expressions before it is known whether their values are needed.
Andrew Partridge
Monday, 10 October 1994,
4:05 p.m. (Room F161)
This talk describes schemes for controlling speculative tasks, and gives simulation results for an idealised system incorporating speculative evaluation.
GHCI2 - An interpreter for Glasgow HaskellIf you want a program to run fast, your compiler's your only man. If you want to test or debug your program, though, a slow batch-mode compiler is the last thing you want. Using the Glasgow Haskell Compiler as a base, I have developed a Haskell interpreter which:
Alastair Reid
Monday, 17 October 1994
The G"odel Programming LanguageIn this seminar, I will discuss the programming language G\"odel, which is a declarative, general-purpose programming language in the family of logic programming languages.
J.W. Lloyd, University of Bristol
Monday, 24 October 1994
It is a strongly typed language, the type system being based on many-sorted logic with parametric polymorphism. It has a module system.
G\"odel supports infinite precision integers, infinite precision rationals, and also floating-point numbers. It can solve constraints over finite domains of integers and also linear rational constraints. It supports processing of finite sets. It also has a flexible computation rule and a pruning operator which generalises the commit of the concurrent logic programming languages. Considerable emphasis is placed on G\"odel's meta-logical facilities which provide significant support for meta-programs that do analysis, transformation, compilation, verification, debugging, and so on.
The declarative nature of G\"odel makes it particularly suitable for use as a teaching language, narrows the gap which currently exists between theory and practice in logic programming, makes possible advanced software engineering tools such as declarative debuggers and compiler generators, reduces the effort involved in providing a parallel implementation of the language, and offers substantial scope for parallelization in such implementations.
I will illustrate the main features of the language with various example programs.
Improving Granularity for Parallel Functional Programs:Winnow (v.): To treat (as grain) by exposure to a current of air so that waste matter is eliminated.
a Graphical Winnowing System for Haskell
Kevin Hammond
Monday, 31 October 1994
A big problem with writing parallel programs is choosing the optimal granularity, or size of task. It is even possible for parallel *slowdown* to occur as a result of choosing the wrong grain size, either through poor load distribution, excessive communication costs, or simply because of task creation overheads. The problem is most acute for distributed-memory machines, but still appears in shared-memory or dataflow machines.
In this talk, I will describe some experiments we have performed that expose the granularity of parallel functional programs, both for GRIP and for a detailed parallelism simulator. Our objective is to use these results to design tools that will help optimise granularity, either directly through manual placement of annotations, or indirectly through automated granularity analyses.
Preliminary planning for the Summer 95 Research Expo
Simon Peyton Jones (moderator)
Monday, 14 November 1994
Discussing the FP Group's plans for the Summer 95 Research Expo
John O'Donnell (moderator)
Monday, 21 November 1994
Automatic assessment of undergraduate SML programsQ) In a 9 week 1st year functional programming class of 100 students, each carries out 90 practical exercises in Standard ML. If it takes around 1 minute to mark each exercise, how long does a lecturer spend on marking per week on average?
Greg Michaelson, Heriot-Watt University
Monday, 28 November 1994
A) The Ceilidh system was developed at the University of Nottingham to support the automatic assessment of C programs by comparing their behaviours on test data sets with those of specimen answers. We have been extending Ceilidh to Standard ML as part of the TLTP Ceilidh consortium. As well as checking dynamic function behaviour, we assess students' abilities to identify type signatures. We also look at various simple aspects of functional programming style using program transformation techniques and suggest improvements to student functions. In this seminar the benefits and pitfalls of Ceilidh's empirical assessment of programs are discussed and our approach to the automatic assessment of functional programming style is presented.
Implementing a "paradigm oriented" parallel programming environment for static iterative algorithmsA more efficient control of the implicit parallelism in functional languages is possible if parallel algorithmic structures (or skeletons) are used in the design of the algorithm. A structure captures the behaviour of a parallel programming paradigm and acts as a template in the design of an algorithm.
Johann Schwarz, University of Hull
Conference Room, 4 p.m.
In this talk I will address the issue of defining a structure for static iterative transformation (SIT) algorithms which exploit coarse grained data parallelism. This will be followed by the description of a parallel implementation on a network of workstations. Details of the implementation which uses the Glasgow Haskell Compiler as well as examples will be presented.
Johann Schwarz is in the third year of a PhD in Computer Science at the University of Hull, working on a skeleton-based implementation of functional languages on parallel computers. He did his undergraduate degree in Computer Science at FH Regensburg, Germany and came to Hull in October 1992.
Time and space profiling for non-strict, higher-order functional languagesWe present the first profiler for a compiled, non-strict, higher-order, purely functional language capable of measuring {\em time} as well as {\em space} usage. Our profiler is implemented in a production-quality optimising compiler for Haskell, has low overheads, and can successfully profile large applications. A unique feature of our approach is that we give a formal specification of the attribution of execution costs to cost centres. This specification enables us to discuss our design decisions in a precise framework. Since it is not obvious how to map this specification onto a particular implementation, we also present an implementation-oriented operational semantics, and prove it equivalent to the specification. (This is the talk I will be giving at POPL'95)
Patrick Sansom
Conference Room, 4 p.m.
An overview of POPL '95
Simon Peyton Jones
Conference Room, 4 p.m.
The Glasgow Haskell compiler: recent developmentsI will review the second-half-of-'94 developments of the Glasgow Haskell compiler, now the undisputed king of Haskell compilers. I will illustrate the talk with some making-Haskell-go-fast tricks that you can then try in the privacy of your own home.
Will Partain
Conference Room, 4 p.m.
SchwammigsortThere are two key ideas behind Quicksort: a divide-and-conquer strategy and a highly efficient partitioning algorithm based on an unusual bidirectional loop. The usual way of expressing Quicksort in a functional language captures the divide-and-conquer but it replaces the bidirectional loop with a less efficient pair of list comprehensions.
John O'Donnell
Conference Room, 4 p.m.
It seems promising to try expressing the partitioning algorithm using bidirectional scan. This apparently leads to a clean method for deriving Quicksort, and it also leads to a parallel sorting algorithm with some very interesting properties. (We don't know whether this algorithm is already known, or whether it's new.) One interesting aspect of the work is that the algorithms are rather subtle, and we're finding it necessary to use formal methods in the discovery of the algorithms, not just in proving them correct after they are finished.
Many open questions remain. This talk is a report on current joint work with Gudula Ruenger.
Department seminar: parallel and distributed computing
Chris Jesshope
Conference Room or F161, 4 p.m.
Lennart Augustsson, Chalmers
structs: Filling the fourth corner
Conference Room, 4 pm
Constructive Regular Algebra and Views of DatatypesIn category theory the names given to type forming operations are borrowed from the terminology of arithmetic: The terminal object in a category is called a unit and denoted by 1; the type formed by considering pairs of elements, the first element of type A and the second of type B, is called the product of A and B and is denoted by AxB, the function space constructor is called exponentiation and denoted A^B, etc. A reason for doing so is that ``up to isomorphism'' these operations obey the usual laws of arithmetic: Product is associative and distributes through sum, exponentiation obeys the usual arithmetic law A^(B+C) = (A^B)x(A^C), etc. In regular algebra a similar naming convention is used. Concatenation of languages is called ``product'' and denoted by a multiplication sign, union of two languages is called ``sum'' and denoted by addition. The empty language is denoted by 0, and the language containing just the empty word is denoted by 1. There is a further analogy between regular algebra and arithmetic that has been used to observe the close correspondence between various path-finding algorithms and algorithms for inverting (real) matrices. Specifically, the * operator has properties in common with the function mapping a to 1/(1-a). For example, the star decomposition rule (a+b)* = b*.(a.b*)* corresponds to the rule of arithmetic: 1/(1-(a+b)) = (1/(1-b)).(1/(1-a/(1-b))) In 1980, Tarjan observed the theorem that two ``non-redundant'' regular expressions are equal if and only if their interpretations as functions on real values are equal, thus providing a formal link between regular algebra and real arithmetic. (``Non-redundant'' basically means that no use is made of the axiom a+a = a .) Returning to type forming operations, we may also interpret the * of regular algebra as the list type constructor. A regular expression thus denotes a datatype formed by some composition of the sum, product and list type constructors. The question then arises whether two non-redundant regular expressions denote isomorphic datatypes if and only if the two expressions are equal when interpreted as functions of real values. In this talk I will discuss progress towards solving this problem. The problem is a concrete instance of a general theory of ``views'' of datatypes that I am trying to develop, inspiration for this theory coming from an understanding of category theory as constructive lattice theory. Elements of the theory (in particular a constructive fixed point calculus), together with its practical relevance will also be discussed.
Roland Backhouse
Conference Room, 3pm
Graph Reduction in the Pi-CalculusSome new encodings of the lambda-calculus in Milner's pi-calculus are presented which model several practical graph reduction strategies: call-by-value, call-by-need and call-by-process. The programming language interest lies in the use of pi-calculus as an abstract yet realistic concurrent intermediate language. From a theoretical perspective, the pi-calculus representation of computational strategies with shared reductions is novel and answers a question raised by Milner. The encodings emerged from some earlier work on designing parallelising compilers for functional languages and have an intuitive appeal. A brief introduction to the pi-calculus will be given.
Gerald Ostheimer
Conference Room, 4 pm
Higher-Order Computation with ConstraintsIn this talk we survey the Concurrent Constraint Language Oz and its operational models, the Gamma- and Rho-Calculus.
Martin Mueller, Universitaet des Saarlandes
Conference Room, 4 pm
The recently developed programming language Oz integrates higher-order functional, object-oriented, and constraint programming including search. Operationally, this integration relies on a novel family of calculi which integrate higher-order abstractions with logic variables.
At its center, the Gamma-Calculus [Smolka 1994] captures the essentials of functional and object-oriented programming in Oz. Functional programming can be adequatly embedded into Gamma [Niehren 1994], where the logic variable allows to express lazy functional programming with the appropriate complexity (call-by-need) [Niehren 1995]. Apart from Lambda, the closest relative of Gamma is the Pi-Calculus, to which a relation is sketched.
The Gamma Calculus allows an elegant extension by constraints which is called Rho-Calculus [Niehren and Smolka 1994, Niehren and M"uller, 1995]. The Rho-Calculus models the third important programming style in Oz.
Gamma- and Rho-Calculus, as well as the language Oz are untyped. The great flexibility in terms of programming styles challenges the development of a type system for this kind of language. While the talk is not about types, remarks on typing issues will be given throughout.
*** On interest, a demonstration of the the DFKI Oz System can be given after the talk.
Discussion of the Haskell 1.3 Proposal
Alastair Reid, Yale University
Conference Room, 4 pm
Applying the Bird--Meertens FormalismThe Bird-Meertens formalism (BMF) of higher-order functions over lists has become popular for the calculational derivation of algorithms from specifications. This talk reports results of two case studies on the systematic use of BMF in the process of parallel program development.
To Parallel Program Development: Case Studies
Sergei Gorlatch, Universitaet Passau
Conference Room, 4 pm
First, we develop a parallel program for polynomial multiplication, starting with a straight-forward mathematical specification and arriving at a processor topology together with a program for each processor in it. The development process is based on formal transformations in BMF; design decisions concerning data partitioning, processor interconnections, etc. are governed by a type analysis and performance considerations. The SPMD target program is parameterized for an arbitrary number of processors; the choice of number either makes the program cost-optimal or enables logarithmic time complexity. We compare our results with systolic solutions to polynomial multiplication.
Second, a parallel implementation of divide-and-conquer template (skeleton) is derived systematically from a functional specification. A new topology, named N-graph, is introduced which has following properties: there are not more than 4 links per processor, overlapping of computations and communication within a processor is exploited, the processor network is of an arbitrary fixed size, the load is balanced and all communications between processors are local. The derivation proceeds by semantics-preserving transformations in BMF which guarantees the correctness of the parallel implementation. A parallel merge-sort algorithm is used to illustrate the derivation process and the target program with message passing.
University Holiday
Cancelled -- no meeting room is available.
Cancelled -- University Holiday
A prototype equational reasoning assistant(Note: this talk will be on Tuesday May 9, in the normal Formal Methods time slot, instead of Monday May 8.)
Andy Gill
Conference Room, 4 pm
One of the often quoted advantages of functional programming is the ability to perform proofs using equational reasoning. In practice, however, few proofs are ever performed, even on small programs. In order to allow non-trivial equational reasoning using Haskell, we have developed a prototype Equational Reasoning Assistant (ERA).
In this talk we present three aspects of the ERA system. We overview the problems involved with performing machine assisted equational reasoning. We discuss the design decisions taken during the prototypes construction. Finally we describe some interesting internals details of the ERA prototype.
Scheduling, Synchronisation and Coherence in Parallel Functional Transaction ProcessingPaul H. J. Kelly, Department of Computing, Imperial College, London, UK. (email phjk@doc.ic.ac.uk). We have been studying parallel functional programming in various forms for several years, with particular emphasis on optimising data movement using algebraic transformation of the source code. More recently we have also been looking at how best to maintain cache coherency in parallel graph reduction and related models (e.g. futures). In this talk I will present the results from a detailed study we have made of a single benchmark (originally from Phil Trinder at Oxford University, now at Glasgow) which has proven particularly rich and instructive.
Paul Kelly, Imperial College
Conference Room, 4 pm
The example, a pipelined functional formulation of a simple on-line transaction processing system, makes a good benchmark because of its spatial locality, data-dependent sharing, and because its high rate of synchronisation reflects a fundamental requirement of the algorithm (whereas in many parallel functional programs it is an implementation artifact).
We have built on Trinder's work, using program transformation to maximise parallelism by removing unnecessary control dependences, and to optimise grain size. Using simulation we isolate communication and scheduling issues. We ensure good scheduling by eliminating a source of unwanted blocking, and use a queueing model for load distribution to control space requirements. We simulate both a conventional cache-coherency protocol and a protocol which exploits the consistency requirements of the application. The revised protocol is shown to achieve the minimum number of messages required by the algorithm, and makes effective use of spatial locality with no invalidation.
(paper available from http://www-ala.doc.ic.ac.uk/papers/A.Bennett/)
Tupling - An Automatic Compile-Time Memoisation Transformation
Wei-Ngan Chin, National Universidy of Singapore
Room F171, 4 pm
The tupling transformation can be used to merge loops together by combining multiple recursive calls and also to eliminate redundant calls for a class of functional programs. The clever (and difficult) step of this transformation technique is to find appropriate sets of calls, called {\em eureka tuples}, which would allow each set of calls to be computed recursively from its previous set.
We present a tupling transformation algorithm which is able to systematically search for eureka tuples. This transformation algorithm is formulated for a sub-class of functions, with a single recursion parameter per function. The algorithm's termination can be guaranteed by applying two simple syntactic restrictions, called {\em non-NI-circular}\, and {\em bounded-arguments} restrictions.
Though it is nice to guarantee termination of the transformer, the imposed restrictions reduce the scope of the transformation algorithm. In order to alleviate this shortcoming, we also propose some additional pre-processing techniques.
Wei-Ngan Chin is presently a lecturer in the Department of Information Systems and Computer Science, National University of Singapore. He graduated with a BSc and an MSc from University of Manchester in 1982 and 1983 respectively, and a PhD from Imperial College, University of London in 1990. His present research interests are in functional programming, program transformation and parallel processing.
Derivation of a Fast Addition Circuit
John O'Donnell
This is joint work with Gudula Ruenger, Universitaet Saarbruecken.
We present a case study in the use of equational reasoning in a functional language: the derivation of a parallel binary addition circuit from an abstract mathematical specification.
This is an important algorithm since an adder lies on the critical path of most processors. Although the algorithm has been known for many years, our presentation of it is new, and is well-suited for the design of processor ALUs that require bidirectional communication. Furthermore, the derivation provides a precise explanation for a notoriously tricky algorithm.
The derivation requires several nontrivial steps. The aim is to express the addition using Scan and then apply the Parallel Tree Scan theorem. However, that theorem requires an associative auxiliary function, and the auxiliary function in the adder is not associative. We get around this difficulty by introducing a new technique: the partial evaluation of fold and scan.
Cancelled -- University Holiday
An Introduction to the Programming Language Forsythe
John C. Reynolds, Imperial College and Carnegie Mellon Univeristy
By using concepts of modern programming-language theory, such as higher-order procedures and intersection types, it is possible to design a programming language that is extremely general without being complicated. This thesis is illustrated by the language Forsythe, which is a descendent of Algol 60 intended to be as uniform and general as possible, while retaining the basic character of its progenitor.
Passivity and Linear Types
John C. Reynolds, Imperial College and Carnegie Mellon Univeristy
In various proposals (e.g. by Lafont, Wadler, and Abramsky) for programming languages based on intuitionistic linear logic, linear types describe values that are used exactly once, so that destructive operations are possible, while the "of course" type-constructor describes values that can be copied or discarded, as well as being used destructively.
One would expect that imperative languages could be translated into these linear-typed languages in such a way that state transformations become linear functions, reflecting the fact that states are never copied in imperative langauges. Such a translation, however, cannot deal with expressions that read parts of the same state concurrently.
To overcome this difficulty, we propose additional "passive" constructors describing values that can be copied or discarded, but are only subject to nondestructive "read-only" operations. Such values are obtained by temporarily "freezing" values of linear type.
In contrast to earlier proposals by Wadler, Odersky, and Swarup, Reddy, and Ireland, our language is an extension of a conventional language based on intuitionistic linear logic. To handle the unfreezing of passive values, it uses "regions" in a way suggested by Tofte's treatment of storage allocation in ML.