cs341 Lecture Notes
Spring 2002
Week 4, Thursday

For today you should have

1) solved the last semaphore puzzle.

2) Worked on hw03.

3) reread the lottery scheduling paper.

4) Read Sections 8.1 and 8.2 and answered the preparation
   questions.

For next time you should:

1) Do the practice exams and the practice quiz and bring
   questions on Monday.

2) Finish hw02


Today's topics

1) solution to the reusable barrier problem

2) the long-postponed second part of our discussion
   of scheduling strategies

3) the preparation questions from Chapter 8


Barrier Solution
----------------

Key idea: a barrier has two states, locked and unlocked.

When locked, everyone waits.

When unlocked, everyone can pass.

To lock, execute wait (when you know it's unlocked).

To unlock, execute signal (when you know it's locked).

Once you have an abstract model of a turnstile, it is
easier to build complex solutions by assembling components.

Problem: very hard to demonstrate correctness

	 testing is not sufficient!

Goal: code that is demonstrably (if not provably) correct.

1) Use symmetry to help make code demonstrably correct.

2) Look for intermediate-level claims about the code.

3) Think of different parts of the program as rooms separated
   by doors.