About the Course

The spread of multicore architectures has a pervasive effect on how we develop software. In this course, we focus on programming techniques for modern multicore machines. The two major paradigms for managing concurrency are shared memory programming and message passing. We will present the basic formal models for these paradigms and use these models to develop verification techniques. The course is structured into three major parts. In the first part, we look at classical performance oriented concurrent programming techniques for shared memory concurrency. In the second part, we look into transactional memories, a new shared memory programming paradigm developed to achieve better programmability. In the third part, we then study message passing concurrency. We focus on message passing programming models that are common in modern functional and object-oriented programming languages.

  • Instructors: Pavol Cerny, Vasu Singh, and Thomas Wies
  • Time: Thursdays, 1pm-3pm (starting October 7, 2010)
  • Location: Seminar Room Mondi 1, IST Austria
  • Grading: The course will be graded based on a course project (60% of the course grade) and homework (40%). There will be six assignments, only the four best grades will be counted towards the course grade.
  • Credits: 3EC

  • Registration: We ask that those interested in taking the course register with the Graduate School at IST. You can register by email: gradschool@ist.ac.at. Please remember to indicate whether you will be participating in the shuttle bus.
  • Shuttle: IST Austria will operate a shuttle-bus, free of charge, from Heilingenstadt (terminus of the U4) to our campus before the class time and a return trip following the class. Please register for the shuttle bus a week before the course starts by emailing gradschool@ist.ac.at.

  • Recommended additional material:
    • The Art of Multiprocessor Programming. Herlihy and Shavit, Morgan Kaufmann, 2008.
    • Actors in Scala. Haller and Sommers, Artima, to appear 2011 (preprint available).
    • Concurrent Programming in ML. Reppy, Cambridge University Press, 1999.
    • Communicating and Mobile Systems: The Pi-Calculus. Milner, Cambridge University Press, 1999.

Schedule

DateLecture
 7.10.2010  Introduction
 Slides: Part 1 Part 2  TxAccount.java   Part 3 (ping pong, concurrent merge sort)
 14.10.2010  Mutual exclusion
 Slides: ppt
 21.10.2010  Theory of Concurrent Objects
 Slides: ppt
 28.10.2010  Proving Linearizability
 Slides: ppt
 04.11.2010  Case study: Concurrent Linked Lists
 fine-grained locking, optimistic, lazy, lock-free implementations
 Slides: ppt
 Homework 1: pdf and Java source files.
 11.11.2010  Introduction to transactional memories: Hardware TM
Slides: ppt
Links: McRTSTM NZTM OSTM SwissTM TinySTM UTM
 18.11.2010  Software transactional memories, safety and liveness properties
Slides: ppt
Homework: HW 2 & 3
 25.11.2010  Formal semantics of transactional programs
 02.12.2010  Performance and correctness issues in implementing TM
Homework: HW 4
 09.12.2010  Message passing (MP) programming paradigms: actors
 Slides: ppt
 16.12.2010  MP programming paradigms: channels, first-class synchronous events
 Slides: ppt  Source code: reference cell  Homework: HW 5
 13.01.2011  Formal semantics of MP programs: pi calculus
 Slides: ppt
 20.01.2011  Formal reasoning about MP: behavioral equivalence, covering problem
 Slides: ppt
 27.01.2011  no lecture
 03.02.2011  Project presentations