text:
\makeatletter \@ifundefined{rootpath}{\input{../../setup/preamble.tex}}\makeatother
\worksheetstart{Threads \& Locks}{1}{April 24, 2013}{Andreas}{../../}
This chapter presents the \ac{TL} concurrency model. We describe the key concepts of \ac{TL} in \bsref{sec:tl_key_concepts}. These are essential in order to understand the issues and solutions presented in \bsref{sec:tl_ci}, where we present the concurrency issues. In \bsref{sec:tl_discussion} we discuss specific properties related to \ac{TL}. \bsref{sec_tl_char} evaluates the characteristics of \ac{TL}.

\label{chap:threads_locks}
\section{Key Concepts}\label{sec:tl_key_concepts}
This section will present the key concepts of the \ac{TL} concurrency model. \bsref{subsec:threads_shared_memory} describes how \ac{TL} relies on threads and shared memory while \bsref{subsec:race_coditions} describes the issue of race conditions. Finally \bsref{sec:locks_me} describe concepts of mutual exclusion and locks.
\subsection{Threads and Shared Memory}\label{subsec:threads_shared_memory}
As the name implies the \ac{TL} concurrency model builds upon the concept of threads, discussed in \bsref{sec:processes_threads}. Threads are started to introduce concurrency. Some implementations map the started threads directly to hardware threads in the underlying \ac{OS}, while others rely on software threads.

The \ac{TL} concurrency model uses the shared memory of threads, to facilitate communication between them. Communication is achieved by reading from and writing to the shared memory\cite[p. 93]{tanenbaum2008modern}. Accessing shared data facilitates fast communication between threads, but presents the issue of race conditions. If threads do not read data that can be modified from other threads, these issues are not present. So multiple threads can run without introducing race conditions, as long as they do not modify any shared data.

\subsection{Race Conditions}\label{subsec:race_coditions}
One issue that can arise in concurrent applications, is that the result of a computation, consisting of two or more threads which share data, depends on how the threads are scheduled. That is, the behaviour of the application depends on the timing of the threads. This issue is called a race condition\cite[p. 983]{bryant2011computer}\cite[p. 115]{tanenbaum2008modern}\cite[p. 44]{sevenModels}.

Consider the example presented in \bsref{lst:racecondition} using Java threads. Here we see a small Java program that starts the two threads \bscode{t1} and \bscode{t2} and waits for each of them to finish, printing out the result of their computations before exiting. Both threads access the shared number variable. The first thread \bscode{T1} checks if the static variable \bscode{number} is equal to ten (which is its initial value) on line 7. If the condition is true, it sets the \bscode{result} variable to \bscode{number} times three, as seen on line 8. Line 11 shows the second thread \bscode{t2}, simply sets the value of \bscode{number} to 20.

\begin{lstlisting}[label=lst:racecondition,
  caption={Race condition example},
  language=Java,
  showspaces=false,
  showtabs=false,
  breaklines=true,
  showstringspaces=false,
  breakatwhitespace=true,
  commentstyle=\color{greencomments},
  keywordstyle=\color{bluekeywords},
  stringstyle=\color{redstrings}]  % Start your code-block

	public class RaceCondition {
    private static int number = 10;
    private static int result = 0;

    public static void main(String[] args) throws InterruptedException {
        Thread t1 = new Thread(() -> {
            if (number == 10){
                result = number * 3;
            }
        });
        Thread t2 = new Thread(() -> number = 20);
        t1.start(); t2.start();
        t1.join(); t2.join();
        System.out.println("Result is: " + result);
    }
	}
\end{lstlisting}

Due to the concurrent execution of the two threads, multiple results are possible. The first possible result occurs if \bscode{t1} is executed before \bscode{t2}. This interleaving is shown in \bsref{fig:race_interleaving1}.

\begin{figure}[htbp]
\centering
 \includegraphics[width=0.65\textwidth]{\rootpath/worksheets/threads_and_locks/figures/race_interleaving1}
 \caption{First possible interleaving of threads}
\label{fig:race_interleaving1}
\end{figure}

Here it can be seen that \bscode{t1} executes both the evaluation of the if statement and the assignment to result before \bscode{t2} changes value of the number variable. The result is:
\begin{verbatim}
Result is: 30
\end{verbatim}

The second possible result occurs if \bscode{t2} is executed before \bscode{t1}. This interleaving is depicted in \bsref{fig:race_interleaving2}.
\begin{figure}[htbp]
\centering
 \includegraphics[width=0.65\textwidth]{\rootpath/worksheets/threads_and_locks/figures/race_interleaving2}
 \caption{Second possible interleaving of threads}
\label{fig:race_interleaving2}
\end{figure}
Here it is shown how \bscode{t2} changes the value of the number variable to 20, before \bscode{t1} has evaluated its precondition. Because of this \bscode{t1} never evaluates the assignment to the result variable and the printed result becomes:
\begin{verbatim}
Result is: 0
\end{verbatim}

The final possible result occurs if \bscode{t1} evaluates the precondition for the if statement on line 7, after which it is paused by the operating system, and \bscode{t2} gets to run instead. \bscode{t2} then changes the value of the number variable which \bscode{t1} just evaluated to be equal to 10. \bscode{t2} then exits and \bscode{t1} is resumed calculating the value assigned to the result variable based on the value of the number value set by \bscode{2}. The result of this is:
\begin{verbatim}
Result is: 60
\end{verbatim}
The third possible interleaving is shown in \bsref{fig:race_interleaving3}.
\begin{figure}[htbp]
\centering
 \includegraphics[width=0.65\textwidth]{\rootpath/worksheets/threads_and_locks/figures/race_interleaving3}
 \caption{Third possible interleaving of threads}
\label{fig:race_interleaving3}
\end{figure}

While the threads in \bsref{fig:race_interleaving1} and \bsref{fig:race_interleaving2} have exclusive access to the number variable, this is not the case in \bsref{fig:race_interleaving3}. The interleaving shown in \bsref{fig:race_interleaving3} does not provide threads with atomic access to the shared number variable, as described in \bsref{sec:synchronization}. As a result, it is not guaranteed that other threads will not access the shared data while a thread is using it, resulting in unintended behaviour by the program.

\subsection{Mutual Exclusion \& Locks}\label{sec:locks_me}
Mutual exclusion is the property of shared memory concurrency which ensures that only a single thread can access a given critical region at a time\cite[p. 117]{tanenbaum2008modern}\cite[p. 962]{bryant2011computer}\cite[p. 6]{herlihy2012art}. A critical region being a thread accessing some memory that is shared with other threads\cite[p. 117]{tanenbaum2008modern}\cite[p. 961]{bryant2011computer}. Mutual exclusion provides atomic synchronization as discussed in \bsref{sec:synchronization}. Having only a single thread execute within all critical regions at a time, ensures that the program will behave as if it runs sequentially, even though this might not be the case. Access to critical regions is often restricted by the use of different forms of locks\cite[p. 58]{sutter2005software}.

Locks are a general class of constructs used for providing mutual exclusion. Locks come in a variety of different forms such as Mutex, Monitor, and Semaphore. Each of these operate in their own way, but the overall goal remains the same. Locks provide mutual exclusion by allowing only a single thread to enter its critical region at a time. When a thread \bscode{t1} attempt to acquire a lock that is already held by another thread \bscode{t2},\bscode{t1} blocks, effectively waiting for \bscode{t2} to exit its critical region and release the lock before proceeding. Locks prevent race conditions but introduce issues such as deadlocks, priority inversion, and starvation, which will be presented in \bsref{sec:tl_ci}. These issues leads to threads spending time blocked instead of executing parts of the program. Furthermore, it is up to the programmer to apply locking to the correct places and in the correct order, which in itself is hard. If he succeeds in using locks as synchronization mechanism, a major caveat is that they are not composable\cite[p. 58]{sutter2005software}. That is, you cannot compose two correct lock-based pieces of code and know the result is still correct. This significantly limits the reuseability of software components. This will be discussed further in \bsref{subsec:tl_composability}.

Consider the example presented in \bsref{lst:mutualexclusion}, which is a modified version of the exampled presented in \bsref{lst:racecondition}. As seen at line 11-15 and 18-19, the two threads have had their critical regions locked, limiting the access to one thread at a time. If either \bscode{t1} or \bscode{t2} attempts to acquire the lock while the other already holds it, they would block, ensuring mutual exclusion. As a result the interleaving presented in \bsref{fig:race_interleaving3} is no longer possible and the race condition has been removed.

%\bsref{lst:mutualexclusion} depicts a modified version of the example presented in \bsref{lst:racecondition}. The two threads have had their critical regions locked, limiting the access to one thread at a time. Because of this, the case where \bscode{t1} runs just until its about to compute the result and  \bscode{t2} taking over will no longer occur. \bscode{t2} will now not be able to change the value of number as \bscode{t2} still holds the lock on the critical region, even though it is paused. As a result the output result is: 60, can no longer occur. The output does however still depend on the order in which access to the critical regions is acquired.
\begin{lstlisting}[label=lst:mutualexclusion,
  caption={Mutual exclusion in Java using a lock},
  language=Java,
  showspaces=false,
  showtabs=false,
  breaklines=true,
  showstringspaces=false,
  breakatwhitespace=true,
  commentstyle=\color{greencomments},
  keywordstyle=\color{bluekeywords},
  stringstyle=\color{redstrings}]  % Start your code-block

	import java.util.concurrent.locks.Lock;
	import java.util.concurrent.locks.ReentrantLock;

	public class MutualExclusion {
    private static int number = 10;
    private static int result = 0;
    private final static Lock lock = new ReentrantLock();

    public static void main(String[] args) throws InterruptedException {
        Thread t1 = new Thread(() -> {
            lock.lock();
            if (number == 10){
                result = number * 3;
            }
            lock.unlock();
        });
        Thread t2 = new Thread(() -> {
            lock.lock();
            number = 20;
            lock.unlock();
        });
        t1.start(); t2.start();
        t1.join(); t2.join();
        System.out.println("Result is: " + result);
    }
	}
\end{lstlisting}

%Executor service
%Futres
%Still based on threads

\section{Concurrency Issues}\label{sec:tl_ci}
This section presents an overview of known issues related to concurrency in \ac{TL}. Many of the issues arise as a result of locking access to shared memory. Some of the issues are also present in other concurrency models. The overview is used for evaluating the characteristics of the \ac{TL} concurrency model. Furthermore knowing what issues can arise for each of the selected concurrency models, will assist in comparing their complexity.
%Some of the issues are related mainly to shared memory concurrency while others apply to a broader spectrum, including asynchronous message passing.

\subsection{Deadlocks}
A deadlock occurs when all threads in a set are waiting on some event, that can only be caused by another thread in the set\cite[p. 435]{tanenbaum2008modern}. Because all the threads are blocked and waiting on one of the other threads, none of them will ever continue and they will block indefinitely.

As an example consider \bsref{fig:deadlockexample}. Here the three threads T1, T2 and T3 are illustrated. The three threads are all waiting on a resource, that has been acquired by one of the other threads, as illustrated by the arrows. Each thread is waiting on a resource held by one of the other threads and is deadlocked. The event the threads are waiting for being the release of the resource.
\begin{figure}[htbp]
\centering
 \includegraphics[width=0.5\textwidth]{\rootpath/worksheets/threads_and_locks/figures/deadlock}
 \caption{Illustration of a deadlock. All the threads are waiting for the release of a resource held by another thread.}
