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: firstname.lastname@example.org. Please remember to indicate whether you will be participating in the shuttle bus.
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 email@example.com.
- 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.
|7.10.2010|| Introduction |
Slides: Part 1 Part 2 TxAccount.java Part 3 (ping pong, concurrent merge sort)
|14.10.2010|| Mutual exclusion |
|21.10.2010|| Theory of Concurrent Objects |
|28.10.2010|| Proving Linearizability |
|04.11.2010|| Case study: Concurrent
Linked Lists |
fine-grained locking, optimistic, lazy, lock-free implementations
Homework 1: pdf and Java source files.
|11.11.2010|| Introduction to transactional memories: Hardware TM
Links: McRTSTM NZTM OSTM SwissTM TinySTM UTM
|18.11.2010|| Software transactional memories, safety and liveness properties
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 |
|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 |
|20.01.2011|| Formal reasoning about MP: behavioral equivalence, covering problem |