Other Classic Synchronization Problems

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

## Example: Sleeping Barber - Actor-Resource Decomposition
 
### Actors:
1. Barber (1 instance, service provider)
2. Customers (N instances, service consumers)
 
### Resources:
1. Barber chair (exclusive, 1 instance)
2. Waiting chairs (shared, N instances)
3. Barber's attention (exclusive, 1 instance)
 
### Access Patterns:
- Customer accesses: waiting chairs (claim/release), barber chair (claim/release)
- Barber accesses: barber chair (service), waiting chairs (check count)
 
### Symmetry:
- Customers are symmetric (all behave identically)
- Barber is asymmetric (different role from customers)
 
### Insight from Analysis:
This structure suggests producer-consumer (customers produce work, 
barber consumes) with bounded waiting capacity and asymmetric roles.

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
47

/*
 * Example: Formal Property Specification for Bounded Buffer
 * 
 * These properties guide design and verification.
 */
 
/*
 * SAFETY PROPERTIES
 * ==================
 * 
 * S1: 0 <= count <= BUFFER_SIZE (capacity invariant)
 *     At all times, buffer contents are within bounds.
 * 
 * S2: No concurrent modifications to the same slot
 *     Each buffer slot is accessed by at most one thread at any instant.
 * 
 * S3: Items are consumed in order of production within same producer
 *     (But total order may interleave across producers)
 */
 
// Can express in code as assertions:
void buffer_invariant_check(Buffer* b) {
    assert(b->count >= 0);
    assert(b->count <= BUFFER_SIZE);
    assert(b->head >= 0 && b->head < BUFFER_SIZE);
    assert(b->tail >= 0 && b->tail < BUFFER_SIZE);
}
 
/*
 * LIVENESS PROPERTIES
 * ====================
 * 
 * L1: Deadlock-free - The system always makes progress
 * L2: If a producer calls produce(), it eventually returns
 * L3: If a consumer calls consume(), it eventually returns
 *     (Assuming finite pauses between operations)
 * 
 * FAIRNESS PROPERTIES
 * ===================
 * 
 * F1: Bounded waiting - No producer/consumer waits indefinitely
 *     while others make progress
 * F2: Strong fairness - If a producer/consumer is continuously
 *     waiting, it is eventually served
 */
 
// Liveness is harder to test; often proven by argument or model checking

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
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77

/*
 * Example: Assembling a Readers-Writers Solution
 * 
 * Constraints identified:
 * - C1: Multiple readers can read simultaneously
 * - C2: Writers need exclusive access (no readers or other writers)
 * - C3: Writers should not starve (fairness)
 * 
 * Patterns matched:
 * - Lightswitch for readers (first locks, last unlocks)
 * - Mutex for writer exclusion
 * - Turnstile for writer priority
 */
 
/* Step 1: Define shared state */
int readers = 0;           // Count of active readers
 
/* Step 2: Define synchronization variables */
pthread_mutex_t mutex;     // Protects readers count
sem_t room_empty;          // 1 when no readers/writers, 0 otherwise
sem_t turnstile;           // Writer priority mechanism
 
/* Step 3: Initialize */
void init() {
    pthread_mutex_init(&mutex, NULL);
    sem_init(&room_empty, 0, 1);   // Room starts empty
    sem_init(&turnstile, 0, 1);    // Turnstile open
}
 
/* Step 4: Reader code using Lightswitch pattern */
void reader() {
    // Turnstile: let waiting writers through first
    sem_wait(&turnstile);
    sem_post(&turnstile);
    
    // Lightswitch: first reader locks out writers
    pthread_mutex_lock(&mutex);
    readers++;
    if (readers == 1) {
        sem_wait(&room_empty);  // First reader locks room
    }
    pthread_mutex_unlock(&mutex);
    
    // READ (critical section)
    read_data();
    
    // Lightswitch: last reader allows writers
    pthread_mutex_lock(&mutex);
    readers--;
    if (readers == 0) {
        sem_post(&room_empty);  // Last reader unlocks room
    }
    pthread_mutex_unlock(&mutex);
}
 
/* Step 5: Writer code */
void writer() {
    // Lock turnstile to block new readers
    sem_wait(&turnstile);
    
    // Wait for room to be empty
    sem_wait(&room_empty);
    
    // WRITE (critical section)
    write_data();
    
    // Release room and turnstile
    sem_post(&room_empty);
    sem_post(&turnstile);
}
 
/* 
 * Invariants:
 * - room_empty == 1 iff (readers == 0 AND no writer active)
 * - readers >= 0 always
 * - At most one writer holds room_empty at any time
 */

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: Proving Bounded Buffer Correctness via Invariants
 */
 
/*
 * INVARIANT I1: 
 *   empty_slots.value + full_slots.value + items_in_flight == BUFFER_SIZE
 * 
 * Where items_in_flight = items currently being written (between
 * sem_wait(empty) and sem_post(full))
 * 
 * PROOF OF I1:
 * 
 * Initial state:
 *   empty_slots = BUFFER_SIZE, full_slots = 0, in_flight = 0
 *   Sum = BUFFER_SIZE ✓
 * 
 * Producer before insert (after sem_wait(empty)):
 *   empty_slots decremented, in_flight incremented
 *   Sum unchanged ✓
 * 
 * Producer after insert (after sem_post(full)):
 *   full_slots incremented, in_flight decremented
 *   Sum unchanged ✓
 * 
 * Consumer operations: symmetric argument ✓
 * 
 * Therefore I1 is preserved by all operations. ∎
 */
 
