mirror of
https://github.com/KevinMidboe/linguist.git
synced 2025-10-29 17:50:22 +00:00
216 lines
5.3 KiB
Plaintext
216 lines
5.3 KiB
Plaintext
%{
|
|
#include "./../ATEXT/atextfun.hats"
|
|
%}
|
|
|
|
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN"
|
|
"http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
|
|
<html xmlns="http://www.w3.org/1999/xhtml">
|
|
|
|
<head>
|
|
<meta http-equiv="content-type" content="text/html; charset=UTF-8" />
|
|
<title>EFFECTIVATS-DiningPhil2</title>
|
|
#patscode_style()
|
|
</head>
|
|
|
|
<body>
|
|
|
|
<h1>
|
|
Effective ATS: Dining Philosophers
|
|
</h1>
|
|
|
|
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.
|
|
|
|
<h2>
|
|
The Original Problem
|
|
</h2>
|
|
|
|
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.
|
|
|
|
<h2>
|
|
A Variant of the Original Problem
|
|
</h2>
|
|
|
|
The following twist is added to the original version:
|
|
|
|
<p>
|
|
|
|
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.
|
|
|
|
<h2>
|
|
Channels for Communication
|
|
</h2>
|
|
|
|
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:
|
|
|
|
<pre
|
|
class="patsyntax">
|
|
#pats2xhtml_sats("\
|
|
fun{a:vt0p} channel_insert (channel (a), a): void
|
|
fun{a:vt0p} channel_takeout (chan: channel (a)): (a)
|
|
")</pre>
|
|
|
|
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.
|
|
|
|
<h2>
|
|
A Channel for Each Fork
|
|
</h2>
|
|
|
|
Forks are resources given a linear type. Each fork is initially stored in a
|
|
channel, which can be obtained by calling the following function:
|
|
|
|
<pre
|
|
class="patsyntax">
|
|
#pats2xhtml_sats("\
|
|
fun fork_changet (n: nphil): channel(fork)
|
|
")</pre>
|
|
|
|
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).
|
|
|
|
|
|
<h2>
|
|
A Channel for the Fork Tray
|
|
</h2>
|
|
|
|
A tray for storing "dirty" forks is also a channel, which can be obtained
|
|
by calling the following function:
|
|
|
|
<pre
|
|
class="patsyntax">
|
|
#pats2xhtml_sats("\
|
|
fun forktray_changet ((*void*)): channel(fork)
|
|
")</pre>
|
|
|
|
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).
|
|
|
|
<h2>
|
|
Philosopher Loop
|
|
</h2>
|
|
|
|
Each philosopher is implemented as a loop:
|
|
|
|
<pre
|
|
class="patsyntax">
|
|
#pats2xhtml_dats('\
|
|
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]
|
|
')</pre>
|
|
|
|
It should be straighforward to follow the code for [phil_loop].
|
|
|
|
<h2>
|
|
Fork Cleaner Loop
|
|
</h2>
|
|
|
|
A cleaner is implemented as a loop:
|
|
|
|
<pre
|
|
class="patsyntax">
|
|
#pats2xhtml_dats('\
|
|
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]
|
|
')</pre>
|
|
|
|
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:
|
|
|
|
<pre
|
|
class="patsyntax">
|
|
#pats2xhtml_dats('\
|
|
implement
|
|
cleaner_return (f) =
|
|
{
|
|
val n = fork_get_num (f)
|
|
val ch = fork_changet (n)
|
|
val () = channel_insert (ch, f)
|
|
}
|
|
')</pre>
|
|
|
|
It should now be straighforward to follow the code for [cleaner_loop].
|
|
|
|
<h2>
|
|
Testing
|
|
</h2>
|
|
|
|
The entire code of this implementation is stored in the following files:
|
|
|
|
<pre>
|
|
DiningPhil2.sats
|
|
DiningPhil2.dats
|
|
DiningPhil2_fork.dats
|
|
DiningPhil2_thread.dats
|
|
</pre>
|
|
|
|
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.
|
|
|
|
<hr size="2">
|
|
|
|
This article is written by <a href="http://www.cs.bu.edu/~hwxi/">Hongwei Xi</a>.
|
|
|
|
</body>
|
|
</html>
|
|
|
|
%{
|
|
implement main () = fprint_filsub (stdout_ref, "main_atxt.txt")
|
|
%}
|