\label{fig:deadlockexample}
\end{figure}

Deadlocks occur for different reasons in different concurrency models. As described, \bsref{fig:deadlockexample} illustrates an example of a deadlock using \ac{TL}. Here the deadlock is caused by threads acquiring a lock on a resource \bscode{R}, where after they attempt to acquire a lock on a resource that is held by another thread, that is directly or indirectly waiting on \bscode{R}. This type of deadlock is called a resource deadlock\cite[p. 435]{tanenbaum2008modern}.

%Another type of deadlock that can occur in, for example, the Actor concurrency model is called a \emph{communication deadlock}\cite[p. 124]{tanenbaum2008modern}. Instead of deadlocks being caused by locks, a deadlock is here cause by actors waiting on messages. In the context of \bsref{fig:deadlockexample} this would mean that T1, T2 and T3 where actors and the arrows represented an actor waiting on a message from a given actor, so that T1 is waiting on a message from T2. A communication deadlock can occur both over network as well as on a single machine.
%threads and lock = resource aqusision
%async message passing = wating on messages as with resources

\subsection{Livelocks} A livelock is similar to a deadlock in that no progress is being made. While a deadlocked thread is blocked, a livelocked thread is still executing. The execution does however not result in any progress. A livelock can occur when multiple threads attempts to recover from an error such as a deadlock\cite[p. 457]{tanenbaum2008modern}. Consider two threads \bscode{A} and \bscode{B}. \bscode{A} and \bscode{B} both attempt to write to some common storage, after which they check if the data was written correctly. If that is not the case they attempt the write again. This could lead to another failed attempt and another retry, which could go on indefinitely. \bscode{A} and \bscode{B} are then said to be livelocked.

In this scenario, the livelock could be avoided by having each task wait a random period of time $t < m$, where $m$ is the current maximum wait time, before retrying. Having $m$ grow for each time a task has to retry its operation minimizes the risk of the other tasks interfering with the write as it is more likely that the retry will occur at different times. It is however also of interest to minimize wait time as no progress is made during this period.

\subsection{Priority Inversion}
Priority inversion is the problem of a high priority thread blocking, while waiting for a low priority thread to finish\cite[p. 456]{tanenbaum2008modern}. As an example consider the two threads \bscode{H} and \bscode{L} shown in \bsref{fig:priority_inversion}. \bscode{H} has a high priority while \bscode{L} has a low priority. \bscode{L} starts running, enters its critical region and acquires a lock on some shared resource \bscode{R}. The high priority task \bscode{H} is then started. It attempts to acquire a lock on the resource \bscode{R} in order to enter its critical region. The lock on \bscode{R} is however still held by \bscode{L} and the high priority task \bscode{H} must now wait for the low priority task \bscode{L} to finish.

\begin{figure}[htbp]
\centering
 \includegraphics[width=0.95\textwidth]{\rootpath/worksheets/threads_and_locks/figures/pi_graf}
 \caption{Priority inversion example}
\label{fig:priority_inversion}
\end{figure}
If a thread \bscode{M} that do not need to acquire resource R was introduced with medium priority, the scenario could instead look as depicted in \bsref{fig:priority_inversion_m}. The scenario is similar to the previous but here \bscode{M} starts up after \bscode{L} has acquired the lock on \bscode{R}. Because \bscode{M} is a medium priority task it is scheduled before \bscode{L}. As a result \bscode{H} has to wait on both a low and medium priority task to finish before acquiring the lock on \bscode{R}.

\begin{figure}[htbp]
\centering
 \includegraphics[width=0.95\textwidth]{\rootpath/worksheets/threads_and_locks/figures/pi_graf2}
 \caption{Priority inversion with medium priority task}
\label{fig:priority_inversion_m}
\end{figure}
%\andreas{Move M so H acquire R before M starts}
\subsection{Starvation}
A thread is said to be starved if, it is denied access to a resource indefinitely\cite[p. 459]{tanenbaum2008modern}. The task can be denied based on many different criteria. For example, priority or the size of the job that it is to perform.

As an example, imagine a scheduler that gives threads access to some resource R based on the priority of the thread. Threads with a high priority gets access to the resource before threads with a low priority. Now imagine a low priority thread \bscode{A} attempts to acquire a lock on some resource \bscode{R}. The lock on \bscode{R} is however currently held by some other task and \bscode{A} is blocked waiting for access to \bscode{R}. While \bscode{A} is blocked, a high priority task \bscode{B} also attempts to acquire the lock on \bscode{R} and is blocked as well. When the lock on \bscode{R} is released it is given to the high priority task \bscode{B} even though \bscode{A} blocked first and \bscode{A} remains blocked. If this scenario keeps repeating and a high priority task keeps getting the lock over \bscode{A}, \bscode{A} is said to be starved.

%The same scenario can without the use of locks for synchronization. Imagine a printing service in a asynchronous message passing system. The printing service accepts, schedules and handles print jobs on behalves of a number of clients. The printing services givers a higher priority to jobs created by some clients than jobs created by others. If a client submitted the low priority job \bscode{A} to the printing service, but the queue of the printing service already contained a number of high priority jobs, \bscode{A} would have to wait until the high priority jobs where finished. If the printing services keeps receiving new high priority jobs at a pace such that the queue allways contains atleast a single high priority job, then \bscode{A} will never be executed and will be starved. The similar scenario could occur if the printing service gave priority to the smallest job. A very large job might starve as smaller jobs keep getting prioritized

One strategy to avoid starvation, can be to use a \ac{LIFO} scheduling strategy\cite[p. 459]{tanenbaum2008modern}.

\section{Discussion}
\label{sec:tl_discussion}
This section contains a discussion of a number of issues related to \ac{TL} concurrency. Why \ac{TL} concurrency is considered to be hard is discussed in \bsref{subsec:tl_lock_hard}, followed by a discussion of the composability of the \ac{TL} concurrency model in \bsref{subsec:tl_composability}.
\subsection{Why Locks are Hard}\label{subsec:tl_lock_hard}
Concurrency is generally considered to be hard, the same goes for using locks to provide mutual exclusion\cite[p. 56]{sutter2005software}. Several reasons for this exist. One is that in order for locks to work, programmers have to strictly follow a set of conventions. If, for example, the programmer takes locks in the wrong order, it can potentially lead to deadlocks\cite[p. 58]{sutter2005software}. Furthermore the relationship between a lock and the shared data it is protecting is implicit, that is, it is enforced by the programmer. If the programmer misses or leaks a reference to the shared data, mutual exclusion is no longer ensured and race conditions can occur. This is worsened by locking being a global property that requires local handling. That is, data might be shared between many parts of a system, and each part has to locally reason about locking access to the data.

Locks also has the unfortunate problem of not mixing well with some aspects of \ac{OOP}. Encapsulating data within objects that only allow modification to the data via the objects interface, is well known concept from \ac{OOP}, known as encapsulation or information hiding. Ensuring that multiple threads accessing an object does not corrupt its internal structure, can be done by encapsulating locking, along with the data, inside the object. As an example consider the \bscode{Account} class presented in \bsref{lst:account_example}. The \bscode{Account} class uses an internal lock, which is defined on line 4, to ensure that only a single thread can modify the balance of the account at a time. It uses a \bscode{ReentrantLock}, which is a lock that allows the same thread to acquire it multiple times, and thus cannot block on itself. This solution does however have a number of issues. Firstly, if a programmer was to extend the \bscode{Account} class and provide an overridden version of the credit or debit method, she would have to ensure that mutual exclusion on the balance was maintained. In this simple example such a task could be achieved without too much trouble, assuming that the programmer extending the account class knows about the lock. If however it had been a more complex class, using more sophisticated locking, providing an overridden method might not be a simple task. In any case it is a task with a high potential for programmer error, especially if the programmer does not have access to the source code of the class that is to be extended.

\begin{lstlisting}[float,label=lst:account_example,
  caption={Encapsulated locking},
  language=Java,
  showspaces=false,
  showtabs=false,
  breaklines=true,
  showstringspaces=false,
  breakatwhitespace=true,
  commentstyle=\color{greencomments},
  keywordstyle=\color{bluekeywords},
  stringstyle=\color{redstrings}]  % Start your code-block

	public class Account {

    private int balance;
    protected final Lock lock = new ReentrantLock();

    public Account(int balance){
       this.balance = balance;
    }

    public void credit(int amount){
        lock.lock();
        balance += amount;
        lock.unlock();
    }

    public void debit(int amount){
        lock.lock();
        balance -= amount;
        lock.unlock();
    }
	}
\end{lstlisting}

Secondly consider the example of transferring funds from one account to another. \bsref{lst:account_example_transfer} shows one way in which this could be achieved. The two accounts \bscode{a1} and \bscode{a2} are created with balances of 500 and 100 respectively. 200 is debited from \bscode{a1} followed by crediting \bscode{a2} with 200 completing the transfer. The problem arises because the encapsulated locking only protects each call to debit and credit but not the transfers as a whole\cite[p. 59]{sutter2005software}. A thread can read the inconsistent state of the accounts in between the debiting of \bscode{a1} and crediting of \bscode{a2}. Additional locking has to be provided  if this is to be avoided.

\begin{lstlisting}[float,label=lst:account_example_transfer,
  caption={Funds transfer between two accounts},
  language=Java,
  showspaces=false,
  showtabs=false,
  breaklines=true,
  showstringspaces=false,
  breakatwhitespace=true,
  commentstyle=\color{greencomments},
  keywordstyle=\color{bluekeywords},
  stringstyle=\color{redstrings}]  % Start your code-block

    Account a1 = new Account(500);
    Account a2 = new Account(100);
    a1.debit(200);
    a2.credit(200);
\end{lstlisting}

In \cite{lee2006problem} the author argues that introducing threads into a program makes the program nondeterministic, that is, the program can produce different results for each time it is run. This is exactly the effect race conditions, described in \bsref{subsec:race_coditions}, have on a program. The author argue that it becomes the job of the programmer to prune away this nondeterminism in order to produce a deterministic program. Using the \ac{TL} concurrency model this is done using different forms of lock. However such pruning is not an easy task and using the \ac{TL} model introduces a number of other issues such as deadlocks and starvation.

%Some locking constructs, such as Java's syncronized methods, provide object based locking.
%\subsection{\ac{TL} and OOP}

\subsection{Composability}\label{subsec:tl_composability}

As mentioned in \bsref{sec:locks_me}, lock based concurrent implementations are not composable. Creating new software by composing existing implementations, in the form of libraries, is a common practice in software development. As software libraries does not perish on use, it is natural to reuse existing libraries. If such libraries use locks to correctly ensure mutual exclusion, it is not guaranteed that combining these libraries, results in an application free of concurrency related errors.

Deadlocks are the primary reason for locks not composing\cite[p. 58]{sutter2005software}. Event based frameworks call code, that has been defined by programmers using the framework, to signal that some event occurred. If such frameworks use locks to ensure correct synchronization, calling code which the framework itself knows nothing about, while holding locks, can lead to deadlocks.

