COMP2310 - Week 4 - Verification of Concurrent Programs

Table of Contents

• Temporal Logic
• Logical Specification
• Inductive Proofs of Invariants
• Model Checking
• Deadlock vs Livelock

---

Temporal Logic

Logical Specification

• A formula is either true or false for a given state of the system, e.g.

p1 ^ q1 ^ ~wantp ^ ~wantq -> Is true in the initial state of the system

• Mutual exclusion property, e.g.

~(p4 ^ q4) -> I.e. not both are in the critical section at the same time and must be true for all possible states of computation

Inductive Proofs of Invariants

• To prove invariance of logical formula $A$:

1. Prove that $A$ is true in the initial state; and then
2. Assuming $A$ is true in all states up to current state, prove $A$ is true in the next state

NOTE: Easy for implication forms

Model Checking

• Specify states, transitions, and correctness properties formally in temporal logic

• Check each possible state for violations of correctness properties

  • Deadlock -> No allowed transitions

  • TLA+ software

Deadlock vs Livelock

• Livelock -> "Around and around in a loop"

  • A cycle of different states occurs, processes are changing/moving between states, however they eventually return to the start

• Deadlock -> Arrive at a state where no possible transitions are possible to move forward