(***********************************************************************)
(* *)
(* ATS/contrib/libats-hwxi *)
(* *)
(***********************************************************************)
(*
** Copyright (C) 2015-2017 Hongwei Xi, ATS Trustful Software, Inc.
**
** Permission is hereby granted, free of charge, to any person obtaining a
** copy of this software and associated documentation files (the "Software"),
** to deal in the Software without restriction, including without limitation
** the rights to use, copy, modify, merge, publish, distribute, sublicense,
** and/or sell copies of the Software, and to permit persons to whom the
** Software is furnished to do so, subject to the following stated conditions:
**
** The above copyright notice and this permission notice shall be included in
** all copies or substantial portions of the Software.
**
** THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
** OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
** FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL
** THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
** LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
** FROM OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
** IN THE SOFTWARE.
*)
(* ****** ****** *)
//
// HX-2015-01:
// An array-based linear channel
//
(* ****** ****** *)
//
staload
UN =
"prelude/SATS/unsafe.sats"
//
(* ****** ****** *)
//
staload
"libats/SATS/athread.sats"
//
staload
"libats/SATS/deqarray.sats"
//
(* ****** ****** *)
//
staload "./../SATS/channel_vt.sats"
//
(* ****** ****** *)
//
absvtype
queue_vtype
(a:vt@ype+, int(*id*)) = ptr
//
vtypedef
queue(a:vt0p, id:int) = queue_vtype(a, id)
//
vtypedef queue(a:vt0p) = [id:int] queue(a, id)
//
(* ****** ****** *)
//
extern
fun
{a:vt0p}
queue_make(cap: sizeGt(0)): queue(a)
//
extern
fun
{a:t@ype}
queue_free_type(que: queue(a)): void
//
(* ****** ****** *)
//
absprop
ISNIL(id:int, b:bool)
absprop
ISFUL(id:int, b:bool)
//
(* ****** ****** *)
//
extern
fun
{a:vt0p}
queue_isnil
{id:int}
(
que: !queue(a, id)
) : [b:bool] (ISNIL(id, b) | bool(b))
extern
fun
{a:vt0p}
queue_isful
{id:int}
(
que: !queue(a, id)
) : [b:bool] (ISFUL(id, b) | bool(b))
//
(* ****** ****** *)
//
extern
fun
{a:vt0p}
queue_insert
{id:int}
(
pf: ISFUL(id, false)
| xs: !queue(a, id) >> queue(a, id2), x0: a
) : #[id2:int] void
//
extern
fun
{a:vt0p}
queue_takeout
{id:int}
(
pf: ISNIL(id, false) | xs: !queue(a, id) >> queue(a, id2)
) : #[id2:int] (a) // end of [queue_takeout]
//
(* ****** ****** *)
local
//
staload
"libats/SATS/deqarray.sats"
//
assume
queue_vtype
(a:vt0p, id:int) = deqarray(a)
//
assume ISNIL(id:int, b:bool) = unit_p
assume ISFUL(id:int, b:bool) = unit_p
//
in (* in-of-local *)
implement
{a}(*tmp*)
queue_make(cap) = deqarray_make_cap(cap)
implement
{a}(*tmp*)
queue_free_type(q0) =
deqarray_free_nil{a}
(
$UN.castvwtp0{deqarray(a,1,0)}(q0)
) // end of [queue_free_type]
implement
{a}(*tmp*)
queue_isnil(xs) =
(unit_p() | deqarray_is_nil{a}(xs))
implement
{a}(*tmp*)
queue_isful(xs) =
(unit_p() | deqarray_is_full(xs))
implement
{a}(*tmp*)
queue_insert
(pf | xs, x0) =
{
//
prval () =
__assert(pf) where
{
extern
praxi
__assert
{id:int}
(
pf: ISFUL(id, false)
) : [false] void
} (* end of [prval] *)
//
val () =
deqarray_insert_atend(xs, x0)
//
} (* end of [queue_insert] *)
(* ****** ****** *)
implement
{a}(*tmp*)
queue_takeout
(pf | xs) = let
//
prval () =
__assert(pf) where
{
extern
praxi
__assert
{id:int}
(
pf: ISNIL(id, false)
) : [false] void
} (* end of [prval] *)
//
in
deqarray_takeout_atbeg(xs)
end (* end of [queue_takeout] *)
end // end of [local]
(* ****** ****** *)
//
datavtype
channel_ =
{
l0,l1,l2,l3:agz
} CHANNEL of
@{
cap=sizeGt(0)
, spin=spin_vt(l0)
, rfcnt=intGt(0)
, mutex=mutex_vt(l1)
, CVisnil=condvar_vt(l2)
, CVisful=condvar_vt(l3)
, queue=ptr // deqarray
} (* end of [channel] *)
//
(* ****** ****** *)
//
assume
channel_vtype(a:vt0p) = channel_
//
(* ****** ****** *)
implement
{a}(*tmp*)
channel_create_exn
(cap) = let
//
extern
praxi
__assert(): [l:agz] void
//
prval [l0:addr] () = __assert()
prval [l1:addr] () = __assert()
prval [l2:addr] () = __assert()
prval [l3:addr] () = __assert()
//
val chan = CHANNEL{l0,l1,l2,l3}(_)
//
val+CHANNEL(ch) = chan
//
val () = ch.cap := cap
val () = ch.rfcnt := 1
//
local
val x = spin_create_exn()
in(*in-of-local*)
val () = ch.spin := unsafe_spin_t2vt(x)
end // end of [local]
//
local
val x = mutex_create_exn()
in(*in-of-local*)
val () = ch.mutex := unsafe_mutex_t2vt(x)
end // end of [local]
//
local
val x = condvar_create_exn()
in(*in-of-local*)
val () = ch.CVisnil := unsafe_condvar_t2vt(x)
end // end of [local]
//
local
val x = condvar_create_exn()
in(*in-of-local*)
val () = ch.CVisful := unsafe_condvar_t2vt(x)
end // end of [local]
//
val () = ch.queue := $UN.castvwtp0{ptr}(queue_make(cap))
//
in
fold@(chan); chan
end // end of [channel_create_exn]
(* ****** ****** *)
implement
{a}(*tmp*)
channel_ref
(chan) = let
//
val@CHANNEL(ch) = chan
//
val
spin =
unsafe_spin_vt2t(ch.spin)
//
val
(pf | ()) = spin_lock(spin)
val () = ch.rfcnt := ch.rfcnt + 1
val ((*void*)) = spin_unlock(pf | spin)
//
prval () = fold@(chan)
//
in
$UN.castvwtp1{channel(a)}(chan)
end // end of [channel_ref]
(* ****** ****** *)
implement
{a}(*tmp*)
channel_unref
(chan) = let
//
val
@CHANNEL
{l0,l1,l2,l3}(ch) = chan
//
val
spin =
unsafe_spin_vt2t(ch.spin)
//
val
(pf | ()) = spin_lock(spin)
val rfcnt = ch.rfcnt
val ((*void*)) = spin_unlock(pf | spin)
//
in (* in-of-let *)
//
if
(
rfcnt >= 2
)
then let
val () = ch.rfcnt := rfcnt - 1
prval ((*fold*)) = fold@(chan)
prval ((*freed*)) = $UN.cast2void(chan)
in
$UN.castvwtp0{queueopt(a)}(0)
end // end of [then]
else let
val que =
$UN.castvwtp0{queue(a)}(ch.queue)
// end of [val]
val ((*freed*)) = spin_vt_destroy(ch.spin)
val ((*freed*)) = mutex_vt_destroy(ch.mutex)
val ((*CVisnil*)) = condvar_vt_destroy(ch.CVisnil)
val ((*CVisful*)) = condvar_vt_destroy(ch.CVisful)
val ((*freed*)) = free@{l0,l1,l2,l3}(chan)
in
$UN.castvwtp0{queueopt(a)}(que)
end // end of [else]
//
end // end of [channel_unref]
(* ****** ****** *)
implement
{}(*tmp*)
channel_get_refcount
{a}(chan) = let
//
val@CHANNEL
{l0,l1,l2,l3}(ch) = chan
//
val rfcnt = ch.rfcnt
//
in
fold@(chan); rfcnt
end // end of [channel_get_refcount]
(* ****** ****** *)
local
//
extern
fun{a:vt0p}
channel_insert_buf
(!channel(a), !queue(a) >> _, a): void
//
in
(* ****** ****** *)
implement
{a}(*tmp*)
channel_insert
(chan, x0) = let
//
val+CHANNEL
{l0,l1,l2,l3}(ch) = chan
//
val
mutex = unsafe_mutex_vt2t(ch.mutex)
val (pfmut | ()) = mutex_lock(mutex)
//
val xs =
$UN.castvwtp0{queue(a)}((pfmut|ch.queue))
val () = channel_insert_buf(chan, xs, x0)
//
prval
pfmut = $UN.castview0{locked_v(l1)}(xs)
val ((*void*)) = mutex_unlock(pfmut | mutex)
//
in
// nothing
end // end of [channel_insert]
(* ****** ****** *)
implement
{a}(*tmp*)
channel_insert_opt
(chan, x0) = opt where
{
//
val+
CHANNEL
{l0,l1,l2,l3}(ch) = chan
//
val
mutex = unsafe_mutex_vt2t(ch.mutex)
val (pfmut | ()) = mutex_lock(mutex)
//
val xs =
$UN.castvwtp0{queue(a)}((pfmut|ch.queue))
//
val (pf | isful) = queue_isful(xs)
//
val opt =
(
if
isful
then Some_vt(x0)
else None_vt(*void*) where
{
val isnil =
queue_isnil(xs)
val ((*void*)) =
queue_insert(pf | xs, x0)
val ((*void*)) =
if isnil.1 then
condvar_broadcast(unsafe_condvar_vt2t(ch.CVisnil))
// end of [then] // end of [if]
}
) : Option_vt(a) // end of [val]
//
prval
pfmut = $UN.castview0{locked_v(l1)}(xs)
val ((*void*)) = mutex_unlock(pfmut | mutex)
//
} (* end of [channel_insert_opt] *)
(* ****** ****** *)
implement
{a}(*tmp*)
channel_insert_buf
(chan, xs, x0) = let
//
val+
CHANNEL
{l0,l1,l2,l3}(ch) = chan
//
val (pf | isful) = queue_isful(xs)
//
in
//
if
isful
then let
prval
(pfmut, fpf) =
__assert((*void*)) where
{
extern
praxi
__assert
(
// argless
) : vtakeout0(locked_v(l1))
}
val mutex =
unsafe_mutex_vt2t(ch.mutex)
val CVisful =
unsafe_condvar_vt2t(ch.CVisful)
val ((*void*)) =
condvar_wait(pfmut|CVisful,mutex)
prval ((* returned *)) = fpf(pfmut)
in
channel_insert_buf(chan, xs, x0)
end // end of [then]
else let
val isnil =
queue_isnil(xs)
val ((*void*)) =
queue_insert(pf | xs, x0)
val ((*void*)) =
if isnil.1 then
condvar_broadcast(unsafe_condvar_vt2t(ch.CVisnil))
// end of [then] // end of [if]
in
// nothing
end // end of [else]
//
end // end of [channel_insert_buf]
end // end of [local]
(* ****** ****** *)
local
//
extern
fun{a:vt0p}
channel_takeout_buf
(chan: !channel(a), !queue(a) >> _): (a)
//
in (* in-of-local *)
(* ****** ****** *)
implement
{a}(*tmp*)
channel_takeout
(chan) = x0_out where
{
//
val+
CHANNEL
{l0,l1,l2,l3}(ch) = chan
//
val
mutex = unsafe_mutex_vt2t(ch.mutex)
val (pfmut | ()) = mutex_lock(mutex)
//
val xs =
$UN.castvwtp0{queue(a)}((pfmut|ch.queue))
//
val x0_out = channel_takeout_buf(chan, xs)
//
prval
pfmut = $UN.castview0{locked_v(l1)}(xs)
val ((*void*)) = mutex_unlock(pfmut | mutex)
//
} // end of [channel_takeout_opt]
(* ****** ****** *)
implement
{a}(*tmp*)
channel_takeout_opt
(chan) = opt where
{
//
val+
CHANNEL
{l0,l1,l2,l3}(ch) = chan
//
val
mutex = unsafe_mutex_vt2t(ch.mutex)
val (pfmut | ()) = mutex_lock(mutex)
//
val xs =
$UN.castvwtp0{queue(a)}((pfmut|ch.queue))
//
val (pf | isnil) = queue_isnil(xs)
//
val opt =
(
if
isnil
then None_vt()
else Some_vt(x0_out) where
{
val isful =
queue_isful(xs)
val x0_out =
queue_takeout(pf | xs)
val ((*void*)) =
if isful.1 then
condvar_broadcast(unsafe_condvar_vt2t(ch.CVisful))
// end of [then] // end of [if]
} (* end of [else] *)
) : Option_vt(a) // end of [val]
//
prval pfmut =
$UN.castview0{locked_v(l1)}(xs)
//
val ((*void*)) = mutex_unlock(pfmut | mutex)
//
} // end of [channel_takeout_opt]
(* ****** ****** *)
implement
{a}(*tmp*)
channel_takeout_buf
(chan, xs) = let
//
val+
CHANNEL
{l0,l1,l2,l3}(ch) = chan
//
val (pf | isnil) = queue_isnil(xs)
//
in
//
if
isnil
then let
prval
(pfmut, fpf) =
__assert((*void*)) where
{
extern
praxi
__assert
(
// argless
) : vtakeout0(locked_v(l1))
}
val mutex =
unsafe_mutex_vt2t(ch.mutex)
val CVisnil =
unsafe_condvar_vt2t(ch.CVisnil)
val ((*void*)) =
condvar_wait(pfmut|CVisnil,mutex)
// end of [val]
prval ((* returned *)) = fpf (pfmut)
in
channel_takeout_buf(chan, xs)
end // end of [then]
else let
val isful = queue_isful(xs)
val x0_out = queue_takeout(pf | xs)
val ((*void*)) =
if isful.1 then
condvar_broadcast(unsafe_condvar_vt2t(ch.CVisful))
// end of [then] // end of [if]
in
x0_out
end // end of [else]
//
end // end of [channel_takeout_buf]
end // end of [local]
(* ****** ****** *)
(* end of [channel_vt.dats] *)