/*
 * From I1, derive SAFETY PROPERTY S1: 0 <= buffer_count <= BUFFER_SIZE
 * 
 * buffer_count == full_slots.value + items_being_consumed
 * 
 * Since semaphore values are non-negative and <= BUFFER_SIZE (by I1),
 * buffer_count is bounded. ∎
 */

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

## Interleaving Analysis: Rendezvous Deadlock Check
 
### Operations to analyze:
Thread A: [A1: post(a_arrived)] [A2: wait(b_arrived)]
Thread B: [B1: post(b_arrived)] [B2: wait(a_arrived)]
 
### Case 1: A1 → A2 → B1 → B2
- A posts a_arrived (a_arrived = 1)
- A waits on b_arrived (A blocks, b_arrived = 0)
- B posts b_arrived (b_arrived = 1, A unblocks)
- B waits on a_arrived (B continues, a_arrived = 1)
Result: Both complete ✓
 
### Case 2: A1 → B1 → A2 → B2
- A posts a_arrived (a_arrived = 1)
- B posts b_arrived (b_arrived = 1)
- A waits on b_arrived (A continues, b_arrived was 1)
- B waits on a_arrived (B continues, a_arrived was 1)
Result: Both complete ✓
 
### Case 3: B1 → B2 → A1 → A2
- B posts b_arrived (b_arrived = 1)
- B waits on a_arrived (B blocks, a_arrived = 0)
- A posts a_arrived (a_arrived = 1, B unblocks)
- A waits on b_arrived (A continues, b_arrived = 1)
Result: Both complete ✓
 
### All orderings checked: No deadlock possible ✓

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

// DEADLOCK: Circular wait
void transfer(Account* from, Account* to, int amount) {
    lock(&from->mutex);
    lock(&to->mutex);    // If another thread does opposite order: deadlock!
    // transfer...
    unlock(&to->mutex);
    unlock(&from->mutex);
}
 
// FIX: Resource ordering by account ID
void transfer_fixed(Account* from, Account* to, int amount) {
    Account* first = (from->id < to->id) ? from : to;
    Account* second = (from->id < to->id) ? to : from;
    
    lock(&first->mutex);     // Always acquire lower ID first
    lock(&second->mutex);    // Then higher ID
    // transfer...
    unlock(&second->mutex);
    unlock(&first->mutex);
}

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

// RACE: Non-atomic check-then-act
if (counter < MAX) {        // RACE: another thread might
    counter++;              // increment between check and act
}
 
// FIX 1: Extend critical section
mutex_lock(&mutex);
if (counter < MAX) {
    counter++;
}
mutex_unlock(&mutex);
 
// FIX 2: Atomic compare-and-swap
int old;
do {
    old = atomic_load(&counter);
    if (old >= MAX) break;
} while (!atomic_compare_exchange_weak(&counter, &old, old + 1));

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
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73

/*
 * Stress Test Framework for Concurrent Code
 */
 
#define NUM_THREADS 100
#define OPERATIONS_PER_THREAD 10000
#define TEST_ITERATIONS 1000
 
typedef struct {
    atomic_int produced_count;
    atomic_int consumed_count;
    atomic_int checksum_produced;
    atomic_int checksum_consumed;
} TestStats;
 
void* producer_test(void* arg) {
    TestStats* stats = (TestStats*)arg;
    
    for (int i = 0; i < OPERATIONS_PER_THREAD; i++) {
        int value = random();
        produce(value);
        
        atomic_fetch_add(&stats->produced_count, 1);
        atomic_fetch_add(&stats->checksum_produced, value);
        
        // Random delay to vary interleaving
        if (random() % 10 == 0) {
            usleep(random() % 100);
        }
    }
    return NULL;
}
 
void* consumer_test(void* arg) {
    TestStats* stats = (TestStats*)arg;
    
    for (int i = 0; i < OPERATIONS_PER_THREAD; i++) {
        int value = consume();
        
        atomic_fetch_add(&stats->consumed_count, 1);
        atomic_fetch_add(&stats->checksum_consumed, value);
        
        if (random() % 10 == 0) {
            usleep(random() % 100);
        }
    }
    return NULL;
}
 
void run_stress_test() {
    for (int iter = 0; iter < TEST_ITERATIONS; iter++) {
        TestStats stats = {0};
        pthread_t producers[NUM_THREADS], consumers[NUM_THREADS];
        
        // Launch threads
        for (int i = 0; i < NUM_THREADS; i++) {
            pthread_create(&producers[i], NULL, producer_test, &stats);
            pthread_create(&consumers[i], NULL, consumer_test, &stats);
        }
        
        // Wait for completion
        for (int i = 0; i < NUM_THREADS; i++) {
            pthread_join(producers[i], NULL);
            pthread_join(consumers[i], NULL);
        }
        
        // Verify invariants
        assert(stats.produced_count == stats.consumed_count);
        assert(stats.checksum_produced == stats.checksum_consumed);
        
        printf("Iteration %d: PASS\n", iter);
    }
}