COSC 6490A 3.0 Concurrent Object Oriented Languages
Winter 2007
Brief overview
In this course, we focus on concurrent programming in the object
oriented language Java. The course consists of four parts.
In the first part, we discuss concurrent programming in general.
In the second part, we focus on modelling concurrent programs.
In the third part, we concentrate on writing concurrent programs
in Java. In the fourth and final part, we look at techniques and
tools to verify concurrent Java programs.
General information
Time: Monday and Wednesday, 17:30-19:00
Place: Chemistry Building, room 122
Instructor: Franck van Breugel
Office hours: Monday and Wednesday, 19:00-19:30 or by appointment
Office: Computer Science and Engineering Building, room 3046
Email: franck@cse.yorku.ca
Evaluation
The performance of the students will be evaluated as a combination of
four assignments (60%), two presentations (10%) and a paper (30%).
Conversion from numeric to letter grade is applied to the overall mark
only and in accordance with the following standard:
F |
C |
B |
B+ |
A- |
A |
A+ |
<60 |
>=60 |
>=70 |
>=75 |
>=80 |
>=85 |
>=90 |
You can view your marks at any time using the following form:
Assignments
There will be four assignments.
The objective of the first assignment is to find a nontrivial concurrent
algorithm in the literature. In the second assignment, the focus is on
modelling the algorithm in Promela and checking some properties of the
model using Spin. In the third assignment, the aim is the implementation
of the concurrent algorithm presented in the first assignment in Java.
The focus of the fourth assignment is to apply Java Pathfinder to verify
the concurrent Java program of the third assignment.
More details can be found below.
- Assignment 1 (due January 29)
- Assignment 2 (due February 19)
- Assignment 3 (due March 20)
- Assignment 4 (due April 6)
Presentations
There will be two presentations. The first presentation covers the
first and second assignment. The second presentation covers the third
and fourth assignment. Each presentation is 20 minutes. The presentations
will be scheduled around the due dates of the second and fourth
assignment.
Paper
The paper has to be based on Assignment 1, 3 and 4. The paper is due
on Friday April 20. More details can be found
here.
Calendar
January 3
H. Sutter and J. Larus.
Software and the Concurrency Revolution.
Queue, 3(7):54-62,September 2005.
January 8
E.W. Dijkstra.
Cooperating Sequential Processes.
EWD 123. 1968.
Focus on pages 10, 11, 19, 26-39. The other pages are also of interest and
you are encouraged to at least skim through them.
John A. Trono.
A new exercise in concurrency.
SIGCSE Bulletin, 26(3):8-10, September 1994.
John A. Trono.
Corrigendum to "A new exercise in concurrency".
SIGCSE Bulletin, 26(4):63, December 1994.
January 10
The lecture will take place in the Steacie Building, room 021.
Ask at the library reference desk for room 021 if you cannot find it.
Leah Graham and Panagiotis Takis Metaxas.
Of course it's true; I saw it on the Internet!
Communications of the ACM, 46(5):70-75, May 2003.
Some information about literature search can be found
here.
January 15
C.A.R. Hoare.
Communicating Sequential Processes.
Communications of the ACM, 21(8):666-677, August 1978.
January 17
Chapter 1 and 2 of
Gerard J. Holzmann.
The SPIN Model Checker.
Addison-Wesley.
2003.
This book is on reserve in the Steacie library.
Some Promela examples:
philosopher.pml,
prodcons.pml
January 22
Chapter 3 of
Gerard J. Holzmann.
The SPIN Model Checker.
Addison-Wesley.
2003.
Some Promela examples:
run1.pml,
run2.pml,
run3.pml,
splurge.pml,
toggle.pml,
list.pml,
sieve.pml
More information about SPIN can be found
here.
January 24
Chapter 4 of
Gerard J. Holzmann.
The SPIN Model Checker.
Addison-Wesley.
2003.
Some Promela examples:
assertion.pml,
endlabel.pml,
progresslabel.pml,
acceptlabel.pml,
never.pml
January 29
Chapter 5 of
Gerard J. Holzmann.
The SPIN Model Checker.
Addison-Wesley.
2003.
A Promela example:
scheduler.pml
January 31
Chapter 11 and 12 of
Gerard J. Holzmann.
The SPIN Model Checker.
Addison-Wesley.
2003.
February 5
Hai Feng Huang.
A general translation from SCOOP to Promela.
February 2007.
February 7
Mary Campione, Kathy Walrath and Alison Huml.
The Java Tutorial.
Lesson: Threads: Doing Two or More Tasks At Once.
Some Java examples:
Printer
(PrinterTest),
Printer
(PrinterTest),
Printer
(PrinterTest),
PrinterTest,
Runner,
Race
February 12
No lecture.
February 14
No lecture.
February 19
Mary Campione, Kathy Walrath and Alison Huml.
The Java Tutorial.
Lesson: Threads: Doing Two or More Tasks At Once.
Some Java examples:
Buffer,
Producer,
Consumer,
Relay
February 21
Mary Campione, Kathy Walrath and Alison Huml.
The Java Tutorial.
Lesson: Threads: Doing Two or More Tasks At Once.
P.J. Courtois, F. Heymans and D.L. Parnas.
Concurrent control with "readers" and "writers".
Communications of the ACM, 14(10): 667-668, October 1971.
An applet of the readers-writers problem can be found
here.
Some Java examples:
Reader,
Writer,
Database,
Simulator.
February 26
Presentations.
February 28
Presentations.
March 5
Presentations.
March 7
Some Java examples:
Value,
WriterMin,
WriterMax,
Sequencer,
Buffer,
Worker,
Coordinator.
March 12
James Gosling, Bill Joy, Guy Steele and Gilad Bracha.
The Java Language Specification.
Chapter 17: Threads and Locks.
The sleeping barber problem can be found on page 38 of
E.W. Dijkstra.
Cooperating Sequential Processes.
EWD 123. 1968.
March 14
Willem Visser, Klaus Havelund, Guillaume Brat, SeungJoon Park and Flavio Lerda.
Model Checking Programs.
Automated Software Engineering, 10(2): 203-232, April 2003.
More information about Java PathFinder can be found
here.
Java PathFinder Tutorial by Willem Visser and Peter Mehlitz.
March 19
Course evaluation (first 15 minutes)
Sergey's material can be found here.
March 21
No lecture.
March 26
No lecture.
March 28
No lecture.
April 2
Presentations
April 4
Presentations