Introduction

Sprachkonzepte der parallelen Programmierung

Concepts of Parallelism

From Concept to Implementation

notice the gap:

who bridges the gap?

note the difference between: \(\sum_{0\le i< n} x_i\) (intent)
and: for(i=0;i<n;i++){s+=x[i];} (sequencing)

Abstract! Abstract! Abstract!

main thesis

example (C#, mono) just one annotation expresses the intent of parallel execution:

Enumerable.Range(0,1<<25)
     .Select(bitcount).Sum() 
Enumerable.Range(0,1<<25).AsParallel()
     .Select(bitcount).Sum()

this is why we focus on functional programming
(e.g., Select is a higher-order function)

Why did this work, exactly?

Enumerable.Range(...).AsParallel().Sum()

Types for Pure Computations

measure run-times and explain (C# vs. Haskell)

Enumerable.Range(0,1<<25).Select(bitcount).Sum() 
Enumerable.Range(0,1<<25).Select(bitcount).Count()
Enumerable.Range(0,1<<25)                 .Count()
length $ map bitcount $ take (2^25) [ 0 .. ]
length                $ take (2^25) [ 0 .. ]

If we absolutely must program imperatively,

(imp. program execution \(=\) sequence of state changes)

Typical Concurrency Problems

Semantics for Concurrent Systems

…via mathematical models:

Concurrency Primitives

Homework

  1. which are associative? (give proof or counter-example)

    1. on \(\mathbb{Z}\): multiplication, subtraction, exponentiation

    2. on \(\mathbb{B}\) (booleans): equivalence, antivalence, implication

    3. on \(\mathbb{N}^2\): \((a,b) \circ (c,d) := (a\cdot c, a\cdot d + b)\)

  2. sum-of-bitcounts

    1. re-do the C# bitcounting example in Java (hint: java.util.stream)

    2. discuss efficient implementation of int bitcount (int x); (hint: time/space trade-off)

    3. discuss efficient implementation of sum-of-bitcounts

      1. from \(0\) to \(2^e-1\)

      2. bonus: from \(0\) to \(n-1\) (arbitrary \(n\))

      hint:

      how did little Carl Friedrich Gauß do the addition?

      morale:

      the computation in the example should never be done in real life, but it makes a perfect test-case since it keeps the CPU busy and we easily know the result.

  3. sorting network exercise: https://autotool.imn.htwk-leipzig.de/new/aufgabe/2453

  4. on your computer, install compilers/RTS for languages:
    Haskell (ghc), C# (mono), Java, Go, (Scala, Clojure)

    or make sure that you can ssh to Z430 computers

Petri-Netze

Einleitung

Vergleiche: Beschreibung/Modellierung sequentieller Systeme durch reguläre Sprachen/endliche Automaten

Vorgehen hier: erst konkrete Modelle,
dann Spezifikationssprache (Logik).

Definition: Netz

Stellen/Transitions-Netz \(N=(S,T,F)\)

das ist ein gerichteter bipartiter Graph

Bezeichnungen:

Zustände, Übergänge

Petri-Netze modellieren…

Bsp: gegenseitiger Ausschluß

Für jeden erreichbaren Zust. \(z\) gilt: \(z(a)=0 \vee z(b)=0\).

Beispiel aus: Kastens und Kleine Büning: Modellierung, Hanser, 2008. http://www.hanser-elibrary.com/isbn/9783446415379

Zeichnung mit TIKZ, vgl. http://www.texample.net/tikz/examples/nodetutorial/

Petri-Netze und UML

UML-2.5, Sect. 13.2.1

A variety of behavioral specification mechanisms are supported by UML, including:

Sprache eines Netzes (I)

Sprache eines Netzes (II)

Kapazitäten und -Schranken

Erweiterung:

Einschränkung:

falls alle Kapazitäten beschränkt \(\Rightarrow\) Zustandsmenge endlich (aber mglw. groß) \(\Rightarrow\) vollständige Analyse des Zustandsübergangsgraphen (prinzipiell) möglich

Formale Definition der Ü.-Relation

Bedingung/Ereignis-Netze

…erhält man aus allgemeinem Modell durch:

Beispiele:

Eigenschaften von Petri-Netzen

Definitionen (für Netz \(N\) mit \(d\) Stellen, Zustand \(m\in \mathbb{N}^d\))

Eigenschaften (Beispiele):

Alain Finkel und Jerome Leroux: Neue, einfache Algorithmen für Petri-Netze, Informatik-Spektrum 3/2014, S. 229–236

Beschränktheit ist entscheidbar

\(\operatorname{\textsf{Post}}_N^*(m_0)\) endlich?

Entscheidungsverfahren: wir zählen abwechselnd auf:

zu zeigen ist: \(\operatorname{\textsf{Post}}_N^*(m_0)\) unendlich \(\iff\) Zeuge existiert

\(\Leftarrow\): ist klar. Für \(\Rightarrow\):

Lemma von Higman, WQO

Aufgaben

Spezifikation und Verifikation nebenläufiger Prozesse

Einleitung

wie überall,

so auch hier:

Literatur

erfordert eigentlich eine eigene Vorlesung, vergleiche

Kripke-Strukturen, Omega-Wörter

allgemein: Kripke-Struktur zu Variablenmenge \(V\) ist

hier speziell:

Beispiel:

Omega-Wörter und -Sprachen

PLTL: propositional linear time logic

Syntax:

Beispiele: \(\Diamond (p\vee q)\), \(\Box\Diamond p\), \(\Diamond\Box p\)

Semantik: Wert der Formel \(F\) in Struktur \(K\) zur Zeit \(s\):

Übung: \(\Diamond\Box \phi \Rightarrow \Box\Diamond\phi\) ist allgemeingülitg (gilt in jeder Struktur), …aber die Umkehrung nicht

PLTL-Spezifikationen von Systemeigenschaften

PLTL: Algorithmen

Satz: die folgenden Fragen sind entscheidbar:

Beweis-Idee: die Mengen \(\{w\in\Sigma^\omega \mid 1=\operatorname{wert}(F,w,0)\}\)

sind \(\omega\)-regulär (Def. auf nächster Folie)

und lassen sich durch endliche Automaten beschreiben.

(J. R. Büchi 1962, A. Pnueli 1977)

\(\omega\)-(reguläre) Sprachen

Übung PLTL

Konkrete Syntax der PLTL-Operatoren

deutsch Symbol englisch autotool NuSMV Spin
irgendwann \(\Diamond\) finally (eventually) \(\operatorname{\mathsf{F}}\) <>
immer \(\Box\) globally generally \(\operatorname{\mathsf{G}}\) []
bis until \(\operatorname{\mathsf{U}}\) U
nächster next \(\operatorname{\mathsf{X}}\) X

Vergleich der PLTL-Operatoren

Ausdrucksstärke von \(\operatorname{\text{PLTL}}(M)\) für \(M\subseteq\{\operatorname{\mathsf{F}},\operatorname{\mathsf{G}},\operatorname{\mathsf{U}},\operatorname{\mathsf{X}}\}\):

Nebenläufige Java-Programme

Threads erzeugen und starten

Thread-Objekt implementiert run(),

diese Methode wird aufgerufen durch start(),

das aber sofort zurückkehrt (mglw. bevor run() endet).

for (int t=0; t<8; t++) { new Thread() { 
        public void run() {
            System.out.println (t);
        }
    }.start();
}

alternative Notation (Java \(\ge\) 8)

new Thread( () -> System.out.println(t) );

Auf das Ende von Threads warten

t.join() blockiert aufrufenden Thread

und kehrt erst zurück, wenn t beendet ist:

t1.start(); t2.start();
...
t1.join() ; t2.join();

Gemeinsamer Speicher

(Vorsicht, Code ist absichtlich falsch)

int s = 0; // gemeinsamer Speicher
// Threads erzeugen:
for (int t=0; t<threads; t++) {
 new Thread ( () -> 
  { for (int i = 0; i<steps; i++)  s++; });
// Threads starten: ...
// auf Threads warten: ...
System.out.println (s);

Das Java-Speichermodell

Sequentielle Konsistenz (Plan)

Beispiel Umordnung

vorher  : A == 0; B == 0;
Thread 1: r2 = A ; B = 1;
Thread 2: r1 = B ; A = 2;

Beispiel Code-Änderung

vorher: p == q und p.x == 0
Thread 2:
  r6=p; r6.x=3;
Thread 1: 
  r1=p; r2=r1.x; r3=q; r4=r3.x; r5=r1.x;

Def. Speichermodell (Plan)

Merksatz:

Def. Speichermodell (Detail)

Data Races

volatile-Variablen

vereinfachtes Denkmodell

(\(=\) Veranschaulichung der happens-before-Relation)

Übung JMM

Semaphore und Monitore

Semaphore

Semaphor: Geschichte

Gegenseitiger Ausschluß (grundsätzlich)

Semaphore s := 1; Gemeinsame Ressource r;
Prozeß Nr i : while (true) { 
    non_critical_section;
    Wait (s);
    critical_section; // benutze r
    Signal (s);    }

Eigenschaften:

Gegenseitiger Ausschluß (Korrektheit)

Bezeichnungen:

Zeige Invariante: \(S+C= 1\).

Beweis:

aus Invariante folgt Korrektheit (\(C\le 1\))

Gegenseitiger Ausschluß in SMV

https://gitlab.imn.htwk-leipzig.de/waldmann/skpp-ws17/blob/master/kw46/semaphore.smv

formuliere und prüfe Bedingungen:

Semaphore und Monitore

Monitore in Java

Explizites wait/notify für Monitore

Beispiel: Philosophen in der Mensa

(Edsger Dijkstra, Tony Hoare, ca. 1965)

gewünschte System-Eigenschaften:

Modellierung des Ressourcenzugriffs

Modellierung des ausschließlichen Ressourcenzugriffs:

class Fork { 
    private boolean taken = false;
    synchronized void take () {
        while (taken) { this.wait (); }  
        taken = true;               }
    synchronized void drop () {
        taken = false; this.notifyAll ();   } }

Q: warum wird expliziter Semaphor (wait/notify) benutzt?

A: jeder Prozeß (Philosoph) benötigt zwei Ressourcen (Gabeln) gleichzeitig, kann aber nicht zwei synchro- nized- Methoden gleichzeitig ausführen (kann die erste Gabel nicht festhalten, während die zweite geholt wird)

5 Philosophen

class Fork { void take() ; void drop () }
Philosoph i : new Thread () { void run () { 
 while(true) { this.nachdenken();
    fork[i].take(); fork[i+1].take();
    this.essen();
    fork[i].drop(); fork[i+1].drop(); 
}}} . start();

welche Eigenschaften? wie kann man das ggf. reparieren?

Quelltexte: https://gitlab.imn.htwk-leipzig.de/waldmann/skpp-ws17

Übung Monitor

Verhalten dieses Programmes ausprobieren, diskutieren:

final Object lock = new Object();
Thread t = new Thread(() -> {
  synchronized (lock) {  lock.wait(); } });
t.start();
synchronized (lock) { lock.notifyAll(); }
t.join();

Übung Dining Philosphers

Algorithmen implementieren und Eigenschaften (Liveness, Fairness) diskutieren/beweisen:

Realisierung des Modells

Eisenbahnbetrieb: Gegenseitiger Ausschluß

Übung Binärer Semaphor

binärer Semaphor: \(S\in\{0,1\}\) und …
Signal(S) : …sonst \(S := 1\)

Simulation allgemeiner Semaphor durch binären Semaphor http://www.csc.uvic.ca/~mcheng/460/notes/gensem.pdf

weiter Beispiele zu Semaphoren: Allen B. Downey: The Little Book of Semaphores, http://greenteapress.com/semaphores/downey08semaphores.pdf

Software Transactional Memory

Motivation/Plan

für nebenläufige Programme, die gemeinsamen Speicher benutzen:

Quelle: Simon Peyton Jones: Beautiful Concurrency, \(=\) Kapitel 24 in: Andy Oram und Greg Wilson (Hrsg.): Beautiful Code, O’Reilly, 2007. http://research.microsoft.com/en-us/um/people/simonpj/papers/stm/

Beispiel: Kontoführung (I)

das ist das (bisher) naheliegende Modell:

class Account { int balance;
  synchronized void withdraw (int m) 
    { balance -= m; }
  synchronized void deposit (int m) 
    { withdraw (-m); }

welche Fehler können hier passieren:

void transfer 
      (Account from, Account to, int m) 
{
  from.withdraw (m); 
  to.deposit (m);
}

Beispiel: Kontoführung (II)

ist das eine Lösung?

void transfer 
       (Account from, Account to, int m) 
{
  from.lock(); to.lock ();
  from.withdraw (m);
  to.deposit (m);
  from.unlock(); to.unlock();
}

Beispiel: Kontoführung (III)

wann funktioniert diese Lösung und wann nicht?

  if (from < to) { from.lock(); to.lock() }
  else           { to.lock(); from.lock() }
  ...

Locks are Bad

locks do not support modular programming

John Ousterhout: Why Threads are a Bad Idea (for most puroposes) USENIX 1996, https://web.stanford.edu/~ouster/cgi-bin/papers/threads.pdf

Speicher-Transaktionen (Benutzung)

from <- atomically $ newTVar 10
atomically $ do x <- readTVar from
                if x < a then retry 
                else writeTVar from (x-a)

Speicher-Transaktionen (Implementierung)

Einzelheiten, Erweiterungen: https://ghc.haskell.org/trac/ghc/wiki/Commentary/Rts/STM

Deklaration von Nebenwirkungen in Typen

in Java (u.v.a.m.) ist der Typ nur ein Teil der Wahrheit:

public static int f (int x) {
  y++ ; new File ("/etc/passwd").delete(); 
  return x+1;
}

in Haskell: Typ zeigt mögliche Nebenwirkungen an.

damit kann man trennen:

Nebenwirkungen in Haskell: IO a

Werte:

4 :: Int  ;   "foo" ++ "bar" :: String

Aktionen mit Resultat und Nebenwirkung:

writeFile "foo.text" "bar" :: IO ()
readFile "foo.text" :: IO String
putStrLn (show 4) :: IO ()

Nacheinanderausführung von Aktionen:

do s <- readFile "foo.text" 
   putStrln (show (length s))

Start einer Aktion: im Hauptprogramm

main :: IO ()
main = do ...

Nebenwirkungen auf den Speicher

import Data.IORef
data IORef a -- abstrakt
newIORef :: a -> IO (IORef a)
readIORef :: IORef a -> IO a
writeIORef :: IORef a -> a -> IO ()

Transaktionen: STM a

jede Transaktion soll atomar sein

\(\Rightarrow\) darf keine IO-Aktionen enthalten (da man deren Nebenwirkungen sofort beobachten kann)

\(\Rightarrow\) neuer Typ STM a für Aktionen mit Nebenwirkungen nur auf Transaktionsvariablen TVar a

type Account = TVar Int
withdraw :: Account -> Int -> STM ()
withdraw account m = do
    balance <- readTVar account
    writeTVar account ( balance - m )
transfer :: Account -> Account -> Int -> IO ()
transfer from to m = atomically 
  ( do withdraw from m ; deposit to m    )

Bedingungen und Auswahl

STM-Typen und -Operationen

data STM a -- Transaktion mit Resultat a
data IO  a -- (beobachtbare) Aktion 
           -- mit Resultat a
atomically :: STM a -> IO a
retry      :: STM a
orElse     :: STM a -> STM a -> STM a

data TVar a -- Transaktions-Variable 
            -- mit Inhalt a
newTVar    :: a -> STM ( TVar a )
readTVar   :: 
writeTVar  ::

(\(=\) Tab. 24-1 in Beautiful Concurrency)

vgl. http://hackage.haskell.org/packages/archive/stm/2.2.0.1/doc/html/Control-Monad-STM.html

STM - Beispiele, Übungen

The Santa Claus Problem

Santa repeatedly sleeps until wakened by either all of his nine reindeer, back from their holidays, or by a group of three of his ten elves. If awakened by the reindeer, he harnesses each of them to his sleigh, delivers toys with them and finally unharnesses them (allowing them to go off on holiday). If awakened by a group of elves, he shows each of the group into his study, consults with them on toy R&D and finally shows them each out (allowing them to go back to work). Santa should give priority to the reindeer in the case that there is both a group of elves and a group of reindeer waiting.

J. A. Trono: A new Exercise in Concurrency, SIGCSE Bull. 26, 1994.

Lösung mit STM in Peyton Jones: Beautiful Concurrency, 2007

Philosophen mit STM

forM [ 1 .. num ] $ \ p -> forkIO $ forever $ do
    atomically $ do 
        take $ left  p ; take $ right p
    atomically $ drop $ left  p
    atomically $ drop $ right p
take f = do
    busy <- readTVar f
    when busy $ retry
    writeTVar f True

kein Deadlock (trivial). — nicht fair, siehe

http://thread.gmane.org/gmane.comp.lang.haskell.parallel/305

Quelltexte:

https://gitlab.imn.htwk-leipzig.de/waldmann/skpp-ws17

Übung STM

STM in Clojure (Beispiele)

Clojure \(=\) LISP für JVM

(def foo (ref "bar"))  -- newTVar

(deref foo)            -- readTVar
@foo

(ref-set foo "oof")    -- writeTVar
(dosync (ref-set foo "oof"))

Quellen:

STM in Clojure (Sicherheit)

Transaktionsvariablen ohne Transaktion benutzen:

IO innerhalb einer Transaktion:

Übung: ein Programm konstruieren, bei dem eine IO-Aktion innerhalb einer Transaktion stattfindet, aber die Transaktion nicht erfolgreich ist.

Transaktion mit Nebenwirkung

Transaktionen:

(def base 100)
(def source (ref (* base base)))
(def target (ref 0))
(defn move [foo]
   (dotimes [x base]
      (dosync (ref-set source (- @source 1))
          (ref-set target (+ @target 1))) ))
(def movers (for [x (range 1 base)] (agent nil)))
(dorun (map #(send-off % move) movers))

Nebenwirkung einbauen:

(def c (atom 0)) ... (swap! c inc) ... 
(printf c)

STM und persistente Datenstrukturen

“The Clojure MVCC STM is designed to work with the persistent collections, and it is strongly recommended that you use the Clojure collections as the values of your Refs. Since all work done in an STM transaction is speculative, it is imperative that there be a low cost to making copies and modifications.”

“The values placed in Refs must be, or be considered, immutable!!”

Beispiel Suchbäume:

Bsp: persistenter Suchbaum in Haskell

Nicht blockierende Synchronsiation

Einleitung

Synchronisation (geordneter Zugriff auf gemeinsame Ressourcen) durch

Literatur

Compare-and-Set (Benutzung)

Der Inhalt einer Variablen soll um 1 erhöht werden.

Mit STM wäre es leicht:

atomically $ do 
    v <- readTVar p ; writeTVar p $! (v+1)

ohne STM, mit einfachen atomaren Transaktionen:

AtomicInteger p;  boolean ok;
do { int v = p.get();
     ok = p.compareAndSet(v,v+1);
} while ( ! ok);

Compare-and-Set (Implementierung)

Modell der Implementierung:

class AtomicInteger {  private int value;
  synchronized int get () { return value; }
  synchronized boolean 
    compareAndSet (int expected, int update) {
      if (value == expected) {
        value = update ; return true;
      } else {
        return false; } } }

moderne CPUs haben CAS (oder Äquivalent)
im Befehlssatz (Ü: suche Beispiele in x86-Assembler)

JVM (ab 5.0) hat CAS für Atomic{Integer,Long,Reference}

Compare-and-Set (JVM)

Assembler-Ausgabe (des JIT-Compilers der JVM):

javac CAS.java
java -Xcomp -XX:+UnlockDiagnosticVMOptions -XX:+PrintAssembly CAS

Vorsicht, Ausgabe ist groß. Mit nohup in Datei umleiten, nach AtomicInteger::compareAndSet suchen.

Non-Blocking Stack

Anwendung: Scheduling-Algorithmen:

(jeder Thread hat Stack mit Aufgaben, andere Threads können dort Aufgaben hinzufügen und entfernen)

private static class Node<E> {
  E item; Node<E> next;
}
class Stack<E> { 
  AtomicReference<Node<E>> top 
    = new AtomicReference<Stack.Node<E>>();
  public void push (E x) 
  public E pop ()
}

Spezifikation f. Concurrent Stacks

Stack-spezifisch:

allgemein:

vgl. Hendler, Shavit, Yerushalmi: A Scalable Lock-free Stack Algorithm (Sect. 5) (16th ACM Symp. on Parallelism in Algorithms and Architectures) http://www.cs.bgu.ac.il/~hendlerd/papers/scalable-stack.pdf

Abstraktion, Linearisierbarkeit

vgl. Shavit: Art of Multiproc. Prog. Sect. 9.3 Concurrent Reasoning

Non-Blocking Queue (Problem)

Auslesen (am Anfang) ist leicht,

Problem beim Einfügen (am Ende):

Non-Blocking Queue (Lösung)

(Michael and Scott, 1996) http://www.cs.rochester.edu/research/synchronization/pseudocode/queues.html

Idee: die zwei zusammengehörigen Änderungen mglw. durch verschiedene Threads ausführen (!)

Queue hat zwei Zustände:

wer B bemerkt, muß reparieren.

in Java realisiert als ConcurrentLinkedQueue

Non-Blocking Übung

  1. wie kann man CAS durch STM simulieren?

    • Typ

    • Implementierung

  2. enqueue/dequeue für non-blocking Queue:

    Vgl. Code in

    Welche Auszeichnung hat Michael Scott für seine Forschungen im Verteilten Rechnen erhalten? Betrachten Sie auch die Liste der Themen der anderen Preisträger.

  3. das Bitcount-Programm in Java:

    • Summation in AtomicLong

    • Thread-Synchronisation nicht durch join, sondern durch ein AtomicInteger, in dem immer die Anzahl der noch laufenden Prozesse steht.

  4. addAndGet durch compareAndSet implementieren, vergleichen

  5. Finden Sie den CAS-Maschinenbefehl im JVM-Assemblercode:

    java -XX:+UnlockDiagnosticVMOptions -XX:+PrintAssembly BC

    Finden Sie die Semantik des Maschinenbefehls in der offiziellen Prozessorbeschreibung.

Lokale Prozeßkommunikation (I)

Motivation

bisher betrachtete Modelle zur Thread-Kommunikation:

jetzt:

Beispiel: Rendezvous (Ada), Actors (Scala), Channels (Go)

Communicating Sequential Processes (CSP)

CSP: Syntax

\(E\) ist eine Menge von Ereignissen

Die Menge \(\operatorname{\mathbb{P}}(E)\) der Prozesse über \(E\) definiert durch:

CSP: Semantik

Semantik eines Prozesses \(P\in\operatorname{\mathbb{P}}(E)\) definiert durch:

CSP: von Prozess zu Automat

Übergangsrelation von \(A(P)\) definiert durch Regeln zu

Regeln zur Kommunikation

das Ereignis gehört zum Kommunikations-Alphabet:

beide Prozesse führen es gemeinsam (synchron) aus

das Ereignis gehört nicht zum Kommunikations-Alphabet oder ist ein \(\epsilon\)-Übergang: einer der beiden Prozesse führt es aus (der andere wartet)

definiert synchrone Kommunikation, realisiert u.a. in

Ada (Rendezvous), Scala (Operation !?),
Go (Kanal mit Kapazität 0).

Regeln für Auswahloperatoren

Beispiel: (mit verkürzter Notation \(a\) für \(a\to\text{STOP}\))

diese Automaten sind verschieden, aber die Sprachen stimmen überein.

Rendez-Vous (I) in Ada

task body Server is
   Sum : Integer := 0;
begin loop
      accept Foo (Item : in Integer) 
        do Sum := Sum + Item; end Foo;
      accept Bar (Item : out Integer) 
        do Item := Sum; end Bar;
   end loop;      
end Server;
A : Server; B : Integer;
begin
   A.Foo (4); A.Bar (B); A.Foo (5); A.Bar (B);
end B;

Rendezvous (II)

Verschiedene Prozeß-Semantiken

Ablehnungs-Semantik

-Semantik eines Prozesses ist Menge von Paaren von

\((s,F)\in \text{Ab}(P) :\iff \exists Q: P\stackrel{s}{\to} Q \wedge F=\{e \mid \exists R: Q\stackrel{e}{\to} R\}\).

Beispiel: -Semantik ist genauer als -Semantik:

Bisimulation von Prozessen

Plan

betrachten Zustandsübergangssysteme allgemein (Beispiele: endliche Automaten, Petri-Netze, CSP)

Semantiken und durch sie definierte Äquivalenzen:

Definition

Zustandsübergangssystem \(S=(\Sigma, Q, T, i)\)

(Alphabet \(\Sigma\), Zustandsmenge \(Q\),
Transitionen \(T\subseteq Q\times \Sigma\times Q\), Startzustand \(i\in Q\))

Def: \(R\subseteq Q_1\times Q_2\) ist Bisimulation zwischen \(S_1\) und \(S_2\), falls:

Beispiele, Kommentar

Bestimmung einer Bisimulation (Plan)

Sätze: Korrektheit, Vollständigkeit,

Termination für endliche \(Q_1, Q_2\).

vergleiche: Verfahren zur Minimierung von Automaten (Tabelle zur Markierung nicht äquivalenter Zustände)

Bestimmung einer Bisimulation (Impl.)

aus Definition \(R\) ist Bisimulation:

leite Verfeinerungsverfahren ab:

gegeben \(R_k\), definiere \(R_{k+1}\) durch:

\((p_1, p_2)\in R_{k+1}\), falls \((p_1,p_2)\in R_k\) und

Bisimulation (Übung)

Lokale Prozeßkommunikation (II)

Kommunikations-Kanäle

zur asynchronen Kommunikation

(Eigenschaften: vgl. Postbrief statt Rendezvous)

Bsp. in Go: (http://golang.org)

ch := make (chan int) // anlegen
ch <- 41 // schreiben
x := <- ch // lesen

Kanäle in Haskell

Kanal ist typisiert, FIFO, unbeschränkt.

data Chan a -- abstrakt
newChan   :: IO (Chan a)
writeChan :: 
readChan  ::

Dok.:

http://www.haskell.org/ghc/docs/latest/html/libraries/base/Control-Concurrent-Chan.html

Übungen

Haskell: MVar

ist Kanal der Kapazität 1

data MVar a = ...

takeMVar :: MVar a      -> IO a 
-- blockiert, wenn leer

putMVar  :: MVar a -> a -> IO ()
-- blockiert, wenn voll

Actors (Scala)

http://www.scala-lang.org/node/242

object Stop
class Server extends Actor { def act() {
    var running = true;
    while (running) { receive {
        case x : Int => println(x)
        case Stop => running = false; } } } }
var s = new Server()
s.start ; s ! 42 ; s ! Stop

Good Actors Style

Kap. 30.5 in: Odersky, Spoon, Villers: Programming in Scala, Artima 2007,

Rendezvous-Zusammenfassung

Übung: Kanäle in Go

Sprachdefinition: http://golang.org/

Compiler/Runtime:

Kanäle:

Übung:

Futures in Java

submit startet eine asynchrone Berechnung,
get ist der blockierende Zugriff auf das Resultat.

Implementierung könnte einen Kanal benutzen
(die Rechnung schreibt, get liest)

package java.util.concurrent;
interface Callable<R> { R call() } 
interface ExecutorService { 
  <R> Future<R> submit (Callable<R>)
  void shutdown() }
interface Future<R> { R get() }
class Executors {
  ExecutorService newFixedThreadPool(int) }

Ü: Bitcount-Summation. Stream<Future<Integer>>

Übungen

  1. Kanäle in Go, https://gitlab.imn.htwk-leipzig.de/waldmann/skpp-ws17/tree/master/kw49

    Kanal-Kapazität ändern, ausprobieren.

    Auch GOMAXPROCS=2 usw. probieren.

  2. Kanäle in Haskell (BC.hs) ausprobieren

  3. Kanäle in STM: Schnittstelle und Implementierung https://hackage.haskell.org/package/stm/docs/Control-Concurrent-STM-TChan.html

  4. Ändern Sie das bekannte Java-Bitcount-Programm, so daß Futures benutzt werden (und keine Threads).

  5. Ergänzen Sie den Quelltext des verteilten Mergesort (ms.go) https://gitlab.imn.htwk-leipzig.de/waldmann/skpp-ws16/tree/master/kw50

    Nur zum Zweck der Übung des Nachrichtentransport über Kanäle, für paralleles Sortieren gibt es besser geeignete Verfahren.

Verteilte Programme

Verteiltes Rechnen

Realisierungen:

Erlang

Ericsson Language, http://www.erlang.org/

Anwendung: Steuerung von Telekommunikationsanlagen

grundsätzliche Spracheigenschaften:

(also ungefähr LISP)

Besonderheiten:

Cloud Haskell: Übersicht

Jeff Epstein, Andrew Black, and and Simon Peyton Jones. Towards Haskell in the Cloud, Haskell Symposium, Tokyo, Sept 2011. http://research.microsoft.com/en-us/um/people/simonpj/papers/parallel/ http://haskell-distributed.github.io/

Cloud-Haskell: elementare Operationen

findSlaves :: Backend -> Process [NodeId]
spawn :: NodeId -> Closure (Process ()) 
      -> Process ProcessId
send :: Serializable a 
     => ProcessId -> a -> Process ()
expect :: Serializable a => Process a

newChan :: Serializable a 
    => Process (SendPort a, ReceivePort a)
sendChan :: Serializable a 
    => SendPort a -> a -> Process ()
receiveChan :: Serializable a 
    => ReceivePort a -> Process a

Beispiele/Übung

Paralleles Sortieren

Einleitung

Kostenmodelle für parallele Alg.

Work und Span für einfache Sortierverfahren

Massiv paralleles Sortieren

for i,j : 
  boolean c[i,j] := (a[i] < a[j])
for j : 
  out[j] := a[sum (c[1,j] .. c[n,j])]

Sortiernetze

Konkrete Sortiernetze geringer Breite

Das 0-1-Prinzip

Odd-Even-Merge

Verteiltes Zählen

Motivation

Motivation: zentrale Ausgabe von Tickets (mit eindeutigen und aufsteigenden Nummern).

mit höherem Durchsatz als mit einen zentralen Zähler

class Counter { int count;
synchronized int next () { return count++;}}

James Aspnes, Maurice Herlihy, and Nir Shavit.

Counting networks, JACM 41(5):1020–1048, Sept. 1994

http://www.cs.yale.edu/homes/aspnes/papers/ahs-abstract.html

wesentlicher Baustein: AtomicBoolean.negate()

Spezifikation für Zählnetze

korrekte Behandlung der Token:

gute Verteilung der Token:

Folgerung aus Spezifikation für Zählnetze

Satz: für jedes \(n>0, S\ge 0\) gibt es genau eine Schrittfolge \([z_1,\ldots,z_n]\) mit \(S=\sum z_i\).

Satz: für jeden Zustand jedes Zählnetzes gilt:

Folgerung: auch wenn der Ruhezustand nie eintritt, sind die Ausgänge gut verteilt

(hoher Durchsatz \(\implies\) kleines \(D\) \(\implies\) gute Verteilung)

Netzwerke aus Verteilern

Verteiler:

Eigenschaften/Fragen:

Bitonisches Zählen und Zusammenfügen (I)

Ansatz für Konstruktion eines \(2^k\)-Zählnetzes aus Verteilern:

Bitonisches Zählen und Zusammenfügen (II)

Induktionsschritt:

\(M_{2n}(\vec{x},\vec{y}) = \left\{ \begin{array}{l} M_n(\operatorname{odd}\vec{x},\operatorname{even}\vec{y}) ;\\ M_n(\operatorname{even}\vec{x},\operatorname{odd}\vec{y}); \\ V(x_1,x_2);\ldots; V(y_{n-1},y_n) \end{array} \right.\)

mit \(V(p,q)\) = Verteiler, \(\operatorname{odd}(x_1,x_2,\ldots) = (x_1, x_3,\ldots)\), \(\operatorname{even}(x_1,x_2,\ldots) = (x_2, x_4, \ldots)\).

Satz: jedes solche \(M_n\) erfüllt die Spezifikation.

Übung: konstruiere \(C_4, M_4\)

Übung: Beweis für \(M_8\) mit Eingangsfolge \((3,3,3,2;9,9,8,8)\), unter der Annahme, daß der Satz für \(M_4\) gilt.

Übung: Beweis für \(M_{2n}\) mit beliebiger Eingangsfolge,
unter der Annahme, daß der Satz für \(M_n\) gilt.

Implementierung für Verteiler und Netze

Plan:

struct Balancer {
    AtomicBoolean state; 
    Balancer [Boolean] next; 
}
traverse (Balancer b) {
    while (nicht fertig) {
        boolean i = b.state.getAndNegate();
        traverse(b.next[i]);         } }

Aufgaben:

Anwendungen von Zählnetzen

http://www.cs.yale.edu/homes/aspnes/papers/ahs-abstract.html Section 5

Übung Zählnetze

Beweise: die folgenden Bedingungen sind äquivalent:

Wenn \(x\) eine Schrittfolge ist, welche Beziehungen gelten zwischen \(\sum\operatorname{odd}(x), \sum (x)/2, \sum\operatorname{even}(x)\)?
(Möglichst genau! Benutze ggf. \(\lceil\cdot\rceil, \lfloor\cdot\rfloor\)

Beweise: Wenn \(x\) und \(y\) gleichlange Schrittfolgen mit \(\sum x = 1 + \sum y\), dann gilt für alle bis auf ein \(i\): \(x_i=y_i\).
Was gilt stattdessen für dieses \(i\)?

periodische Zählnetze

Parallele Auswertungsstrategien

Überblick

Algebraische Datentypen und Pattern Matching

ein Datentyp mit zwei Konstruktoren:

data List a 
   = Nil             -- nullstellig 
   | Cons a (List a) -- zweistellig

Programm mit Pattern Matching:

length :: List a -> Int
length xs = case xs of
    Nil       -> 0
    Cons x ys -> 1 + length ys

beachte: Datentyp rekursiv \(\Rightarrow\) Programm rekursiv

append :: List a -> List a -> List a

Alg. Datentypen (Beispiele)

data Bool = False | True
data Maybe a = Nothing | Just a
data Tree a = 
    Leaf | Branch ( Tree a ) a ( Tree a)

Ü: inorder, preorder, leaves, depth

Ü: Schlüssel in Blättern

data N = Z | S N

Ü: Rechenoperationen

Notation für Listen in Haskell:

anstatt data List a = Nil | Cons a (List a)

wird benutzt data [a] = [] | (a : [a])

Berechnung von Sortiernetzen

Bedarfsauswertung

Normalformen

Experiment zu Liste, Sequence, whnf

ghci
:set +s

let xs = [1..10^6] :: [Int]
seq xs () ; head xs ; last xs ; last xs

import qualified Data.Sequence as S
let ys = S.fromList xs
seq ys () ; S.index ys 0 
S.index ys (10^6-1)

Bedarfsauswertung und Parallelisierung

Beispiel: Mergesort

Sequentieller Algorithmus, wesentlicher Teil:

msort :: Ord a => [a] -> [a] -> [a]
msort xs = 
  let ( here, there ) = split xs
      sh = msort here ; st = msort there
  in  merge sh st

parallelisiert durch: import Control.Parallel

  .. in  par sh $ pseq st $ merge sh st

Beispiel: Primzahlen

Aufgabe: bestimme \(\pi(n) :=\) Anzahl der Primzahlen in \([1..n]\) auf naive Weise (durch Testen und Abzählen)

num_primes_from_to :: Int -> Int -> Int
num_primes_from_to lo hi 
 = length $ filter id $ map prime [lo .. hi]
prime :: Int -> Bool

parallele Auswertung durch Strategie-Annotation

withStrategy ( parListChunk 100000 rdeepseq )
  ( map prime [lo..hi] )

getrennte Beschreibung von Wert und Strategie

Beschreibungssprache (EDSL) für Strategien

http://hackage.haskell.org/package/parallel/docs/Control-Parallel-Strategies.html

Parallel LINQ

Beispiel:

(from n in Enumerable.Range(lo, hi-lo)
                    .AsParallel()
 where Prime(n)  select true).Count ();

Typen:

http://msdn.microsoft.com/en-us/library/dd997425.aspx

Übung:

Übung

Flexible Parallelisierung durch assoziative Operationen

Motivation

Beispiel Summe eine Liste durch beliebige Klammerung von zweistelligen Additionen

sum [3,1,2,4] = ((3+1)+2)+4 = 3+(1+(2+4))

wähle den Berechnungsbaum, der am besten zu verfügbarer Hardware (Anzahl Prozessoren) paßt

 ... = (3+1)+(2+4)

Verallgemeinerung statt Addition: beliebige assoziative Operation, nicht notwendig kommutativ, d.h. Blatt-Reihenfolge muß erhalten bleiben

Monoide

Homomorphismen

homo-morph \(=\) gleich-förmig

Signatur \(\Sigma\) (\(=\) Menge von Funktionssymbolen)

Abbildung \(h\) von \(\Sigma\)-Struktur \(A\) nach \(\Sigma\)-Struktur \(B\) ist Homomorphismus, wenn:

\(\forall f\in \Sigma, x_1,\ldots,x_k\in A:\)
\(h(f_A(x_1,\ldots,x_k)) = f_B(h(x_1),\ldots,h(x_k))\)

Beispiel:

Homomorphismen von Listen

Abbildung [a] -> b ist gegeben durch

foldb :: b -> (a->b)->(b->b->b) -> [a]-> b
foldb n e f xs = case xs of
  [] -> n ; [x] -> e x
  _ -> let (l,r) = splitAt ... xs
       in  f (foldb n e f l) (foldb n e f r)

Satz: f assoziativ und n links und rechts neutral für f \(\Rightarrow\) foldb n e f ist Monoid-Homomorphismus von ([a],[],++) nach (b,n,f)

Maximale Präfix-Summe

mps :: [Int] -> Int
mps xs = maximum $ map sum $ inits xs

mps [1,-1,0,2,0,-1] = maximum [0,1,0,0,2,2,1] = 2

ist kein Homomorphismus (Gegenbeispiel?) aber das:

mpss :: [ Int ] -> ( Int, Int )
mpss xs = ( mps xs, sum xs )

Bestimme die Verknüpfung in (Int,Int)

(die Darstellung als foldb)

beweise Assoziativität

Sequentielle Folds

für sequentielle Berechnung sind geeignet

foldr :: ( a -> b -> b) -> b -> [a] -> b
foldr f e xs = case xs of
  [] -> e ;  x : ys -> f x (foldr f e ys)
  
foldl :: (b -> a -> b) -> b -> [a] -> b
foldl f e xs = case xs of
  [] -> e ;  x : ys -> foldl f (f e x) ys

foldl paßt zum Iterator-Muster (Berechnung über einen Stream, mit einem Akkumulator), vgl. Aggregate in C#/Linq

Homomorphie-Sätze

  1. für jeden Hom exist. Zerlegung in map und reduce — und das reduce kann man flexibel parallelisieren!

    Bsp: length = reduce (+) . map (const 1)

    map: parallel ausrechnen, reduce: balancierter Binärbaum.

  2. jeden Hom. kann man als foldl und als foldr schreiben

  3. (Umkehrung von 2.) Wenn eine Funktion sowohl als foldl als auch als foldr darstellbar ist, dann ist sie ein Hom. — und kann (nach 1.) flexibel parallelisiert werden

    m.a.W: aus der Existenz zweier sequentieller Algorithmen folgt die Existenz eines parallelen Alg.

Literatur

Diskussion: Kommutativität

Methode aus PLINQ (http://msdn.microsoft.com/en-us/library/ff963547.aspx)

Aggregate<S, A, R>(
  this ParallelQuery<S> source, 
  Func<A> seedFactory, 
  Func<A, S, A> updateAccumulatorFunc, 
  Func<A, A, A> combineAccumulatorsFunc, 
  Func<A, R> resultSelector);

Übung Assoc.

Das Map/Reduce-Framework

Schema und Beispiel

map_reduce 
  :: ( (ki, vi) -> [(ko,vm)] )  -- ^ map
  -> ( (ko, [vm]) -> vo ) -- ^ reduce
  -> [(ki,vi)] -- ^ eingabe
  -> [(ko,vo)] -- ^ ausgabe

Beispiel (word count)

ki = Dateiname, vi = Dateiinhalt
ko = Wort     , vm = vo = Anzahl

Literatur

Implementierungen

Implementierung in Haskell

import qualified Data.Map as M

map_reduce :: ( Ord ki, Ord ko ) 
  => ( (ki, vi) -> [(ko,vm)] )  -- ^ distribute
  -> ( ko -> [vm] -> vo ) -- ^ collect
  -> M.Map ki vi -- ^ eingabe  
  -> M.Map ko vo -- ^ ausgabe
map_reduce distribute collect input 
    = M.mapWithKey collect
    $ M.fromListWith (++) 
    $ map ( \ (ko,vm) -> (ko,[vm]) )
    $ concat $ map distribute
    $ M.toList $ input

Anwendung: Wörter zählen

main :: IO ()
main = do
  files <- getArgs
  texts <- forM files readFile
  let input = M.fromList $ zip files texts
      output = map_reduce    
        ( \ (ki,vi) -> map ( \ w -> (w,1) )
                           ( words vi ) )
        ( \ ko nums -> Just ( sum nums))
        input
  print $ output

wo liegen die Möglichkeiten zur Parallelisierung?

(in diesem Programm nicht sichtbar.)

Hadoop

Bestandteile:

Betriebsarten:

Voraussetzungen:

Hadoop-Benutzung

Informationen:

Wörter zählen

public static class TokenizerMapper 
   extends Mapper<Object, Text, Text, IntWritable>{
   public void map(Object key, Text value, Context context) { } }
public static class IntSumReducer 
   extends Reducer<Text,IntWritable,Text,IntWritable> {
   public void reduce(Text key, Iterable<IntWritable> values, Context context ) { } } 
 }
public static void main(String[] args) { ...
   job.setMapperClass(TokenizerMapper.class);
   job.setCombinerClass(IntSumReducer.class);
   job.setReducerClass(IntSumReducer.class);  .. }

hadoop/src/examples/org/apache/hadoop/examples/WordCount.java

Sortieren

vgl. http://sortbenchmark.org/, Hadoop gewinnt 2008.

Beispielcode für

(jeweils mit map/reduce)

Index-Berechnung

Spezialfall: Quelle \(=\) Wort \(=\) URL, ergibt das Web.

Page Rank (I)

Definition: eine Webseite (URL) ist wichtig, wenn wichtige Seiten auf sie zeigen.

Modifikationen für

Page Rank (Eindeutigkeit)

Resultat ist (quadr.) stochastische Matrix mit positiven Einträgen, nach Satz von Perron/Frobenius

Page Rank (Berechnung)

durch wiederholte Multiplikation:

beginne mit \(w_0=\) Gleichverteilung,

dann \(w_{i+1} = L \cdot w_i\) genügend oft

(bis \(|w_{i+1}-w_i|<\epsilon\))

diese Vektor/Matrix-Multiplikation kann ebenfalls mit Map/Reduce ausgeführt werden.

(Welches sind die Schlüssel?)

(Beachte: Matrix ist dünn besetzt. Warum?)

Quelle: Massimo Franceschet: PageRank: Standing on the Shoulders of Giants Comm. ACM 6/2011, http://cacm.acm.org/magazines/2011/6/108660

Übung Map/Reduce

Hardwarenahe Parallelität: CUDA

Beispiel

Sequentielle und parallele Lösung (Ansatz)

for (int k = 0; k < K; k++) {
  float mindist = +infinity;
  for (int p = 0; p < P; p++) {
    for (int q = p + 1; q < P; q++ ) {
      float s = abstand (c[k][p], c[k][q]);
      mindist = MIN (mindist, s); } }
  c[k].fitness = mindist;  }

dim3 blocks (K, 1) ; dim3 threads (P, P);
kernel <<<blocks,threads>>> (c);
__global__ kernel (config *c) {
  int k = blockIdx.x; 
  int p = threadIdx.x; int q = threadIdx.y;
  if (p < q) { float s = abstand (c[k][p], c[k][q]); }
  // Berechnug des MIN?
}

Threadkommunikation

Binäre Reduktion

Datentransport zwischen Host und Decive

config * dev_c ;
cudaMalloc ( (void**) &dev_c, K*sizeof(config) );

cudaMemcpy ( dev_c, c, K*sizeof(config), 
   cudaMemcpyHostToDevice );
...
cudaMemcpy ( c, dev_c, K*sizeof(config), 
   cudaMemcpyDeviceToHost );
cudaFree (dev_c);

…das ist teuer (\(\Rightarrow\) möglichst wenige Daten transportieren)

Zusammenfassung CUDA

Literatur CUDA

Zusammenfassung,Ausblick

Zusammenfassung

Parallele Algorithmen

Komplexitätstheorie für parallele Algorithmen