Effective ATS:
Dining Philosophers (2)

In this article, I present an implementation of a slight variant of the famous problem of 5-Dining-Philosophers by Dijkstra that makes simple but convincing use of linear types.

The Original Problem

There are five philosophers sitting around a table and there are also 5 forks placed on the table such that each fork is located between the left hand of a philosopher and the right hand of another philosopher. Each philosopher does the following routine repeatedly: thinking and dining. In order to dine, a philosopher needs to first acquire two forks: one located on his left-hand side and the other on his right-hand side. After finishing dining, a philosopher puts the two acquired forks onto the table: one on his left-hand side and the other on his right-hand side.

A Variant of the Original Problem

The following twist is added to the original version:

After a fork is used, it becomes a "dirty" fork and needs to be put in a tray for dirty forks. There is a cleaner who cleans dirty forks and then puts them back on the table.

Channels for Communication

A channel is just a shared queue of fixed capacity. The following two functions are for inserting an element into and taking an element out of a given channel: 
fun{a:vt0p} channel_insert (channel (a), a): void
fun{a:vt0p} channel_takeout (chan: channel (a)): (a)
If [channel_insert] is called on a channel that is full, then the caller is blocked until an element is taken out of the channel. If [channel_takeout] is called on a channel that is empty, then the caller is blocked until an element is inserted into the channel.

A Channel for Each Fork

Forks are resources given a linear type. Each fork is initially stored in a channel, which can be obtained by calling the following function: 
fun fork_changet (n: nphil): channel(fork)
where the type [nphil] is defined to be [natLt(5)] (for natural numbers less than 5). The channels for storing forks are chosen to be of capacity 2. The reason that channels of capacity 2 are chosen to store at most one element (in each of them) is to guarantee that these channels can never be full (so that there is no attempt made to send signals to awake callers supposedly being blocked due to channels being full).

A Channel for the Fork Tray

A tray for storing "dirty" forks is also a channel, which can be obtained by calling the following function: 
fun forktray_changet ((*void*)): channel(fork)
The capacity chosen for the channel is 6 (instead of 5) so that it can never become full (as there are only 5 forks in total).

Philosopher Loop

Each philosopher is implemented as a loop: 
implement
phil_loop (n) = let
//
val () = phil_think (n)
//
val nl = phil_left (n) // = n
val nr = phil_right (n) // = (n+1) % 5
//
val ch_lfork = fork_changet (nl)
val ch_rfork = fork_changet (nr)
//
val lf = channel_takeout (ch_lfork)
val () = println! ("phil_loop(", n, ") picks left fork")
//
val () = randsleep (2) // sleep up to 2 seconds
//
val rf = channel_takeout (ch_rfork)
val () = println! ("phil_loop(", n, ") picks right fork")
//
val () = phil_dine (n, lf, rf)
//
val ch_forktray = forktray_changet ()
val () = channel_insert (ch_forktray, lf) // left fork to dirty tray
val () = channel_insert (ch_forktray, rf) // right fork to dirty tray
//
in
  phil_loop (n)
end // end of [phil_loop]
It should be straighforward to follow the code for [phil_loop].

Fork Cleaner Loop

A cleaner is implemented as a loop: 
implement
cleaner_loop () = let
//
val ch = forktray_changet ()
val f0 = channel_takeout (ch) // [f0] is dirty
//
val () = cleaner_wash (f0) // washes dirty [f0]
val () = cleaner_return (f0) // puts back cleaned [f0]
//
in
  cleaner_loop ()
end // end of [cleaner_loop]
The function [cleaner_return] first finds out the number of a given fork and then uses the number to locate the channel for storing the fork. Its actual implementation is given as follows: 
implement
cleaner_return (f) =
{
  val n = fork_get_num (f)
  val ch = fork_changet (n)
  val () = channel_insert (ch, f)
}
It should now be straighforward to follow the code for [cleaner_loop].

Testing

The entire code of this implementation is stored in the following files: 
DiningPhil2.sats
DiningPhil2.dats
DiningPhil2_fork.dats
DiningPhil2_mylib.dats
There is also a Makefile available for compiling the ATS source code into an excutable for testing. One should be able to encounter a deadlock after running the simulation for a while.

This article is written by Hongwei Xi.