02152 Concurrent Systems        Fall 2008
Monday, September 15

Home

Plan

Material

<-prev

next->

Building 308, Auditorium 12

8.15-  9.50	Proof of Peterson's Algorithm Test-and-set solutions Ticket algorithms Barriers
	Verfication tools Model checking Introduction to the SPIN verifier

Building 306, Rooms 98+99

10.00-12.00

CP Exercise Class 2 (ps)(pdf)

Texts and exercises

Today	Invariant proofs: [Basic 3.5] [skip 3.5.2] Spin locks: [Andrews 3.2-3.3] Barriers: [Andrews 3.4]. You may also look at [Andrews 3.5] to see some barrier applications. SPIN: [Spin] (but skip section 3.6 and all of 6 for now)
Coming	Temporal logic: [Basic 4.1-4.3] (skim section 4.3)
Exercises	1. Do Andrews Ex. 3.2. 2. Do Andrews Ex. 3.13.

Supplementary material and links

The SPIN home page.

Hans Henrik Løvengreen, Sep 15, 2008