(***********************************************************************) (* *) (* ATS/contrib/libats-hwxi *) (* *) (***********************************************************************) (* ** Copyright (C) 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-2017-02-07: Start it now! *) (* ****** ****** *) (* // // HX-2017-02-11: // It is supposed to be // included rather than staloaded // #define ATS_PACKNAME "ATSCNTRB.HX.fworkshop" // *) (* ****** ****** *) staload UN = "prelude/SATS/unsafe.sats" (* ****** ****** *) staload AT = "libats/SATS/athread.sats" typedef tid = $AT.tid typedef spin1 = $AT.spin1 (* ****** ****** *) abstype fws$store_type() = ptr typedef fws$store = fws$store_type (* ****** ****** *) absvtype fws$fwork_vtype() = ptr vtypedef fws$fwork = fws$fwork_vtype (* ****** ****** *) extern fun fws$store_capacity() : intGte(1) extern fun fws$store_insert(fws$store, fws$fwork) : void extern fun fws$store_takeout(store : fws$store) : fws$fwork extern fun fws$fwork_process(fws$fwork) : int (* ****** ****** *) abstype fworkshop_type() = ptr typedef fworkshop = fworkshop_type (* ****** ****** *) vtypedef fworkshop_struct = @{ FWS_spin = spin1 , FWS_store = fws$store , FWS_workerlst = List0_vt(tid) } (* ****** ****** *) extern fun fworkshop_create_exn() : fworkshop extern fun fws$store_create_exn() : fws$store (* ****** ****** *) extern fun fworkshop_add_tid(fws : fworkshop, tid) : void (* ****** ****** *) extern fun fworkshop_get_spin(fws : fworkshop) : spin1 (* ****** ****** *) extern fun fworkshop_get_store(fws : fworkshop) : fws$store (* ****** ****** *) extern fun fworkshop_get_nworker(fws : fworkshop) : intGte(0) (* ****** ****** *) extern fun fworkshop_insert_work(fws : fworkshop, fwork : fws$fwork) : void extern fun fworkshop_takeout_work(fws : fworkshop) : fws$fwork extern fun fworkshop_process_work(fws : fworkshop, fwork : fws$fwork) : int (* ****** ****** *) extern fun fworkshop_add_worker(fws : fworkshop) : int extern fun fworkshop_add_nworker {n:nat} (fws : fworkshop, int(n)) : natLte(n) (* ****** ****** *) local assume fworkshop_type() = ref(fworkshop_struct) in (* ****** ****** *) implement fworkshop_add_nworker {n} (fws, n) = loop(0, 0) where { fun loop { i : nat | i <= n } (i : int(i), res : natLte(i)) : natLte(n) = let in if i < n then let val err = fworkshop_add_worker{}(fws) in if err = 0 then loop(i + 1, res + 1) else res end else res end } (* ****** ****** *) implement fworkshop_add_worker (fws) = err where { fun fworker(fws : fworkshop) : void = let val fwork = fworkshop_takeout_work(fws) val status = fworkshop_process_work(fws, fwork) in if (status >= 0) then fworker(fws) else fworker_exit(fws) end and fworker_exit(fws : fworkshop) : void = let val tid0 = $AT.athread_self() fun auxrmv(tids : &List0_vt(tid) >> _) : void = (case+ tids of | list_vt_nil() => () | @list_vt_cons (tid, tids_tl) => (if (tid0 != tid) then { val () = auxrmv(tids_tl) val () = fold@(tids) } else { val tids_ = tids val () = tids := tids_tl val () = free@{..,0}(tids_) })) val (vbox pf | p0) = ref_get_viewptr(fws) val spn = p0->FWS_spin val (pflock | ()) = $AT.spin_lock(spn) val () = $effmask_ref(auxrmv(p0->FWS_workerlst)) val () = $AT.spin_unlock(pflock | spn) in end var tid: lint? with val err = $AT.athread_create_cloptr{}(tid, llam () => fworker(fws)) val () = if (err = 0) then fworkshop_add_tid{}(fws, tid) } (* ****** ****** *) implement fworkshop_get_nworker (fws) = let val (vbox pf | p0) = ref_get_viewptr(fws) val spn = p0->FWS_spin val (pflock | ()) = $AT.spin_lock(spn) val nworker = list_vt_length(p0->FWS_workerlst) val () = $AT.spin_unlock(pflock | spn) in nworker end (* ****** ****** *) implement fworkshop_get_store (fws) = let val (vbox pf | p0) = ref_get_viewptr(fws) in p0->FWS_store end (* ****** ****** *) implement fworkshop_get_spin (fws) = let val (vbox pf | p0) = ref_get_viewptr(fws) in p0->FWS_spin end (* ****** ****** *) implement fworkshop_add_tid (fws, tid) = let val (vbox pf | p0) = ref_get_viewptr(fws) val spn = p0->FWS_spin val (pflock | ()) = $AT.spin_lock(spn) val tids = p0->FWS_workerlst val () = p0->FWS_workerlst := list_vt_cons(tid, tids) val () = $AT.spin_unlock(pflock | spn) in end (* ****** ****** *) implement fworkshop_create_exn () = let val (pf, fpf | p0) = ptr_alloc() val () = p0->FWS_spin := $AT.spin_create_exn() val () = p0->FWS_store := fws$store_create_exn{}(()) val () = p0->FWS_workerlst := list_vt_nil() in $UN.castvwtp0{fworkshop}((p0, fpf, pf)) end (* ****** ****** *) end (* ****** ****** *) implement fworkshop_insert_work (fws, x0) = let val store = fworkshop_get_store{}(fws) in fws$store_insert{}(store, x0) end (* ****** ****** *) implement fworkshop_takeout_work (fws) = let val store = fworkshop_get_store{}(fws) in fws$store_takeout{}(store) end (* ****** ****** *) implement fworkshop_process_work (fws, fwork) = status where { val status = fws$fwork_process{}(fwork) } (* ****** ****** *) (* end of [fworkshop.dats] *)