diff --git a/samples/ATS/main.atxt b/samples/ATS/main.atxt deleted file mode 100644 index 3bba35f0..00000000 --- a/samples/ATS/main.atxt +++ /dev/null @@ -1,215 +0,0 @@ -%{ -#include "./../ATEXT/atextfun.hats" -%} - - - - - - -EFFECTIVATS-DiningPhil2 -#patscode_style() - - - - -

-Effective ATS: Dining Philosophers -

- -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: - -
-#pats2xhtml_sats("\
-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: - -
-#pats2xhtml_sats("\
-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: - -
-#pats2xhtml_sats("\
-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: - -
-#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]
-')
- -It should be straighforward to follow the code for [phil_loop]. - -

-Fork Cleaner Loop -

- -A cleaner is implemented as a loop: - -
-#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]
-')
- -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: - -
-#pats2xhtml_dats('\
-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_thread.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. - - - - -%{ -implement main () = fprint_filsub (stdout_ref, "main_atxt.txt") -%}