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 8/9, Scala, Clojure, Go

    or make sure that you can ssh to Z423/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}}\}\):

Model-Checking mit NuSMV

Überblick

NuSMV: Programm und Simulation

NuSMV: Spezifikation und Verifikation

NuSMV: Modellierungssprache

NuSMV: Simulation Petrinetz

MODULE transition(vor,nach)
ASSIGN
  next (vor)  :=
    case vor > 0 :  vor - 1; TRUE : vor ; esac;
  next (nach) :=
    case vor > 0 & nach < 7 : nach + 1; TRUE : nach ; esac;
MODULE main
VAR s1 : 0 .. 7; s2 : 0 .. 7; s3 : 0 .. 7;
    t1 : process transition(s1, s2);
    t2 : process transition(s2, s1);
    t3 : process transition(s1, s3);
ASSIGN init (s1):=1; init(s2):=2; init (s3):=0;
LTLSPEC G s1 > 0;

Ü: überprüfe mit dieser Methode Eigenschaften von Petrinetzen aus Vorlesung (z.B. Ampelschaltung)

Entscheiden der PLTL-Erfüllbarkeit

NuSMV – build from source

falls Fehler

NuSMV-2.6.0/cudd-2.4.1.1/util/pipefork.c:46:16: error: storage size of ‘status’ isn’t known
     union wait status;

dann in ändere in dieser Datei Zeile 43 zu

#if (defined __linux__) || (defined __hpux) || (defined __osf__) || (defined _IBMR2) || (defined __SVR4) || (defined __CYGWIN32__) || (defined __MINGW32__)

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

(allgemeiner) Semaphor ist abstrakter Datentyp
mit Zustand \(S\in\mathbb{N}\) und atomaren Operationen:

Invariante: \(S = S_0 + \#\texttt{Signal} - \#\texttt{Wait}\)

(\(\#\texttt{Wait} =\) Anzahl der abgeschlossenen Aufrufe
von \(\#\texttt{Wait}\), entspr. für \(\#\texttt{Signal}\))

Beweis der Invarianz: Induktionsanfang
und 4 Fälle im Induktionsschritt

Semaphor: Geschichte

Gegenseitiger Ausschluß (grundsätzlich)

Semaphore s := 1;
Gemeinsame Ressource r;
Prozeß Nr i { 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

Ü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