I. Correctness and Progress

In a concurrent setting, we need to specify both the safety and the liveness properties of an object

1. Safety and Liveness

Safety ⇒ Can be checked

• nothing “bad” will ever happen
• the program will never produce a wrong result (“partial correctness”)
• those properties whose violation always has a finite witness

Liveness ⇒ Can’t be checked

• something “good” will happen eventually (but we don’t know when)
• the program will produce a result (“termination”)
• those properties whose violation never has a finite witness

2. Objective

Need a way to define

1. When an implementation is correct
2. The conditions under which it guarantees progress

In this lecture, we focus on correctness.

II. Sequential Objects