Theoretical Computer Science

Concurrency Theory 2014

News

• On Tuesday, July 29th there will be a meeting in which we talk about the exam content. We meet at 11.30 in Room 34/420.
• There are no more exam dates available in August. If you still need an exam date, please choose a day from the second exam period. We will preferably schedule exams for September 29th and 30th.
• The oral exams will take place in the last weeks of August and September. In each of these weeks, we will fix two days for the exams. Please send Reiner an E-Mail telling him your preferred dates and times for your exam in the following periods:
  • 25th August - 29th August
  • 29th September - 2nd October.
• The tutorials scheduled for June 19th (public holiday) will take place on Monday, June 23rd, starting at 15:30 and 17:15 in 13-305.
• The axiom ConsistentRFdom was missing from the axiomatic TSO model in the lecture notes. It has been added.
• The tutorials scheduled for May 29th (public holiday) will take place on Monday, June, 2nd, at 08:15 in 11-222
and 17:15 in 13-305.
• Exercise 4.2 had a bug in the definition of the list predicate (emp was missing).
• There was a bug in exercise 1.2: the first line must read "... and (P*emp)<=>P". The PDF is now correct.
• There is some more material on separation logic in the Lecture Notes section.
• The room for the lecture on tuesdays has been changed to 48-210.
• The tutorials scheduled for May 1st (public holiday) will take place on Monday, May 5th, starting at 15:30 and 17:00 in 13-305.

Organisation

Dates and rooms:

• Tuesdays 8:15 - 09:45 in 48-210
• Wednesdays 13:45 - 15:15 in 46-280
• Tutorials take place on:
• Thursdays 15:30 - 17:00 in 48-462.
• Thursdays 17:15 - 18:45 in 48-462.
• Tutorials start in the second week.
• The lecture in KIS and in the Module Handbook.

Exams:

1. 60 percent of your exercises have to be marked by a plus.
2. You have to present some of your exercise solutions on the board .

Lecture Notes

• Basics on separation logic (week 1)
• Concurrent separation logic (weeks 1-2) [UPDATED: 30.04.2014]
• Concurrent separation logic examples (weeks 1-2)
• Rely-guarantee (week 3)
• Owicki-Gries (week 3). More on Owicki-Gries.
• RGSep (week 4).
• Well-structured transition systems (chapter 6, pp. 39) (week 5).
• TSO-Reachability (week 6).
• TSO-Reachability (week 7).
• Bounded-round TSO-reachability (week 7).
• Axiomatic memory models (week 8) [UPDATED: 16.06.2014]
• Data race freedom (week 9)
• Compiler optimisations under C11 (week 9)
• Robustness against TSO (week 10). The lectures this week were based on Sections 2, 3, and Appendix A and B in this paper.
• Minimal violations and dichotomy (week 10).
• Locality (week 11).
• Attacks (week 11).
• Instrumentation and complexity (week 12).
• Robustness against TSO for parameterized programs (week 12).
• Robustness against PSO, normal form violations (week 13).
• From normal form violations to multi-headed automata (week 13).
• Relaxed separation logic (week 14).
• CAS (week 14).

Further material on separation logic:

• J. C. Reynolds. Separation logic: A logic for shared mutable data structures.
• P. W. O’Hearn. A Primer on Separation Logic (and Automatic Program Verification and Analysis).
• V. Vafeiadis. Concurrent separation logic and operational semantics

Further material on TSO-reachability

• M. F. Atig, A. Bouajjani, S. Burckhardt, M. Musuvathi. On the Verification Problem for Weak Memory Model. This is the first proof of decidability for TSO-reachability.
• P. A. Abdulla, M. F. Atig, Y.-F. Chen, C. Leonardsson, A. Rezine. Counter-Example Guided Fence Insertion under Weak Memory Models. A newer proof of decidability for TSO-reachability, contains the construction presented in the lecture.
• M. F. Atig, A. Bouajjani, G. Parlato. Getting Rid of Store-Buffers in TSO Analysis. Bounded-round TSO-reachability as presented in the lecture.

Exercises

Organisation:

• Exercises will be made available here (Wednesday evenings).
• Solutions are due on Tuesdays at noon.
• Please hand in solutions in groups of 3 to 4 people.
• The mailbox is in the staircase between buildings 34 and 36, 4th floor, close to the SofTech AG.

