CSE 128 Spring
2005
Concurrency
Class meets Mondays
and Wednesdays in McGill 2322 from 5 to 6:20pm
Discussion
section Wednesdays in my office (APM 4824) from 2 to 2:50pm
Professor Keith
Marzullo.
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
checker.
We will cover
the following topics:
- TLA, TLA+, and TLC.
- Alternation
- Refinement mappings
- Two phase handshake protocol
- Grain of atomicity
- Fairness and liveness
- Semaphores
- Threads and semaphores in Java
- Producer-Consumer synchronization
- Specification
- Java implementation
- Shift register
- Another approach to producer-consumer.
- Revisiting grain of atomicity
- Multiclient server systems
- Mutual exclusion
- Readers/Writers
- Monitors as multiclient server systems
- Monitors in Java
- Resource Allocation
- Nonatomic operations and memory models
- The impact on writing concurrent programs.
- The Bakery algorithm
- Linearizability
- Sequentially consistent memory
- Weak lazy caching
- Distributed multiclient servers
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
examination (25%).
Notes
Homework
Please turn in your homework by emailing it to marzullo@cs.ucsd.edu.
Give it a subject that starts with CSE128 (to help my poor spam filter).
Please
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.
Project
A weak
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
and set.
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.
TLA+/TLC/Java
files
Chapter
1
Chapter 2
Chapter 3
Chapter 4