mirror of
https://github.com/KevinMidboe/linguist.git
synced 2025-10-29 17:50:22 +00:00
179 lines
3.2 KiB
Plaintext
179 lines
3.2 KiB
Plaintext
(* ****** ****** *)
|
|
//
|
|
// HX-2013-11
|
|
//
|
|
// Implementing a variant of
|
|
// the problem of Dining Philosophers
|
|
//
|
|
(* ****** ****** *)
|
|
//
|
|
#include
|
|
"share/atspre_define.hats"
|
|
#include
|
|
"share/atspre_staload.hats"
|
|
//
|
|
(* ****** ****** *)
|
|
|
|
staload
|
|
UN = "prelude/SATS/unsafe.sats"
|
|
|
|
(* ****** ****** *)
|
|
|
|
staload "libc/SATS/stdlib.sats"
|
|
staload "libc/SATS/unistd.sats"
|
|
|
|
(* ****** ****** *)
|
|
|
|
staload "{$LIBATSHWXI}/teaching/mythread/SATS/channel.sats"
|
|
|
|
(* ****** ****** *)
|
|
|
|
staload _ = "libats/DATS/deqarray.dats"
|
|
staload _ = "{$LIBATSHWXI}/teaching/mythread/DATS/channel.dats"
|
|
|
|
(* ****** ****** *)
|
|
|
|
staload "./DiningPhil2.sats"
|
|
|
|
(* ****** ****** *)
|
|
|
|
implement phil_left (n) = n
|
|
implement phil_right (n) = (n+1) \nmod NPHIL
|
|
|
|
(* ****** ****** *)
|
|
//
|
|
extern
|
|
fun randsleep (n: intGte(1)): void
|
|
//
|
|
implement
|
|
randsleep (n) =
|
|
ignoret (sleep($UN.cast{uInt}(rand() mod n + 1)))
|
|
// end of [randsleep]
|
|
//
|
|
(* ****** ****** *)
|
|
|
|
implement
|
|
phil_think (n) =
|
|
{
|
|
val () = println! ("phil_think(", n, ") starts")
|
|
val () = randsleep (6)
|
|
val () = println! ("phil_think(", n, ") finishes")
|
|
}
|
|
|
|
(* ****** ****** *)
|
|
|
|
implement
|
|
phil_dine (n, lf, rf) =
|
|
{
|
|
val () = println! ("phil_dine(", n, ") starts")
|
|
val () = randsleep (3)
|
|
val () = println! ("phil_dine(", n, ") finishes")
|
|
}
|
|
|
|
(* ****** ****** *)
|
|
|
|
implement
|
|
phil_loop (n) = let
|
|
//
|
|
val () = phil_think (n)
|
|
//
|
|
val nl = phil_left (n)
|
|
val nr = phil_right (n)
|
|
//
|
|
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) // HX: try to actively induce deadlock
|
|
//
|
|
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)
|
|
val () = channel_insert (ch_forktray, rf)
|
|
//
|
|
in
|
|
phil_loop (n)
|
|
end // end of [phil_loop]
|
|
|
|
(* ****** ****** *)
|
|
|
|
implement
|
|
cleaner_wash (f) =
|
|
{
|
|
val f = fork_get_num (f)
|
|
val () = println! ("cleaner_wash(", f, ") starts")
|
|
val () = randsleep (1)
|
|
val () = println! ("cleaner_wash(", f, ") finishes")
|
|
}
|
|
|
|
(* ****** ****** *)
|
|
|
|
implement
|
|
cleaner_return (f) =
|
|
{
|
|
val n = fork_get_num (f)
|
|
val ch = fork_changet (n)
|
|
val () = channel_insert (ch, f)
|
|
}
|
|
|
|
(* ****** ****** *)
|
|
|
|
implement
|
|
cleaner_loop () = let
|
|
//
|
|
val ch = forktray_changet ()
|
|
val f0 = channel_takeout (ch)
|
|
//
|
|
val () = cleaner_wash (f0)
|
|
val () = cleaner_return (f0)
|
|
//
|
|
in
|
|
cleaner_loop ()
|
|
end // end of [cleaner_loop]
|
|
|
|
(* ****** ****** *)
|
|
|
|
dynload "DiningPhil2.sats"
|
|
dynload "DiningPhil2_fork.dats"
|
|
dynload "DiningPhil2_thread.dats"
|
|
|
|
(* ****** ****** *)
|
|
|
|
local
|
|
//
|
|
staload
|
|
"{$LIBATSHWXI}/teaching/mythread/SATS/mythread.sats"
|
|
//
|
|
in (* in of [local] *)
|
|
//
|
|
val () = mythread_create_cloptr (llam () => phil_loop (0))
|
|
val () = mythread_create_cloptr (llam () => phil_loop (1))
|
|
val () = mythread_create_cloptr (llam () => phil_loop (2))
|
|
val () = mythread_create_cloptr (llam () => phil_loop (3))
|
|
val () = mythread_create_cloptr (llam () => phil_loop (4))
|
|
//
|
|
val () = mythread_create_cloptr (llam () => cleaner_loop ())
|
|
//
|
|
end // end of [local]
|
|
|
|
(* ****** ****** *)
|
|
|
|
implement
|
|
main0 () =
|
|
{
|
|
//
|
|
val () = println! ("DiningPhil2: starting")
|
|
val ((*void*)) = while (true) ignoret (sleep(1))
|
|
//
|
|
} (* end of [main0] *)
|
|
|
|
(* ****** ****** *)
|
|
|
|
(* end of [DiningPhil2.dats] *)
|