CSE 128 Spring
Class meets Mondays
and Wednesdays in McGill 2322 from 5 to 6:20pm
section Wednesdays in my office (APM 4824) from 2 to 2:50pm
Office hours WF 10-11 in my office (APM 4824) or by appointment.
Concurrency is more
than semaphores, threads, and synchronized classes in Java. Concurrency
is a characteristic of systems including distributed systems, computer
hardware, and physical systems. The aim of this class is to give you
some tools to help you think about concurrency and to come up with
concurrent programs and systems that are more likely to be correct.
One of the main
themes of this course is teaching you how to specify a concurrent
system and show that it implements properties that you desire. You will
learn a specification language, TLA+, that can be mechanically checked
using a model
We will cover
the following topics:
Your grade in
this class will be determined by your performance in five homeworks
(25% total), a class project (50%), and a closed-book and notes final
- TLA, TLA+, and TLC.
- Refinement mappings
- Two phase handshake protocol
- Grain of atomicity
- Fairness and liveness
- Threads and semaphores in Java
- Producer-Consumer synchronization
- Java implementation
- Shift register
- Another approach to producer-consumer.
- Revisiting grain of atomicity
- Multiclient server systems
- Mutual exclusion
- Monitors as multiclient server systems
- Monitors in Java
- Resource Allocation
- Nonatomic operations and memory models
- The impact on writing concurrent programs.
- The Bakery algorithm
- Sequentially consistent memory
- Weak lazy caching
- Distributed multiclient servers
Please turn in your homework by emailing it to firstname.lastname@example.org.
Give it a subject that starts with CSE128 (to help my poor spam filter).
turn in any .tla/.cfg/.java files as attachments to a message that
contains any explanation or other text answers.
- Due April
11, 2005 at 5pm: Problem 1.1 and Problem 1.2 in notes.
- Due April 20, 2005 at 5pm:
Problems 2.3, 2.8 and 2.9 in notes. Comments and corrections here.
- Due May
11, 2005 at 5pm: Problems 3.4, 3.5 and 3.8.
binary semaphore is a binary
semaphore with weak fairness. Thus, if you have two processes using a
single binary semaphore to protect a critical region, it is possible
for one process to never enter the critical region: it could infinitely
often find itself in contention with the other process, and the other
process could always win the contention. An example of a weak binary
semaphore is one implemented with test
Implement n process mutual exclusion using
only weak binary semaphores. The number of processes n is a parameter of the system.
Show your solution is correct using TLA+. Then, write a Java program
that implements a test and set class,
and then implements your solution. Your program should create a set of
threads that repeatedly try to enter the critical section, and that
perform some simple diagnostics to determine whether the solution
violates safety and fairness.