As an example consider the observer pattern\cite{gamma1994design} in which an object (the observable) is observed by a number of observers. Observers can register and unregister for notifications and the observable notifies any registered observers whenever some event occurs.

\bsref{lst:observer} shows the implementation of an observable that attempts to use a semaphore in order to ensure thread safety. In this example, the \bscode{Observable} represents the framework, and the \bscode{Observer} represents the client code using the framework.

The \bscode{ValueStore} class implements the \bscode{Observable} interface, overriding the two methods \bscode{register} and \bscode{unregister} defined on the interface. Besides these two methods the \bscode{ValueStore} class defines the \bscode{setValue} method which allows others to set the stored value as well as triggering a notification to all registered observers. As mentioned the \bscode{ValueStore} class uses a semaphore to ensure mutual exclusion. The semaphore is used to lock access to the \bscode{ValueStore}'s internal value and list of observers. On lines 18-20 and 25-27 the semaphore locks access to the list of observers while while a registration or unregistration is in progress. On lines 8-13 the semaphore locks access to the internal value and list of observers while the value is changed and any registered observers are notified. This prevents changes to the internal value as well as preventing any observers from registering and unregistering, while the value store is notifying existing observers.

\begin{lstlisting}[label=lst:observer,
  caption={Observer pattern with locks},
  language=Java,
  showspaces=false,
  showtabs=false,
  breaklines=true,
  showstringspaces=false,
  breakatwhitespace=true,
  commentstyle=\color{greencomments},
  keywordstyle=\color{bluekeywords},
  stringstyle=\color{redstrings}]  % Start your code-block

	public class ValueStore implements Observable{

    private int value = 0;
    private List<Observer> observers = new ArrayList<>();
    private Semaphore sem = new Semaphore(1);

    public void setValue(int newValue) throws InterruptedException {
        sem.acquire();
        value = newValue;
        for (Observer o : observers) {
            o.notify(this,value);
        }
        sem.release();
    }

    @Override
    public void register(Observer observer) throws InterruptedException {
        sem.acquire();
        observers.add(observer);
        sem.release();
    }

    @Override
    public void unregister(Observer observer) throws InterruptedException {
        sem.acquire();
        observers.remove(observer);
        sem.release();
    }
	}

	public class ValueObserver implements Observer {

    @Override
    public void notify(Observable sender, int value) throws InterruptedException {
        sender.unregister(this);
    }
	}

	public class Main {

    public static void main(String[] args) throws InterruptedException {
        ValueStore observable = new ValueStore();
        observable.register(new ValueObserver());
        observable.setValue(5);
        System.out.println("Done");
    }
	}
\end{lstlisting}

The \bscode{ValueObserver} class implements the observer interface and overrides its notify method. The notify method simply unregisters from the observable supplying the notification.

The \bscode{Main} class and its \bscode{main} method defines the behaviour of the program. On line 42 a \bscode{ValueStore} is created followed by the registration of a \bscode{ValueObserver}, setting the value of the \bscode{ValueStore} to 5 and printing \bscode{"Done"} to the console. The printing will however never occur as the program deadlocks before it can happen. The deadlock occurs because the \bscode{ValueObserver} attempts to unregister from the \bscode{ValueStore} while the \bscode{ValueStore} hold the lock. As part of setting the value on line 44 the \bscode{ValueStore} acquires the lock, sets the value and proceeds to notify all observes while still holding the lock, as seen on lines 8-13. Notifying an observer entail calling its \bscode{notify} method, which in the case of the \bscode{ValueObserver} means the \bscode{ValueObserver} unregistering from the observable. As the \bscode{unregister} method attempts to acquire the lock currently held by the \bscode{ValueStore} within the \bscode{setValue} method, a deadlock is created resulting in the \bscode{"Done"} string never being printed.

In order to remove the deadlock one could move the notification of observers in the \bscode{setValue} method outside of the locked section. This would however mean that access to the list of observers would not be thread safe as nothing prevents the registration and unregistration of observers while the \bscode{setValue} method iterates over it. One way to solve this, would be to produce a shallow copy of the observer list within the locked section and iterate over the copy outside the locked section. This eliminates the call to outside defined code while holding locks. This idea is exemplified in the updated version of the \bscode{setValue} method depicted in \bsref{lst:observer_updated}.

\begin{lstlisting}[float,label=lst:observer_updated,
  caption={Observer pattern with locks},
  language=Java,
  showspaces=false,
  showtabs=false,
  breaklines=true,
  showstringspaces=false,
  breakatwhitespace=true,
  commentstyle=\color{greencomments},
  keywordstyle=\color{bluekeywords},
  stringstyle=\color{redstrings}]  % Start your code-block

    public void setValue(int newValue) throws InterruptedException {
        List<Observer> shallowCopy;
        sem.acquire();
        value = newValue;
        shallowCopy = new ArrayList<>(observers);
        sem.release();

        for (Observer o : shallowCopy) {
            o.notify(this,newValue);
        }
    }
\end{lstlisting}

%As an example imagine if that the programmer defined code takes the attempts to acquire the same lock that the framework currently holds.  Because the framework holds the locks

\section{\acl{TL} Characteristics}\label{sec_tl_char}
This section presents how the \ac{TL} concurrency model relates to the selected characteristics presented in \bsref{chap:char}.

\subsection{Implicit or Explicit Concurrency}
As described in \bsref{subsec:threads_shared_memory}, the \ac{TL} concurrency model specifies concurrency and synchronization by starting threads and applying locks on shared memory. Correctness is assured by locking access to critical regions. All of these operations are explicitly stated by the programmer. As such we say that the \ac{TL} concurrency model explicitly states concurrency. The placement is visualized in \bsref{fig:char_implicit_explicit}.

\begin{figure}[htbp]
\centering
 \includegraphics[width=0.9\textwidth]{\rootpath/worksheets/threads_and_locks/figures/tl_char_implicit_explicit}
 \caption{\ac{TL} on the implicit - explicit concurrency spectrum}
\label{fig:char_implicit_explicit}
\end{figure}

\subsection{Fault Restrictive or Expressive Model}
\ac{TL} forces very little upon the programmer. The programmer is left alone to ensure correct execution using locks as well as deciding on a fitting lock granularity. The programmer is given a lot of freedom in expressing concurrency at the cost of having to ensure correct execution herself. Based on these observations we say that \ac{TL} is an expressive concurrency model as shown in \bsref{fig:char_fault_expressive}.

\begin{figure}[htbp]
\centering
 \includegraphics[width=0.9\textwidth]{\rootpath/worksheets/threads_and_locks/figures/tl_char_fault_expressive}
 \caption{\ac{TL} on the fault restrictive - expressive spectrum}
\label{fig:char_fault_expressive}
\end{figure}

\subsection{Pessimistic or Optimistic Model}
As described in \bsref{sec:locks_me}, the \ac{TL} concurrency model uses locks to ensure mutual exclusion in order to eliminate race conditions. That is, the \ac{TL} concurrency model uses locks to eliminate errors. \ac{TL} assumes that errors will occur and attempts to prevent them. Furthermore, \ac{TL} provides no options for recovery in case of errors. Based on these observations we say that \ac{TL} is a pessimistic model as shown in \bsref{fig:char_pes_opti}.

\begin{figure}[htbp]
\centering
 \includegraphics[width=0.9\textwidth]{\rootpath/worksheets/threads_and_locks/figures/tl_char_pessimistic_optemistic}
 \caption{\ac{TL} on the pessimistic - optimistic spectrum}
\label{fig:char_pes_opti}
\end{figure}

\subsection{Readability \& Writability}\label{subsec:tl_charac_read_and_write}
As mentioned in \bsref{sec:readability} and \bsref{sec:writablity}, the evaluation of readability and writablity will be based upon the evaluation of the sub characteristics, on which they are based. As two of these, simplicity and orthogonality, are common for both readability and writability, an evaluation of these is presented first. After this, an evaluation of the readability properties of the \ac{TL} concurrency model is presented, followed by the evaluation of \ac{TL} concurrency models level of abstraction and expressivity. Finally an evaluation of the writability of the \ac{TL} concurrency model is presented.

%that of simplicity and orthogonality as well as a number of other considerations. Simplicity and orthogonality is described in the following sections followed by a final evaluation of readability.
\subsubsection{Low or High Simplicity}\label{subsec:tl_simplicity_read}
As described in \bsref{subsec:tl_lock_hard} and \bsref{subsec:tl_composability} the \ac{TL} concurrency model has a number of issues which contribute negatively to its simplicity. When taking multiple locks, taking them in incorrect order might result in a deadlock. Locking is however, as described in \bsref{subsec:tl_lock_hard}, a global property and the correct order might not be directly discernible by the reader, from within the local context. As such it is no simple task for the reader to reason about the order of locking.

\bsref{subsec:tl_composability} describes how the \ac{TL} model is not composable. Implementing the observer pattern in a thread safe manner was shown to entail a number of issues. The potential for concurrency related programmer errors in similar implementations is high and identifying these errors can potentially be a non trivial task.

In \cite{lee2006problem} the author describes development of the Ptolemy project\cite{lee1999overview}, which involved a significant aspect of concurrency. During the development phase of this project, the software engineering approaches of design reviews, code reviews, nightly builds, regression tests, and automated code coverage metrics where employed in order to produce a bug free program\cite[p. 8]{lee2006problem}. Even though the team achieved 100\% code coverage and all code was reviewed by experts, the system still deadlocked after having been in production for four years, indicating that employing good software engineering principles, might not be enough to catch all concurrency related errors, even among experts.

Based on the issues mentioned here, as well as the sheer number of concurrency related issue that can arise when using the \ac{TL} concurrency model, we say that the \ac{TL} model has low simplicity. Its placements on the simplicity spectrum is depicted in \bsref{fig:char_read_simplicity}.

\begin{figure}[htbp]
\centering
 \includegraphics[width=0.9\textwidth]{\rootpath/worksheets/threads_and_locks/figures/tl_char_read_simplicity}
 \caption{\ac{TL} on the low - high simplicity spectrum}
\label{fig:char_read_simplicity}
\end{figure}

\subsubsection{Low or High Orthogonality}\label{sec:tl_orthogonality}
The \ac{TL} concurrency model consists of only a few constructs. Threads are started in order to introduce concurrency and synchronization is achieved using some form of locking. These basic constructs can be combined in a large number of ways, in order to produce concurrent programs. As such the \ac{TL} concurrency model seems to be orthogonal as it consists of a small number of constructs, which can be combined in a large number of ways. Each of the constructs does however have its own distinct purpose, which means that only certain combinations of the constructs are useful. In fact some erroneous combinations can lead to serious issues such as deadlocks. We say that the \ac{TL} concurrency model is towards the high orthogonality end of the low - high orthogonal spectrum. This was chosen based on the number of constructs and combinations of these. The fact that some combinations can lead to program errors which are hard to detect has however kept the \ac{TL} concurrency model from being considered truly orthogonal. The placement of the \ac{TL} concurrency model on the spectrum is depicted in \bsref{fig:char_tl_orthogonality}.

\begin{figure}[htbp]
\centering
 \includegraphics[width=0.9\textwidth]{\rootpath/worksheets/threads_and_locks/figures/tl_char_orthogonality}
 \caption{\ac{TL} on the low - high orthogonality spectrum}
