Compilers - Abstract Mashines WiSe 24/25

Uncertainty in Artificial Intelligence and Machine Learning WiSe 24/25

Strukturbioinformatik WiSe 24/25

Systems Biomedicine WiSe 24/25

Algorithmen auf Sequenzen WiSe 24/25

Algorithmische Bioinformatik: Netzwerke, Graphen und Systeme WiSe 24/25

Complexity Theory WiSe 24/25

Automated Theorem Proving WiSe 24/25

Program Analysis for Security WiSe 24/25

Summary: This course deals with applying formal methods for reasoning about programs to low-level code (such as x86 machine code) to find bugs, prove their absence, or simply gain more information about software (reverse engineering).

Topics we intend to cover include:

  • Executable formats and machine code
  • Disassembly and decompilation
  • Classic dataflow analysis, theory and practice
  • Recovering control flow
  • Fuzzing (mutation-based, grammar-based)
  • Debugging and dynamic binary instrumentation
  • Taint analysis and symbolic execution

Enrolment key: pasec24

Verification of Parallel Programs WiSe 24/25

Enrollment Key: VerParProg 24/25

The course deals with mostly automatic verification approaches for multi-threaded programs with shared memory. Topics of the course are:

  • Semantics of parallel programs, e.g., interleaving semantics
  • Static and dynamic approaches for data race detection
  • Techniques for deadlock detection
  • Verification of program properties (e.g., with sequentialization, bounded model checking, etc.)
  • Partial Order Reduction
  • Thread-modular verification

At the end of the course, students can name a number of techniques for the verification of parallel programs, especially in the area of data race and deadlock detection as well as for verification of safety properties. They should be able to explain the underlying formalisms of the techniques, to describe the work flow of the different techniques, and to apply the techniques on examples. Moreover, the students know the strengths and weaknesses of the techniques.

Literature

Program Semantics

  • K. R. Apt, F. S. de Boer, E.-R. Olderog: Verification of Sequential and Concurrent Programs. Springer 2009.

Data Race Detection

  • S. Savage, M. Burrows, G. Nelson, P. Sobalvarro, T. E. Anderson: Eraser: A Dynamic Data Race Detector for Multi-Threaded Programs. SOSP 1997.
  • E. Poznianski, A. Schuster: Efficient On-the-Fly Data Race Detection in Multithreaded C++ Programs. IPDPS 2003.
  • C. Flanagan, S. N. Freund: FastTrack: efficient and precise dynamic race detection. PLDI 2009.

Deadlock Detection

  • Dawson R. Engler, Ken Ashcraft: RacerX: effective, static detection of race conditions and deadlocks. SOSP 2003.
  • Mayur Naik, Chang-Seo Park, Koushik Sen, David Gay: Effective static deadlock detection. ICSE 2009.

Sequentialization

  • Akash Lal, Thomas W. Reps: Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis. CAV 2008.
  • Omar Inverso, Ermenegildo Tomasco, Bernd Fischer, Salvatore La Torre, Gennaro Parlato: Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization. CAV 2014.

Bounded Model Checking

  • L. C. Cordeiro, B. Fischer: Verifying multi-threaded software using SMT-based context-bounded model checking. ICSE 2011

Thread-modular Verification

  • C. Flanagan, S. N. Freund, S. Qadeer: Thread-Modular Verification for Shared-Memory Programs. ESOP 2002

Partial Order Reduction

  • D. Peled: Partial-Order Reduction. Handbook of Model Checking 2018.
  • P. Godefroid, D. Pirottin: Refining Dependencies Improves Partial-Order Verification Methods (Extended Abstract). CAV 1993.
  • P. Godefroid, P. Wolper: Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties. Formal Methods in System Design 2(2) 1993.

Atomicity Checking

  • C. Flanagan, S. N. Freund: Atomizer: a dynamic atomicity checker for multithreaded programs. POPL 2004

Principles of Compiler Design WiSe 24/25

Machine Learning WiSe 24/25

Deep Learning and Artificial Intelligence WiSe 24/25

Data Mining Algorithmen I WiSe 24/25

Intelligent Systems WiSe 24/25

Computational Intelligence WiSe 24/25

Virtual Reality WiSe 24/25

