Page 111 - DCAP403_Operating System

Operating System

Notes SR Program: The Dining Philosophers

This semaphore solution to the readers-writers problem can let writers starve because readers
arriving after a now-waiting writer arrived earlier can still access the database to read if enough
readers continually trickle in and ‘‘keep the database in a read state’’ then that waiting writer will
never get to write
resource philosopher
import dining_server
body philosopher(i : int; dcap : cap dining_server; thinking, eating: int)
write(“philosopher”, i, “alive, max think eat delays”, thinking, eating)
procedure think()
var napping : int
napping := int(random(1000*thinking))
writes(“age=”,age(),”, philosopher “,i,” thinking for “,napping,” ms\n”)
nap(napping)
end think
procedure eat()
var napping : int
napping := int(random(1000*eating))
writes(“age=”,age(),”, philosopher “,i,” eating for “,napping,” ms\n”)
nap(napping)
end eat
process phil
do true ->
think()
writes(“age=”, age(), “, philosopher “, i, “ is hungry\n”)
dcap.take_forks(i)
writes(“age=”, age(), “, philosopher “, i, “ has taken forks\n”)
eat()
dcap.put_forks(i)
writes(“age=”, age(), “, philosopher “, i, “ has returned forks\n”)
od
end phil
end philosopher
resource dining_server
op take_forks(i : int), put_forks(i : int)
body dining_server(num_phil : int)
write(“dining server for”, num_phil, “philosophers is alive”)
sem mutex := 1
type states = enum(thinking, hungry, eating)
var state[1:num_phil] : states := ([num_phil] thinking)
sem phil[1:num_phil] := ([num_phil] 0)
procedure left(i : int) returns lft : int
if i=1 -> lft := num_phil [] else -> lft := i-1 fi

104 LOVELY PROFESSIONAL UNIVERSITY