|
Week
|
Date
|
Read Book
|
Read Slides
|
(Who) Discussion
|
Book Exercises & Practicals
|
|
1
|
Jan 06
|
|
Sequential Processes #1-15
|
(BG) Slides #1-16
|
1.1 (BG#1, BH#2, SD#3); 1.2; 1.4; (BG)1.5; (BH)1.6; (SD)1.7; 1.8-11; 1.14-15
|
|
2
|
Jan 13
|
CRS Preface; chs. 1 & 2
|
Concurrency #16-34
|
(BG) Slides #16-34; CRS chs 1 & 2
|
2.1; 2.2 (hint: look for deadlock); 2.4 (hint: use channel I/O); 2.5 (what prevents DCUSTOMER from leaving without paying?); 2.9 (make a counterexample)
Practicals: Using ProBe & Parallel Processes
|
|
3
|
Jan 20
|
CRS 4.1 only
|
Traces #35-60
|
(SD) Examples 2.1.12-13; slides; ch 4.1
|
4.1 (note: tau is an internal event that doesn't show up in the trace); 4.2; 4.8 (you can write out just the maximal length traces that end in check; read ch 3.4 before doing part 4); 4.11; 4.12
Practicals: Using FDR
|
|
4
|
Jan 27
|
CRS 3.1 to 3..3
|
Specification; Abstraction #61-67
|
(BH) Slides; ch 3
|
3.1; 3.3 (continues on next page! if you say "no", provide a counterexample); 3.5; 3.7; 3.8 (counterexample for "no"); 3.9 (enter your spec into Probe and be ready to demo it; can you do any verification with FDR?)
Practicals: Specifications
1st Progress Report: e-mail: TW, cc: BG by 1/31
|
|
5
|
Feb 03
|
CRS 9.1 to 9.5
|
Choice between processes #68-93 (this goes back to CRS already read)
|
(SD) Slides; ch 9.1-5
|
9.1-4
For 9.3, use these interface events:
question.
q
= question
q
is asked
team.{1,2} = team presses its buzzer
reply.{1,2}.
x
= team replies with answer
x
There is also a function answer(
q
) which returns the correct answer to question
q
.
Practicals: Internal Choice
|
|
6
|
Feb 10
|
CRS 9.6 to 9.8
|
Examples #94-103
|
(BH) Slides; rest of ch 9
|
Practicals: Deadlocks
|
|
Feb. 16-20
|
READING WEEK (BG away 2/16 to 3/6)
|
|
|
7
|
Feb 24
|
Create case studies
Do literature review
Meet for "show & tell": discoveries, progress, challenges, solutions
|
(SD)
|
|
|
8
|
Mar 02
|
(BH)
|
2nd Progress Report: include "minutes" from your 2/24 & 3/2 meetings; e-mail: TW, cc: BG by 3/5
|
|
9
|
Mar 09
|
CRS 10
|
Traces & Choice #104-111
|
(SD) Slides; ch. 10
|
9.6, 7, 10, 11
(none from ch. 10)
Practicals: The Cyclic Scheduler
|
|
10
|
Mar 16
|
CRS 11.1; 12.1, 5; 13.1, 4
|
|
|
For these, BH do odd subparts, SD do even: 11.1 (state why any are not legitimate), 2 (explain why or why not), 3 (state why any are not consistent)
Look at 12.1-3; I'll supply the answers for us to study.
Practicals: Liveness Specs (end)
|
|
11
|
Mar 23
|
CRS 13.4
A.1, and enough of A.2 to get the idea
|
Liveness Specifications #112-125 (end)
|
(BH) Slides
(SD) chs. 13 & A
|
13.5
Look at 13.6, and we will study the solution.
13.8, writing up TCOLLEGE using the timeout operator, then answer the 3 questions.
A.5
B.3 (put Example 13.4 into CSPm and enter it into FDR)
|
|
12
|
Mar 30
|
CRS B
|
|
Exer. 12.1-3 & chs. 13, A, B
Practical: Liveness Spec
csp++ demo
|
|