Advanced Topics in Computer Graphics WiSe 24/25

IT-Sicherheit WiSe 24/25

Parallel and High Performance Computing WiSe 24/25

Welcome to the course webpage for Parallel and High Performance Computing for winter-term 2024/25 at LMU Munich. Here you will find details on the lecture and the accompanying practical lab exercises.

Lecture slides will be made available chapter-by-chapter through this webpage.

Material from the lab exercises will be available via Moodle.

Here is the enrollment key: ParallelPioneers

Content

Parallel computing is concerned with using multiple compute units to solve a problem faster or with higher accuracy. Historically, the main application area for parallel machines is found in engineering and scientific computing, where high performance computing (HPC) systems today employ tens- or even hundreds of thousand compute cores.

The application area for parallel computing has, however, expanded recently to essentially include all areas of information technology. Virtually all servers, desktop, and notebook systems, and even smartphones and tables are today equipped with CPUs that contain multiple compute cores. In each case, the potential for these systems can only be fully realized by explicit parallel programming. As such understanding the benefits, challenges, and limits of parallel computing is increasingly becoming a "must have" qualification for IT professionals.

This course addresses the increasing importance of parallel and high performance computing and is covering three interwoven areas: Parallel hardware architectures, parallel algorithm design, and parallel programming. The successful student will be able to identify potentials for parallel computing in various application areas, judge the suitability of contemporary hardware architectures for a parallel computing problem and understand efficient implementation strategies using modern parallel programming approaches.

The lecture is partially based on material that has been developed at UC Berkeley and which has been funded by the US National Science Foundation. The course slides will be made available for download by the date of the lecture and will be in English.

Audience

The course is intended for both bachelor and master students of computer science and related fields. More formally, in German: Die Vorlesung richtet sich an Studenten der Informatik bzw. Medieninformatik (Diplom) nach dem Vordiplom sowie an Studenten der Informatik, Bioinformatik bzw. Medieninformatik (Bachelor, Master) im Rahmen der vertiefenden Themen der Informatik. Für Vorlesung und Übung werden 6 ECTS-Punkte vergeben.

Lab Exercises

The lecture is accompanied by a lab exercises to deepen the understanding of topics covered in the lecture. High performance computing systems hosted at the Leibniz Supercomputing Center will be made available to the students. Worksheets for the lab exercises will be made available on Moodle.

Grid und Cloud Computing WiSe 24/25

Grids und Clouds stellen unterschiedliche Ausprägungen eines verteilten Informatikparadigmas dar, durch das unter Ausnutzung von geographisch und administrativ verteilten Systemen im Bedarfsfall ein Pool von Ressourcen und abstrakten, virtualisierten und dynamisch-skalierbaren Services (z. B. Rechenleistung, Speicherkapazität, Plattformen, Visualisierung) über das Internet bereitgestellt wird.

In dieser Vorlesung (und den begleitenden Übungen) werden die Grids und Clouds zu Grunde liegenden Fragestellungen und Technologien vorgestellt und praktisch angewandt. Nach einer ausführlichen Motivation werden zunächst grundlegende verteilte Systemmodelle und Basistechnologien betrachtet. Darauf aufbauend werden folgende Themen behandelt: Cloud-Architekturen, Cloud-Programmierung und Software-Umgebungen (Workflows, MapReduce, Spark, Google Cloud Dataflow, Amazon AWS, Data Lakes, etc.), Virtuelle Organisationen, Grid Computing-Umgebungen, Resource Management, Data Management, Ubiquitous Computing mit Clouds und im Internet of Things, Grids of Clouds, Clouds of Grids. 
Abschließend werden spezielle Fragestellungen zu Realzeitaspekten, wie sie zum Beispiel im Urgent Computing auftreten, und neue Trends behandelt.

Die Vorlesung richtet sich vornehmlich an Master-Studenten, die sich mit neueren Entwicklungen im verteilten Hochleistungsrechnen (Systemarchitektur, Programmierparadigmen, Leistungseffizienz, Energieeffizienz) vertraut machen wollen.

Der Relevanz des Themas wird durch Gastbeiträge externer Experten Rechnung zu tragen. Diese Vorträge werden teilweise in englischer Sprache gehalten.