Solution Evaluation: A Systematic… — Requirements for… | OneNoughtOne

0/105

Operating SystemsRequirements for Solutions

Requirements for Solutions to the Critical Section Problem

LevelIntermediate

Duration90 mins

TopicRequirements for Solutions

4 / 5

Solution Evaluation: A Systematic Framework

From Requirements to Analysis

We now possess deep knowledge of the three requirements for correct synchronization solutions: mutual exclusion, progress, and bounded waiting. But knowledge of requirements is incomplete without the ability to evaluate whether a given solution satisfies them. This page bridges theory and practice. We will develop a systematic framework for analyzing synchronization algorithms—a structured methodology that transforms informal reasoning into rigorous analysis. By the end, you will have a toolkit for evaluating any proposed solution to the critical section problem. This skill is essential because: Synchronization bugs are subtle and testing is insufficient Correct-looking algorithms can have hidden flaws New problems require designing solutions that provably work Code review of concurrent code demands analytical rigor Let us build the analytical framework step by step.

What You Will Learn

By the end of this page, you will be able to systematically evaluate any synchronization solution against all three requirements, construct adversarial execution traces to find flaws, use state-space analysis for exhaustive verification, and apply evaluation checklists to avoid common analytical mistakes.

The Evaluation Methodology

Evaluating a synchronization solution requires systematic analysis, not intuition. Here is a structured methodology: Step 1: Formalize the Algorithm Before analysis, ensure the algorithm is precisely specified: Identify shared variables : What state is shared among processes? Specify initial values : What is the starting configuration? Delineate sections : Where exactly are entry, critical, exit, and remainder sections? Define atomic operations : What operations are indivisible? Ambiguity in any of these leads to incorrect analysis.

algorithm_formalization.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
// Example: Formalizing a synchronization algorithm
 
// STEP 1: Identify shared variables
Shared:
  bool flag[2]  -- Process intention flags
  int turn      -- Turn indicator
 
