Moodle.UP

https://puls.uni-potsdam.de/qisserver/rds?state=verpublish&status=init&vmfile=no&publishid=94124&moduleCall=webInfo&publishConfFile=webInfo&publishSubDir=veranstaltung

Waren Anfang des Jahrtausends parallele Systeme noch dem High-Performance-Computing (HPC) vorbehalten, so haben sie mit dem Hardware-Trend hin zu Multicoresytemen mittlerweile auch im Desktop-PC und Serverbereich Einzug gehalten. Um diese Hardwareplattformen optimal ausnutzen zu können sind spezielle Programmierparadigmen, -sprachen und -werkzeuge notwendig.

Im HPC-Bereich hat die Vernetzung von Arbeitsplatzrechnern mittels leistungsfähiger Kommunikationstechnologien (z. B. Gigabit Ethernet, InfiniBand) zu einer preisgünstigen Plattform für parallele Anwendungen geführt – den sogenannten Compute Clustern.

Die Vorlesung stellt die Konzepte der Parallelverarbeitung vor und legt ihren Schwerpunkt auf den Bereich Cluster Computing.

In der Veranstaltung steht die Planung und Organisation von Informatikunterricht im Vordergrund. Es werden Konzepte erstellt, präsentiert und gemeinsam diskutiert und reflektiert.

Die Veranstaltung bietet einen Einstieg in die Didaktik der Informatik. Wir charakterisieren das Wesen der Wissenschaft Informatik und ihrer Didaktik. Vorgestellt werden verschiedene Konzepte und Ansätze zur Didaktik der Informatik, u.a. frühe Ansätze der Schulinformatik oder das Konzept zur Informatik im Kontext. Es wird der allgemeinbildende Charakter der Informatik thematisiert und Unterrichtssituationen genauer beleuchtet.

Unter Verteilten Systemen verstehen wir vernetze Rechnerressourcen, die miteinander kooperieren. Ein klassisches Interaktionsmuster ist das Client-Server-Computing. Dieses finden wir in lokalen Netzen zwischen Client und Fileserver, aber auch im Internet bei Webapplikationen wie Suchmaschinen und sozialen Netzwerken. Voraussetzung für die Interaktion ist jeweils die Möglichkeit der Kommunikation zwischen den Rechnerressourcen. Neben dem Client-Server-Computing hat sich auch das P2P-Computing als erfolgreiches Interaktionsmuster durchgesetzt. Aktuelle Erscheinungsformen der Verteilten Systeme finden wir auch im Cloud Computing, sowie in Sensornetzen bis hin zum IoT.

Die Vorlesung behandelt Kommunikationsmodelle für Verteilte Anwendungen (socketbasierte Kommunikation, RPC, REST, Publish-Subscribe), Konzepte verteilter Dateisysteme, verteilte Algorithmen, Synchronisationsverfahren für verteilte Anwendungen sowie Konzepte zur Lastverteilung in Hochverfügbarkeits-Clustern wie Google.

Informatik-Studierende finden Themen der Theoretischen Informatik grundsätzlich interessant, aber korrespondierende Übungsaufgaben -- insbesondere Beweisaufgaben -- stellen immer wieder eine große Herausforderung dar. Der Kurs greift diesen Punkt auf und stellt das mathematische Beweisen in den Mittelpunkt der Auseinandersetzung.

Zum Erlernen der klassischen „Papier&Stift”-Beweise werden wir einen indirekten Weg einschlagen: Zunächst werden wir lernen, mit dem Beweisassistenten Coq Beweise zu führen (Erklärung Beweisassistent s.u.). Später werden wir daran arbeiten, diese Form der Beweise in „Papier&Stift”-Beweise zu übertragen. Schließlich wird auch eingeübt werden, „Papier&Stift”-Beweise direkt zu führen.

Die Inhalte, anhand derer wir die Beweismethodik einstudieren werden, sind die folgenden:
1) Logik
  a) Aussagenlogik
  b) Prädikatenlogik
2) Datenstrukturen
  a) Nicht-rekursive Datenstrukturen (Records)
  b) Listen
  c) Natürliche Zahlen
  d) Binärbäume
Das Ziel allerdings ist hierbei weniger einen konkreten Themenbereich der Mathematik oder Theoretischen Informatik durchzuarbeiten, sondern den Teilnehmerinnen und Teilnehmern des Kurses ein grundlegendes Verständnis mathematischer Beweisformen, formaler Methoden und dem dazugehörigen Handwerkszeug zur Entwicklung und Erstellung dieser zu vermitteln.

Was sind Beweisassistenten?

Computergestützte Systeme zur Durchführung mathematischer Beweise werden seit den 1960ern entwickelt. Man unterscheidet zwischen Systemen, die Beweise erzeugen, sowie solchen, die Menschen beim Erzeugen von Beweisen unterstützen. Letztere werden auch Beweisassistenten oder interaktive Theorembeweiser genannt, ein solches System ist Coq, welches wir im Kurs einsetzen werden.

Bei Beweisassistenten im engeren Sinne des Begriffes kann der Nutzer Schritt für Schritt Wissen aus den Voraussetzungen generieren und das bisherige Ziel durch ein leichter zu zeigendes, aber hinreichendes Ziel ersetzen. Konkret werden Beweise durch eine Auflistung von sogenannten Taktiken innerhalb einer dem Programmieren ähnlichen Entwicklungsumgebung gewonnen, wobei den Taktiken systemintern Inferenzregeln zugrunde liegen. Das System führt die durch die Taktiken vermittelten Inferenzregeln aus. Dabei prüft es jeden Beweisschritt auf seine formale Korrektheit. Dies ist in erster Näherung mit dem Compilereinsatz beim Programmieren vergleichbar.

Beweisassistenten haben gegenüber Stift und Papier verschiedene Vorteile:
-    Sie liefern unmittelbares Feedback auf eine Beweisidee, indem sie genau anzeigen, ob ein Beweisschritt erfolgreich anwendbar ist und welche Schritte noch auszuführen sind, damit ein Beweis vollständig abgeschlossen ist.
-    Studierende können zu Beginn verschiedene Beweisideen ausprobieren, indem sie mit dem jeweiligen System spielen. Das garantiert höhere Flexibilität gegenüber Stift- und Papierbeweisen, in denen man nur sehr schlecht Dinge streichen oder verbessern kann, ohne den Beweis neu aufschreiben zu müssen. Aus dem gleichen Grund sollte ein Beweisassistent auch besser darin unterstützen, mit einem Beweis überhaupt zu beginnen.

Aktuelle (Multimedia-)Applikationen setzen i.d.R. nicht nur leistungsfähige Clients voraus, sondern sind für den Einsatz in Rechnernetzen konzipiert. Häufig handelt es sich um parallelisierte Anwendungen. Neben Servern und Netzwerktechnik erfordert dies spezielle netzbasierte Architekturen, um die Interoperabilität der einzelnen Komponenten in heterogenen Umgebungen zu gewährleisten. Die Vorlesung geht nach einer Einführung in die Thematik auf ausgewählte Konzepte ein, wie z.B. Grid Computing, Peer-to-Peer Kommunikation oder Service-Orientierte Architekturen. In der begleitenden Übung werden die vorgestellten Konzepte vertiefend betrachtet.