Dining philosophers $(20$ marks$)$

The dining philosopher$$s problem is a classic problem in Computer Science that is used to explore issues in

deadlock, arbitration, and mutual exclusion. In the problem, we have a set of n philosophers, n chopsticks, and n

bowls of noodles. The philsophers are sitting at a round table with one chopstick between each pair of philosophers.

To eat, a philosopher must have two chopsticks.

When a philosopher is hungry, they request the chopstick to

their right and the chopstick to their left.

The challenge is to define an arbitration mechanism of allo$-$

cating chopsticks to philosophers such that if a philosopher is

hungry, the philosopher eventually gets both the chopstick to

their left and the chopstick to their right and so gets to eat.

In this question, you will prove a small part of the Dining

Philosopher$$s problem.

Your proof will probably require approximately $20$ steps.

You will probably not use some of the assumptions.

Part way through the proof, you will probably do an $$Or$-$elim

on asm$$ and then have two subproofs with very similar rea$-$

soning.

Be careful to avoid variable capture!

The proof rules used in the solution are:

$$ Forall$-$elim

$$ Exists$-$elim

$$ Impl$-$elim

$$ Or$-$elim

$$ Subst

$$ Asms $($to finish the proof$)$

$1/2$

ECE$-108$: $2024-$Winter Asn$04$: Dining Philosophers

Given the environment:

Type phil $//$ philosophers

Type stick $//$ chopstick

req$($p : phil, s : stick$)$ : B $//$ p requests the chopstick s

get$($p : phil, s : stick$)$ : B $//$ p gets the chopstick s

lfstk$($p : phil$)$ : stick $//$ the chopstick to the left of p

rtstk$($p : phil$)$ : stick $//$ the chopstick to the right of p

eat$($p : phil$)$ : B :$=$ get$($p$,$ lfstk$($p$))$ get$($p$,$ rtstk$($p$))$

Prove:

$($ s : stick $.$ p : phil $.$ s $=$ rtstk$($p$))$

$($ s : stick $.$ p : phil $.$ s $=$ lfstk$($p$))$

$($ p : phil $.$ req$($p$,$ lfstk$($p$))$ req$($p$,$ rtstk$($p$)))$

$($ p : phil $.$ get$($p$,$ lfstk$($p$))$ get$($p$,$ rtstk$($p$)))$

$($ p : phil $.$ s : stick $.$ req$($p$,$ s$)$ s $=$ lfstk$($p$)$ s $=$ rtstk$($p$))$

$($ p : phil $.$ s : stick $.$ get$($p$,$ s$)$ req$($p$,$ s$))//**$ new $**$

$($ s : stick $.($ p : phil $.$ req$($p$,$ s$))($ p : phil $.$ get$($p$,$ s$)))$

$($ p : phil $.$ s : stick $.$ get$($p$,$ s$)$ p$$ : phil $.$ p$=$ p $($get$($p$,$ s$)))$

$($ p : phil $.$ s : stick $.$ req$($p$,$ s$))($ p : phil $.$ eat$($p$))$