1.1 --- a/doc-isac/mlehnfeld/master/thesis/fundamentals.tex Wed Jul 23 14:09:51 2014 +0200
1.2 +++ b/doc-isac/mlehnfeld/master/thesis/fundamentals.tex Wed Jul 23 14:32:19 2014 +0200
1.3 @@ -13,7 +13,7 @@
1.4
1.5 In 1978 John Backus, who had been heavily involved in the design of \textit{Fortran} and \textit{ALGOL}, held a Turing award lecture which emphasized certain benefits of functional style languages over imperative programming. The document which resulted from the lecture \cite{backus1978can} strongly influenced and fueled research in the area of functional programming. Also in the mid 1970s, Robin Milner and others from the \textit{University of Edinburgh} designed the \textit{ML} {\em metalanguage} as a command language for the theorem prover {\em LCF} \cite{milner1978theory} (see section \ref{sec:ctp}). They continued the development of \textit{ML} and turned it into a stand-alone programming language. Even though it has impure features such as mutable references and an I/O system which is not side effect free, \textit{ML} is known as a functional programming language because it encourages a functional programming style. \textit{ML}'s type system employs the {\em Hindley–Milner type inference algorithm} (see section \ref{sec:hindleymilner}) which reduces the number of required type annotations because it can infer the types of expressions in most cases. Later, a standard for the language was established \cite{milner1997definition}, which resulted in the programming language \textit{Standard ML}.
1.6
1.7 -As a dozen non-strict languages (i.e. employing lazy evaluation) emerged in the 1980s, it was decided at a conference in 1987 that the parallel efforts should be merged into one common language as a basis for an exchange of ideas. This decision resulted in the formation of a commitee which created {\em Haskell} \cite{jones2003haskell}. Research around this purely functional, general-purpose programming language has produced many innovations in the area of functional programming during the last two decades.
1.8 +As a dozen non-strict languages (i.e. employing lazy evaluation) emerged in the 1980s, it was decided at a conference in 1987 that the parallel efforts should be merged into one common language as a basis for an exchange of ideas. This decision resulted in the formation of a committee which created {\em Haskell} \cite{jones2003haskell}. Research around this purely functional, general-purpose programming language has produced many innovations in the area of functional programming during the last two decades.
1.9
1.10 \subsection{Common Features}
1.11 There are certain distinguishing features which can be found in most contemporary functional programming languages. This section outlines the most prevalent ones (e.g., see \cite{hudak1989conception, haskell2013functional}).
1.12 @@ -22,7 +22,7 @@
1.13 The heavy use of immutable data has already been mentioned in section \ref{sec:funprog}. A consequence of pure functions is {\em referential transparency}, which is the property of computations which always yield equal results whenever they are invoked with the same input parameters. Later in this section we will see how pure languages enable e.g. input, output and exception handling whilst preserving purity.
1.14
1.15 \subsubsection{Recursion}
1.16 -Recursion is not a technique which is specific to functional programming. However, since loops require the use of mutable values (counter variables), recursion is used way more excessively than in imperative languages. Often, it is the only way to describe iterations. As recursion can easily cause an overflow of the call stack, most implementations of functional languages employ {\em tail call optimization}. This mechanism discards a function call's environment and thereby aviods creating a new stack frame for the recursive call and saves memory. This only works for true tail recursion, i.e. if the result of the recursive call is the result of the function itself.
1.17 +Recursion is not a technique which is specific to functional programming. However, since loops require the use of mutable values (counter variables), recursion is used way more excessively than in imperative languages. Often, it is the only way to describe iterations. As recursion can easily cause an overflow of the call stack, most implementations of functional languages employ {\em tail call optimization}. This mechanism discards a function call's environment and thereby avoids creating a new stack frame for the recursive call and saves memory. This only works for true tail recursion, i.e. if the result of the recursive call is the result of the function itself.
1.18
1.19 \subsubsection{Higher-Order Functions}
1.20 Higher-order functions (HOFs) are functions which expect other functions as their input parameters or have functions as their return values. Examples for frequently used HOFs are the {\em map} and {\em fold} operations, which apply other functions to lists of values as in the \textit{Standard ML} expression
1.21 @@ -32,7 +32,7 @@
1.22
1.23 \subsubsection{Purity and Effects}
1.24 \label{sec:pureeffects}
1.25 -Many functional programming languages such as \textit{Standard ML} encourage a purely funcional coding style. However, certain functionalities like memory I/O require developers to write impure code. Purely functional programming languages like \textit{Haskell} and \textit{Clean} do not permit any side effects and therefore use other mechanisms to accomplish the desired effects. The \textit{Haskell} developers decided to implement a language construct called {\em monad} \cite{jones2003haskell}. Monads can be described as representations of possibly impure computations. In order to preserve purity, functions which perform e.g. I/O operations have to accept monads as arguments or return them. Similarly, \textit{Clean} uses {\em uniqueness types} \cite{achten1995ins} which ensure that every function's type makes transparent to the environment, which mutable aspects of the environment it manipulates. This is accomplished by allowing these functions exactly one access to the denoted mutable data which they receive as arguments and whose manipulated versions are contained in their return values.
1.26 +Many functional programming languages such as \textit{Standard ML} encourage a purely functional coding style. However, certain functionality like memory I/O require developers to write impure code. Purely functional programming languages like \textit{Haskell} and \textit{Clean} do not permit any side effects and therefore use other mechanisms to accomplish the desired effects. The \textit{Haskell} developers decided to implement a language construct called {\em monad} \cite{jones2003haskell}. Monads can be described as representations of possibly impure computations. In order to preserve purity, functions which perform e.g. I/O operations have to accept monads as arguments or return them. Similarly, \textit{Clean} uses {\em uniqueness types} \cite{achten1995ins} which ensure that every function's type makes transparent to the environment, which mutable aspects of the environment it manipulates. This is accomplished by allowing these functions exactly one access to the denoted mutable data which they receive as arguments and whose manipulated versions are contained in their return values.
1.27
1.28 \subsubsection{Partial Function Evaluation}
1.29 Partial function evaluation facilitates applying less arguments to a function than it requires which results in another function that only requires the remaining arguments. E.g. the function \texttt{fun add x y = x + y} accepts two arguments. Its partial evaluation \texttt{val add2 = add 2} results in a function which only expects one argument and adds 2 to it.
1.30 @@ -47,12 +47,12 @@
1.31
1.32
1.33 \subsubsection{Lazy Evaluation}
1.34 -Due to referencial transparency, the order in which expressions are evaluated does not affect the results. Therefore, some languages like \textit{Haskell} defer the computation of expressions until they are actually needed. This avoids unnecessary calculations and makes infinite data structures possible. On the other hand, lazy evaluation can potentially cause space leaks \cite{launchbury1993natural} and it makes formal reasoning about code hard \cite{lippmeier2009type}. The opposite is called {\em eager} or {\em strict} evaluation which is the standard for most imperative languages and e.g. \textit{Standard ML}.
1.35 +Due to referential transparency, the order in which expressions are evaluated does not affect the results. Therefore, some languages like \textit{Haskell} defer the computation of expressions until they are actually needed. This avoids unnecessary calculations and makes infinite data structures possible. On the other hand, lazy evaluation can potentially cause space leaks \cite{launchbury1993natural} and it makes formal reasoning about code hard \cite{lippmeier2009type}. The opposite is called {\em eager} or {\em strict} evaluation which is the standard for most imperative languages and e.g. \textit{Standard ML}.
1.36
1.37
1.38 \section{Computer Theorem Proving}
1.39 \label{sec:ctp}
1.40 -Computer Theorem Proving is related to functional programming in serveral fundamental ways. My practical work for this thesis concerned TP ({\bf T}heorem {\bf P}roving) on a technical level below the logical level of TP, on the level of parallel execution on multi-core hardware. However, it is the logical level of TP which provides the fundamental relations to functional programming.
1.41 +Computer Theorem Proving is related to functional programming in several fundamental ways. My practical work for this thesis concerned TP ({\bf T}heorem {\bf P}roving) on a technical level below the logical level of TP, on the level of parallel execution on multi-core hardware. However, it is the logical level of TP which provides the fundamental relations to functional programming.
1.42
1.43 \subsection{History}
1.44 \label{ssec:ctp-hist}
1.45 @@ -62,11 +62,11 @@
1.46 Mechanical or ``formal'' reasoning was an original interest of Artificial Intelligence (AI). The first important programming languages in AI were \textit{Prolog} (logic programming) and \textit{Lisp}. The latter was briefly introduced as a functional language in section \ref{sec:funhist}.
1.47
1.48 \paragraph{\textit{Automath}.}
1.49 -A first notable success was the mechanisation of Edmund Landau's {\em Foundations of Analysis} \cite{van1979checking} in {\em Automath} in 1969. {\em Automath} is outdated, but some of its achievements are still used in TP, e.g. de-Brujin indices, the lambda calculus and Curry-Howard correspondence. This early succcess in TP was not acknowledged by mainstream mathematics. Rather, TP was mixed up with predictions of early AI, e.g. Herbert A. Simon's claim that ``{\em [m]achines will be capable, within twenty years, of doing any work a man can do.}'' \cite{simon1965shape}; predictions that soon turned out to be unrealistic. Nevertheless, mechanisation of various logics (sequent calculus, temporal logics, communicating sequential processes (see section \ref{sec:csp}), etc.) was continued and led to many different, unrelated software tools.
1.50 +A first notable success was the mechanization of Edmund Landau's {\em Foundations of Analysis} \cite{van1979checking} in {\em Automath} in 1969. {\em Automath} is outdated, but some of its achievements are still used in TP, e.g. de-Brujin indices, the lambda calculus and Curry-Howard correspondence. This early success in TP was not acknowledged by mainstream mathematics. Rather, TP was mixed up with predictions of early AI, e.g. Herbert A. Simon's claim that ``{\em [m]achines will be capable, within twenty years, of doing any work a man can do.}'' \cite{simon1965shape}; predictions that soon turned out to be unrealistic. Nevertheless, mechanization of various logics (sequent calculus, temporal logics, communicating sequential processes (see section \ref{sec:csp}), etc.) was continued and led to many different, unrelated software tools.
1.51
1.52 \paragraph{\textit{LCF}.}
1.53 \label{sssec:lcf}
1.54 -\textit{LCF} (Logic for Computable Functions) \cite{milner1978theory} denotes an interactive, automated theorem prover developed at the universities of Edinburgh and Stanford in the early 1970s. The \textit{LCF} project is relevant for this thesis, because it introduced the \textit{ML} programming language explored in section \ref{sec:isasml} and was used for the practical work within the thesis. The purpose of \textit{LCF} was to allow users to write theorem proving tactics and to encapsulate theorems as abstract da\-ta\-types, such that only the admitted inference rules can establish a theorem. This is still called {\em LCF princple}. \textit{LCF} became the ancestor of the {\em HOL family} of provers introduced below.
1.55 +\textit{LCF} (Logic for Computable Functions) \cite{milner1978theory} denotes an interactive, automated theorem prover developed at the universities of Edinburgh and Stanford in the early 1970s. The \textit{LCF} project is relevant for this thesis, because it introduced the \textit{ML} programming language explored in section \ref{sec:isasml} and was used for the practical work within the thesis. The purpose of \textit{LCF} was to allow users to write theorem proving tactics and to encapsulate theorems as abstract da\-ta\-types, such that only the admitted inference rules can establish a theorem. This is still called {\em LCF principle}. \textit{LCF} became the ancestor of the {\em HOL family} of provers introduced below.
1.56
1.57 \paragraph{\textit{The Next Seven Hundred Theorem Provers}.}
1.58 \label{par:next-700}
1.59 @@ -88,7 +88,7 @@
1.60 \subsection{Relevance}
1.61
1.62 \paragraph{The executable fragment of HOL and code generation.}
1.63 -As already mentioned, higher-order logic is closely related to functional programming. This relation includes an executable fragment, i.e. equational theorems within HOL, which can model programs and which can be evaluated within the logic. This way of embedding programs in the logical environment provides the best prerequisites for proving properties of programs and for software verification. \isabelle{} recentely implemented a {\em function package}. Execution, or more appropriately, evaluation, within a prover is very inefficient in comparison with state-of-the-art production software. Therefore engineering software cannot be built within a prover. However, it turned out that algorithms described within the executable fragment of HOL are a concise source for automatic generation of efficient code in a surprisingly straight forward manner.
1.64 +As already mentioned, higher-order logic is closely related to functional programming. This relation includes an executable fragment, i.e. equational theorems within HOL, which can model programs and which can be evaluated within the logic. This way of embedding programs in the logical environment provides the best prerequisites for proving properties of programs and for software verification. \isabelle{} recently implemented a {\em function package}. Execution, or more appropriately, evaluation, within a prover is very inefficient in comparison with state-of-the-art production software. Therefore engineering software cannot be built within a prover. However, it turned out that algorithms described within the executable fragment of HOL are a concise source for automatic generation of efficient code in a surprisingly straight forward manner.
1.65
1.66 \paragraph{Functional programming.}
1.67 Software verification tools are presently already more advanced for functional programming languages. And the theoretical background presented in this section indicates that verification tools will develop better in the paradigm of functional programming than in other paradigms. Also, efficiency considerations are expected to change in favor of the functional paradigm. Programs written on an abstract level in a TP can be transformed into efficient code by automated code generation. This transformation can potentially handle parallelization much more conveniently than programs developed within other paradigms \cite{haftmann2010code}.
1.68 @@ -96,7 +96,7 @@
1.69
1.70 \section{Parallelism}
1.71 \label{sec:parallelism}
1.72 -Concurrency in software has been around for a long time and without it, multitasking would be impossible. It means that processes and threads may be started, executed and completed in overlapping time periods. This does not necessarily imply any parallel, i.e. simultaneous, execution. Parallel software is structured in a way which allows for literally simultaneous execution, e.g. on multi-core processors. Now that this kind of processors is used heavily in PCs, laptops and smartphones, efficient software must be able to exploit parallelism. Approaches to parallelism can roughly be grouped into three different levels: {\em instruction-level} (section \ref{sec:multicoreproc}), {\em task parallelism} (section \ref{sec:task_par}) and {\em data} (section \ref{sec:data_parallelism}). The following sections will establish a theoretical background of parallelism.
1.73 +Concurrency in software has been around for a long time and without it, multitasking would be impossible. It means that processes and threads may be started, executed and completed in overlapping time periods. This does not necessarily imply any parallel, i.e. simultaneous, execution. Parallel software is structured in a way which allows for literally simultaneous execution, e.g. on multi-core processors. Now that this kind of processors is used heavily in PCs, laptops and smart phones, efficient software must be able to exploit parallelism. Approaches to parallelism can roughly be grouped into three different levels: {\em instruction-level} (section \ref{sec:multicoreproc}), {\em task parallelism} (section \ref{sec:task_par}) and {\em data} (section \ref{sec:data_parallelism}). The following sections will establish a theoretical background of parallelism.
1.74
1.75 \subsection{Gain, Cost and Limits}
1.76 Formulated in 1967, Amdahl's Law \cite{amdahl1967validity} describes the correlation between the inherently sequential fraction of a program and the resulting maximally possible speedup $S_A$ under parallel execution (see fig. \ref{fig:amdahls}), given by
1.77 @@ -183,13 +183,13 @@
1.78 \begin{description}
1.79 \item[Bit-level parallelism] takes advantage of increased processor word sizes in order to reduce the number of instructions that need to be executed to complete operations on variables which are longer than one word \cite{culler1999parallel}.
1.80
1.81 -\item[Instruction-level parallelism] tries to discover data independent instructions which often can be reordered and computed during the same processing cycle. Also, instruction piplines with multiple stages allow different instructions to be in different stages and thereby overlap their processing \cite{hennessy2012computer}.
1.82 +\item[Instruction-level parallelism] tries to discover data independent instructions which often can be reordered and computed during the same processing cycle. Also, instruction pipelines with multiple stages allow different instructions to be in different stages and thereby overlap their processing \cite{hennessy2012computer}.
1.83
1.84 \item[Simultaneous multithreading] enables multiple threads to issue instructions on a single processing core which may be processed during the same cycle \cite{tullsen1995simultaneous}.
1.85 \end{description}
1.86
1.87 \subsection{Operating Systems}
1.88 -Operating systems are heavily involved in the resource management of their underlying architecture, both for their own operations and for user applications. Besides support for simultaneous multithreading (see previous section), general-purpose OSes have to deal with diverse hardware approaches, e.g. multiprocessors vs. multi-core processors, shared vs. separate cache models. Scheduling algorithms and memory management are facing new challenges because they must balance loads between cores while avoiding cache misses and reducing the number of context switches. In this thesis we will assume symmetric multiprocessing (SMP), i.e. systems whose processing cores are identical and access the same main memory. Scheduling algorithms in OSes for more heterogenous systems also need to take into account differing performance characteristics and possibly even instruction sets of several processors.
1.89 +Operating systems are heavily involved in the resource management of their underlying architecture, both for their own operations and for user applications. Besides support for simultaneous multithreading (see previous section), general-purpose OSes have to deal with diverse hardware approaches, e.g. multiprocessors vs. multi-core processors, shared vs. separate cache models. Scheduling algorithms and memory management are facing new challenges because they must balance loads between cores while avoiding cache misses and reducing the number of context switches. In this thesis we will assume symmetric multiprocessing (SMP), i.e. systems whose processing cores are identical and access the same main memory. Scheduling algorithms in OSes for more heterogeneous systems also need to take into account differing performance characteristics and possibly even instruction sets of several processors.
1.90
1.91 \subsection{Functional Programming}
1.92 \label{sec:par_funprog}
1.93 @@ -214,7 +214,7 @@
1.94 \label{sec:refacfunprogs}
1.95 Refactoring is a process which changes the design and structure of existing software without changing its external behavior. It can result in simpler programs, remove duplicate code or prepare an extension of the program's functionality. Because refactoring is a potentially tedious and error-prone process \cite{thompson2005refactoring}, there is a variety of tools which automatically check preconditions for and apply refactoring steps for object-oriented programming languages. The number of such tools for functional programming languages, however, is limited. One of the few existing projects targets \textit{Haskell} code and is called {\em HaRe} (\textit{\textbf{Ha}skell} \textbf{Re}factorer). It follows five main strategies:
1.96 \begin{enumerate}
1.97 - \item {\bf Generalisation.} Extract some of a function's behavior into an argument, possibly a HOF, and thereby make the function more general and reusable.
1.98 + \item {\bf Generalization.} Extract some of a function's behavior into an argument, possibly a HOF, and thereby make the function more general and reusable.
1.99 \item {\bf Commonality.} Similar or identical parts of a program are identified, extracted into a single function which is invoked at the respective locations and with appropriate parameters.
1.100 \item {\bf Data Abstraction.} Replacing algebraic da\-ta\-types by abstract da\-ta\-types often allows programmers to modify concrete implementations without touching client code.
1.101 \item {\bf Overloading.} The use of {\em type classes} and {\em instances} allows for overloading of names. This may improve readability and facilitate code reuse.