\label{fig:char_tl_orthogonality}
\end{figure}

\subsubsection{Low or High Readability}
\label{subsec:tl_char_readability}
As described in \bsref{subsec:tl_simplicity_read} the simplicity of the \ac{TL} model as residing in the low end of the low - high simplicity spectrum. \bsref{sec:tl_orthogonality} say that the orthogonality resides slightly towards the high end of the low - high orthogonality spectrum. These results directly influence the readability of the \ac{TL} concurrency model.

\ac{TL} based concurrency implementations can be very fragmented. Shared memory can be accessed from different parts of the program and requires locking in each of these places. When a programmer reads the code present at one of these places, she can choose to focus only on understanding this part of the code, reducing the scope of what she has to reason about. Doing so will however only allow the programmer to understand this segment of the code, but not reason about its correctness as this depends on the code present at every place where the shared memory is accessed. Reasoning about the correctness of a \ac{TL} based implementation, requires knowledge of all these places and is generally considered to be a non trivial task.

Considering this as well as the evaluation of simplicity and orthogonality we say that the \ac{TL} concurrency model is on the low end of the low - high readability spectrum. The main reason for this assessment being the low simplicity of the model, which makes it hard to reason about the correctness of a implementation. Gathering the intent of a code segment locking access to some shared memory is relatively straight forward, but reasoning about the correctness of the code, in the context of the entire systems, is much harder. The number of issues that the programmer has to reason about when determining correctness further exacerbates the issue. The placement of the \ac{TL} concurrency model on the low - high readability spectrum is depicted in \bsref{fig:char_tl_readability}.

\begin{figure}[htbp]
\centering
 \includegraphics[width=0.9\textwidth]{\rootpath/worksheets/threads_and_locks/figures/tl_char_readability}
 \caption{\ac{TL} on the low - high readability spectrum}
\label{fig:char_tl_readability}
\end{figure}

\subsubsection{Low or High Level of Abstraction}\label{sec:tl_level_of_abstraction}
The \ac{TL} concurrency model is tightly coupled with the underlying hardware architecture. Threads are part of the process model used in the \ac{OS} and the \ac{TL} concurrency model directly uses threads in order to introduce concurrency. Synchronization happens via shared memory which is also part of the process model. The locking is done via supporting hardware instructions such as Test-and-set or Compare-and-swap\cite[p. 1990]{scott2011sync}. Many languages now include abstractions, such as Java's ExecutorService\footnote{\url{http://docs.oracle.com/javase/7/docs/api/java/util/concurrent/ExecutorService.html}}, which hide the underlying threads from the programmer. However, such abstractions only helps in managing reuse of threads, and not where to deploy locks. Because the abstractions which the \ac{TL} concurrency model offers is so tightly coupled with the hardware and \ac{OS}, we say that the \ac{TL} concurrency model has a low level of abstraction. The placement of the \ac{TL} concurrency model on the low - high level of abstraction spectrum is depicted in \bsref{fig:char_tl_readability}.

\begin{figure}[htbp]
\centering
 \includegraphics[width=0.9\textwidth]{\rootpath/worksheets/threads_and_locks/figures/tl_char_level_of_abstraction}
 \caption{\ac{TL} on the low - high level of abstraction spectrum}
\label{fig:char_tl_level_of_abstraction}
\end{figure}

\subsubsection{Low or High Expressivity}\label{sec:tl_expressivity}
The expressivity of the \ac{TL} concurrency model is tightly coupled with its level of abstraction. As the constructs that \ac{TL} offers are so close to the hardware primitives, the expressivity of the \ac{TL} concurrency model suffers.

Using the \ac{TL} concurrency model, concurrency is expressed by starting threads and locking access to critical regions. Starting a thread to introduce concurrency is a low level operation, directly related to the process model discussed in \bsref{sec:processes_threads}.

As with starting threads, locking is a low level construct. As discussed in \bsref{sec:locks_me} locking introduces a number of issues which are left up to the programmer to handle. Having to consider these issues limits the expressivity of the model.

Based on these considerations, we say that the \ac{TL} concurrency model has low expressivity. The placement of the \ac{TL} concurrency model on the low - high expressivity spectrum is depicted in \bsref{fig:char_tl_expressivity}.

\begin{figure}[htbp]
\centering
 \includegraphics[width=0.9\textwidth]{\rootpath/worksheets/threads_and_locks/figures/tl_char_expressivity}
 \caption{\ac{TL} on the low - high expressivity spectrum}
\label{fig:char_tl_expressivity}
\end{figure}

\subsubsection{Low or High Writability}
Writing correct \ac{TL} based concurrent implementations is generally considered to be hard\cite[p. 56]{sutter2005software}. As discussed in \bsref{sec:tl_level_of_abstraction}, the \ac{TL} concurrency model has a low level of abstraction where the programmer has to deal with a number of low level details. As a result the programmer is in control of these details but is also forced to manage them limiting the writability of the model.

As discussed in \bsref{sec:tl_expressivity} the \ac{TL} concurrency model has low expressivity, which in turn limits the writablity of the model. If it is cumbersome to correctly express concurrency, writing a concurrent implementation naturally becomes more cumbersome.

The orthogonality of the \ac{TL} concurrency model contributes positively to its writability. Having only a few basic constructs makes it easier for the programmer to learn, recall and use them. As combining these constructs correctly is a non trivial task, the positive effect of the \ac{TL} concurrency models orthogonality properties is limited, resulting in only limited impact on the models writability.

As discussed in \bsref{subsec:tl_simplicity_read}, providing mutual exclusion by locking access to critical regions is a cumbersome task, which is left up to the programmer. While starting threads to introduce concurrency is a relatively simple task, locking requires the programmer to reason about every part of the program in which synchronization is to be made. If the programmer misses just one of these parts, it can introduce race conditions. Furthermore if the programmer makes mistakes while implementing the required locking, it can lead to serious errors such as deadlocks.

In \bsref{sec:tl_ci} a number of concurrency related issues which can arise in the \ac{TL} concurrency model is discussed. Programmers using the \ac{TL} concurrency model have to considerer these issues, which contributes negatively to the models writability. The programmer is forced to think about how these issues can be avoided, which in turn limits the mental effort the programmer can put into solving the problem. Furthermore, having factor these issues in, decreases the productivity of the programmer.

Based on these observations, as well as the evaluation of simplicity and orthogonality, we say that the \ac{TL} concurrency model has low writability. The placement of the \ac{TL} concurrency model on the low - high writability spectrum is depicted in \bsref{fig:char_tl_writability}.

\begin{figure}[htbp]
\centering
 \includegraphics[width=0.9\textwidth]{\rootpath/worksheets/threads_and_locks/figures/tl_char_writability}
 \caption{\ac{TL} on the low - high writability spectrum}
\label{fig:char_tl_writability}
\end{figure}

\worksheetend

max_stars_repo_name: Felorati/scalability

max_issues_repo_name: Felorati/scalability

max_forks_repo_name: Felorati/scalability


text:
% Options for packages loaded elsewhere
\PassOptionsToPackage{unicode}{hyperref}
\PassOptionsToPackage{hyphens}{url}
\PassOptionsToPackage{dvipsnames,svgnames*,x11names*}{xcolor}
%
\documentclass[
]{article}
\usepackage{lmodern}
\usepackage{amssymb,amsmath}
\usepackage{ifxetex,ifluatex}
\ifnum 0\ifxetex 1\fi\ifluatex 1\fi=0 % if pdftex
  \usepackage[T1]{fontenc}
  \usepackage[utf8]{inputenc}
  \usepackage{textcomp} % provide euro and other symbols
\else % if luatex or xetex
  \usepackage{unicode-math}
  \defaultfontfeatures{Scale=MatchLowercase}
  \defaultfontfeatures[\rmfamily]{Ligatures=TeX,Scale=1}
\fi
% Use upquote if available, for straight quotes in verbatim environments
\IfFileExists{upquote.sty}{\usepackage{upquote}}{}
\IfFileExists{microtype.sty}{% use microtype if available
  \usepackage[]{microtype}
  \UseMicrotypeSet[protrusion]{basicmath} % disable protrusion for tt fonts
}{}
\makeatletter
\@ifundefined{KOMAClassName}{% if non-KOMA class
  \IfFileExists{parskip.sty}{%
    \usepackage{parskip}
  }{% else
    \setlength{\parindent}{0pt}
    \setlength{\parskip}{6pt plus 2pt minus 1pt}}
}{% if KOMA class
  \KOMAoptions{parskip=half}}
\makeatother
\usepackage{xcolor}
\IfFileExists{xurl.sty}{\usepackage{xurl}}{} % add URL line breaks if available
\IfFileExists{bookmark.sty}{\usepackage{bookmark}}{\usepackage{hyperref}}
\hypersetup{
  colorlinks=true,
  linkcolor=blue,
  filecolor=Maroon,
  citecolor=Blue,
  urlcolor=Blue,
  pdfcreator={LaTeX via pandoc}}
\urlstyle{same} % disable monospaced font for URLs
\usepackage{listings}
\newcommand{\passthrough}[1]{#1}
\lstset{defaultdialect=[5.3]Lua}
\lstset{defaultdialect=[x86masm]Assembler}
\usepackage{longtable,booktabs}
% Correct order of tables after \paragraph or \subparagraph
\usepackage{etoolbox}
\makeatletter
\patchcmd\longtable{\par}{\if@noskipsec\mbox{}\fi\par}{}{}
\makeatother
% Allow footnotes in longtable head/foot
\IfFileExists{footnotehyper.sty}{\usepackage{footnotehyper}}{\usepackage{footnote}}
\makesavenoteenv{longtable}
\setlength{\emergencystretch}{3em} % prevent overfull lines
\providecommand{\tightlist}{%
  \setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}}
\setcounter{secnumdepth}{5}

\ifluatex
  \usepackage{selnolig}  % disable illegal ligatures
\fi

\author{}
\date{}

\begin{document}

\lstset{columns=fullflexible,breaklines=true,basicstyle=\small\ttfamily,backgroundcolor=\color{gray!10}}

\hypertarget{naive-bayes-for-classification}{%
\section{Naive Bayes for
Classification}\label{naive-bayes-for-classification}}

\hypertarget{sentiment-analysis}{%
\subsection{Sentiment Analysis}\label{sentiment-analysis}}

\begin{itemize}
\item
  Sentiment analysis is the problem of extracting the author's tone from
  a piece of text.
\item
  A simple example is deciding if a product review is positive or
  negative. Here are some short reviews of Amazon products, labelled
  with a 0 if they are negative or a 1 if they are positive.
\end{itemize}

\begin{lstlisting}
So there is no way for me to plug it in here in the US unless I go by a converter.  0
Good case, Excellent value. 1
Great for the jawbone.  1
Tied to charger for conversations lasting more than 45 minutes.MAJOR PROBLEMS!! 0
The mic is great.   1
\end{lstlisting}

\begin{itemize}
\item
  We have three files each with 1000 labelled reviews, 500 of which are
  positive, 500 negative:

  \begin{itemize}
  \tightlist
  \item
    amazon reviews of products
  \item
    yelp reviews of restaurants
  \item
    imdb reviews of movies
  \end{itemize}
