9 \centering |
9 \centering |
10 \includegraphics[width=.95\textwidth]{chip-speeds} |
10 \includegraphics[width=.95\textwidth]{chip-speeds} |
11 \caption{Intel CPU trends (source: \cite{sutter2005free}).} |
11 \caption{Intel CPU trends (source: \cite{sutter2005free}).} |
12 \label{fig:chip-speeds} |
12 \label{fig:chip-speeds} |
13 \end{figure} |
13 \end{figure} |
14 Concurrency allows for multitasking and asynchronous computations can improve responsiveness even on uniprocessors (see section \ref{sec:concurresp}). But writing efficiently parallel or concurrent software is hard \cite{sutter2005software}. Now that multi-core architectures are commonplace and higly parallel GPUs are beginning to get exploited for general-purpose computing \cite{nickolls2010gpu}, concurrent processes and threads can effectively be running simultaneously and therefore significantly faster. |
14 Concurrency allows for multitasking and asynchronous computations can improve responsiveness even on uniprocessors (see section \ref{sec:concurresp}). But writing efficiently parallel or concurrent software is hard \cite{sutter2005software}. Now that multi-core architectures are commonplace and highly parallel GPUs are beginning to get exploited for general-purpose computing \cite{nickolls2010gpu}, concurrent processes and threads can effectively be running simultaneously and therefore significantly faster. |
15 |
15 |
16 Functional programming is a declarative paradigm based on the lambda calculs. It has been claimed that it is specifically suited not only for prototyping but also for efficient parallelism due to some of its defining features such as immutable data, statelessness and the lack of side effects (e.g. \cite{burge1975recursive}). |
16 Functional programming is a declarative paradigm based on the lambda calculus. It has been claimed that it is specifically suited not only for prototyping but also for efficient parallelism due to some of its defining features such as immutable data, statelessness and the lack of side effects (e.g. \cite{burge1975recursive}). |
17 |
17 |
18 The interactive theorem prover \isabelle{} \cite{nipkow2002isabelle} is a comprehensive, international software project. Its internal logic has been written entirely in {\em Standard ML} which later was embedded in a {\em Scala} environment to simplify interaction with the underlying operating system and software built on top of \isabelle{}. As the use of multi-core systems became more common, \isabelle{}'s computationally complex logic was required to exploit the newly available processing power. Makarius Wenzel, one of the leading developers of \isabelle{}, parallelized essential parts of the system within a few man months (scattered over about two years). This is a surprisingly little amount of effort considering the project's size and complexity. A significant amount of the work was required due to the use of impure code, facilitated by \textit{Standard ML} and \textit{Scala}, i.e. work concerning purification in terms of the functional paradigm. {\em Isabelle/Scala} provides tools for interaction between front-end and proof engine and contains object-oriented components to deal with inherently stateful aspects of the development environment {\em Isabelle/jEdit}. |
18 The interactive theorem prover \isabelle{} \cite{nipkow2002isabelle} is a comprehensive, international software project. Its internal logic has been written entirely in {\em Standard ML} which later was embedded in a {\em Scala} environment to simplify interaction with the underlying operating system and software built on top of \isabelle{}. As the use of multi-core systems became more common, \isabelle{}'s computationally complex logic was required to exploit the newly available processing power. Makarius Wenzel, one of the leading developers of \isabelle{}, parallelized essential parts of the system within a few man months (scattered over about two years). This is a surprisingly little amount of effort considering the project's size and complexity. A significant amount of the work was required due to the use of impure code, facilitated by \textit{Standard ML} and \textit{Scala}, i.e. work concerning purification in terms of the functional paradigm. {\em Isabelle/Scala} provides tools for interaction between front-end and proof engine and contains object-oriented components to deal with inherently stateful aspects of the development environment {\em Isabelle/jEdit}. |
19 |
19 |
20 The educational mathematics system \isac{} is being prototyped at {\em Graz University of Technology}. The prototype combines a \textit{Java} front-end with a mathematics-engine written in \textit{Standard ML}, which reuses logical concepts and mechanisms of \isabelle{} \cite{neuper2012automated}. Both projects are case studies for the use of functional programming in practical, interactive software projects which also demonstrate how the disadvantages of this paradigm's intrinsic properties like side effect free programming can be complemented by integrating functional and imperative programming. Analogous to \isabelle{}'s parallelization, \isac{} was reengineered for multi-core systems. The involved background knowledge, documentation and outcomes of this project form the basis for this document. These topics will be expanded to include common parallelism and concurrency mechanisms suggested and implemented for other functional programming languages as well as previous research on refactoring techniques for multi-core. |
20 The educational mathematics system \isac{} is being prototyped at {\em Graz University of Technology}. The prototype combines a \textit{Java} front-end with a mathematics-engine written in \textit{Standard ML}, which reuses logical concepts and mechanisms of \isabelle{} \cite{neuper2012automated}. Both projects are case studies for the use of functional programming in practical, interactive software projects which also demonstrate how the disadvantages of this paradigm's intrinsic properties like side effect free programming can be complemented by integrating functional and imperative programming. Analogous to \isabelle{}'s parallelization, \isac{} was reengineered for multi-core systems. The involved background knowledge, documentation and outcomes of this project form the basis for this document. These topics will be expanded to include common parallelism and concurrency mechanisms suggested and implemented for other functional programming languages as well as previous research on refactoring techniques for multi-core. |
21 |
21 |
22 |
22 |
23 \section{Thesis Structure} |
23 \section{Thesis Structure} |
24 \label{sec:thesis_structure} |
24 \label{sec:thesis_structure} |
25 The remainder of this thesis is structured as follows. Chapter \ref{cha:fundamentals} establishes a theoretical background on the different areas relevant for the practical work on the case study within \isac{} and includes topics such as functional programming, computer theorem proving, parallelism, concurrency, responsiveness and refactoring of programs within the functional paradigm. Subsequently, various approaches towards parallelism that can and may have been used in functional programming are investigated in chapter \ref{cha:funproglangs_mcsystems}. The end of this chapter briefly talks about refactoring of functional programs for parallelism. Chapter \ref{cha:isabelle_isac} is then dedicated to the two main software projects involved in the practical part of this thesis, \isabelle{} and \isac{}, as well as to a discussion of what has been done in the course of the practical work. A conclusion and outlook on possible futurework are given in chapter \ref{cha:conclusion}. Appendix \ref{app:code} provides code samples in addition to those given in the main text as well as comments and further explanations. Finally, appendix \ref{app:cdrom} lists the contents of the DVD that was handed in along with the thesis. |
25 The remainder of this thesis is structured as follows. Chapter \ref{cha:fundamentals} establishes a theoretical background on the different areas relevant for the practical work on the case study within \isac{} and includes topics such as functional programming, computer theorem proving, parallelism, concurrency, responsiveness and refactoring of programs within the functional paradigm. Subsequently, various approaches towards parallelism that can and may have been used in functional programming are investigated in chapter \ref{cha:funproglangs_mcsystems}. The end of this chapter briefly talks about refactoring of functional programs for parallelism. Chapter \ref{cha:isabelle_isac} is then dedicated to the two main software projects involved in the practical part of this thesis, \isabelle{} and \isac{}, as well as to a discussion of what has been done in the course of the practical work. A conclusion and outlook on possible future work are given in chapter \ref{cha:conclusion}. Appendix \ref{app:code} provides code samples in addition to those given in the main text as well as comments and further explanations. Finally, appendix \ref{app:cdrom} lists the contents of the DVD that was handed in along with the thesis. |