1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-isac/mlehnfeld/master/thesis/introduction.tex	Wed Mar 12 17:43:22 2014 +0100
     1.3 @@ -0,0 +1,30 @@
     1.4 +\chapter{Introduction}
     1.5 +\label{cha:intro}
     1.6 +
     1.7 +
     1.8 +\section{Motivation}
     1.9 +\label{sec:motivation}
    1.10 +Moore's Law \cite{moore1965cramming} states that the density of transistors which can be placed on a single chip doubles about every two years. While the size of transistors is still shrinking, clock speeds hit an upper bound around the year 2004 (fig. \ref{fig:chip-speeds}) due to thermal issues \cite{sutter2005free}. Therefore most CPUs now come with multiple processing cores. This poses a challenge to the software running on these CPUs because it must support parallel or concurrent execution in order to efficiently exploit a computer’s full processing power.\\
    1.11 +
    1.12 +\begin{figure}
    1.13 +\centering
    1.14 +\includegraphics[width=.95\textwidth]{chip-speeds}
    1.15 +\caption{Intel CPU trends. {\it source}: \cite{sutter2005free}}
    1.16 +\label{fig:chip-speeds}
    1.17 +\end{figure}
    1.18 +
    1.19 +Concurrency allows for multitasking and asynchronous computations can improve responsiveness even on uniprocessors. But writing efficiently parallel or concurrent software is hard \cite{sutter2005software}. Now that multicore architectures are commonplace and higly parallel GPUs are beginning to get exploited for general-purpose computing \cite{luebke2006gpgpu}, concurrent processes and threads can effectively be running simultaneously and therefore significantly faster.\\
    1.20 +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 like immutable data, statelessness and the lack of side effects (e.g. \cite{burge1975recursive}).\\
    1.21 +\\
    1.22 +The interactive theorem prover \isabelle{} \cite{paulson1994isabelle} is a comprehensive, international software project. Its internal logic has been written entirely in {\it Standard ML} which later was embedded in a {\it Scala} environment to simplify interaction with the underlying operating system and software built on top of \isabelle{}.\\
    1.23 +As the use of multicore systems became more common, \isabelle{}'s computationally complex logic was required to exploit the newly available processing power. {\it 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 done was due to the use of impure code facilitated by {\it Standard ML} and {\it Scala}. {\it 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 {\it Isabelle/jEdit}.\\
    1.24 +\\
    1.25 +The educational mathematics system \isac{} was developed at {\it Graz University of Technology} on the basis of \isabelle{} and combines a {\it Java} frontend with a logical {\it Standard ML} core \cite{neuper2001reactive}.\\
    1.26 +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.\\
    1.27 +Analogous to \isabelle{}'s parallelization, \isac{} was reengineered for multicore 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 multicore.
    1.28 +
    1.29 +
    1.30 +\section{Thesis Structure}
    1.31 +\label{sec:thesis_structure}
    1.32 +TODO
    1.33 +