\item
  Our method will be \emph{supervised learning} where we use a set of
  pre-labelled reviews to develop an algorithm that we can then apply to
  new, unlabelled reviews.
\item
  Building a Spam filter is another example of this type of problem.
\end{itemize}

\newpage

\hypertarget{bernoulli-tests}{%
\subsection{Bernoulli tests}\label{bernoulli-tests}}

\begin{itemize}
\tightlist
\item
  Building block: presence or absence of keywords. Each word is a
  ``test.''
\end{itemize}

\begin{longtable}[]{@{}llll@{}}
\toprule
& + & - & total\tabularnewline
\midrule
\endhead
\textbf{great} & 92 & 5 & 97\tabularnewline
\textasciitilde{}\textbf{great} & 408 & 495 & 903\tabularnewline
total & 500 & 500 & 1000\tabularnewline
\bottomrule
\end{longtable}

\[ P (\mathbf{great} | +) =  .184 \]

\[ P(\mathbf{great})  = .097 \]

\[P(+|\mathbf{great}) = .948 \]

\[P(+|\sim\mathbf{great}) = .452\]

\begin{longtable}[]{@{}llll@{}}
\toprule
& + & - & total\tabularnewline
\midrule
\endhead
\textbf{waste} & 0 & 14 & 14\tabularnewline
\textasciitilde{}\textbf{waste} & 500 & 486 & 986\tabularnewline
total & 500 & 500 & 1000\tabularnewline
\bottomrule
\end{longtable}

\begin{align*}
P(+|\mathbf{waste}) &= 0\\
P(+|\sim\mathbf{waste}) &= .51
\end{align*}

\hypertarget{independence-assumption}{%
\subsection{Independence assumption}\label{independence-assumption}}

\begin{itemize}
\tightlist
\item
  We make the (false) assumption that each keyword gives an independent
  test.
\end{itemize}

\begin{align*}
P(\mathbf{great},\mathbf{waste}|\pm) &= P(\mathbf{great}|\pm)P(\mathbf{waste}|\pm)\\
P(\mathbf{great},\sim\mathbf{waste}|\pm) &= P(\mathbf{great}|\pm)P(\sim\mathbf{waste}|\pm)\\
 &\vdots \\
\end{align*}

\[
P(+|\mathbf{great},\sim\mathbf{waste}) = \frac{P(\mathbf{great}|+)P(\sim\mathbf{waste}|+)P(+)}{P(\mathbf{great},\sim\mathbf{waste})}
\]

\[
P(-|\mathbf{great},\sim\mathbf{waste}) = \frac{P(\mathbf{great}|-)P(\sim\mathbf{waste}|-)P(-)}{P(\mathbf{great},\sim\mathbf{waste})}
\]

\begin{itemize}
\tightlist
\item
  Decision rule: compare probabilities. But only the numerator matters
  -- this is called the ``likelihood.''
\end{itemize}

\[
L(+|\mathbf{great},\sim\mathbf{waste}) = (.184)(1)(.5) = .092
\]

\[
L(-|\mathbf{great},\sim\mathbf{waste}) = (.01)(.028)(.5) = .00014
\]

\hypertarget{feature-vectors}{%
\subsection{Feature vectors}\label{feature-vectors}}

\begin{itemize}
\item
  Given words \(w_1,\ldots, w_k\), with probabilities \(P(w_{i}|\pm)\),
  we imagine independent tests.
\item
  The ``naive'' probabilities come from the training data:
\end{itemize}

\[
P(w_{i}|\pm) = \frac{\hbox{\rm number of \pm reviews that include $w_{i}$}}{\hbox{\rm total $\pm$ reviews}}
\]

\begin{itemize}
\item
  All we need to know about a document is whether or not each of the key
  words appears.
\item
  So a document can be replaced by a vector of \(1/0\) (called a
  ``feature vector'') where \(f_{i}=1\) if \(w_{i}\) appears, and \(0\)
  if it doesn't appear.
\end{itemize}

\end{document}

ext: tex


text:
\documentclass{article}

\usepackage{pifont}
\usepackage{graphicx} %[pdftex] OR [dvips]
\usepackage{fullpage}
\usepackage{wrapfig}
\usepackage{float}
\usepackage{titling}
\usepackage{hyperref}
\usepackage{tikz}
\usepackage{color}
\usepackage{footnote}
\usepackage{float}
\usepackage{algorithm}
\usepackage{algpseudocode}
\usetikzlibrary{arrows}
\usetikzlibrary{positioning}
\setlength{\droptitle}{-6em}

