Tutorium 10¶

Gruppen 2 und 4
Samuel Teuber
propa@teuber.dev
https://teuber.dev/propa

State of the Lecture¶

Verlängerte Abgabe für Übungsblatt von letzter Woche
Erneut Änderungen am Übungblatt(!) und an Klausurrelevanz
Heute Fokus auf Design by Contract, wegen Kürze in Vorlesung

Klausurrelevant:¶

Parallel Fundamentals: Amdahls Law, Task und Daten Paralellismus etc.
C/C++:
- Alles was in den Folien NICHT im Appendix steht (also Fokus auf Arbeit mit Pointern, Pointer Arithmetik und einfachen Deklarationen) à das was sie für das Arbeiten mit MPI brauchen.
- Ausnahme: Präzedenzregeln und der Decoder-Ring sind NICHT Relevant.
MPI: Alles außer MapReduce
Java Basic: Thema „Memory-Consistency-Errors“ ist relevant.
Java Advanced: Alles was nicht im Appendix ist, das heißt:
- NICHT Klausurrelevant ist: Semaphores und Barriers (kommen in aktualisierter Folienversion noch in den Appendix) und anderes im Appendix
- Klausurrelevant ist alles was in der Vorlesung dran war z.B.: Alles zu Executors, Futures, Fork-Join, Streams und Actors
Design by Contract: tbd

Nachträge zu letzter Woche¶

Producer/Consumer¶

synchronized(tasks) {
    while (cond) {
        try{ 
            wait();
        } catch (InterruptedException e) {}
    }
}

IllegalMonitorStateException

Richtig:

synchronized(tasks) {
    while (cond) {
        try{ 
            tasks.wait();
        } catch (InterruptedException e) {}
    }
}

`AtomicInteger`¶

The specifications of these methods enable implementations to employ efficient machine-level atomic instructions that are available on contemporary processors. However on some platforms, support may entail some form of internal locking. Thus the methods are not strictly guaranteed to be non-blocking -- a thread may block transiently before performing the operation.

Quelle: https://docs.oracle.com/javase/8/docs/api/java/util/concurrent/atomic/package-summary.html

Übungsblatt¶

...und einige Ergänzungen...¶

Aufgabe 1: Amdahlsches Gesetz¶

Geg.: Puffer

90% Leser Threads: Gleichzeitig, 2s
10% Schreiber Threads: Blockiert, 3s

$$ P = \frac{2*0,9}{2*0,9+3*0,1} \approx 0,86\\ S(P) = \frac{1}{(1-P)+\frac{P}{N}} = \frac{1}{(1-0,86) + \frac{0,86}{4}} \approx 2,82 $$

Aufgabe 2:¶

Problem:¶

Keine Happens-Before-Beziehung zwischen dem Lesen und Schreiben von ping
=> Hier: Lesen/Schreiben aus/in Cache
=> Ein Thread terminiert nicht

Lösung:¶

public static volatile boolean ping = false;

Aufgabe 3¶

Futures als Proxies¶

Haskell:

mydef = [1,3..]
mydef !! 10

21

mydef ist ein Proxy der die Evaluation erst ausführt, wenn notwendig

Aufgabe 3¶

Futures als Proxies¶

Java:

Future<Integer> myfuture = executor.submit(() -> {
    return returnComplicatedInt();
});

myfuture ist ungefähr ein Proxy, der einen in der Zukunft auf das Ergebnis zugreifen lässt:

System.out.println(myfuture.get()); // blockiert bis Ergebnis

Aufgabe 4¶

Completable Futures¶

Javascript:

$.ajax("/my-page").done(function() {
    // do something
});

Aufgabe 4¶

Completable Futures¶

Java:

CompletableFuture.supplyAsync(() -> {
    return /*something complicated*/;
}).thenAccept((res) -> {/* do something */})

Aufgabe 4¶

Streams¶

Haskell:

foldl max 0 (map (+1) [1,2,3,4,5])

6

Aufgabe 4¶

Streams¶

Java:

List<Integer> input = Arrays.asList(1,2,3,4,5);
int result = input.stream()
    .mapToInt(x -> x+1) // [2,3,4,5,6]
    .max() // OptionalInt
    .orElse(Integer.MIN_VALUE);

Fragen zu Advanced Java?¶

Als nächstes:

Aktoren
ganz viel (?) JML

Actor-Model¶

Aktoren (Threads oder Prozesse) kommunizieren per Nachrichten

Wie MPI, aber:

