The questions that we will address in the remaining part of this semester are

• How do you model concurrent systems? (Quick answer: We will look at both shared-memory models and message-passing models.)
• What properties do we typically expect of concurrent systems? (Quick answer: We will look at safety and liveness properties.)
• How do you state and reason about those properties? (Quick answer: We will use both standard logic as well as special logic called temporal logic.)

Before we address any of these questions in detail, let's consider what the essential problem concurrency raises. Andrews and Schneider's paper gives much more detail about all of the issues I discuss in this handout; here, I just highlight the main points.

• The Essence of Concurrency
  • A Simple Example
  • Another Simple Example
• Issues to Consider When Modeling Concurrency
  • Atomicity
  • Communication
  • Synchronization
• About this document ...