\newcommand{\Red}[1]{{\color{red} #1}}

\input{commands-new-new.tex}

\newcommand{\nuAA}{\nu_\mathit{AA}}
\newcommand{\nuAB}{\nu_\mathit{AB}}
\newcommand{\nuGA}{\nu_\mathit{GA}}
\newcommand{\nuGB}{\nu_\mathit{GB}}
\newcommand{\betaPL}{\beta_\mathit{PL}}
\newcommand{\betaAA}{\beta_\mathit{AA}}
\newcommand{\betaAS}{\beta_\mathit{AS}}
\newcommand{\thinandalso}{\hspace{.45cm}}
\newcommand{\thinnerandalso}{\hspace{.38cm}}

\input{commands-rebindings.tex}

\newcommand{\var}[1]{\textsf{#1}}

\newcommand{\ghcfile}[1]{\textsl{#1}}

\title{$\mu$Backpack}

\begin{document}

\maketitle

$\mu$Backpack is a simplified version of
Backpack which is easier to implement and explain. Changes:

\begin{itemize}
    \item A reexport may not be used to implement a declaration in a signature, \emph{unless} the implementation comes textually before all signature, including included signatures (i.e., absent mutual recursion.)
\item Type identity is computed by considering \emph{all} of the holes in the package.
\item No aliases, unless shaping is used.
\item Mutual recursion is not permitted, unless shaping is used.
\end{itemize}

Generally speaking, you are subject to \verb|hs-boot| style restrictions when mutual
recursion is used, and no restrictions otherwise.

\section{Things that don't work}

\paragraph{No re-exports} Signatures cannot be implemented using a module
which reexports the entity in question, unless the implementation preceeds
the signature.  This example is rejected:

\begin{example}
\Pdef{p}{
    \Psig{A}{x :: Bool}
    \Pmod{B}{x = True}
    \Pmod{A}{\Mimp{B}; \Mexp{x}}
}
\end{example}

This restriction is the same as the restriction in \verb|hs-boot| files.

\paragraph{No module-level granularity} In the following example, \verb|B1.B| and
\verb|B2.B| are not type-equal:

\begin{example}
\Pdef{p}{
    \Psig{A}{data A}
    \Pmod{B}{data B = B}
} &
\Pdef{q}{
    \Pmod{A1}{data A = A1}
    \Pmod{A2}{data A = A2}
    \Pinct{p}{\Emvp{A}{A1}, \Emvp{B}{B1}}
    \Pinct{p}{\Emvp{A}{A2}, \Emvp{B}{B2}}
}
\end{example}

\paragraph{No inter-package mutual recursion} Inter-package mutual recursion requires a separate shaping pass
to determine module identities (for same-package mutual recursion, the identity is known in advance.)

\section{Worked example}

\begin{example}
\Pdef{p}{
    \Psig{A}{data A; x :: A}
    \Pmod{B}{\Mimp{A}; data B = B A}
} &
\Pdef{q}{
    \Psig{A}{data A; y :: A}
    \Pmod{C}{\Mimp{A}; data C = C A}
} \\
\Pdef{r}{
    \Pmod{P}{data A = A; x = A}
    \Pmod{A2}{\Mimp{P}; \Mexp{A}}
    \Pinc{p}
    \Pinc{q}
%    \Pref{A3}{A}
    \Pinct{p}{\Emvp{A}{A2}, \Emvp{B}{B2}}
    \Pmodbig{D}{\ldots \textit{stuff} \ldots}
}
\end{example}

This example exercises a few features that Backpack provides:

\begin{itemize}
\item \verb|A| is never instantiated, so we can only typecheck these packages.
\item \verb|A| from \verb|p| and \verb|q| are linked together.
\item A fresh instance of \verb|A| from \verb|p| is linked against \verb|A2|.
%\item \verb|A| is aliased with \verb|A3|, so the same hole is exported from a package under different names.
\end{itemize}

At the end of type-checking \verb|r|, we have the following mapping of
module names to identities:

\begin{itemize}
    \item \mname{A} has identity $\alpha_A$.  When we import \mname{A}, we
        actually see \emph{two} interfaces: one which exports
        $\alpha_{A}.$\verb|A| and $\alpha_{A}.$\verb|x| (from
        \pname{p}), and one which exports $\alpha_{A}.$\verb|A| and
        $\alpha_{A}.$\verb|y| (from \pname{q}).  An import of \mname{A}
        effectively imports the merge of these two interfaces, but this
        merging process is left to be handled at the Haskell source
        level.\footnote{From an implementation perspective, this is
        helpful because otherwise, it's not really clear who should actually
        do signature merging.  Deferring merges to import time is convenient
    to implement.}  The mapping of
        interfaces is a local property: for example, when type-checking
        \mname{B}, only one interface is available (the one from
        \pname{p}).
\item \mname{B} has identity $\nu_B$, where $\nu_B=$ \pname{p}(\mname{A} $\mapsto\alpha_A$):\mname{B} (read this as, ``module \mname{B} from package \pname{p} with \mname{A} instantiated with $\alpha_A$'').  Its interface exports $\nu_{B}.$\verb|B| with a single constructor $\nu_{B}.$\verb|B| $\cc$ $\alpha_{A}.$\verb|A| $\rightarrow$ $\nu_{B}.$\verb|B|
\item \mname{C} has identity $\nu_C$, where $\nu_C=$ \pname{q}(\mname{A} $\mapsto\alpha_A$):\mname{C}. Its interface exports $\nu_{C}.$\verb|C| with a single constructor $\nu_{C}.$\verb|C| $\cc$ $\alpha_{A}.$\verb|A| $\rightarrow$ $\nu_{C}.$\verb|C|
\item \mname{P} has identity $\nu_P$, where $\nu_P=$ \pname{r}(\mname{A} $\mapsto\alpha_A$):\mname{P}. Its interface exports $\nu_{P}.$\verb|A| and $\nu_{P}.$\verb|x|.
\item \mname{A2} has identity $\nu_{A2}$, where $\nu_{A2}=$ \pname{r}(\mname{A} $\mapsto\alpha_A$):\mname{A2}. Its interface exports $\nu_{P}.$\verb|A| (nota bene, this is \emph{not} $\nu_{A2}.$\verb|A|!)
\item \mname{B2} has identity $\nu_{B2}$, where $\nu_{B2}=$ \pname{p}(\mname{A} $\mapsto\nu_{A2}$):\mname{B}. Its interface exports $\nu_{B2}.$\verb|B| with a single constructor $\nu_{B2}.$\verb|B| $\cc$ $\alpha_{A}.$\verb|A| $\rightarrow$ $\nu_{B2}.$\verb|B|
%\item \mname{A3} is $\alpha_A$
\item \mname{D} has identity $\nu_{D}$, where $\nu_{D}=$ \pname{r}(\mname{A} $\mapsto\alpha_A$):\mname{D}. Its interface exports stuff.
\end{itemize}

\section{The rules}

\paragraph{Nomenclature}  We use \emph{interface} ($\tau$) to refer to the type of a module.

\paragraph{The environment}  While type-checking a package, we have the following pieces of information:

\begin{itemize}
    \item A package environment $\Delta$, which holds the package definitions of all packages in scope.
    \item The current package name $P$ and hole instantiation $\mathcal{H}$, such that for any module $m$ defined in the package, $P(\mathcal{H})$:$m$ is the identity of that module (package level granularity).
    \item The package context $\Gamma$.  This is a mapping from a module name to its identity and interfaces (plural!), accumulated from the modules/signatures we have type-checked and put into scope under this name.
    \item \textbf{Optional.} An implementation cache $\Phi$.  This is a mapping from module identity to interface for each identity that has a final implementation type-checked.  This context is used to determine if an implementation comes textually before a signature (if so, when type checking the signature, the module will be present in the implementation cache).  In the absence of this cache, reexports are never allowed in implementations (the \verb|hs-boot| restriction always applies).
\end{itemize}

To begin type-checking of a particular indefinite package, generate fresh module variables $\alpha$ for each hole of the package (this is the only time module variables are generated).  Set $P$ to the name of the package, and $\mathcal{H}$ to be a mapping of each hole to the fresh module identity variables and begin type-checking each binding starting with an empty package context and implementation cache.

\paragraph{Calculate holes}  As a pre-processing step, we elaborate the
syntax with the holes each package
requires.  This proceeds recursively: the holes of a package are any
signatures it defines, as well as the renamed holes of any packages it includes,
minus any implemented modules.  We assume for any package definition in the
package environment $\Delta$, we can tell what holes it requires.
In the worked example, the set of
holes for each of the packages is just \mname{A}.

\paragraph{Typing modules} A module definition $m = [M]$ is
straightforwardly type-checked by using the Haskell level typing
judgment $\Gamma; \nu_0 \vdash M : \tau$, where $\nu_0 =
P(\mathcal{H})$:$m$.  The resulting interface $\tau$ is brought into the
package context as the logical binding $m \mapsto \nu_0@\tau$; we also
record $\nu_0 : \tau$ in the implementation cache.

\paragraph{Typing signatures}  A signature definition $m :: [S]$ is
type-checked with the Haskell level typing judgment
$\Gamma; \nu_0 \vdash S : \tau$, where $\nu_0 = \mathcal{H}(m)$ if
this hole was instantiated externally, or $\nu_0 = \Gamma(m)$ if it
was instantiated internally.  If the identity $\mathcal{H}(m)$ is
already in the physical cache $\Phi$, then the identities
of the declarations in the signature are taken from the interface $\Phi(\mathcal{H}(m))$ (with the types checked for consistency);
otherwise, they are given \emph{fresh} identities originating from $\mathcal{H}(m)$
(in the same manner as an hs-boot file).  The resulting type $\tau$ is brought into
the package context as the logical binding $p \mapsto \mathcal{H}(m)@\tau$.

From the worked example, when \mname{A} is type-checked from \pname{p} of
the first inclusion, $\mathcal{H}($\mname{A}$) = \alpha_A$, there is no implementation in $\Phi$, so the type \verb|T|
is assigned the original name $\alpha_A.$\verb|T|.  In the second inclusion,
$\mathcal{H}($\mname{A}$) =$ \pname{r}(\mname{A} $\mapsto\alpha_A$):\mname{A2},
which is implemented, so we look at the original name of \verb|T| in \mname{A2} and
assign our type \verb|T| the same: \pname{r}(\mname{A} $\mapsto\alpha_A$):\mname{P}.\verb|T|
(notably, \mname{A2} is no where to be seen in this identifier, as it would be under
the rule for holes.)

\paragraph{Typing includes}

An include of package $P$ with renaming $r$ is typed by recursively typechecking the
source pointed to by $P$ ($\Delta(P)$), but with an adjusted
$\mathcal{H}'$ given thinning and renaming (and an empty context $\Gamma'$.  In particular: the new
$\mathcal{H}'$ is computed by taking the holes of $P$,
renaming them according to $r$, and then finding the identities in
$\mathcal{H}$ or $\Gamma$.  In the case of cross-package mutual recursion, this
lookup would fail (the shaping pass serves as an oracle which provides the
correct identity).

In the worked example, we type-check with the following parameters:

\begin{itemize}
    \item Top-level: $P=$ \pname{r}, $\mathcal{H}=A\mapsto\alpha_A$
    \item \verb|include p|: $P=$ \pname{p}, $\mathcal{H}=A\mapsto\alpha_A$
    \item \verb|include q|: $P=$ \pname{q}, $\mathcal{H}=A\mapsto\alpha_A$
    \item \verb|include p (A as A2, B as B2)|: $P=$ \pname{p}, $\mathcal{H}=A\mapsto\nu_{A2}$

\end{itemize}

After recursively typechecking, we are left with a new context $\Gamma'$.  The
logical mapping of this context is renamed according to $r$, and then added to
our current context (along with the implementation cache).

This is a non-compositional typing rule.

\paragraph{Merging package contexts} If you have two bindings $m \mapsto \nu:\overline{\tau}$;
check that the identities $\nu$ agree, and that all of the types are consistent with one another. If so, create a new binding with the lists of $\tau$
concatenated together. As an optimization, if one $\tau$ is from the final implementation, all other $\tau$s can be discarded (as they are guaranteed to be subsets of the final $\tau$).

\paragraph{Merging implementation caches} Cache merging is a trivial union; given
two equal physical module identities their interfaces are guaranteed to be the same.

\section{Complications}

\subsection{Signature consistency}

Suppose that you want to use a signature, but you don't want to export it:

\begin{example}
\Pdeft{p}{\m{P}}{
    \Psig{A}{data A = A Bool}
    \Pmod{P}{\Mimp{A}; \ldots}
} &
\Pdef{q}{
    \Pinc{p}
    \Pmod{Q}{\Mimp{P}; \ldots}
}
\end{example}

Evidently, we can't \emph{completely} eliminate \m{A}, since eventually
we'll need to fill it in with an implementation.  Thus, the thinning
must actually be shorthand for making a logical mapping in the context
to an \emph{empty} list of interfaces.  In this example, in the context
visible from \m{Q}, there is a binding for \m{A} which has module
identity $\alpha_A$ but no interfaces.

\paragraph{The bug} If we modify \pname{q} to be:

\begin{example}
\Pdef{q}{
    \Pinc{p}
    \Psig{A}{data A = A Int}
    \Pmod{Q}{\Mimp{P}; \ldots}
}
\end{example}

Both \m{A} from \pname{p} and \m{A} from \pname{q} have the same module
identity, but their signatures are incompatible.  However, while
type-checking, we only check for signature consistency when (1) there is
a backing implementation, and (2) when merging logical contexts.  The
first check is inapplicable in this case (\m{A} is a hole), and the
second check does not see the inconsistency, because $\tau$ from
\pname{p} was dropped.

\paragraph{The fix} The correct approach is to \emph{keep} the
types in the mapping (for consistency checking), but mark them as hidden
(so they are not loaded on import).

\subsection{Hole duplication}

Hole duplication is when an indefinite module identity $\alpha$ is
available from a package under multiple names.  While this is
technically disallowed under the current syntax in the absence of
aliases, there are easy to imagine syntactic extensions which achieve
this, e.g.

\begin{example}
\Pdeft{p}{\m{P}}{
    \Psig{A}{data A}
} &
\Pdef{q}{
    \Pinct{p}{\Emvp{A}{A1}, \Emvp{A}{A2}}
    \Pinct{p}{\Emvp{A}{A3}}
}
\end{example}

In this example, \m{A1} and \m{A2} have the same identity, while \m{A3}
has a different identity.  Another example would be to have the multiple
renaming occur in the thinning specification of a package.

\paragraph{The bug} If the holes of \pname{q} are specified to be
\m{A1}, \m{A2} and \m{A3}, then when type-checking \pname{q} we will
create three fresh identities, and \m{A1}.\verb|A| and \m{A2}.\verb|A|
will not unify, even though they should.

\paragraph{The fix} For every module identity, there must be a module
name which is nominated as the \emph{principal} hole: this is the only
module which is included in the list of holes.  This is the \emph{only}
hole which can be linked against to set the identity of the hole; any
other occurrence of the module identity is ineligible.  Thus, in the
previous example, if \m{A1} is the principal hole, then the holes of
\pname{q} are \m{A1} and \m{A3}, and there is one valid linking:

\begin{example}
\Pdef{r-ok}{
    \Pmod{A1}{data A = A}
    \Pinc{q}
} &
\Pdef{r-failed}{
    \Pmod{A2}{data A = A}
    \Pinc{q}
}
\end{example}

\subsection{Module binding reordering}

We stated that re-exports are not allowed if the implementation preceeds
the signature, as in this example:

\begin{example}
\Pdef{p}{
    \Psig{A}{x :: Bool}
    \Pmod{C}{\Mimp{A}; y = True}
    \Pmod{B}{x = True}
    \Pmod{A}{\Mimp{B}; y = False; \Mexp{x, y}}
    \Pmod{D}{\Mimp{A}; \Mimp{C}; \ldots}
}
\end{example}

However, in this particular example, \m{B} does not depend on the signature of \m{A},
so the bindings in this package could be reordered to restore ordering:

\begin{example}
\Pdef{p}{
    \Pmod{B}{x = True}
    \Pmod{A}{\Mimp{B}; y = False; \Mexp{x, y}}
    \Psig{A}{x :: Bool}
    \Pmod{C}{\Mimp{A}; y = True}
    \Pmod{D}{\Mimp{A}; \Mimp{C}; \ldots}
}
\end{example}

This reordering is always possible as long as there is no mutual recursion.

\paragraph{The bug} We've changed the semantics of the
package: in the original example, only \verb|x| was visible in \m{C}; in
the reordered example, both \verb|x| and \verb|y| are visible.

\paragraph{The fix} Float implementations to be type-checked
as early as possible, but do not add the resulting interface to the package
context until you arrive at their original definition site:

\begin{example}
\Pdef{p}{
    \Pmod{B}{\textit{-- hidden}; x = True}
    \Pmod{A}{\textit{-- hidden}; \Mimp{B}; y = False; \Mexp{x, y}}
    \Psig{A}{x :: Bool}
    \Pmod{C}{\Mimp{A}; y = True}
    \Pmod{B}{\textit{-- visible }}
    \Pmod{A}{\textit{-- visible }}
    \Pmod{D}{\Mimp{A}; \Mimp{C}; \ldots}
}
\end{example}

In this example, the \m{A} signature is type-checked with $\Gamma($\m{A}$) = $\pname{p}:\m{A}, which is present in the implementation cache; however, \m{C} is type-checked in a package context that only has $\tau$ from the signature, and not the implementation.

\end{document}

max_stars_repo_name: michalt/ghc

max_issues_repo_name: michalt/ghc

max_forks_repo_name: michalt/ghc


text:
\section{Continuous Random Variables}
For a probability space $(\Omega,\mathscr F,\mathbb P)$ and $X:\Omega\to\mathbb R$ such that $\{X\le x\}=\{\omega\in\Omega:X(\omega)\le x\}\in\mathscr F$.
Recall that $\forall x\in\mathbb R$ we defined the probability distribution function $F(x)=\mathbb P(X\le x)$.
\begin{proposition}
    1. $x\le y\implies F(x)\le F(y)$.\\
    2. $\forall a<b,\mathbb P(a<X\le b)=F(b)-F(a)$.\\
    3. $F$ is right continuous and the left limits always exists as well.
    Also,
    $$F(x-)=\lim_{y\to x^-}F(y)\le F(x)$$
    4. We have
    $$\lim_{x\to-\infty}F(x)=0,\lim_{x\to\infty}F(x)=1$$
\end{proposition}
\begin{proof}
    Trivial.
\end{proof}
\begin{definition}
    $X$ is a continuous random variable if $F$ is continuous.
\end{definition}
So for a continuous random variable $X$ and any $x\in\mathbb R$,
$$F(x-)=F(x)\implies\mathbb P(X<x)=\mathbb P(X\le x)\implies\mathbb P(X=x)=0$$
In this course, we shall only consider the case where $F$ is also differentiable.
Set $f(x)=F^\prime(x)$.
Call $f$ the probability density function of $X$.
\begin{proposition}
    1. $f(x)\ge 0$.\\
    2.
    $$\int_{-\infty}^x f(y)\,\mathrm dy=F(x)$$
    In particular,
    $$\int_{-\infty}^\infty f(y)\,\mathrm dy=1$$
\end{proposition}
\begin{proof}
    Obvious.
\end{proof}
Intuitively, for $\Delta x$ small, we have
$$\mathbb P(x<X\le x+\Delta x)=\int_x^{x+\Delta x}f(y)\,\mathrm dy\approx f(x)\Delta x$$
which is like approximating a continuous random variable by the probability density function of a discrete random variable.\\
Now define, as usual, $X_+=\max\{X,0\}$ and $X_-=\min\{X,0\}$.
\begin{definition}
    Let $Y\ge 0$ be a nonnegative continuous random variable, then define
    $$\mathbb E[Y]=\int_0^\infty yf(y)\,\mathrm dy$$
    And for $g\ge 0$ we define, for any $Y$ (not necessarily positive),
    $$\mathbb E[g(Y)]=\int_{-\infty}^\infty g(y)f(y)\,\mathrm dy$$
    If at least one of $\mathbb E[X_+],\mathbb E[X_-]$ is finite, we define
    $$\mathbb E[X]=\mathbb E[X_+]-\mathbb E[X_-]=\int_{-\infty}^\infty xf(x)\,\mathrm dx$$
\end{definition}
Now the expectation is again a linear function from definition.
\begin{proposition}
    Let $X$ be nonnegative, then
    $$\mathbb E[X]=\int_0^\infty\mathbb P(X\ge x)\,\mathrm dx$$
\end{proposition}
Note that due to lack of measure theory some of the steps are not fully justified.
\begin{proof}[First proof]
    Write
    $$X=\int_0^\infty 1_{X\ge x}\,\mathrm dx$$
    then taking expectation on both sides yields what we want.
\end{proof}
\begin{proof}[Second proof]
    \begin{align*}
        \mathbb E[X]&=\int_0^\infty xf(x)\,\mathrm dx\\
        &=\int_0^\infty \int_0^xf(x)\,\mathrm dy\,\mathrm dx\\
        &=\int_0^\infty\int_y^\infty f(x)\,\mathrm dx\,\mathrm dy\\
        &=\int_0^\infty\mathbb P(X\ge x)\,\mathrm dx
    \end{align*}
    As we wish.
\end{proof}
\begin{definition}
    The variance is also defined as $\operatorname{Var}(X)=\mathbb E[(X-\mathbb E[X])^2]$.
\end{definition}
\begin{example}
    1. The uniform distribution $\operatorname{Unif}(a,b)$ for $a<b$, where
    $$f(x)=\begin{cases}
        1/(b-a)\text{, if $x\in [a,b]$}\\
        0\text{, otherwise}
    \end{cases}$$
    Suppose $X$ has density $f$, then
    $$F(x)=\mathbb P(X\le x)=\int_{-\infty}^xf(x)\,\mathrm dx=\begin{cases}
        0\text{, if $x<a$}\\
        (x-a)/(b-a)\text{, if $x\in [a,b]$}\\
        1\text{, if $x>b$}
    \end{cases}$$
    So we have
    $$\mathbb E[X]=\int_{\mathbb R}xf(x)\,\mathrm dx=\int_a^bxf(x)\,\mathrm dx=\frac{a+b}{2}$$
    2. The exponential distribution $\operatorname{Exp}(\lambda)$ has density function $f(x)=\lambda e^{-\lambda x}$ where $\lambda,x>0$.
    Therefore for $x$ positive,
    $$F(x)=\int_0^x\lambda e^{-\lambda x}\,\mathrm dx=1-e^{-\lambda x}$$
    and one can check that $\mathbb E[X]=\lambda^{-1}$.\\
    The exponential distribution is kind of a limit of the geometric distribution.
    Let $T\sim\operatorname{Exp}(\lambda)$ and $T_n=\lfloor nT\rfloor$, so
    $$\mathbb P(T_n\ge k)=\mathbb P(T\ge k/n)=e^{-k\lambda/n}=(e^{-\lambda/n})^k$$
    So $T_n$ is distributed geometrically with parameter $p_n=1-e^{-\lambda/n}$, so as $n\to\infty$, we have $p_n\sim \lambda/n$ and $T_n/n\to T$.
    So the exponential distribution arises as the limit of a rescaled sequence of geometrics.\\
    The exponential distribution also has the memoryless property, that is, for any $t,s\ge 0$,
    $$\mathbb P(T>s+t|T>s)=\mathbb P(T>t)$$
    Conversely, if $T$ has the memoryless property, then let $g(t)=\mathbb P(T>t)$ (which is decreasing), then $g(t+s)=g(t)g(s)$.
    Now $g$ must be exponential in $\mathbb Q$ by simple iteration.
    Also $g$ is continuous, so $g$ must be the exponential function (with appropriate scalings), so $T$ is distributed exponentially.
\end{example}
\begin{theorem}
    Let $X$ be a continuous random variable with density $f$.
    Let $g$ be a continuous, strictly monotone function with $g^{-1}$ differentiable.
    Then $g(X)$ is a continuous random variable with density $f(g^{-1}(x))|\mathrm dg^{-1}(x)/\mathrm dx|$.
\end{theorem}
\begin{proof}
    First assume that $g$ is strictly increasing, then $\mathbb P(g(X)\le x)=\mathbb P(X\le g^{-1}(x))=F(g^{-1}(x))$, so the density of $g(X)$ would be
    $$\frac{\mathrm d}{\mathrm dx}F(g^{-1}(x))=f(g^{-1}(x))\frac{\mathrm dg^{-1}(x)}{\mathrm dx}=f(g^{-1}(x))\left|\frac{\mathrm dg^{-1}(x)}{\mathrm dx}\right|$$
    As for $g$ strictly decreasing, $\mathbb P(g(X)\le x)=\mathbb P(X\ge g^{-1}(x))=1-F(g^{-1}(x))$, so then density is
    $$\frac{\mathrm d}{\mathrm dx}(1-F(g^{-1}(x)))=-f(g^{-1}(x))\frac{\mathrm dg^{-1}(x)}{\mathrm dx}=f(g^{-1}(x))\left|\frac{\mathrm dg^{-1}(x)}{\mathrm dx}\right|$$
    as desired.
\end{proof}
\begin{example}
    For $\mu\in\mathbb R,\sigma>0$, we define the density of the normal distribution to be
    $$f(x)=\frac{1}{\sqrt{2\pi\sigma^2}}e^{-(x-\mu)^2/(2\sigma^2)}$$
    We know how to integrate the Gaussian integral, so we can verify that this is indeed a density.
    Now for a random variable $X$ having this density, we have
    $$\mathbb E[X]=\int_{-\infty}^\infty \frac{x}{\sqrt{2\pi\sigma^2}}e^{-(x-\mu)^2/(2\sigma^2)}\,\mathrm dx=\mu$$
    So $\mu$ is actually the expected value.
    Also
    $$\operatorname{Var}(X)=\mathbb E[(X-\mathbb E[X])^2]=\int_{-\infty}^\infty \frac{(x-\mu)^2}{\sqrt{2\pi\sigma^2}}e^{-(x-\mu)^2/(2\sigma^2)}\,\mathrm dx=\sigma^2$$
    This is called the normal distribution $\mathcal N(\mu,\sigma^2)$.
    We call $\mathcal N(0,1)$ the standard normal.
    So the distribution and density of the standard normal would be
    $$\Phi(x)=\int_{-\infty}^x\frac{e^{-t^2/2}}{\sqrt{2\pi}}\,\mathrm dt,\phi(x)=\frac{e^{-x^2/2}}{\sqrt{2\pi}}$$
    If we have $X\sim\mathcal N(\mu,\sigma^2)$, then for $a,b\in\mathbb R$ with $a\neq 0$, $Y=aX+b$ would have $\mathbb E[Y]=a\mu+b,\operatorname{Var}(Y)=a^2\sigma^2$ (note that $X$ needs not be normal to get these), we shall show that $Y$ is also normal with $Y\sim\mathcal N(a\mu+b,a^2\sigma^2)$.
    Let $g(x)=ax+b$, then $Y=g(X)$, we know that the density $f_Y$ of $Y$ has
    $$f_Y(y)=f(g^{-1}(Y))\left|\frac{\mathrm dg^{-1}(y)}{\mathrm dy}\right|=\frac{1}{\sqrt{2\pi a^2\sigma^2}}e^{-(y-(a\mu+b))^2/(2a^2\sigma^2)}$$
    by some calculations.
    And this is what we wanted.
    So $(X-\mu)/\sigma\sim\mathcal N(0,1)$.
    More than $95\%$ of the normal distribution lies within two standard deviations of the mean, that is $\mathbb P(|(X-\mu)/\sigma|<2)=\mathbb P(\mu-2\sigma<X\le \mu+2\sigma)\ge 95\%$.
    By some computer stuff or other calculation methods, $\mathbb P(|(X-\mu)/\sigma|<2)\ge \mathbb P(|(X-\mu)/\sigma|<1.96)\approx 0.95$
\end{example}
\begin{definition}
    Let $X$ be a continuous random variable with density $f$, the median $m$ of $X$ is a number satisfying $\mathbb P(X>m)=\mathbb P(X\le m)=1/2$.
\end{definition}
The median always exists due to intermediate value theorem.
For symmetric distributions, i.e. $f(\mu+x)=f(\mu-x)$, then $\mu$ is its median.

max_stars_repo_name: david-bai-notes/IA-Probability

max_issues_repo_name: david-bai-notes/IA-Probability

max_forks_repo_name: david-bai-notes/IA-Probability


text:
\chapter{Combat}
\textbf{Combat} has an ugly tendency to be at the forefront of most roleplaying games, be they pen-and-paper or computer-based. Whether we like it or not, most roleplayers expect combat to happen at one point or another in the campaign. As such, it is necessary to offer a clear guidline on how combat works in the World of Artograch roleplaying system.\newline
Observance of the guidline should depend on the nature of the game being played: treating this roleplaying system as a genuine pen-and-paper tabletop RPG warrants a turn-based system. Likewise, should a game developer decide to adapt this system and take inspiration from the \textit{Baldur's Gate} series, \textit{Icewind Dale} series, \textit{Planescape: Torment}, \textit{Arcanum} or \textit{Star Wars: Knights of the Old Republic}, the aforementioned turn-based system can be and should be faithfully adapted. Should the game developer instead choose to create a looser adaptation combined with gameplay inspired by the \textit{Elder Scrolls} or the \textit{Gothic} series \textemdash which is precisely what the author of this document intends in the future \textemdash then the turn-based system that is to be documented in the following pages is to be discarded entirely, as the only thing that should dictate the pace of combat in an action-RPG should be the length of weapon animations.


text:
\documentclass[12pt]{article}

\thispagestyle{empty}

\usepackage{a4wide}

\input{psfig}

\renewcommand{\baselinestretch}{0.95}

\newcommand{\ciao}{\psfig{figure=ciao_st.ps}}

\setlength{\textwidth}{17.2cm}
\setlength{\textheight}{27.3cm}

\begin{document}

\topmargin -40pt

\Large

\centerline{\ciao}

\vspace*{-0.5cm}
\section*{What is Ciao?}
\vspace*{-0.5cm}

\begin{itemize}

\item Next generation, multi paradigm (including logic, functional,
  constraints, objects) programming system.

\item Free Software distributed under GNU GPL and LGPL.

\item Result of several EU and Spain funded projects.

\item Large number ($>$ 5000) of downloads.

\item Interest shown by important software companies.

\item Many supported platforms: Linux/Unix, Windows, Mac OS X\ldots

%%\item Designed with extensibility in mind.

\item Many interesting characteristics:
  \begin{itemize}
  \item Robust module system, incremental stand-alone compiler (plus
    traditional toplevel), multi-architecture executables.
  \item Foreign interfaces: C, Java, SQL, Tcl/Tk, etc.
  \item Web/Internet programming: \emph{Pillow} library.
  \item Distribution / agent programming being actively worked on.
  \end{itemize}

\item Industry standard performance.

\end{itemize}

\vspace*{-0.9cm}
\section*{Some possible venues for EU funded projects}
\vspace*{-0.5cm}
\begin{itemize}
\item  Remote and mobile agent programming. Coordination protocols.

\item  Rule-based dynamic customization of web sites.

\item  Constraint-based document search.
\end{itemize}

\vspace*{-0.7cm}
\section*{How to contact us}
\vspace*{-0.5cm}

\begin{itemize}

\item Germ\'{a}n Puebla. {\tt german@fi.upm.es}
\item The CLIP Group. Technical University of Madrid.\\
 {\tt http://clip.dia.fi.upm.es}
\end{itemize}
\end{document}

max_stars_repo_name: leuschel/ecce

max_issues_repo_name: leuschel/ecce

max_forks_repo_name: leuschel/ecce


text:
\section{Outline of the Project}

\begin{enumerate}
  \item Review functional requirements against the business goals
  \item Develop a user management system for customers, drivers,
  operational managers and human resources, etc.
  \begin{enumerate}
    \item Implement a user login system
    \item Implement registration for customers
    \item Implement a timetable/rota for drivers (dashboard)
    \item Restrict data modification to staff with the required role
    (e.g. managers)
  \end{enumerate}
  \item Develop a timetabling service for buses
  \begin{enumerate}
    \item Implement bus lines
    \item Implement bus routes for each line
    \item Implement bus stops and allow associating routes with
    these stops
    \item Build a front-end for route information
    \item Allow customers to favourite the routes and lines
  \end{enumerate}
  \item Check the implemented system satisfies the functional
  requirements outlined by the business goals
  \begin{enumerate}
    \item Make any required changes to meet the requirements
  \end{enumerate}
\end{enumerate}


text:
\section{Approach}

Based on weeks of literature reviewing and testing,
we have designed our overall approach to this task as followed:

\begin{enumerate}
    \item Energy-Based VAD

      Input audio signals are very likely to contain significantly large ratio of blank signals.
      VAD (Voice Activity Detector)
      is a preprocessing technique to filter out the blank period.
      The most common approach toward this goal is to use energy-based feature of signals.

      \item Cepstrum-Based Features

        Research showed that cepstrum-based features are more discrimitive in the task of speech and speaker recognition/verification.
        We decide to apply common cepstrum features extraction routine, such as MFCC (Mel-frequency Cepstrum Coefficients), LFCC,
        after the original signals are preprocessed by VAD.

       The basic procedure of MFCC is shown below, and the details about
       extracting MFCC is already been explained in the previous reports.
       The output of this step, is a sequence of fixed-dimension vectors, which will be used later in model training.

      \begin{figure}[H]
        \centering
        \includegraphics[width=\textwidth]{res/MFCC.png}
      \end{figure}

    \item GMM and UBM Model

      Since the feature vectors of a speaker tend to cluster into \textbf{several} groups
      in the feature space,
      the model of a specific speaker can be well described by using GMM (Gaussian Mixture Model).
      Moreover, for different speakers, the components of their individual GMMs
      will also have similar distributions, which discriminate different syllables.
      Therefore, an UBM (Universal Background Model) can be first trained for all speakers,
      and then we can get adapted GMMs which fit this task better.

      \begin{figure}[H]
        \centering
        \includegraphics[width=0.7\textwidth]{res/ubm.png}
      \end{figure}

      \item JFA
        GMM-based model can describe the clusterred distribution, but it fails to account for
        different types of variability in each clusterred group.
        However, we only need inter-speaker variability to be modeled,
		but not channel or noise variability. Join Factor Analysis can convey
		such information.

  \end{enumerate}


text:
\section{Task 1: Matrix Transpose}
The code for this assignment can be found in the \textit{src/Task1} folder
handed in with this report. All functions (where applicable) have been templated
so the datatype contianed in the matrices can be any class \texttt{T}.

The code ships with a make file that supports the \texttt{clean},
\texttt{compile} and \texttt{run} targets. The current setup of the file will
run both GPU kernels on an assymetric matrix and compare to the CPU runs.

\subsection{Task 1.a: Sequential CPU Code}
The code for this subtask is implemented in the file \textit{cpuFunc.cu.h},
there is not a whole lot of spectacular work going on, the file just contains
convenience functions for creating, comparing and freeing matrices of specific
sizes. The transpose function itself is implemented in
\texttt{flatMatrixTranspose}.

\subsection{Task 1.c: Naive GPU Code}
The code for this subtask is implemented in \textit{gpuFunc.cu.h} as well as
in \textit{task1.cu}. The following functions are implemented to solve this
task:
\begin{itemize}
    \item \textit{gpuFunc.cu.h:}\begin{itemize*}
        \item \texttt{flatNaiveTransposeKernel} The actual transpose kernel.
        \item \texttt{flatMatrixCudaMalloc} Allocates device memory for a
        matrix of a given size.
        \item \texttt{flatmatrixCudaFree} Frees the device memory.
        \item \texttt{flatMatrixHostToDevice} Copies a matrix from host- to
        device memory.
        \item \texttt{flatMatrixDeviceToHost} Copies a matrix from device- to
        host memory.
    \end{itemize*}

    \item \textit{task1.cu}\begin{itemize*}
        \item \texttt{gpuNaiveTranspose} Does the setup for a transepose and
        calls the actual transpose kernel.
        \item \texttt{naiveTransposeTest} Compares the results of the CPU
        transpose and the GPU transpose as well as printing the result and how
        long each call took on average.
    \end{itemize*}
\end{itemize}

In the \texttt{main} part of the \textit{task1.cu} file, there is a region that
contains tests I used to find where the CPU transpose starts being slower than
the GPU transpose. The timings are listed in Table \ref{tab:task1time}.

\subsection{Task 1.d: Shared-Memory GPU Code}
For this task additional code is implemented in \textit{task1.cu} and
\textit{gpuFunc.cu.h}, the following methods we're implemented:
\begin{itemize}
    \item \textit{gpuFunc.cu.h:}\begin{itemize*}
        \item \texttt{flatSharedTransposeKernel} The actual transpose kernel.
    \end{itemize*}

    \item \textit{task1.cu}\begin{itemize*}
        \item \texttt{gpuSharedTranspose} Does the setup for a transepose and
        calls the actual transpose kernel.
        \item \texttt{sharedTransposeTest} Compares the results of the CPU
        transpose and the GPU shared memory kernel and prints results and
        running times.
    \end{itemize*}
\end{itemize}

\subsection{Execution Time}

Table \ref{tab:task1time} shows the running times of the CPU code and the
Shared-Memory GPU kernel. Time time is done for 10 runs of each method and the
time represents the average time for a single run. The times only cover the time
spent in the calulation kernels, and does not cover the overhead for copying
data to device memory.

\begin{table}
    \begin{tabular}{|r|r|r|r|}
        \hline
        \textbf{Matrix Dimensions} & \textbf{CPU Time} & \textbf{Naive GPU Time} & \textbf{Tiled-Memory GPU Time}\\\hline
        $100 \times  50$  & $28 \mu s$  & $31 \mu s$ & $21 \mu s$ \\
        $50 \times  100$  & $18 \mu s$  & $19 \mu s$ & $17 \mu s$ \\
        $10 \times  10$   & $>0 \mu s$  & $16 \mu s$ & $15 \mu s$ \\
        $100 \times  100$ & $37 \mu s$  & $19 \mu s$ & $17 \mu s$ \\
        $200 \times  200$ & $163 \mu s$ & $33 \mu s$ & $26 \mu s$ \\
        $300 \times  300$ & $349 \mu s$ & $57 \mu s$ & $46 \mu s$ \\
        $1024\times 1025$ & $18303 ms$  & $272\mu s$ & $145\mu s$ \\\hline

    \end{tabular}
    \caption{The running times for the CPU and GPU code as the average over 10
    runs.}
    \label{tab:task1time}
\end{table}

Table \ref{tab:task1time} shows that the CPU based code while very fast for the
first small entry is quickly overtaken by both GPU kernels. Among the GPU
kernels the Shared-Memory is the fastest from the beginning.


text:
\chapter*{DRACULA\footnotemark}
\footnotetext{Something - maybe related to your recent inquiries - triggered pre-set codes in the GCHQ datahouses. It got me a mailpointing to a certain dossier. It appears to contain an original version of Bram Stoker's Dracula, annotated by two different hands - The second is using "Van Sloan" and "Cushing" to refer to both. I'm using, therefore "Hopkins" for myself. I can't send you the original - to conspicuous if missing - so I've copied most annotations on this copy of the published novel. There's a lot of fact checking to do, but the gist of it is - the events are real, according to Cushing! \newline \hfill Hopkins}
How these paper have been placed in sequence will be made manifest in the reading of them.
All needless matters have been eliminated,
\footnote{Also, many documents, expunged}
so that a history almost at variance with the possibilites of latter-day belief may stand forth as simple fact.
There is throughout no statement of past things wherein memory may err, for all the records choosen are exactly contemporary, given from stand-points and within the range of knowledge of those who made them.

max_stars_repo_name: ggbioing/DraculaDossier

max_issues_repo_name: ggbioing/DraculaDossier

max_forks_repo_name: ggbioing/DraculaDossier