Nachrichten immer asynchron
Aktoren werden zur Laufzeit von anderen Aktoren erzeugt
Aktoren dienen zur Abstraktion (können untersch. Code ausführen)

Beispiel

Design by Contract¶

public static int binarySearch(int[] a, int key) {
    int low = 0;
    int high = a.length - 1;

    while (low <= high) {
        int mid = (low + high) / 2;
        int midVal = a[mid];

        if (midVal < key)
            low = mid + 1
        else if (midVal > key)
            high = mid - 1;
        else
            return mid;
    }
    return -1;
}

Umfrage

Program testing can be used to show the presence of bugs, but never to show their absence!

Edsger W. Dijkstra

Java Modelling Language (JML)¶

Formale Spezifikation von Methoden
z.B. durch Angabe von Vor- und/oder Nachbedingungen

Warum?

Verwendung¶

Dynamische Überprüfung zur Laufzeit: assertions
- Für Fehlersuche

Statische Überprüfung
- Garantiert Eigenschaften der Software

Als Spezifikation

Zum Generieren von Test Cases (vgl. QuickCheck Property tests)

Vor- und Nachbedingungen¶

Syntax: Kommentare mit @ beginnend

Jede Bedingung: Gewöhnliche Java-Expression vom Typ boolean
- Nur Expressions ohne Seiteneffekte

Zusätzliche Boolsche Operatoren:
- ==> Implikation
- <==> Äquivalenz
- <=!=> XOR

Neue Schlüsselwörter (nur für Nachbed.):
- \old(expr) Wert von expr vor Methode
- \result Rückgabewert

public int x;
public int y;
public int z;
/*@ requires y!=0;
  @ ensures \old(y)+1 == y;
  @ ensures x == \old(y);
  @*/
public void doStuff() {
    x = y++;
    z = 10/x;
}

Quantoren¶

Ersatz für Schleifen
(\forall C x; B; R)
- ergibt: $\forall x \in C: (B \implies R)$
(\exists C x; B; R)
- ergibt $\exists x \in C: (B \land R)$

"Generalized Quantifiers"¶

(\sum C x; B; R)
(\product C x; B; R)
(\max C x; B; R)
(\min C x; B; R)
(\num_of C x; B; R)

Diesmal R numerischer Ausdruck bzw. Boolean (num_of)

Sortieren spezifizieren¶

/*@
  @ ???
  @*/
void sort(int[] arr){/*...*/}

Parameter und Attribute¶

Standardmäßig nicht null
nullable:
```
/*@ nullable @*/ List<Integer> list
```
Gilt auch für Methoden

Welche Parameter sind veränderbar?
- assignable für veränderbare Parameter
- assignable \nothing

Klasseninvarianten¶

Nach jedem Konstruktoraufruf
Vor/Nach jedem Methodenaufruf
- Während Aufruf verletzbar
Ähnlich: Schleifen-Invarianten

class IntegerSet {
    byte[] a; /* The arraya is sorted*
    /*@
      @ invariant (\forall int i;
      @                 0 <= i && i < a.length-1;
      @                 a[i]< a[i+1]);
      @*/
}

Seiteneffekte¶

//...
public int doSth() {
    this.i+=10;
    return this.j;
}
/*@ requires a > 0
  @ ensures doSth() = \old(a)
  @*/
public void doSthElse(int a) {/*...*/}
//...

Geht das?

Nein! Denn doSth hat Seiteneffekte.

Jede Funktion, die aus JML aufgerufen wird darf keine Seiteneffekte haben!

public /*@ pure @*/ int getBalance() {/*..*/}

/*@ requires a != null && 0 < a.length < Integer.MAX_VALUE;
  @ requires (\forall int i; 0 <= i < a.length; (\forall int j; i < j < a.length; a[i] <= a[j]));
  @ ensures (\exists int i; 0 <= i < a.length; a[i] == key) <==> a[\result]==key;
  @ ensures !(\exists int i; 0 <= i < a.length; a[i] == key) <==> \result == -1;
  @*/
public static int binarySearch(int[] a, int key) {
    int low = 0;
    int high = a.length - 1;

    while (low <= high) {
        int mid = low + (high-low) / 2;
        int midVal = a[mid];

        if (midVal < key)
            low = mid + 1
        else if (midVal > key)
            high = mid - 1;
        else
            return mid;
    }
    return -1;
}

Trusting Trust (Ken Thompson)
The moral is obvious. You can't trust code that you did not totally create yourself. (Especially code from com- panies that employ people like me.)
Auch die Spezifikation kann Fehler enthalten(!)

