(***********************************************************************)
(* *)
(* 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) = 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
(* ****** ****** *)
local
assume ISFUL(id : int, b : bool) = unit_p
assume ISNIL(id : int, b : bool) = unit_p
assume queue_vtype(a : vt0p, id : int) = deqarray(a)
staload "libats/SATS/deqarray.sats"
in
implement {a} queue_takeout (pf | xs) =
let
prval () = __assert(pf) where
{ extern
praxi __assert {id:int} (pf : ISNIL(id, false)) : [ false ] void }
in
deqarray_takeout_atbeg(xs)
end
(* ****** ****** *)
implement {a} queue_insert (pf | xs, x0) =
{
prval () = __assert(pf) where
{ extern
praxi __assert {id:int} (pf : ISFUL(id, false)) : [ false ] void }
val () = deqarray_insert_atend(xs, x0)
}
implement {a} queue_isful (xs) =
(unit_p() | deqarray_is_full(xs))
implement {a} queue_isnil (xs) =
(unit_p() | deqarray_is_nil{a}(xs))
implement {a} queue_free_type (q0) =
deqarray_free_nil{a}($UN.castvwtp0{deqarray(a, 1, 0)}(q0))
implement {a} queue_make (cap) =
deqarray_make_cap(cap)
end
(* ****** ****** *)
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
}
(* ****** ****** *)
assume channel_vtype(a : vt0p) = channel_
(* ****** ****** *)
implement {a} 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
val () = ch.spin := unsafe_spin_t2vt(x)
end
local
val x = mutex_create_exn()
in
val () = ch.mutex := unsafe_mutex_t2vt(x)
end
local
val x = condvar_create_exn()
in
val () = ch.CVisnil := unsafe_condvar_t2vt(x)
end
local
val x = condvar_create_exn()
in
val () = ch.CVisful := unsafe_condvar_t2vt(x)
end
val () = ch.queue := $UN.castvwtp0{ptr}(queue_make(cap))
in
(fold@(chan) ; chan)
end
(* ****** ****** *)
implement {a} 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 () = spin_unlock(pf | spin)
prval () = fold@(chan)
in
$UN.castvwtp1{channel(a)}(chan)
end
(* ****** ****** *)
implement {a} 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 () = spin_unlock(pf | spin)
in
if (rfcnt >= 2) then
let
val () = ch.rfcnt := rfcnt - 1
prval () = fold@(chan)
prval () = $UN.cast2void(chan)
in
$UN.castvwtp0{queueopt(a)}(0)
end
else
let
val que = $UN.castvwtp0{queue(a)}(ch.queue)
val () = spin_vt_destroy(ch.spin)
val () = mutex_vt_destroy(ch.mutex)
val () = condvar_vt_destroy(ch.CVisnil)
val () = condvar_vt_destroy(ch.CVisful)
val () = free@{l0,l1,l2,l3}(chan)
in
$UN.castvwtp0{queueopt(a)}(que)
end
end
(* ****** ****** *)
implement channel_get_refcount {a} (chan) =
let
val @CHANNEL{ l0, l1, l2, l3 }(ch) = chan
val rfcnt = ch.rfcnt
in
(fold@(chan) ; rfcnt)
end
(* ****** ****** *)
local
extern
fun {a:vt0p} channel_insert_buf (!channel(a), !queue(a) >> _, a) : void
in
implement {a} 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() where
{ extern
praxi __assert() : vtakeout0(locked_v(l1)) }
val mutex = unsafe_mutex_vt2t(ch.mutex)
val CVisful = unsafe_condvar_vt2t(ch.CVisful)
val () = condvar_wait(pfmut | CVisful, mutex)
prval () = fpf(pfmut)
in
channel_insert_buf(chan, xs, x0)
end
else
let
val isnil = queue_isnil(xs)
val () = queue_insert(pf | xs, x0)
val () = if isnil.1 then
condvar_broadcast(unsafe_condvar_vt2t(ch.CVisnil))
in end
end
(* ****** ****** *)
implement {a} 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 where
{ val isnil = queue_isnil(xs)
val () = queue_insert(pf | xs, x0)
val () = if isnil.1 then
condvar_broadcast(unsafe_condvar_vt2t(ch.CVisnil)) }) : Option_vt(a)
prval pfmut = $UN.castview0{locked_v(l1)}(xs)
val () = mutex_unlock(pfmut | mutex) }
(* ****** ****** *)
implement {a} 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 () = mutex_unlock(pfmut | mutex)
in end
(* ****** ****** *)
end
(* ****** ****** *)
local
extern
fun {a:vt0p} channel_takeout_buf (chan : !channel(a), !queue(a) >> _) :
a
in
implement {a} 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() where
{ extern
praxi __assert() : vtakeout0(locked_v(l1)) }
val mutex = unsafe_mutex_vt2t(ch.mutex)
val CVisnil = unsafe_condvar_vt2t(ch.CVisnil)
val () = condvar_wait(pfmut | CVisnil, mutex)
prval () = fpf(pfmut)
in
channel_takeout_buf(chan, xs)
end
else
let
val isful = queue_isful(xs)
val x0_out = queue_takeout(pf | xs)
val () = if isful.1 then
condvar_broadcast(unsafe_condvar_vt2t(ch.CVisful))
in
x0_out
end
end
(* ****** ****** *)
implement {a} 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 () = if isful.1 then
condvar_broadcast(unsafe_condvar_vt2t(ch.CVisful)) }) : Option_vt(a)
prval pfmut = $UN.castview0{locked_v(l1)}(xs)
val () = mutex_unlock(pfmut | mutex) }
(* ****** ****** *)
implement {a} 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 () = mutex_unlock(pfmut | mutex) }
(* ****** ****** *)
end
(* ****** ****** *)
(* end of [channel_vt.dats] *)