Exercise Sheets:

• Download Exercise Sheet 1 here.
• Download Exercise Sheet 2 here.
• Download Exercise Sheet 3 here.
• Download Exercise Sheet 4 here.
• Download Exercise Sheet 5 here.
• Download Exercise Sheet 6 here.
• Download Exercise Sheet 7 here.
• Download Exercise Sheet 8 here.
• Download Exercise Sheet 9 here.
• Download Exercise Sheet 10 here.
• Download Exercise Sheet 11 here.
• Download Exercise Sheet 12 here.
• Download Exercise Sheet 13 here.
• Download Exercise Sheet 14 here.
• This last sheet is optional. There will be no tutorial and it does not count towards the exam requirements.

Content

• Concurrent program logics (extensions of Hoare logic for concurrency)
  • Concurrent separation logic
  • Rely-guarantee
  • RGSep and further logics
• Weak memory models
  • Sequential consistency
  • TSO (Sparc, x86)
  • PowerPC/ARM
  • C/C++11
  • DRF-Theorem and extensions for different memory models
• Multi-threaded programs and Petri nets
• Petri net specific analyses
  • Karp and Miller coverability graphs
  • Invariants
  • Unfoldings + SAT
• Static networks and lossy channel systems (lcs)
• Analysis of well-structured transition systems (wsts), with lcs as an example
  • Wsts and Finkel's finite reachability tree
  • Abdulla's backwards algorithm
  • Geeraerts' EEC algorithm
• Reconfigurable networks and process algebras
• Analysability
  • Structural stationarity, depth, and breadth
  • Well-structuredness in bounded depth
  • Turing completeness in bounded breadth
• Bisimilarity, an alternative correctness notion
• Analysis and its limits
  • Fixed points in the finite
  • Communication freedom and prime elements in the infinite
  • Undecidability following Jančar

Literature

• J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In Logic in Computer Science, 2002. Proceedings. 17th Annual IEEE Symposium on (pp. 55-74). IEEE, 2002. Free version can be found here.
• P. W. O’hearn. A Primer on Separation Logic (and Automatic Program Verification and Analysis). In Software Safety and Security: Tools for Analysis and Verification 33: 286, 2012 Free version can be found here.
• L. Priese and H. Wimmel. Petri-Netze. Springer-Verlag, 2003.
• W. Reisig. Petri nets: An Introduction. Monographs in Theoretical Computer Science. An EATCS Series. Springer-Verlag, 1985.
• P. H. Starke. Analyse von Petri-Netz-Modellen. Leitfäden und Monographien der Informatik. Teubner, 1990.
• J. Esparza and M. Nielsen. Decibility issues for Petri nets-a survey. Journal of Information Processing and Cybernetics EIK, 30(3):143-160, 1994. Free version can be found here.
• J. Esparza. Decidability and complexity of Petri net problems - an introduction. In Lectures on Petri Nets I: Basic Models. Advances in Petri Nets, volume 1491 of LNCS, pages 374-428, Springer-Verlag, 1998. Free version can be found here.
• J. Esparza and S. Melzer. Verification of safety properties using integer programming: Beyond the state equation. Formal Methods in System Design, 16:159-189, 2000. Free version can be found here.
• J. Esparza and K. Heljanko. Unfoldings. Monographs in Theoretical Computer Science. An EATCS Series. Springer-Verlag, 2008. Free version can be found here.
• A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1-2):63-92, 2001. Free version can be found here.
• G. Geeraerts, J.-F. Raskin, L. Van Begin. Expand, Enlarge and Check: new algorithms for the coverability problem of WSTS. Journal of Computer and System Sciences, 72(1):180-203, 2005. Free version can be found here.
• P. Abdulla, A. Bouajjani, B. Jonsson. On-the-Fly Analysis of Systems with Unbounded, Lossy Fifo Channels. In Proc. of the 10th International Conference on Computer Aided Verification, CAV, volume 1427 of LNCS, pages 305-318, Springer-Verlag, 1998. Free version can be found here.
• R. Meyer. Structural Stationarity in the pi-Calculus. PhD thesis, Department of Computing Science, University of Oldenburg, 2008. Free version can be found here.