/*@ requires a != null && 0 < a.length < Integer.MAX_VALUE;
  @ requires (\forall int i; 0 <= i < a.length; (\forall int j; i < j < a.length; a[i] <= a[j]));
  @ ensures (\exists int i; 0 <= i < a.length; a[i] == key) <==> a[\result]==key;
  @ ensures !(\exists int i; 0 <= i < a.length; a[i] == value) <==> \result == -1;
  @ pure
  @*/
public static int binarySearch(int[] a, int key) {
    int low = 0;
    int high = a.length - 1;

    while (low <= high) {
        int mid = low + (high-low) / 2;
        int midVal = a[mid];

        if (midVal < key)
            low = mid + 1
        else if (midVal > key)
            high = mid - 1;
        else
            return mid;
    }
    return -1;
}

/*@ requires a != null && 0 < a.length < Integer.MAX_VALUE;
  @ requires (\forall int i; 0 <= i < a.length; (\forall int j; i < j < a.length; a[i] <= a[j]));
  @ ensures (\exists int i; 0 <= i < a.length; a[i] == key) <==> a[\result]==key;
  @ ensures !(\exists int i; 0 <= i < a.length; a[i] == value) <==> \result == -1;
  @ pure
  @*/
public static int binarySearch(int[] a, int key) {
    int low = 0;
    int high = a.length - 1;

    while (low <= high) {
        int mid = low + (high-low) / 2;
        int midVal = a[mid];

        if (midVal < key)
            low = mid + 1
        else if (midVal > key)
            high = mid - 1;
        else
            return mid;
    }
    return -1;
}

binarySearch(null,4);

/*@ requires a != null && 0 < a.length < Integer.MAX_VALUE;
  @ requires (\forall int i; 0 <= i < a.length; (\forall int j; i < j < a.length; a[i] <= a[j]));
  @ ensures (\exists int i; 0 <= i < a.length; a[i] == key) <==> a[\result]==key;
  @ ensures !(\exists int i; 0 <= i < a.length; a[i] == value) <==> \result == -1;
  @ pure
  @*/
public static int binarySearch(int[] a, int key) {
    int low = 0;
    int high = a.length - 1;

    while (low <= high) {
        int mid = low + (high-low) / 2;
        int midVal = a[mid];

        if (midVal < key)
            low = mid + 1
        else if (midVal > key)
            high = mid - 1;
        else
            return mid+1;
    }
    return -1;
}

binarySearch(new int[]{1,2,3,4,5},4);

Liskovsches Substitutionsprinzip¶

Barbara Liskov

Subtype Requirement:
Let $\Phi(x)$ be a property provable about objects $x$ of type $T$.
Then $\Phi(y)$ should be true for objects $y$ of type $S$ where $S$ is a subtype of $T$.

Schwächere Vorbedingungen
Stärkere Nachbedingungen

Ansonsten...¶

Private Behavior¶

private/*@ spec_public@*/ int size = 0;
// ....
/*@ ensures \result!= null;
  @ private behavior
  @ requires size > 0;
  @*/
Object pop() { /*...pop logic ...*/ }

Assertions als Contracts¶

Object pop() {
    assert size > 0;
    int _oldSize = size;
    int _oldTop = top();
    // pop logic
    assert size == _oldSize-1;
    assert result == _oldTop;
    return result;
}

Tutorium 10¶

State of the Lecture¶

Klausurrelevant:¶

Nachträge zu letzter Woche¶

Producer/Consumer¶

AtomicInteger¶

Übungsblatt¶

...und einige Ergänzungen...¶

Aufgabe 1: Amdahlsches Gesetz¶

Aufgabe 2:¶

Problem:¶

Lösung:¶

Aufgabe 3¶

Futures als Proxies¶

Aufgabe 3¶

Futures als Proxies¶

Aufgabe 4¶

Completable Futures¶

Aufgabe 4¶

Completable Futures¶

Aufgabe 4¶

Streams¶

Aufgabe 4¶

Streams¶

Fragen zu Advanced Java?¶

Actor-Model¶

Design by Contract¶

Java Modelling Language (JML)¶

Verwendung¶

Vor- und Nachbedingungen¶

Quantoren¶

"Generalized Quantifiers"¶

Sortieren spezifizieren¶

Parameter und Attribute¶

Klasseninvarianten¶

Seiteneffekte¶

Liskovsches Substitutionsprinzip¶

Ansonsten...¶

Private Behavior¶

Assertions als Contracts¶

`AtomicInteger`¶