Bonn-Aachen International Center for Information Technology


News	Application for Master Programs	B-IT Universities Institute
About B-IT	B-IT Research School	B-IT Applied Science Institute

Lecture 3 - Race-free concurrency

In this lecture, we will extend the core proof system in order to support synchronization constructs like Hoare monitors, locks, semaphores, or asynchronous message-passing, for the support of which separating conjunction allows quite elegant proof rules. This proof system will ensure that proved programs are race-free, in the sense that a memory cell cannot be accessed by two threads simultaneously. We will then investigate a weaker notion of race, where multiple readers are allowed to read (but not write) the same cell simultaneously, which will drive us to the notion of permission algebras. We will also consider the problem of distributed memory leaks, and we will answer it by a notion of communication's contract.

NEWS

Best Contribution Award for B-IT Student
[more]

Best Student Paper Award for B-IT Research School Student
[more]

B-IT Professor participates with "Silhouettes" at the EXPO 2010 Shanghai
Silhouettes: An Interactive Collaborative Gesture-Based Experience for the EXPO 2010 Shanghai [more]

Symposium in honour of Professor von zur Gathen 60th Birthday - "Professor von zur Gathen: A Modern Computer Algebraist"
International Symposium to celebrate Professor von zur Gathen's 60th Birthday [more]

B-IT Life Science Informatics Lecture Series 2010
[more]