COMP2310 - Week 3 - Critical Section Problem

Table of Contents

• The Problem
• Atomic Load and Store
• Proving Correctness: State Diagrams

---

The Problem

• $N$ processes executing infinite instruction sequencies concurrently

• Process divided into

  • Critical section
  • Non-critical section

• Correctness properties

  • Mutual exclusion -> Instructions from critical sections must never be interleaved
    • Safety property -> Must always be true
  • No deadlock -> If some processes are trying to enter their critical sections then one of them must eventually succeed
    • Liveness property -> Progress property. System will continue executing.
  • No starvation -> If any process tries to enter its critical section, then one of them must eventually succeed
    • Nothing can stop a process from ever reaching its critical section

• Futher assumptions

  • Synchronisation mechanism consists of a pre and post-protocol (before and after) each critical section
  • Protocols can use variables not accessed by critical or non-critical section
  • Process may delay infinitely in non-critical sections
  • Processes do not delay infinitely in critical sections
  • Efficiency -> Pre and post-protocols require as little time and memory as possible in case of no contention

Atomic Load and Store

• Assumption 1 -> Every individual base memory cell (word) load and store access is atomic
• Assumption 2 -> There is no atomic combined load-store access, i.e. one or the other

Proving Correctness: State Diagrams

• Program state can be represented as a tuple

  • Program counters

  • Variable values stored

  • E.g. (p2, q3,1), where process p is at statement p2, process q is at statement q3 with turn value of 1

• State diagram consists of

  • States (Tuples)
  • Transitions
  • Starting state