Effective ATS:
Dining Philosophers

The three most distinguished features of ATS are dependent types, linear types, and embeddable templates (that can be implemented inside the body of a function). In this article, I present an implementation of the famous problem of 5-Dining-Philosophers by Dijkstra that makes simple but convincing use of linear types.

Description of the 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 Linear Type for Resources

First, let us introduce a type definition as follows:

typedef phil = int

The sole purpose of using [phil] instead of [int] as the type for philosophers is to make the presented code easier to follow.

The forks mentioned in the description of the problem refer to shared resources. Let us next introduce a linear abstract type for the forks:

absvt@ype fork = int

This declaration means that [fork] is an abstract viewtype (that is, a linear abstract type) whose size equals the size of [int]. Please note that the information on [fork] and [int] being of the same size is not available until after typechecking when abstract types are replaced with concrete types.

For a philosopher to acquire and release his left fork, the following functions can be called:

fun phil_acquire_lfork (n: phil): fork
fun phil_release_lfork (n: phil, f: fork): void

For a philosopher to acquire and release his right fork, the following functions can be called:

fun phil_acquire_rfork (n: phil): fork
fun phil_release_rfork (n: phil, f: fork): void

As forks are shared resources, these functions for acquiring and releasing forks should in general involve some sort of locking mechanism. If a fork is acquired, then it should be released after its use. By assigning a linear type to forks, we can rely on the type system of ATS to keep track of forks, ensuring their being handled properly.

Philosopher Implemented as a Loop

According to the description of the problem, we implement a loop as follows to simulate a philosopher:

extern
fun phil_loop (n: phil): void
implement
phil_loop (n) = let
  val () = phil_think (n)
  val ((*void*)) = phil_dine (n)
in
  phil_loop (n)
end // end of [phil_loop]

The function [phil_think], which requires no resources, can be implemented as follows:

extern
fun phil_think (n: phil): void
implement
phil_think (n) =
(
  randsleep (10) // for sleeping up to 10 secs
)

The function [phil_dine], which involves acquiring and releasing resources, can be implemented as follows:

extern
fun phil_dine (n: phil): void
implement
phil_dine (n) = let
//
  val lf = phil_acquire_lfork (n)
  val () = randsleep (1) // for sleeping up to 1 secs
  val rf = phil_acquire_rfork (n)
//
  val () = randsleep (3) // for sleeping up to 3 secs
//
  val () = phil_release_lfork (n, lf)
  val () = phil_release_rfork (n, rf)
//
in
  // nothing
end // end of [phil_dine]

Note that both [lf] and [rf] are assigned the linear type [fork], making them linear values. As every linear value must be consumed in some way or returned, removing the call to [phil_release_lfork] (or [phil_release_rfork]) causes a type-error that can be readily detected during typechecking. This is a great advantage of assigning linear types to values representing resources.

Summary of the Remaining Implementation

If we run [phil_loop] on 5 threads, then we can employ 5 mutexes to protect 5 forks (one for each). We can also employ one mutex to protect 5 forks and then introduce some conditional variables to avoid busy-waiting. Instead, the implementation given here runs [phil_loop] on 5 processes (which are created by invoking the system call [fork]) and calls [mmap] to obtain memory for storing the 5 forks shared by these processes. It creates a lock based on the underlining file system to protect these forks and inserts sleeps of random length to avoid complete busy-waiting. This style of implementation is chosen primarily for the purpose of a demo. The interested reader is encouraged to give a thread-based implementation that employs mutexes and possibly conditional variables.

Testing

Note that each philosopher in the given implementation picks first his left fork and then his right fork. In the case where everyone of them holds a fork on his left hand, a deadlock occurs. A simple way to avoid such a deadlock is to have a philosopher (among the 5) who picks first his right fork and then his left fork.

The problem of 5-Dining-Philosphers was precisely introduced to study deadlocks and deadlock avoidance. If one tests the given implementation, he or she should likely to see a deadlock occurring in a few minutes. Please use the command [kill] to remove all of the deadlocked processes.