// STEP 2: Specify initial values
Initial:
  flag[0] = false
  flag[1] = false
  turn = 0  (or 1, doesn't matter)
 
// STEP 3: Delineate sections (for process i, where j = 1-i)
 
ENTRY SECTION:
  E1: flag[i] = true
  E2: turn = j
  E3: while (flag[j] && turn == j) { }
 
CRITICAL SECTION:
  CS: <access shared resource>
 
EXIT SECTION:
  X1: flag[i] = false
 
REMAINDER SECTION:
  RS: <non-critical work>
 
// STEP 4: Define atomic operations
Atomic:
  - Reading a single shared variable
  - Writing a single shared variable
  - The read + compare in E3's while condition
    (or if not atomic, analyze as separate operations)
 
// NOTE: Assumptions about atomicity MUST be explicit.
// Different assumptions can lead to different conclusions!

Step 2: Check Mutual Exclusion Attempt to prove that no two processes can be in their critical sections simultaneously. Approach : Find an invariant that implies mutual exclusion and prove it holds. Common invariant patterns : in_cs[i] \to lock == true (lock-based) in_cs[i] \to some condition uniquely held by i (algorithm-specific) Step 3: Check Progress Verify that if the critical section is empty and processes want to enter, one will enter. Approach : Consider states where: No process is in CS At least one process is in entry section Show that from any such state, some process eventually enters CS. Step 4: Check Bounded Waiting Verify that a bound exists on how many times a waiting process can be bypassed. Approach : Track what happens after a process enters its entry section. Count maximum possible entries by others before this process enters. Step 5: Document Assumptions Explicitly state all assumptions: Atomicity of operations Memory model (sequential consistency, or weaker?) Process behavior (non-failing, finite CS execution) Scheduling (fair scheduler, or adversarial?)

The Order Matters

Always check mutual exclusion first. If mutual exclusion fails, the algorithm is fundamentally broken—there's no point analyzing progress or bounded waiting. Progress comes second; bounded waiting builds on progress.

Adversarial Execution Traces

A powerful technique for finding flaws is constructing adversarial execution traces —carefully designed interleavings that attempt to violate each requirement. The Adversarial Scheduler Mindset Imagine a scheduler determined to break your algorithm: It knows the algorithm's logic It can choose any valid interleaving It will exploit every opportunity for failure Your task is to predict what this malicious scheduler would do. Constructing Traces for Mutual Exclusion Violations To find a mutual exclusion violation: Start with both processes wanting to enter Interleave their entry sections to get both into CS Look for windows where neither process's check would block the other

mutual_exclusion_violation_trace.c
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
// Demonstrating a mutual exclusion violation via adversarial trace
 
// Flawed algorithm (no turn variable):
// Entry: flag[i] = true; while (flag[j]) { }
// Exit:  flag[i] = false
 
// ADVERSARIAL TRACE:
 
// Initial: flag[0] = false, flag[1] = false
 
// Time | P₀ Action           | P₁ Action           | flag[0] | flag[1]
// -----+---------------------+---------------------+---------+---------
//  t1  | (in remainder)      | flag[1] = true      | false   | true
//  t2  | flag[0] = true      | (about to check)    | true    | true
//  t3  | while(flag[1]): T   | while(flag[0]): T   | true    | true
//      | ... wait ...        | ... wait ...        |         |
//
// DEADLOCK! Neither can proceed. But wait, let's try a different trace:
 
// ALTERNATIVE ADVERSARIAL TRACE:
 
// Time | P₀ Action           | P₁ Action           | flag[0] | flag[1]
// -----+---------------------+---------------------+---------+---------
//  t1  | flag[0] = true      | (in remainder)      | true    | false
//  t2  | while(flag[1]): F   | (in remainder)      | true    | false
//  t3  | ENTER CS            | flag[1] = true      | true    | true
//  t4  | (in CS)             | while(flag[0]): T   | true    | true
//  t5  | (in CS)             | ... wait ...        | true    | true
 
// OK, this scenario shows deadlock OR one enters first.
// But can BOTH enter? Let's try:
 
// MUTUAL EXCLUSION VIOLATION TRACE:
 
// Time | P₀ Action           | P₁ Action           | flag[0] | flag[1]
// -----+---------------------+---------------------+---------+---------
//  t1  | flag[0] = true      |                     | true    | false
//  t2  |                     | flag[1] = true      | true    | true
//  t3  | while(flag[1]): T   | while(flag[0]): T   | true    | true
//
// Both wait. No violation yet. This algorithm actually has
// a PROGRESS problem (potential deadlock), not mutual exclusion.
 
// The algorithm IS deadlock-prone but DOES satisfy mutual exclusion
// (when progress exists, only one enters at a time).

Constructing Traces for Progress Violations To find a progress violation: Set up a state where CS is empty Have one or more processes waiting in entry section Show that no process ever enters

progress_violation_trace.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
// Finding a progress violation: Strict Alternation
 
// Algorithm:
// Entry: while (turn != i) { }
// Exit:  turn = j  (where j = 1-i)
 
// ADVERSARIAL TRACE FOR PROGRESS VIOLATION:
 
// Setup: turn = 0, P₀ is in remainder section (long computation)
 
// Time | P₀ Action           | P₁ Action           | turn
// -----+---------------------+---------------------+------
//  t1  | (in remainder)      | wants to enter      | 0
//  t2  | (in remainder)      | while(turn != 1): T | 0
//  t3  | (in remainder)      | wait...             | 0
//  t4  | (in remainder)      | wait...             | 0
//  ... | (stays in remainder)| wait FOREVER        | 0
 
// ANALYSIS:
// - CS is empty (turn = 0 means P₀ could enter, but P₀ isn't trying)
// - P₁ wants to enter (in entry section)
// - P₁ cannot enter (turn ≠ 1)
// - P₀ is in remainder section - not contending
 
// This violates the progress definition:
// "only processes NOT in remainder participate in decision"
// Here, P₀ in remainder section is blocking P₁'s entry.
 
// CONCLUSION: Progress is violated. Algorithm is incorrect.

Constructing Traces for Bounded Waiting Violations To find a bounded waiting violation: Have a process Pᵢ request entry Show other processes can enter unboundedly many times While Pᵢ never enters

Trace Construction is an Art

Constructing the right trace requires understanding the algorithm's weak points. Start by asking: 'What could go wrong?' For mutual exclusion, look for race conditions in the entry section. For progress, look for dependencies on non-contending processes. For bounded waiting, look for lack of ordering mechanisms.

State-Space Analysis

For exhaustive verification, we can enumerate all reachable states of a synchronization algorithm. This technique, called state-space analysis or model checking, guarantees finding any violations. Building the State Space A state captures all relevant information about the system: Values of all shared variables Each process's current program point (location) Any local variable values relevant to the algorithm A transition is an atomic step that moves from one state to another. Example: State Space for a Simple Algorithm

state_space_example.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
// State-space analysis of a 2-process algorithm
 
// Algorithm (each process i, j = 1-i):
// Entry: flag[i] = true; while (flag[j]) { }
// Exit:  flag[i] = false
 
// STATE REPRESENTATION:
// (loc₀, loc₁, flag[0], flag[1])
// where loc ∈ {RS, E1, E2, CS, X1} 
//   RS = remainder, E1 = set flag, E2 = check loop, CS = critical, X1 = clear flag
 
// INITIAL STATE: (RS, RS, false, false)
 
// STATE SPACE ENUMERATION:
 
// State 0: (RS, RS, F, F) - initial
//   P₀ moves to E1: → State 1
//   P₁ moves to E1: → State 2
 
// State 1: (E1, RS, F, F) - P₀ about to set flag
//   P₀ sets flag: → State 3 (E2, RS, T, F)
//   P₁ moves to E1: → State 4
 
// State 2: (RS, E1, F, F) - P₁ about to set flag
//   P₁ sets flag: → State 5 (RS, E2, F, T)
//   P₀ moves to E1: → State 4
 
// State 3: (E2, RS, T, F) - P₀ checking, P₁ in remainder
//   P₀ checks flag[1]=F, enters CS: → State 6 (CS, RS, T, F)
//   P₁ moves to E1: → State 7 (E2, E1, T, F)
 
// ... continuing enumeration ...
 
// State 8: (E2, E2, T, T) - BOTH checking, BOTH flags true
//   P₀ checks flag[1]=T, stays in E2: → State 8 (self-loop)
//   P₁ checks flag[0]=T, stays in E2: → State 8 (self-loop)
//   
//   PROBLEM: This is a DEADLOCK state! No progress possible.
//   Both processes spin forever, neither enters CS.
 
// VERIFICATION RESULTS:
// - Mutual exclusion: ✓ (no state has both in CS)
// - Progress: ✗ (State 8 is deadlocked)
// - Bounded waiting: N/A (no progress means bounded waiting undefined)

Properties Checked via State-Space Analysis Mutual Exclusion : Check that no reachable state has two processes in CS. Progress : Check that from any state where CS is empty and entry sections are occupied, there's a path to a state where someone is in CS. Bounded Waiting : Check that for any state where Pᵢ is waiting, there's a bound on transitions before Pᵢ enters CS. Limitations: State Explosion The number of states grows exponentially with: Number of processes Number of shared variables Size of variable domains For n processes, each with k locations and v shared variables each of size s : |States| = k^n \times s^v This limits exhaustive enumeration to small systems. Large systems require: Abstraction (reduce state space by grouping equivalent states) Symmetry reduction (exploit process symmetry) Partial order reduction (eliminate equivalent orderings) Symbolic model checking (represent states implicitly)

Model Checking Tools

Tools like SPIN, TLA+, and Promela automate state-space analysis. They're invaluable for verifying synchronization algorithms. For critical systems, formal verification with these tools is standard practice.

Evaluation Checklists

To ensure thorough evaluation, use these checklists when analyzing synchronization algorithms. Mutual Exclusion Checklist

Mutual Exclusion Verification

•Identify the gate condition: What prevents simultaneous entry?
•Check atomicity: Is the check-and-enter sequence atomic?
•Enumerate race scenarios: Try every interleaving of entry sections
•Verify invariant: State and prove an invariant implying mutual exclusion
•Consider all process counts: Does it work for 2 processes? n processes?

Progress Checklist

Progress Verification

•Remainder independence: Can a process in remainder block entry of contenders?
•Deadlock analysis: Can all contenders be simultaneously blocked?
•Livelock analysis: Can contenders spin forever without any entering?
•Entry decision: Who decides which contender enters next?
•Decision termination: Does the decision mechanism always complete?

Bounded Waiting Checklist

Bounded Waiting Verification

•Ordering mechanism: How is the entry order determined?
•Bypass count: Can a waiting process be bypassed unboundedly?
•Fairness guarantee: Does each process eventually get priority?
•Bound computation: What is the explicit bound B?
•Worst-case scenario: Construct a trace that maximizes wait

Common Pitfalls Checklist

Common Analysis Errors to Avoid
Pitfall	Description	How to Avoid
Atomicity assumption	Assuming multi-step operations are atomic	Explicitly list atomic operations
Benevolent scheduler	Assuming scheduler helps correctness	Use adversarial scheduler model
Small-scale reasoning	Verifying only 2 processes when n > 2	Test with maximum process count
Confirming intuition	Finding traces that work, not that fail	Try to break the algorithm
Memory model ignorance	Ignoring reordering on weak models	State memory model assumptions

Worked Example: A Complete Evaluation

Let's apply our evaluation framework to analyze a synchronization algorithm end-to-end. The Algorithm Under Analysis Consider this proposed 2-process solution:

algorithm_under_test.c
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
// Proposed solution for 2-process mutual exclusion
 
// Shared variables
bool flag[2] = {false, false};  // Interest flags
int turn = 0;                    // Priority indicator
 
// Process i (where j = 1 - i)
void process(int i) {
    int j = 1 - i;
    
    while (true) {
        // ENTRY SECTION
        flag[i] = true;           // Line E1: Declare interest
        while (flag[j]) {         // Line E2: While other interested
            if (turn == j) {      // Line E3: If it's their turn
                flag[i] = false;  // Line E4: Withdraw temporarily
                while (turn == j) { }  // Line E5: Wait for my turn
                flag[i] = true;   // Line E6: Re-declare interest
            }
        }
        
        // CRITICAL SECTION
        critical_section();
        
        // EXIT SECTION
        turn = j;                 // Line X1: Give turn to other
        flag[i] = false;          // Line X2: Clear interest
        
        // REMAINDER SECTION
        remainder_section();
    }
}

Step 1: Formalization Shared variables : flag[0], flag[1], turn Initial values : flag[0] = false, flag[1] = false, turn = 0 Atomic operations : Single reads and writes Process locations : RS, E1-E6, CS, X1, X2 Step 2: Evaluate Mutual Exclusion

mutual_exclusion_analysis.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
// MUTUAL EXCLUSION ANALYSIS
 
// Claim: No state has both processes in CS simultaneously.
 
// Proof approach: Show invariant I holds, and I → ¬(in_cs[0] ∧ in_cs[1])
 
// Key observation: To enter CS, process i must:
// 1. Set flag[i] = true
// 2. Find flag[j] = false (exit the while loop at E2)
 
// Invariant attempt:
// I: in_cs[i] → flag[i] = true
 
// If both in CS:
// - flag[0] = true (by invariant, since in_cs[0])
// - flag[1] = true (by invariant, since in_cs[1])
 
// But to enter CS, each must have seen the other's flag as false!
// 
// Case analysis:
// - P₀ saw flag[1] = false at E2, then entered CS
// - P₁ saw flag[0] = false at E2, then entered CS
// - But once in CS, both have flags true
// 
// For both to enter, one must have checked BEFORE the other set flag:
// Sequence: P₀ checks flag[1]=F → P₁ sets flag[1]=T → P₁ checks flag[0]
// But wait, P₀ set flag[0]=T at E1, so P₁ sees flag[0]=T and doesn't enter!
// 
// Actually, be careful about the deference mechanism (E3-E6).
// Let's trace more carefully...
 
// If P₀ clears flag at E4, then P₁ might see flag[0]=false...
// 
// Detailed trace attempt:
// P₀: E1 (flag[0]=T), E2 (flag[1]?), sees T, E3 (turn==1?), ...
// P₁: E1 (flag[1]=T), E2 (flag[0]?), sees T, E3 (turn==0?), ...
// 
// turn is either 0 or 1.
// If turn = 0: P₁ defers (E4: flag[1]=F, E5: wait), P₀ passes E2, enters CS
// If turn = 1: P₀ defers (E4: flag[0]=F, E5: wait), P₁ passes E2, enters CS
// 
// One process defers, allowing the other to enter.
// 
// CONCLUSION: Mutual exclusion holds ✓
 
// The turn variable acts as a tiebreaker when both have flags set.

Step 3: Evaluate Progress

progress_analysis.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
// PROGRESS ANALYSIS
 
// Question: If CS is empty and processes want to enter, can entry happen?
 
// Scenario 1: Only P₀ wants to enter (P₁ in remainder)
// - P₀ sets flag[0] = true
// - P₀ checks flag[1] = false (P₁ didn't set it while in remainder)
// - P₀ exits while loop, enters CS ✓
 
// Scenario 2: Both want to enter
// - Both set their flags true
// - Both fail the outer while condition initially (flag[j] = true)
// - Both check turn
// - Exactly one has turn == j (since turn is 0 or 1)
// - That one defers (clears flag, waits for turn change)
// - The other sees flag[j] = false, enters CS ✓
// - In CS, it eventually exits and sets turn = j
// - The deferred process's E5 waiting ends
// - It re-sets its flag, proceeds, enters CS ✓
 
// Scenario 3: Neither currently in entry, but...(remainder independence)
// - P₀ in remainder, P₁ wants to enter
// - P₁ sets flag[1] = true
// - P₁ checks flag[0] = false (P₀ in remainder, flag[0] = false)
// - P₁ enters CS ✓
// - P₀ being in remainder does NOT block P₁
 
// CONCLUSION: Progress holds ✓
 
// No deadlock: The turn variable breaks symmetry.
// No remainder dependency: Process in remainder has flag = false.

Step 4: Evaluate Bounded Waiting

bounded_waiting_analysis.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
// BOUNDED WAITING ANALYSIS
 
// Question: After P₀ requests entry, can P₁ enter unboundedly often?
 
// Trace analysis:
// 1. P₀ enters entry section (sets flag[0] = true) at time t₀
// 2. P₁ is potentially in CS or also entering
 
// Case A: P₁ in CS at time t₀
// - P₁ will exit, set turn = 0, set flag[1] = false
// - P₀ will see flag[1] = false (if checking E2) or turn = 0 (if in E5)
// - P₀ proceeds, enters CS
// - P₁ entered 1 time after t₀ (was already in CS)
// - Bound: 1 ✓
 
// Case B: P₁ also entering at time t₀
// - Both have flags true, turn is either 0 or 1
// - If turn = 1: P₀ defers, P₁ enters, P₁ exits, sets turn = 0
//   - Now P₀ stops waiting at E5, re-sets flag, checks E2
//   - P₁ might want to enter again and set flag[1] = true
//   - P₁ checks turn = 0, so if P₀'s flag is true, P₁ defers
//   - P₀ enters
//   - P₁ entered 1 time after t₀
// - If turn = 0: P₁ defers, P₀ enters
//   - P₁ entered 0 times before P₀
//   - Bound: 0 ✓
 
// Maximum bypass: 1 (when P₁ was already in CS or had priority)
 
// CONCLUSION: Bounded waiting holds with B = 1 ✓
 
// The turn variable ensures the waiting process gets priority
// after the other process exits.

Evaluation Complete

This algorithm (Dekker's algorithm variant) satisfies all three requirements: Mutual Exclusion ✓, Progress ✓, Bounded Waiting with B=1 ✓. It is a correct solution to the 2-process critical section problem.

Comparative Evaluation of Algorithms

Let's apply our evaluation framework to compare several synchronization approaches: Summary Comparison Table

Comparative Evaluation of Synchronization Algorithms
Algorithm	Mutual Excl.	Progress	Bounded Wait	Bound B	Notes
Disable interrupts	✓	✓*	✓*	0	*Only on uniprocessor; dangerous
Strict alternation	✓	✗	N/A	N/A	Requires alternating access
Flag without turn	✓	✗	N/A	N/A	Can deadlock
Peterson's (2-proc)	✓	✓	✓	1	Classic correct solution
Dekker's (2-proc)	✓	✓	✓	1	First correct algorithm
Lamport's Bakery	✓	✓	✓	n-1	Works for n processes
TAS spinlock	✓	✓	✗	∞	Simple but unfair
Ticket lock	✓	✓	✓	n-1	Fair and practical
MCS lock	✓	✓	✓	n-1	Scalable queue-based

Key Observations 1. Correctness is binary, not gradual An algorithm is correct (all three properties) or incorrect (missing any). There's no 'partially correct.' 2. Simplicity and correctness can conflict The simplest approaches (strict alternation, basic flags) are often incorrect. Correct algorithms require more sophisticated mechanisms. 3. Practical considerations matter An algorithm might be theoretically correct but impractical (e.g., Lamport's Bakery has unbounded ticket numbers). Real implementations need bounded resources. 4. Context determines choice Different contexts favor different algorithms: Real-time systems: Need bounded waiting High-throughput systems: May accept unfair locks Distributed systems: Need fault-tolerant algorithms

Algorithm Selection Guidelines

•For 2 processes: Peterson's or Dekker's (simple, provably correct)
•For n processes, software-only: Lamport's Bakery (but watch unbounded tickets)
•For practical systems: Use OS-provided locks (mutexes)
•For kernel code: Spinlocks with care (short critical sections)
•For high contention: Queue-based locks (MCS, CLH) for fairness and scalability

Automated Verification Tools

Manual evaluation is essential for understanding, but automated tools extend our verification capabilities. Model Checkers Model checkers automatically explore the state space and check properties: SPIN (Simple Promela Interpreter) Uses Promela modeling language Checks safety and liveness properties Widely used for protocol verification TLA+ (Temporal Logic of Actions) High-level specification language Explicit-state model checker (TLC) Developed by Leslie Lamport Alloy Relational modeling language SAT-based analysis Good for structural properties

spin_example.pml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
/* SPIN/Promela model of Peterson's algorithm */
 
bool flag[2] = false;
byte turn = 0;
 
/* Process template */
proctype P(byte i) {
    byte j = 1 - i;
    
    do ::
        /* Entry section */
        flag[i] = true;
        turn = j;
        (flag[j] == false || turn == i);  /* Wait */
        
        /* Critical section */
cs:     skip;  /* Label for property checking */
        
        /* Exit section */
        flag[i] = false;
    od
}
 
/* Mutual exclusion property */
ltl mutex { []!(P[0]@cs && P[1]@cs) }
 
/* Progress property */
ltl progress { [](flag[0] -> <>P[0]@cs) && [](flag[1] -> <>P[1]@cs) }
 
/* Start both processes */
init {
    run P(0);
    run P(1);
}
 
/* 
To verify:
  spin -a peterson.pml
  gcc -o pan pan.c
  ./pan -a
*/

Static Analysis Tools Static analyzers check code without running it: ThreadSanitizer (TSan) : Detects data races at runtime (via instrumentation) Helgrind : Valgrind-based race detector RacerD : Facebook's static race detector for Java/C++ Infer : Static analyzer that can find concurrency bugs Limitations of Automated Tools While powerful, tools have limitations: State explosion : Real systems may have too many states Abstraction required : Must model the system, may miss details False positives/negatives : Tools may report spurious errors or miss real bugs Memory model complexity : Most tools assume sequential consistency

Combine Manual and Automated Analysis

The best approach combines manual reasoning (for understanding and proof development) with automated tools (for exhaustive checking and catching oversights). Use manual analysis to develop invariants and intuition, then encode in a model checker for verification.

Operating SystemsRequirements for Solutions

Requirements for Solutions to the Critical Section Problem

LevelIntermediate

Duration90 mins

TopicRequirements for Solutions

4 / 5

Solution Evaluation: A Systematic Framework

From Requirements to Analysis

We now possess deep knowledge of the three requirements for correct synchronization solutions: mutual exclusion, progress, and bounded waiting. But knowledge of requirements is incomplete without the ability to evaluate whether a given solution satisfies them. This page bridges theory and practice. We will develop a systematic framework for analyzing synchronization algorithms—a structured methodology that transforms informal reasoning into rigorous analysis. By the end, you will have a toolkit for evaluating any proposed solution to the critical section problem. This skill is essential because: Synchronization bugs are subtle and testing is insufficient Correct-looking algorithms can have hidden flaws New problems require designing solutions that provably work Code review of concurrent code demands analytical rigor Let us build the analytical framework step by step.

What You Will Learn

By the end of this page, you will be able to systematically evaluate any synchronization solution against all three requirements, construct adversarial execution traces to find flaws, use state-space analysis for exhaustive verification, and apply evaluation checklists to avoid common analytical mistakes.

The Evaluation Methodology

Evaluating a synchronization solution requires systematic analysis, not intuition. Here is a structured methodology: Step 1: Formalize the Algorithm Before analysis, ensure the algorithm is precisely specified: Identify shared variables : What state is shared among processes? Specify initial values : What is the starting configuration? Delineate sections : Where exactly are entry, critical, exit, and remainder sections? Define atomic operations : What operations are indivisible? Ambiguity in any of these leads to incorrect analysis.

algorithm_formalization.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
// Example: Formalizing a synchronization algorithm
 
// STEP 1: Identify shared variables
Shared:
  bool flag[2]  -- Process intention flags
  int turn      -- Turn indicator
 
// STEP 2: Specify initial values
Initial:
  flag[0] = false
  flag[1] = false
  turn = 0  (or 1, doesn't matter)
 
// STEP 3: Delineate sections (for process i, where j = 1-i)
 
ENTRY SECTION:
  E1: flag[i] = true
  E2: turn = j
  E3: while (flag[j] && turn == j) { }
 
CRITICAL SECTION:
  CS: <access shared resource>
 
EXIT SECTION:
  X1: flag[i] = false
 
REMAINDER SECTION:
  RS: <non-critical work>
 
// STEP 4: Define atomic operations
Atomic:
  - Reading a single shared variable
  - Writing a single shared variable
  - The read + compare in E3's while condition
    (or if not atomic, analyze as separate operations)
 
// NOTE: Assumptions about atomicity MUST be explicit.
// Different assumptions can lead to different conclusions!

Step 2: Check Mutual Exclusion Attempt to prove that no two processes can be in their critical sections simultaneously. Approach : Find an invariant that implies mutual exclusion and prove it holds. Common invariant patterns : in_cs[i] \to lock == true (lock-based) in_cs[i] \to some condition uniquely held by i (algorithm-specific) Step 3: Check Progress Verify that if the critical section is empty and processes want to enter, one will enter. Approach : Consider states where: No process is in CS At least one process is in entry section Show that from any such state, some process eventually enters CS. Step 4: Check Bounded Waiting Verify that a bound exists on how many times a waiting process can be bypassed. Approach : Track what happens after a process enters its entry section. Count maximum possible entries by others before this process enters. Step 5: Document Assumptions Explicitly state all assumptions: Atomicity of operations Memory model (sequential consistency, or weaker?) Process behavior (non-failing, finite CS execution) Scheduling (fair scheduler, or adversarial?)

The Order Matters

Always check mutual exclusion first. If mutual exclusion fails, the algorithm is fundamentally broken—there's no point analyzing progress or bounded waiting. Progress comes second; bounded waiting builds on progress.

Adversarial Execution Traces

A powerful technique for finding flaws is constructing adversarial execution traces —carefully designed interleavings that attempt to violate each requirement. The Adversarial Scheduler Mindset Imagine a scheduler determined to break your algorithm: It knows the algorithm's logic It can choose any valid interleaving It will exploit every opportunity for failure Your task is to predict what this malicious scheduler would do. Constructing Traces for Mutual Exclusion Violations To find a mutual exclusion violation: Start with both processes wanting to enter Interleave their entry sections to get both into CS Look for windows where neither process's check would block the other

mutual_exclusion_violation_trace.c
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
// Demonstrating a mutual exclusion violation via adversarial trace
 
// Flawed algorithm (no turn variable):
// Entry: flag[i] = true; while (flag[j]) { }
// Exit:  flag[i] = false
 
// ADVERSARIAL TRACE:
 
// Initial: flag[0] = false, flag[1] = false
 
// Time | P₀ Action           | P₁ Action           | flag[0] | flag[1]
// -----+---------------------+---------------------+---------+---------
//  t1  | (in remainder)      | flag[1] = true      | false   | true
//  t2  | flag[0] = true      | (about to check)    | true    | true
//  t3  | while(flag[1]): T   | while(flag[0]): T   | true    | true
//      | ... wait ...        | ... wait ...        |         |
//
// DEADLOCK! Neither can proceed. But wait, let's try a different trace:
 
// ALTERNATIVE ADVERSARIAL TRACE:
 
// Time | P₀ Action           | P₁ Action           | flag[0] | flag[1]
// -----+---------------------+---------------------+---------+---------
//  t1  | flag[0] = true      | (in remainder)      | true    | false
//  t2  | while(flag[1]): F   | (in remainder)      | true    | false
//  t3  | ENTER CS            | flag[1] = true      | true    | true
//  t4  | (in CS)             | while(flag[0]): T   | true    | true
//  t5  | (in CS)             | ... wait ...        | true    | true
 
// OK, this scenario shows deadlock OR one enters first.
// But can BOTH enter? Let's try:
 
// MUTUAL EXCLUSION VIOLATION TRACE:
 
// Time | P₀ Action           | P₁ Action           | flag[0] | flag[1]
// -----+---------------------+---------------------+---------+---------
//  t1  | flag[0] = true      |                     | true    | false
//  t2  |                     | flag[1] = true      | true    | true
//  t3  | while(flag[1]): T   | while(flag[0]): T   | true    | true
//
// Both wait. No violation yet. This algorithm actually has
// a PROGRESS problem (potential deadlock), not mutual exclusion.
 
// The algorithm IS deadlock-prone but DOES satisfy mutual exclusion
// (when progress exists, only one enters at a time).

Constructing Traces for Progress Violations To find a progress violation: Set up a state where CS is empty Have one or more processes waiting in entry section Show that no process ever enters

progress_violation_trace.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
// Finding a progress violation: Strict Alternation
 
// Algorithm:
// Entry: while (turn != i) { }
// Exit:  turn = j  (where j = 1-i)
 
// ADVERSARIAL TRACE FOR PROGRESS VIOLATION:
 
// Setup: turn = 0, P₀ is in remainder section (long computation)
 
// Time | P₀ Action           | P₁ Action           | turn
// -----+---------------------+---------------------+------
//  t1  | (in remainder)      | wants to enter      | 0
//  t2  | (in remainder)      | while(turn != 1): T | 0
//  t3  | (in remainder)      | wait...             | 0
//  t4  | (in remainder)      | wait...             | 0
//  ... | (stays in remainder)| wait FOREVER        | 0
 
// ANALYSIS:
// - CS is empty (turn = 0 means P₀ could enter, but P₀ isn't trying)
// - P₁ wants to enter (in entry section)
// - P₁ cannot enter (turn ≠ 1)
// - P₀ is in remainder section - not contending
 
// This violates the progress definition:
// "only processes NOT in remainder participate in decision"
// Here, P₀ in remainder section is blocking P₁'s entry.
 
// CONCLUSION: Progress is violated. Algorithm is incorrect.

Constructing Traces for Bounded Waiting Violations To find a bounded waiting violation: Have a process Pᵢ request entry Show other processes can enter unboundedly many times While Pᵢ never enters

Trace Construction is an Art

Constructing the right trace requires understanding the algorithm's weak points. Start by asking: 'What could go wrong?' For mutual exclusion, look for race conditions in the entry section. For progress, look for dependencies on non-contending processes. For bounded waiting, look for lack of ordering mechanisms.

State-Space Analysis

For exhaustive verification, we can enumerate all reachable states of a synchronization algorithm. This technique, called state-space analysis or model checking, guarantees finding any violations. Building the State Space A state captures all relevant information about the system: Values of all shared variables Each process's current program point (location) Any local variable values relevant to the algorithm A transition is an atomic step that moves from one state to another. Example: State Space for a Simple Algorithm

state_space_example.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
// State-space analysis of a 2-process algorithm
 
// Algorithm (each process i, j = 1-i):
// Entry: flag[i] = true; while (flag[j]) { }
// Exit:  flag[i] = false
 
// STATE REPRESENTATION:
// (loc₀, loc₁, flag[0], flag[1])
// where loc ∈ {RS, E1, E2, CS, X1} 
//   RS = remainder, E1 = set flag, E2 = check loop, CS = critical, X1 = clear flag
 
// INITIAL STATE: (RS, RS, false, false)
 
// STATE SPACE ENUMERATION:
 
// State 0: (RS, RS, F, F) - initial
//   P₀ moves to E1: → State 1
//   P₁ moves to E1: → State 2
 
// State 1: (E1, RS, F, F) - P₀ about to set flag
//   P₀ sets flag: → State 3 (E2, RS, T, F)
//   P₁ moves to E1: → State 4
 
// State 2: (RS, E1, F, F) - P₁ about to set flag
//   P₁ sets flag: → State 5 (RS, E2, F, T)
//   P₀ moves to E1: → State 4
 
// State 3: (E2, RS, T, F) - P₀ checking, P₁ in remainder
//   P₀ checks flag[1]=F, enters CS: → State 6 (CS, RS, T, F)
//   P₁ moves to E1: → State 7 (E2, E1, T, F)
 
// ... continuing enumeration ...
 
// State 8: (E2, E2, T, T) - BOTH checking, BOTH flags true
//   P₀ checks flag[1]=T, stays in E2: → State 8 (self-loop)
//   P₁ checks flag[0]=T, stays in E2: → State 8 (self-loop)
//   
//   PROBLEM: This is a DEADLOCK state! No progress possible.
//   Both processes spin forever, neither enters CS.
 
// VERIFICATION RESULTS:
// - Mutual exclusion: ✓ (no state has both in CS)
// - Progress: ✗ (State 8 is deadlocked)
// - Bounded waiting: N/A (no progress means bounded waiting undefined)

Properties Checked via State-Space Analysis Mutual Exclusion : Check that no reachable state has two processes in CS. Progress : Check that from any state where CS is empty and entry sections are occupied, there's a path to a state where someone is in CS. Bounded Waiting : Check that for any state where Pᵢ is waiting, there's a bound on transitions before Pᵢ enters CS. Limitations: State Explosion The number of states grows exponentially with: Number of processes Number of shared variables Size of variable domains For n processes, each with k locations and v shared variables each of size s : |States| = k^n \times s^v This limits exhaustive enumeration to small systems. Large systems require: Abstraction (reduce state space by grouping equivalent states) Symmetry reduction (exploit process symmetry) Partial order reduction (eliminate equivalent orderings) Symbolic model checking (represent states implicitly)

Model Checking Tools

Tools like SPIN, TLA+, and Promela automate state-space analysis. They're invaluable for verifying synchronization algorithms. For critical systems, formal verification with these tools is standard practice.

Evaluation Checklists

To ensure thorough evaluation, use these checklists when analyzing synchronization algorithms. Mutual Exclusion Checklist

Mutual Exclusion Verification

•Identify the gate condition: What prevents simultaneous entry?
•Check atomicity: Is the check-and-enter sequence atomic?
•Enumerate race scenarios: Try every interleaving of entry sections
•Verify invariant: State and prove an invariant implying mutual exclusion
•Consider all process counts: Does it work for 2 processes? n processes?

Progress Checklist

Progress Verification

•Remainder independence: Can a process in remainder block entry of contenders?
•Deadlock analysis: Can all contenders be simultaneously blocked?
•Livelock analysis: Can contenders spin forever without any entering?
•Entry decision: Who decides which contender enters next?
•Decision termination: Does the decision mechanism always complete?

Bounded Waiting Checklist

Bounded Waiting Verification

•Ordering mechanism: How is the entry order determined?
•Bypass count: Can a waiting process be bypassed unboundedly?
•Fairness guarantee: Does each process eventually get priority?
•Bound computation: What is the explicit bound B?
•Worst-case scenario: Construct a trace that maximizes wait

Common Pitfalls Checklist

Common Analysis Errors to Avoid
Pitfall	Description	How to Avoid
Atomicity assumption	Assuming multi-step operations are atomic	Explicitly list atomic operations
Benevolent scheduler	Assuming scheduler helps correctness	Use adversarial scheduler model
Small-scale reasoning	Verifying only 2 processes when n > 2	Test with maximum process count
Confirming intuition	Finding traces that work, not that fail	Try to break the algorithm
Memory model ignorance	Ignoring reordering on weak models	State memory model assumptions

Worked Example: A Complete Evaluation

Let's apply our evaluation framework to analyze a synchronization algorithm end-to-end. The Algorithm Under Analysis Consider this proposed 2-process solution:

algorithm_under_test.c
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
// Proposed solution for 2-process mutual exclusion
 
// Shared variables
bool flag[2] = {false, false};  // Interest flags
int turn = 0;                    // Priority indicator
 
// Process i (where j = 1 - i)
void process(int i) {
    int j = 1 - i;
    
    while (true) {
        // ENTRY SECTION
        flag[i] = true;           // Line E1: Declare interest
        while (flag[j]) {         // Line E2: While other interested
            if (turn == j) {      // Line E3: If it's their turn
                flag[i] = false;  // Line E4: Withdraw temporarily
                while (turn == j) { }  // Line E5: Wait for my turn
                flag[i] = true;   // Line E6: Re-declare interest
            }
        }
        
        // CRITICAL SECTION
        critical_section();
        
        // EXIT SECTION
        turn = j;                 // Line X1: Give turn to other
        flag[i] = false;          // Line X2: Clear interest
        
        // REMAINDER SECTION
        remainder_section();
    }
}

Step 1: Formalization Shared variables : flag[0], flag[1], turn Initial values : flag[0] = false, flag[1] = false, turn = 0 Atomic operations : Single reads and writes Process locations : RS, E1-E6, CS, X1, X2 Step 2: Evaluate Mutual Exclusion

mutual_exclusion_analysis.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
// MUTUAL EXCLUSION ANALYSIS
 
// Claim: No state has both processes in CS simultaneously.
 
// Proof approach: Show invariant I holds, and I → ¬(in_cs[0] ∧ in_cs[1])
 
// Key observation: To enter CS, process i must:
// 1. Set flag[i] = true
// 2. Find flag[j] = false (exit the while loop at E2)
 
// Invariant attempt:
// I: in_cs[i] → flag[i] = true
 
// If both in CS:
// - flag[0] = true (by invariant, since in_cs[0])
// - flag[1] = true (by invariant, since in_cs[1])
 
// But to enter CS, each must have seen the other's flag as false!
// 
// Case analysis:
// - P₀ saw flag[1] = false at E2, then entered CS
// - P₁ saw flag[0] = false at E2, then entered CS
// - But once in CS, both have flags true
// 
// For both to enter, one must have checked BEFORE the other set flag:
// Sequence: P₀ checks flag[1]=F → P₁ sets flag[1]=T → P₁ checks flag[0]
// But wait, P₀ set flag[0]=T at E1, so P₁ sees flag[0]=T and doesn't enter!
// 
// Actually, be careful about the deference mechanism (E3-E6).
// Let's trace more carefully...
 
// If P₀ clears flag at E4, then P₁ might see flag[0]=false...
// 
// Detailed trace attempt:
// P₀: E1 (flag[0]=T), E2 (flag[1]?), sees T, E3 (turn==1?), ...
// P₁: E1 (flag[1]=T), E2 (flag[0]?), sees T, E3 (turn==0?), ...
// 
// turn is either 0 or 1.
// If turn = 0: P₁ defers (E4: flag[1]=F, E5: wait), P₀ passes E2, enters CS
// If turn = 1: P₀ defers (E4: flag[0]=F, E5: wait), P₁ passes E2, enters CS
// 
// One process defers, allowing the other to enter.
// 
// CONCLUSION: Mutual exclusion holds ✓
 
// The turn variable acts as a tiebreaker when both have flags set.

Step 3: Evaluate Progress

progress_analysis.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
// PROGRESS ANALYSIS
 
// Question: If CS is empty and processes want to enter, can entry happen?
 
// Scenario 1: Only P₀ wants to enter (P₁ in remainder)
// - P₀ sets flag[0] = true
// - P₀ checks flag[1] = false (P₁ didn't set it while in remainder)
// - P₀ exits while loop, enters CS ✓
 
// Scenario 2: Both want to enter
// - Both set their flags true
// - Both fail the outer while condition initially (flag[j] = true)
// - Both check turn
// - Exactly one has turn == j (since turn is 0 or 1)
// - That one defers (clears flag, waits for turn change)
// - The other sees flag[j] = false, enters CS ✓
// - In CS, it eventually exits and sets turn = j
// - The deferred process's E5 waiting ends
// - It re-sets its flag, proceeds, enters CS ✓
 
// Scenario 3: Neither currently in entry, but...(remainder independence)
// - P₀ in remainder, P₁ wants to enter
// - P₁ sets flag[1] = true
// - P₁ checks flag[0] = false (P₀ in remainder, flag[0] = false)
// - P₁ enters CS ✓
// - P₀ being in remainder does NOT block P₁
 
// CONCLUSION: Progress holds ✓
 
// No deadlock: The turn variable breaks symmetry.
// No remainder dependency: Process in remainder has flag = false.

Step 4: Evaluate Bounded Waiting

bounded_waiting_analysis.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
// BOUNDED WAITING ANALYSIS
 
// Question: After P₀ requests entry, can P₁ enter unboundedly often?
 
// Trace analysis:
// 1. P₀ enters entry section (sets flag[0] = true) at time t₀
// 2. P₁ is potentially in CS or also entering
 
// Case A: P₁ in CS at time t₀
// - P₁ will exit, set turn = 0, set flag[1] = false
// - P₀ will see flag[1] = false (if checking E2) or turn = 0 (if in E5)
// - P₀ proceeds, enters CS
// - P₁ entered 1 time after t₀ (was already in CS)
// - Bound: 1 ✓
 
// Case B: P₁ also entering at time t₀
// - Both have flags true, turn is either 0 or 1
// - If turn = 1: P₀ defers, P₁ enters, P₁ exits, sets turn = 0
//   - Now P₀ stops waiting at E5, re-sets flag, checks E2
//   - P₁ might want to enter again and set flag[1] = true
//   - P₁ checks turn = 0, so if P₀'s flag is true, P₁ defers
//   - P₀ enters
//   - P₁ entered 1 time after t₀
// - If turn = 0: P₁ defers, P₀ enters
//   - P₁ entered 0 times before P₀
//   - Bound: 0 ✓
 
// Maximum bypass: 1 (when P₁ was already in CS or had priority)
 
// CONCLUSION: Bounded waiting holds with B = 1 ✓
 
// The turn variable ensures the waiting process gets priority
// after the other process exits.

Evaluation Complete

This algorithm (Dekker's algorithm variant) satisfies all three requirements: Mutual Exclusion ✓, Progress ✓, Bounded Waiting with B=1 ✓. It is a correct solution to the 2-process critical section problem.

Comparative Evaluation of Algorithms

Let's apply our evaluation framework to compare several synchronization approaches: Summary Comparison Table

Comparative Evaluation of Synchronization Algorithms
Algorithm	Mutual Excl.	Progress	Bounded Wait	Bound B	Notes
Disable interrupts	✓	✓*	✓*	0	*Only on uniprocessor; dangerous
Strict alternation	✓	✗	N/A	N/A	Requires alternating access
Flag without turn	✓	✗	N/A	N/A	Can deadlock
Peterson's (2-proc)	✓	✓	✓	1	Classic correct solution
Dekker's (2-proc)	✓	✓	✓	1	First correct algorithm
Lamport's Bakery	✓	✓	✓	n-1	Works for n processes
TAS spinlock	✓	✓	✗	∞	Simple but unfair
Ticket lock	✓	✓	✓	n-1	Fair and practical
MCS lock	✓	✓	✓	n-1	Scalable queue-based

Key Observations 1. Correctness is binary, not gradual An algorithm is correct (all three properties) or incorrect (missing any). There's no 'partially correct.' 2. Simplicity and correctness can conflict The simplest approaches (strict alternation, basic flags) are often incorrect. Correct algorithms require more sophisticated mechanisms. 3. Practical considerations matter An algorithm might be theoretically correct but impractical (e.g., Lamport's Bakery has unbounded ticket numbers). Real implementations need bounded resources. 4. Context determines choice Different contexts favor different algorithms: Real-time systems: Need bounded waiting High-throughput systems: May accept unfair locks Distributed systems: Need fault-tolerant algorithms

Algorithm Selection Guidelines

•For 2 processes: Peterson's or Dekker's (simple, provably correct)
•For n processes, software-only: Lamport's Bakery (but watch unbounded tickets)
•For practical systems: Use OS-provided locks (mutexes)
•For kernel code: Spinlocks with care (short critical sections)
•For high contention: Queue-based locks (MCS, CLH) for fairness and scalability

Automated Verification Tools

Manual evaluation is essential for understanding, but automated tools extend our verification capabilities. Model Checkers Model checkers automatically explore the state space and check properties: SPIN (Simple Promela Interpreter) Uses Promela modeling language Checks safety and liveness properties Widely used for protocol verification TLA+ (Temporal Logic of Actions) High-level specification language Explicit-state model checker (TLC) Developed by Leslie Lamport Alloy Relational modeling language SAT-based analysis Good for structural properties

spin_example.pml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
/* SPIN/Promela model of Peterson's algorithm */
 
bool flag[2] = false;
byte turn = 0;
 
/* Process template */
proctype P(byte i) {
    byte j = 1 - i;
    
    do ::
        /* Entry section */
        flag[i] = true;
        turn = j;
        (flag[j] == false || turn == i);  /* Wait */
        
        /* Critical section */
cs:     skip;  /* Label for property checking */
        
        /* Exit section */
        flag[i] = false;
    od
}
 
/* Mutual exclusion property */
ltl mutex { []!(P[0]@cs && P[1]@cs) }
 
/* Progress property */
ltl progress { [](flag[0] -> <>P[0]@cs) && [](flag[1] -> <>P[1]@cs) }
 
/* Start both processes */
init {
    run P(0);
    run P(1);
}
 
/* 
To verify:
  spin -a peterson.pml
  gcc -o pan pan.c
  ./pan -a
*/

Static Analysis Tools Static analyzers check code without running it: ThreadSanitizer (TSan) : Detects data races at runtime (via instrumentation) Helgrind : Valgrind-based race detector RacerD : Facebook's static race detector for Java/C++ Infer : Static analyzer that can find concurrency bugs Limitations of Automated Tools While powerful, tools have limitations: State explosion : Real systems may have too many states Abstraction required : Must model the system, may miss details False positives/negatives : Tools may report spurious errors or miss real bugs Memory model complexity : Most tools assume sequential consistency

Combine Manual and Automated Analysis

The best approach combines manual reasoning (for understanding and proof development) with automated tools (for exhaustive checking and catching oversights). Use manual analysis to develop invariants and intuition, then encode in a model checker for verification.

Solution Evaluation: A Systematic Framework

From Requirements to Analysis

The Evaluation Methodology

Step 1: Formalize the Algorithm

Step 2: Check Mutual Exclusion

Step 3: Check Progress

Step 4: Check Bounded Waiting

Step 5: Document Assumptions

Adversarial Execution Traces

The Adversarial Scheduler Mindset

Constructing Traces for Mutual Exclusion Violations

Constructing Traces for Progress Violations

Constructing Traces for Bounded Waiting Violations

State-Space Analysis

Building the State Space

Example: State Space for a Simple Algorithm

Properties Checked via State-Space Analysis

Limitations: State Explosion

Evaluation Checklists

Mutual Exclusion Checklist

Progress Checklist

Bounded Waiting Checklist

Common Pitfalls Checklist

Worked Example: A Complete Evaluation

The Algorithm Under Analysis

Step 1: Formalization

Step 2: Evaluate Mutual Exclusion

Step 3: Evaluate Progress

Step 4: Evaluate Bounded Waiting

Comparative Evaluation of Algorithms

Summary Comparison Table

Key Observations

Automated Verification Tools

Model Checkers

Static Analysis Tools

Limitations of Automated Tools

There’s more to understand.

Solution Evaluation: A Systematic Framework

From Requirements to Analysis

The Evaluation Methodology

Step 1: Formalize the Algorithm

Step 2: Check Mutual Exclusion

Step 3: Check Progress

Step 4: Check Bounded Waiting

Step 5: Document Assumptions

Adversarial Execution Traces

The Adversarial Scheduler Mindset

Constructing Traces for Mutual Exclusion Violations

Constructing Traces for Progress Violations

Constructing Traces for Bounded Waiting Violations

State-Space Analysis

Building the State Space

Example: State Space for a Simple Algorithm

Properties Checked via State-Space Analysis

Limitations: State Explosion

Evaluation Checklists

Mutual Exclusion Checklist

Progress Checklist

Bounded Waiting Checklist

Common Pitfalls Checklist

Worked Example: A Complete Evaluation

The Algorithm Under Analysis

Step 1: Formalization

Step 2: Evaluate Mutual Exclusion

Step 3: Evaluate Progress

Step 4: Evaluate Bounded Waiting

Comparative Evaluation of Algorithms

Summary Comparison Table

Key Observations

Automated Verification Tools

Model Checkers

Static Analysis Tools

Limitations of Automated Tools

There’s more to understand.