CSE 128 Spring 2004
Concurrency


Class meets Tuesdays and Thursdays in Sequoyah 147 from 2 to 3:20pm
Discussion section Mondays in CSB 002 from 4 to 4:50pm

Professor Keith Marzullo. Office hours MW 11-12 in my office (APM 4824) or by appointment..
TA Xianan Zhang. Office hours W 1-3 in EBU-1 6307A.

FINAL EXAM Wednesday, June 9 3-6 PM
The exam will be held in EBU 1-3327 (we've reserved the timeslot for the 26 Sun workstations in one part of the room)


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: 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
Specifying Systems by Leslie Lamport
Downloading the TLA+ tools
TLA+ Quick Reference
Notes on running TLA and TLC on ieng9
Chapter 1
Chapter 2
Chapter 3
Chapter 4
Notes on the snapshot protocol


Homework

Please turn in your homework by emailing it to cs128s@ieng9.ucsd.edu. Please turn in any .tla/.cfg/.java files as attachments to a message that contains any explanation or other text answers.
  1. Due April 8, 2004 at 2pm: Problem 1.1 and Problem 1.2 in notes.
  2. Due April 22, 2004 at 2pm: Problems 2.3. 2.4, 2.6. 2.8 and 2.9 in notes. Comments and corrections here.
  3. Due May 6, 2004 at 2pm: Problems 3.4, 3.5, 3.7 and 3.8 in notes. Comments and corrections here.
  4. Due May 20 May 27, 2004 at 2pm: Problems 4.8 and 4.13 in notes. Comments and corrections here.
  5. Due June 10, 2004 at 2pm: Problem 4.14 in notes.


Project

You can work on your class project either by yourself or with one other person. If you do a project with another person, please explain in your report how you divided up the work. In the project descriptions, I give some ideas of how you might extend the project for two people, but these are only ideas. You can decide for youself on how to extend or change the project to accomodate two people.

The written part of the project will be due on Monday Tuesday morning (12:01 AM) of Week 10. This should consist of a paper that describes the problem you considered and your solution. You should also turn in the files for your specification and your implementation. I will also schedule a brief meeting with you during Week 10 for you to give us a presentation of your project.

Please choose one of the following topics for your project:
  1. 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.

For two people working on this project, you might try to do an actual implementation of binary semaphores using test and set (or whatever instruction you find on the hardware you choose to use). You could then do a real implementation, perhaps in C.
  1. Barrier synchronization is a concurrency construct that allows a (fixed) set of threads to block until all threads have arrived at the barrier. If barrier(n) is the construct, then a thread blocks when it executes barrier(n) until all n threads have executed barrier(n). Then, eac blocked thread unblocks, but block again if it again executes barrier(n).
First, come up with a lower bound on the number of semaphores that are required to implement barrier synchronization. Your argument can be informal. Then, devise a solution that uses as few semaphores as you can - ideally, the number you showed to be a lower bound. Use TLA+ to show that your solution does indeed implement barrier synchronization.

For two people working on this project, you might try to examine the implementation of barrier synchronization in a real multiprocessor system, and compare it with your semaphore-based solution.
  1. Consider four processes that communicate by sending messages to each other. You can assume that if a process p sends a message to process q at time t, then q will receive the message by time t + D for some known constant D. Each process i has a value i.input. Your goal is to design a protocol such that each correct process i determines a value i.output where:

No more than one process can be faulty. A faulty process can send any message it wishes. For example, it can tell one correct process that its input value was 1and tell another process that its input value was 17. It can also fail to send some messages, or simply stop running.

Show that your protocol is correct using TLA+. Then, implement your protocol. You will need to define a message class that allows a process on one machine to send a message to another process, on the same or a different machine. Choose a value of D that is reasonable for your experimental setup. Write a demonstration program that illustrates your protocol in action where one process is faulty.

For two people working on this project, you might try to built your protocol where there are seven processes and up to two of them can be faulty.


TLA+/TLC/Java files
Chapter 1
CallReturn.tla
Alternation.tla
Alternation.cfg
AltImplementsOsc.tla
AltImplementsOsc.cfg
Discussion section 1
BadGame.tla
Game.tla
Game.cfg
GenericGame.tla
GenericGame.cfg
TTT.tla
GenericTTTGame.tla
GenericTTTGame.cfg
Chapter 2
TwoPhase.tla
TwoPhase.cfg
MCTwoPhase.tla
MCTwoPhase.cfg
AlternationPgm.tla
AlternationPgm.cfg
FGCallReturn.tla
Semaphores.tla
SemAlternation.tla
SemAlternation.cfg
Semaphore.java
SemAlt.java
Discussion section 2
Alternate.tla
Alternate.cfg
Peterson.tla
Peterson.cfg
Chapter 3
PCCallReturn.tla
ProducerConsumer.tla
MCProducerConsumer.tla
MCProducerConsumer.cfg
SemProducerConsumer.tla
ShiftRegister.tla
NProcProducerConsumer.tla
ListProducerConsumer.tla
SemProducerConsumer.java
Chapter 4
AtomicBakery.tla
BankingSystem.tla
CSCallReturn.tla
Election.java
MCBankingSystem.cfg
MCBankingSystem.tla
MCMultiClientServer.cfg
MCMultiClientServer.tla
MCOneClientRegister.cfg
MCOneClientRegister.tla
MCOneClientServer.cfg
MCOneClientServer.tla
MCSimpleBakery.cfg
MCSimpleBakery.tla
MCSimpleMultiClientServer.cfg
MCSimpleMultiClientServer.tla
MultiClientServer.tla
MutexImplementation.cfg
MutexImplementation.tla
MutualExclusion.tla
OneClientRegister.tla
OneClientServer.tla
ReadPriority.java
ReadersWriters.cfg
ReadersWriters.tla
SimpleBakery.tla
SimpleMultiClientServer.tla